[SCL] weekend update

[pat hayes]

>  > 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
>
>Agreed, but for the consumer version I'd probably prefer to define what
>we mean by TFO completely separately from SCL: saying that TFO is
>a sublanguage of SCL1 and now we present a conversion between
>TFO_sublanguage_of_SCL1 <-> SCL1 is (although correct) a bit confusing.
>
>Best of all we could copy a syntax of TFO from some classical textbook,
>citing it as well. Readers would be more confident that we are not
>going to pull any tricks.

I see your point, but there is also an important point to make in the 
other direction, which is that TFO really *is* an SCL subcase. Maybe 
we can agree to make both points and discuss in what order to make 
them.

>If we were to write it using a classical syntax we'd reformulate
>your two rules for terms/literals into something like this:
>
>convert_term(f(s1,...,sn)) ==
>      appN(convert_term(f),convert_term(s1),...,convert_term(sn))
>convert_literal(p(s1,...,sn)) ==
>      holdsN(convert_term(p),convert_term(s1),...,convert_term(sn))
>
>where we have to indicate whether the converted
>construction is a term or a literal (we cannot use f/p for this,
>since they might be arbitrary variables or terms).

True, I was being careless in the email to get the point across.

>
>>  (Btw, having that 'cons' available is a great aid in writing things like
>>  this. Hmmmm.)
>
>It is nice but I doubt we want to use 'cons' in such a way
>in the consumer version. Also, a question would arise:
>is 'cons' part of the conversion program or a resulting
>term? I assumed myself you are thinking it to be a part
>of the conversion program.

Well, I was; but I can't help noting that it is really useful to be 
able to write things like this, and wondering if there might not be 
some way to incorporate such tricks into the syntax itself. After 
all, we have the notion of sequence built into the syntax, and LISP 
is the premier language for describing such things. But maybe that is 
a task for another day.

>
>>  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.
>
>Right. I like that proposal. One more thing before we can happily
>continue: we need to fix the mapping of the equality predicates:
>from TFOL to SCL and vice versa.

Right. I need to check this, but I think that with our new MT, we can 
map equality 'transparently' (ie leave it alone). This basically 
treats it like a logical symbol rather than a binary relation symbol.

>
>About pure symbols not needing App/Holds: I am very much for the
>simple version above App/Holding everything. Why:
>
>1) No need to invent special language to indicate which symbols
>    are pure (would be horrible if we try to do this, I am afraid)

I agree

>
>2) Most importantly, IMHO: it should be up to each implementor to
>    optimise the encoding.

Yes, that is my instinct also.

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