[SCL] two comments

[pat hayes]

>Hi,
>
>pat hayes wrote:
>>Rather than drafting yet another version, let me put on record some 
>>of the changes Id like to see.  I'd be happy to attempt a rewrite 
>>when the text settles down.
>>
>>First, as currently phrased the AS describes a lexicon as a 
>>collection of sets. I would prefer that we treat the AS as a purely 
>>abstract algebraic structure, in which the 'basic' items are 
>>considered to be grammatical categories - categories of expressions 
>>- rather than sets of syntactic entities. The makes no difference 
>>to the formal stuff but simplifies the AS and makes it more 
>>uniform, and avoids what is otherwise a potentially awkward set of 
>>issues concerning the 'status' of lexical items in some concrete 
>>SCL languages.
>>
>>A concrete SCL language is then obtained by providing a 
>>'lexicalization' which provides for a set of wf expressions and a 
>>way to parse any such expression into an SCL AS structure.  Now we 
>>can distinguish two kinds of lexicalization: those in which the 
>>primitive syntactic elements (the things in the 'lexicon') can be 
>>recognized in isolation, and the others. Call the first 'local' for 
>>now.
>
>This was really a message to Chris, but I cannot help
>intervening :-)

Of course. CCing to the list makes it public.

>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

>I won't understand it until I see the AS presented in this form.

OK, fair enough. I will try to get that done soon. Its very similar 
to what Chris has already done, but I do think that it can be 
presented 'intuitively' in a reasonably convincing way, basically by 
using tables.

>Now, when we get to see AS in this form, and it uses anything
>uncommon, people will have hard time reading it. Before I see
>AS in this particular suggested form, I guess that it is safer
>to stick with what prospective readers are used to. In the
>context of a spec aimed to be used as a standard, being as
>widely understood as we realistically can is IMHO more important
>than being clever.

Well, I agree that we shouldnt show off for the sake of seeming 
clever; but on the other hand, we do have a genuine point to make 
here, which is that we can attach the model theory *in a very general 
way* to a single framework which can then be instantiated in a large 
variety of ways. This is important for standardization since it 
integrates a large variety of notations; for me, this is a central 
purpose of attempting to make this a standard in the first place.

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.

>Chris, I know this is unconventional, but I think it is important to
>
>Again: being unconventional is bad.

Well, yes and no.  There is no point in trying to standardize a 
completely conventional logical syntax, since we already have many 
applications which are chafing under these conventions and will be 
incompatible with it (eg requiring intensional semantics, or wishing 
to allow circular hierarchies, or variadic relations, or reasoning 
over predicate domains, or not having access to a signature); and to 
me the entire point of the SCL project is that we have found a 
simple, elegant, way to remove a host of these difficulties within a 
first-order model theory and (now) even a first-order syntax. So if 
all we do is re-define a BNF for classical FOL, we won't have 
achieved our goal. (We will have an EBNF for a 'standard' SFOL 
concrete syntax as one product, of course, but that is only part of 
the enterprise.)

>has the nice feature that when you use it everything gets simpler 
>and nagging problems just go away, with no real cost, which is 
>always the sign of having got something right :-).  Just forget the 
>doctrine that a language *is* a set of strings.
>
>We could forget that, but readers probably won't.

They will eventually.  CGs are not sets of strings, for example, and 
neither is RDF syntax.  Not to mention ML diagrams, semantic networks 
XML Infosets and other things. For some folk, even character strings 
do not conform to the classical notion of a language, cf. the 
problems of normalizing bidirectional Unicode.

>>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 cannot see how such a distinction will make things simpler
>for SCL. It is simpler to have fewer different categories,
>not more.

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

>If you really want to distinguish them, then we could
>always use SFOL, where they are nicely distinguished.

Well, yes, the issue only comes up when translating into SFOL. 
Perhaps we are speaking past one another here (?)

>However, contra Tanel, it seems to me that this is not really an 
>issue requiring any changes to equality: rather, it is to do with 
>the range of quantification. What it boils down to is that in the 
>holds/app embedding, all quantifiers should be understood as 
>restricted to a class which is not obliged to contain entities which 
>occur only in the first argument position of any holds or app 
>assertion.
>
>You are most probably right that this restriction on
>quantification may work (we talked about it briefly on way from Tampa).
>
>Bur I am still having an opinion that it is easier to have
>two equalities and "ordinary" quantification than one
>equality and "unordinary" quantification. Quantification
>is more important than equality, ergo we should prefer
>to keep quantification as simple as possible, not
>equality.

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.

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.

Pat
-- 
---------------------------------------------------------------------
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://philebus.tamu.edu/pipermail/scl/attachments/20031105/651d835c/attachment-0001.htm