[SCL] Again: new version of SCL draft attached

[pat hayes]

>
>I'll motivate the main change in the draft here:
>
>After some additional thinking about the issues around
>seqvars and the constructions Chris has just presented,
>I'd summarise the main SCL goals like this:
>
>A) presenting a simple (S in SCL) practical standard
>    for first order logic. "Practical" here means vaguely
>    as "being useful for SW languages like RDF, containing
>    some widely used pre-defined predicates and constants, etc"
>
>B) presenting nontrivial extensions in the FOL context,
>    like sequence variables and the possibility to mix
>    polyadic and fixed-arity predicates, like in the
>    latest presentation by Chris.
>
>These two goals are somewhat divergent. It is hard, though
>not impossible (see Chris' presentation!) to reconcile them.
>
>The goal (A) is straightforward to accept, and I doubt
>anybody will oppose to goal (A).

As presented, of course not. Motherhood and apple 
pie. But as we know from long and bitter 
experience, if one tries to get down to details 
on what exactly counts as a simple, practical 
KR/FOL standard, you will not get agreement. To 
most people, "simple and practical" seems to 
mean, "whatever I have managed to implement" or 
"whatever I am used to". The SKIF group had 
members whose answers ranged from full sequence 
quantifiers to untyped FOL with relations having 
no more than 5 arguments and empty clauses not 
allowed.

>
>The goals in (B) are certainly interesting and useful,
>although the extensions are fairly hard to understand
>and may hamper acceptance.

And yet Bill Anderson thinks they are vital. I 
think the largest group that can agree on how to 
make such an A/B split has cardinality 1, and 
even then you had better not let him sleep on it.

>
>In particular, despite the fact that Chris has presented
>a draft MT for (B), there is no presentation of
>proof theory. I think we may need derivation rules for
>the Chris language (for example, a sequence calculus
>for the language).

We did in fact design such a set of ND rules for 
full CL, but Chris has a philosophical aversion 
to structured proofs, so we never published it.

>MT in Chris presentation looks fairly
>different from the traditional MT of FOL, hence there
>does not seem to be a straightforward, intuitive mapping of
>traditional derivation rules to the Chris language.

The complications are almost all to do with 
interpreting atomic sentences, which creates no 
proof complications at all, so apart from new 
rules for handling sequence quantifiers, its is 
all very conventional.

>For the goal (A) we do not need to present sequence
>calculus explicitly, since we have it in a straightforward
>way through a simple mapping to traditional FOL (just
>use sequence calculus for traditional logic, for
>example).
>
>Hence I propose to _split the SCL spec_ into
>two parts, both in the same document:

I really do not want to have such a split, and do 
not feel that it is necessary on either formal or 
expository grounds.

>- SCL which _does not contain sequence variables etc_
>   and has a straightforward mapping to traditional FOL.
>
>- ECL (extended common logic) which does contain
>   everything in the Chris presentation, but is harder
>   to understand and perhaps needs an explicit presentation of
>   the derivation calculus.

This goes back to the old 'onion' model. I don't 
like this because the chief moral advantage which 
SCL has is that it is at base a single language 
with a single MT, and indeed a very simple such 
language. If we have a series of layers with 
distinct MTs then we are just doing the old SKIF 
project once again and we will dissolve into 
arguments about what should be in the core and 
what should be an extension. This was largely why 
we wasted 3 years arguing.

Let me suggest a compromise. Agreed about the 
split, but not about exactly where it goes. Let 
us first define a single 'kernel' language with 
one (abstract) syntax and one model theory.  (We 
can do this without using Greek letters, even 
quite formally, using the general style of XML 
Schematon 
http://xml.com/pub/a/2003/11/12/schematron.html.) 
This admits extensions which can considered as 
syntactic sugar, in the sense that they can be 
transcribed in the kernel without loss of 
meaning; and it allows sub-languages which are 
simply the kernel with some syntax classes 
omitted and maybe some extra syntactic 
restrictions imposed.  Once stated for the 
kernel, the MT never needs to be re-stated: it is 
fixed.  One sublanguage of central importance, 
which we should define as early in the document 
as possible, is a conventional KR/FOL syntax, 
which is probably going to be . Then we should 
describe how to embed the kernel into that 
syntax, by the use of an appropriate holds/app 
translation for the relational quantifications 
and the use of an explicit lists ontology for 
variadic relations and sequence quantifiers. Then 
we should analyze the limitations of this 
embedding, if there are any, and should seriously 
consider whether the kernel needs to be changed 
so as to remove or minimize them. Ideally, it 
should be possible to implement something very 
close to a complete SCL reasoner by applying the 
embedding and using a conventional FO reasoner on 
the result.


>The way to reconcile these two approaches:
>
>The SCL spec paper will present two languages: SCL and
>ECL. SCL is the simple version without the full power
>of the language presented by Chris. It is properly
>"simple" common logic.
>
>ECL is presented as a useful extended language built
>upon SCL. It serves dual purpose in the paper:
>
>- useful in itself
>- gives an example for extending SCL in a nontrivial way
>
>Does that look sensible?

Er.. no, sorry. See above.

>  If it does, then please let
>us split the following work like this:

Please, let us not make more divisions than are 
required. Chris has been putting valiant work 
into writing a unified technical specification. 
Cutting it up into several distinct languages 
just renders that work superfluous. Let us try to 
keep the overall design coherent while 
identifying the various subcases that are of 
interest to us, within it.

I feel that we are beng distracted by this 
December 17th deadline. While we should do our 
best to be helpful, it is better to miss this 
than to produce something inappropriate or that 
we will subsequently be unable to agree on.


>- some people (Chris, for example) are mainly responsible
>   for the ECL chapters
>
>- some people (me, for example) are mainly responsible for
>   the SCL chapters.
>
>It would then be highly desirable to write any modifications
>into the full spec paper, not as separate documents!
>
>The new version attached contains a standalone
>MT for core SCL. Wrote this in a manner which is
>hopefully (a) easily understandable and (b) could
>(I hope so) be extended by Chris for ECL.

I REALLY do not want SCL to have several model 
theories. There would (literally) be no point in 
even publishing such a standard: that is the 
situation we are in at present.

Pat


>Chris: please have a look at the new core
>SCL semantics chapter. Might well be that as it
>stands now, it cannot be sensibly used for ECL,
>but you could introduce modifications to the
>core SCL semantics chapter to make it extendable to ECL.
>
>It is IMHO an interesting challenge  to structure
>this whole text in a sensible manner, so that
>both the (A) and (B) goals would be satisfied,
>possibly with minor compromises.
>
>Chris: BTW, I still cannot fully understand
>your MT. There seem to be some typos here and
>there or notions which are used but not defined,
>especially in the subchapter "interpretations".
>
>Quote:
>"Accordingly, ext is a corresponding extension 
>function from R into ?(I?) subject to the 
>constraint that, for any natural number n > 0, 
>if r ? Rn, then ext(r) ? In; in particular, 
>ext(Id) = {?a,a? : a ? I}."
>
>What does that "?(I?)" stand for, for example?
>
>Regards,
>         Tanel Tammet
>
>
>
>Attachment converted: Betelgeuse:scl16nov.zip (pZIP/«IC») (000A89E3)
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes