[SCL] weekend update

[Tanel Tammet]

pat hayes wrote:
 >
 > Hey, you guys, stop squabbling.

Good to hear something sounding this optimistic! :-)

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

Good. Just for the record - I have not been nagging
at Chris - but stressing every now and then that
the consumer version is highly important and should
be IMHO explained plainly in terms of traditional FOL.

You are of course right that Chris has been doing
most of the work and we should really help by
writing the consumer stuff.

 > Shall we target for a telecon next Tuesday?

Ok for me.

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

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.

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

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

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

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)

2) Most importantly, IMHO: it should be up to each implementor to
    optimise the encoding. I'd certainly write an analyser and a
    formula preprocessor allowing me to drop as many App/Holds
    as possible BEFORE ACTUAL PROOF SEARCH STARTS, but I'd hate
    having the difference built into the language. Observe that
    the question where we can drop App/Holds depends on the
    specific properties of a formula we are searching a proof
    for, and not really on the predicate/function symbols themselves.
    Ie, depending on the formula it occurs in, sometimes
    you can treat a symbol as pure, but sometimes not.
    It is the particular usage which matters, not lexicon.
    And this is highly implementation-dependent, IMHO not
    something we should try to pre-optimise: we'll pre-optimise
    far too badly when compared to a clever implementor.

Regards,
         Tanel Tammet