[SCL] weekend update

[pat hayes]

Hey, you guys, stop squabbling. Tamel, don't nag at Chris, its up to 
you and me to write the 'consumer' version. I have been buried in 
other work for about 3 weeks but I will try to get a draft version 
done by early next week.

Shall we target for a telecon next Tuesday?

>  > 1. Simplicity: introduction with semantics based on FOL

Agreed. In fact it can be virtually be FOL; the only concession we 
make to our new generality is that we forget to mention that the 
lexical categories are disjoint. Then we can discuss all the 
subsequent holds/app stuff in terms of varieties of the language in 
which various disjointness conditions are imposed, and mappings 
between them.

The basic points that need to be got across are (1) the use of a 
central abstract syntax: this is really only a presentation style,. 
and we should mention the various concrete syntaxes early on in order 
to get the point across; and (2) the slight generality in the syntax 
and the fact that it makes no essential difference to the standard 
FOL MT. We can motivate extension mappings on semantic/philosophical 
grounds before showing their full technical utility.

Pat

PS
>  > Since the very same issue is in my understanding absolutely critical
>>  for the wider usability of SCL, I'd propose dropping all the other SCL
>>  developments until the commonly agreeable mapping is worked out :-)
>
>I'd be happy to make this our current focus.

OK, proposal.  First, confine ourselves to the language without 
seqvars, SCL1.  Define TFO to be the class of SCL1 langs L in which:

1. PredL, IndL and FnL are pairwise disjoint
2. every member x of PredL and FnL has arity(x) a singleton.

Now, given any SCL language L, define a particular TFO language H(L) 
in which Pred is the set {holdsN: N >0} with arity(holdsN)=N, Fn is 
the set {appN:N >0} with arity(appN)=N, and Ind is the set PredL 
union FnL union IndL.  Observation: H(L) is a TFO.  Define a mapping 
from terms and atoms of L into those of H(L) in the obvious way 
(applied recursively):
AppL(f,s) ==>>  AppH(L)(appN, cons(f,s)) where N=|s|+1
PredL(f,s) ==>> PredH(L)(holdsN, cons(f,s)) where N=|s|+1

(Btw, having that 'cons' available is a great aid in writing things 
like this. Hmmmm.)

Lemma: A entails B iff H(A) entails H(B). Proof, fairly trivial, by 
mapping interpretations 'through' the appN/holdsN vocabulary.
-----

This is simpler than Chris' version but it produces an uglier result 
since it App/Holds everything, even the 'pure' symbols. Its easier to 
state, though, and it has the merit of uniformity and simplicity, as 
well as of being a clear limiting case: one can then retreat to a 
more conservative translation is one wishes to, and its fairly clear 
that the same result will obtain in all the intermediate cases. Thus 
we can relegate this to a side-observation and make the simpler 
mapping the normative one.

This simple translation also does not require one to know the exact 
lexical category of the symbols of L, since the way each occurrence 
of any symbol is translated into H(L) depends only on its immediate 
syntactic context. This is likely to be critical in practice.

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