[SCL] Concrete embedding proposal to TFOL (GOFOL, SFOL)

[Tanel Tammet]

pat hayes wrote:

>> Please have a look at the following and check out
>> whether it is basically this embedding you have had
>> in mind. I do not guarantee you won't find any errors
>> or omissions.
> 
> 
> Apart from the equality treatment, it is, yes.  But we should revisit 
> the equality discussion in the light of the revision to the SCL MT; 
> there may now no longer be any need to make the distinction. (I havnt 
> checked this either way, but if we can get by with a simpler 
> transmogrification then it would seem better.)

Good. Could you or Chris give an alternative equality
embedding? Would be useful also for the purposes of explaining
the new MT better.

>> I have not put the finer extensions of SCL like tuple variables
>> and integer  types in the embedding. Adding these should
>> be the next step after we agree on the basic embedding
>> (the one below or a modified form of it).
> 
> 
> Agreed, but let us first examine the relationship between seqvars and 
> explicit list constructions. If we can get this sorted out, there my be 
> a more universally acceptable mapping of the seqvar syntax into TFOL, 
> since the use of lists to endcode variadicity is widely familiar and 
> often used in a more or less ad-hoc fashion.

I have very little intuition about what people really expect
from seqvars, but IF it would be somehow possible to fulfill their
wishes with fixed-arity tuples (of various arities) instead of lists,
I'd suggest the tuples any day. A more powerful and flexible
encoding tends to be much less efficient. In that sense
lists are not simple at all. Besides, all the induction issues
appear and people will be surprised seeing that SCL does not
solve the induction issues at all.

This said, we could of course survive lists if really necessary.

>> The side issue associated with this embedding (whether
>> exactly this one or, if modifications are proposed, the
>> modified version) is that IMHO the pure SCL semantics
>> should, in some sense, match the embedding. In case
>> the SCL semantics turns out to be principally different
>> from the embedding, then we should either change
>> the embedding or SCL semantics.
> 
> 
> Agreed.
> 
> BTW, there is another possible relationship between SCL and SFOL 
> reasoners which use unification: tweak the unification so that it calls 
> itself recursively on the relation/function position of every atom or 
> term, just as it does on all other positions. 

Doable in principle, but see the following:

> This is a very small 
> change to the code in most cases (any optimizations which depend on the 
> presence of a relation or function name can still be used, but are 
> called out only after a suitable check for the presence of a name)

I do seriously doubt that "it is a very simple change". It could be a
simple change for NAIVE provers written by undergraduate students as a
coursework but almost all serious provers rely on a large number of 
highly specialised index structures, additional data encodings, etc, all
of which would be immediately broken if the first element of a term
is not a constant. This would mean that most of the core code is
fundamentally broken and beyond repair.

Now, even if you do a reimplementation, ALL THE NEEDS of indexes
and additional data encodings STILL REMAIN, hence you will basically
implement the App/Holds kind of functions anyway in your code, even
if they are hidden from the user of the system.

To summarise: AFAIK in case the function/predicate symbol of a term
may be an arbitrary term, then, implementation-wise you cannot
create a much better solution than just using the app/holds functions
in the prover.

. The
> result still works as before for SFOL, but is also complete for SCL just 
> when it was formerly complete for SFOL, (and for the very same reasons, 
> since this bears the same relationship to the SCL Herbrand universe that 
> traditional unification does to the SFOL Herbrand universe) and no 
> transmogrification is required. I would suggest that this should be our 
> recommended practice for SCL implementers, and that the mapping style 
> you suggest should be considered an interim stop-gap for those who wish 
> to use legacy code.

Even if this scenario materialises (it just might, who knows) it will
take a lot of time. Our immediate worry should be not to
alienate other people in near term. What matters is whether a sufficient 
number of people ('sufficient' means a pretty small number anyway :-)
would be ready to use SCL at all - create the translators, reasoners, etc.

This, like introduction of mostly anything new, means that we should
do absolutely anything we can to lower the entry barrier.

Regards,
           Tanel Tammet