[SCL] New SCL version, seqvars and extensions by Chris

[Tanel Tammet]

Hi,

Attached please find a new draft for SCL, both
as an HTML file and a zipped version of the
same file.

The changes from the version from 1. November
are listed in the appendix D.

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).

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

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). 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.

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:

- 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.

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? If it does, then please let
us split the following work like this:

- 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.

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



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://philebus.tamu.edu/pipermail/scl/attachments/20031116/414dbe55/scl16nov-0001.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: scl16nov.zip
Type: application/x-zip-compressed
Size: 14748 bytes
Desc: not available
Url : http://philebus.tamu.edu/pipermail/scl/attachments/20031116/414dbe55/scl16nov-0001.bin