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

[pat hayes]

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

Right, will try to do it tomorrow.

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

Point taken. To some extent though this ship has sailed, as the 
list-of-arguments style is now embedded into DAML and OWL, so I think 
we have to at least accommodate to it.

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

Some day I would like to get down to details on exactly why this is 
true.  Other high-end implementers have said similar things, so I 
guess I have to concede the point, but Im very suspicious of simple 
implemeter's conservatism being at work here.  About the only thing I 
can imagine breaking would be some kind of hashing scheme based on 
relation/function names, but (1) that would break in any case in an 
open-ended Web setting where new relation symbols could appear at any 
time and (2) hashing can be done on term structures, with a bit more 
work admittedly.

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

Well, OK. But then the app/holds become merely (;-) implementation 
matters to make the code work, which is fine: that is what they are, 
in fact. But they are not part of the actual language: they have no 
semantics, are not in the signature, etc. ; they need not even be 
names, in fact.
BTW, what happens to all your highly specialized index structures and 
data encodings if your entire corpus only uses one relation name and 
one function name?

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

Well, that is sad, if true, but I bow to your knowledge as the Gandalf creator.

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

Fair enough. As a political point this may well be horribly true. 
However, I note that the RDFS inference style has been implemented by 
many non-comp-logic types and they havn't complained about this issue 
at all, in fact have hardly noticed it.  My bet is that if history 
had taken a slightly different course, and Tarski had used Aczel's 
set theory from the word go, then the resolution TPs would have had 
the simpler general unifier from the very first and nobody would be 
any the worse off.

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 ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam