[SCL] two comments

[Tanel Tammet]

pat hayes wrote:

>> When you speak about the "purely abstract algebraic structure"
> 
>> etc then I honestly do not understand what do you exactly mean.
> 
> 
> I mean basically a term algebra.  My own understanding of the basic idea 
> is based on
> http://www-formal.stanford.edu/jmc/towards/node12.html

OK.

> The particular issue here, for example, arises not from any academic 
> concern but in order to be able to accommodate a common use case 
> (central to the SW applications), where expressions are arriving at any 
> time and you do not know the signature of the language in the 
> conventional sense of 'signature' and 'language', but must infer it from 
> parsing the expressions.  This is a real source of tension between the 
> textbook style of defining a language by an unambiguous BNF grammar and 
> a widespread use case. It is often conveniently ignored, but I think we 
> have a duty to give a precise account of how to handle it.

I really think we should NOT worry much about how are people going
to write parsers. Why:

- parsers will be written for concrete syntaxes (some of ours,
   some built by other people), NOT for the abstract syntax.

- writing efficient parsers is a specific area into which
   there is no point to enter in the SCL context.

It will make sense to think about parsing when writing
concrete SCL syntaxes. (Incidentally, at Sanibel I wrote
a parser etc for an SCL concrete syntax of my own,
lispish design).

But, whenever we base our concrete syntax on an existing
syntax (KIF, XML, etc) most of these considerations have
been done before us and again, there is little for
us to add.

 > So if all we do is re-define
> a BNF for classical FOL, we won't have achieved our goal. 

Certainly. IMHO, any kind of abstract syntax we write,
this syntax will not be the main part of our goal.

Hence we might as well re-define a BNF for classical FOL,
the syntax is not a motivational, but a necessary,
part of the SCL spec.

>>> The same effect could be achieved by axioms of the form
>>> holdsn(x y1 ... yn) implies ind(yi)
>>> i.e. by embedding SCL into a FO theory rather than into SFOL itself, 
>>> with a suitable modification to the statement of correspondence 
>>> between full SCL and the holds/app translation.
>>
>>
>> Do you really want to distinguish ind, fun and pred constants?
> 
> 
> Not sure what you mean. SCL already makes the conceptual distinction, 
> though it allows a concrete syntax to identify them.

I am not really sure it should make the distinction on any level.

IMHO once we start distinguishing these categories of constants,
the simplicity (I'd say, the elegant, surprising triviality!)
of SCL starts to fiddle away, while the "non-conventionality"
is preserved: we'll have an artefact which is mainly
characterised by people as "weird".

Again, IMHO, there are two clear choices:

- To give a standardised version of traditional FOL, or

- To give a simplified version of traditional FOL,
   with distinction between constant, function and predicate
   symbols removed and all terms and atoms being treated
   as tuples.

The "in-between" alternatives are complex and a bit weird,
while these two are neither.

But maybe I am just missing something obvious.

> Well, I agree: but if we remove all these distinctions then the language 
> becomes much less conventional. That is the CL wild-west syntax that 
> Chris and I liked so much, but we made a conscious effort to restrict 
> ourselves to a more conventional syntax in SCL in order to win 
> acceptance. 

Then I have been mistaken: I thought you STILL like it.

I started to like it immensely once I realised that it can
be considered to be a simplified version of SFOL.

I assumed that we are NOT going to distinguish predicate,
function and individual constants in the semantics
(we well may distinguish them in syntax, this does
not really matter).

Distinguishing them while still allowing predicates
to range over predicate symbols would imho create
serious problems (do not know immediately which ones,
just a strong gut feeling).

I see no internal controversies betwen the "conventional" syntax
and the wild-west. It is just the matter of presentation,
pedagogical principles and rhetorics.


>In one version of the WW syntax there want even a 
> distinction between connectives and individuals, though that was indeed 
> rather fantastic (but it did work.)

Sure it works. The FOL prover people, for example, practice
their provers on examples like these quite often :-)

Just take examples from combinatory logic. Extend them
a bit if you so wish. There you are.

But I agree that it is unconventional.

> Well, let me suggest that you may well be right, but that this is an 
> issue that should be kept within bounds: it has to do with the best way 
> to implement a full SCL reasoner using a conventional SFOL inference 
> engine. I will defer that decision to you; but I would prefer that we do 
> not let that issue percolate back into the design of the main logic, 
> particularly if it requires something as idiosyncratic as two kinds of 
> identity.

The issue of two equalities is NOT related to provers.

It is related to the observations Ian brought out first.


 > I think we can keep this entire discussion in a section of the
 > document
 > concerned with implementation and the SCL->SFOL embedding, which I see
 > as important but not on the main expository path.

This is IMHO a good idea. Perhaps we can do that, or at least
direct the intuition of the reader to that direction.

We do not really need two equalities for SCL itself:
we need one of them only for translating the traditional FOL
equality into some concrete predicate of SCL.

Regards,
        Tanel