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

[Tanel Tammet]

pat hayes wrote:

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

Hopefully we get a lot of informative feedback from your question to a 
number
of developers (a very good idea, IMHO). Just read Voronkov's comments,
basically confirming what I wrote.

Back to the question "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?".

Obviously they still work, although it would be a bit more efficient to 
be able to have
a number of different function/predicate symbols.

The special enhancements and optimisations in provers are written 
assuming certain
"typical" forms the input examples will have. In other words, people 
optimise for a number
of often-occurring patterns. In case a pattern stemming from 
transmogrifying would be
 extremely common (as it could well be for provers optimised for SCL, 
for example)
then the implementors would surely optimise for this. 

We cannot help them much in doing the optimisations, except by providing 
very clear
and easy to understand semantics and embeddings, plus avoiding highly 
complex features
in the language.

One of the main time-consuming operations in the provers is to find 
atoms/terms which
either subsume, are subsumed by or unify a concrete atom/term under 
investigation.
Philosophically it is a bit similar (though much simpler) to associative 
memory where
you want to locate the relevant facts quickly. Once you have located the 
relevant fact,
then the basic operations like unification are very fast.

BTW, there is a large corpus of classical example problems from 
combinatory logic and
 condensed detachment (CD) where the formulas do have a form similar to 
what we would get
from transmogrifying (the difference is that in the combinatory logics & 
CD examples the
term structure is typically deep and complex, which is not likely to be 
the case for
SCL formulas). The "main" clause in CD examples is "P(i(x,y)) & P(i) => 
P(y)" corresponding
to condensed detachment, with i and P obviously representing "implies" 
and "holds".

In the examples like CD above the indexes and other hash-like mechanisms 
we have been talking
about bascially work over the structure of terms: at each decision point 
the choices are
- one of the constants (typically just a few)
- a variable
- a complex term (every complex term is led by i)

The typical pattern transmogrified SCL formulas will have is somewhat 
different.
At each decision point (for example, comparing one term to another or 
searching for
terms/atoms which subsume an investigated term/atom) the choices are:
- one of the constants (a VERY LARGE set of constants)
- a variable
- one of the complex terms for the arities occurring in our formula

Due to a large number of constants there will be more variations in
a decision point than in "ordinary" ATP examples.

In other words, I have a gut feeling that the typical pattern stemming
from obtained-from-web SCL formulas is quite different from the typical
examples the provers are normally optimised for. Provers tend to be 
optimised
for examples originating from math (TPTP corpus contains mostly such 
examples)
with a complex term structure or verification (where specific forms of
arithmetics and other concrete data structures are highly important).
They are also often optimised for handling equality quickly,
up to treating even ordinary atoms as equalities with a true/false
constant as a possible value (E is an example of such a prover).

The web-obtained formulas are likely to be very large, containing a huge
number of simple clauses (just atoms over constants) with a very large set
of constants occurring in them. Equality is also likely to be less crucial.
The pattern of SCL formulas is likely to be similar to typical datalog
formulas. Considering equality we have to notice that once a predicate
is declared to be functional on some of its arguments (ie a tuple of 
arguments 2,...,n where
atom has value true is a function of one argument) it would be sensible 
for provers
to further transmogrify the formula and represent the atom as a function 
instead.
Ie I expect optimised provers for SCL to do significant inner 
transmogrifications on their
own, depending on how the input formula looks like. In that sense the 
details
of OUR supposed transmogrifications are not as important as we might think,
except, as I repeatedly stressed, the clarity and ease of understanding (and
traditional FOL is easiest to understand for prover hackers).

Finally, to bring up a simple but important point regarding the relevance of
app/holds as a leading term (ie why do we need it, why not just consider an
atom/term as a list?):

The transmogrifying mechanism will not convert everything simply to
a list led by app/holds. Instead, there will be a number of tuples with
different lengths i (corresponding to the arity of the 
predicate/function symbol
in SCL), each tuple led by a different App_i/Holds_i symbol. Ie the 
App/Holds
symbol contains information about the length of the tuple. Since two tuples
of different lengths are not comparable in  our setting (despite that 
the elements of a shorter
tuple might be equal to the corresponding elements of a longer tuple) the
information about tuple lengths  has to be kept somewhere where it is 
accessible
and "hashable" fast. The App_i/Holds_i symbol could be seen as holding
the tuple length information in a suitable way.

Regards,
            Tanel Tammet