[SCL] SCL basic consensus badly needed

[Tanel Tammet]

Hi,

pat hayes wrote:

>> Hi SCL-ers,
>>
>> We need to build a consensus on some
>> basic issues before we can sensibly
>> move on.
>>
>> Please, everybody: let us have a serious
>> look on SCL <-> SFOL (standard FOL)
>> conversion this week and let us try
>> hard to reach a consensus on this
>> by the end of the week.
>
>
> Tamel, sorry Ive been so out of the loop, hope you have not become too 
> discouraged. 

Almost, but not really :-)

Not unexpectedly I am also sometimes out of loop for some projects,
so I expected - from my own experience - that the pause is a pause and
not a complete stop.

Speaking about the substance, your email takes a very
optimistic view, I'd say, assuming that we can have
really nice translations from SCL to SFOL and
that the equality problems can be avoided
very easily. At the same time, I have still seen
no concrete SCL->SFOL transformation rules which would
indicate that the optimism is warranted.

I'll discuss this in the following parts of the email.

>>    Although we need a "holds" predicate and an "app" function
>>    (to be more exact, a separate "holds" for each
>>    arity, ie an infinite supply of "holds_1","holds_2", etc)
>>    to translate SCL formulas like "forall x. x(x)"
>>    to SFOL as "forall x. holds_2(x,x)",
>>    it would seem that in simpler cases we
>>    could avoid inserting "holds".
>>
>>    For example, one could wish to translate SCL
>>    formula "forall x. p(x)" as "forall x. p(x)"
>>    in SFOL, and not as "forall x. holds_2(p,x)".
>>
>>    However, I am convinced that having such a
>>    translation schema with "exceptions" is a very
>>    bad idea and is not usable in practice, for
>>    various reasons. Additionally, it will not
>>    buy us anything performance-wise.
>
>
> ? Surely it does in many cases, with engines which use indexing on 
> relation names. In fact that is the only case I have seen made for not 
> immediately converting the unification algorithm to handle the 
> 'higher-order' constructs directly.

You are right in the sense that it is very easy to index on the predicate
name, and a bit harder to index on the rest of the literal.

However:

- the situation where we only have one predicate symbol
   in the whole problem class (as we could have "holds") is not
   at all unique:  ATP examples in the condensed detachment
   areas and pure equality problems have a similar property.
  
- most of the high-end provers contain very sophisticated indexing
   methods (indexing is an area which has seen a lot of research
   and experimentation in ATP circles during the last 10 years)
   which do index on the whole (or most of) the literal structure,
   not just the predicate symbol. For such indexing methods (actually
   used, as I said) there is not much difference efficiency-wise
   between the two encodings. If there is any difference in
   some cases, then the prover implementors are fully capable
   in modifying the indexing methods in the provers to get
    that last bit of efficiency.

>>    I am suggesting using a uniform translation
>>    schema, ALWAYS inserting "holds" and "app".
>>
>>    QUESTION: Would you agree to that or not?
>
>
> No, unless we are forced to.  I think we can do (have done?) better, 
> in the following sense.
>
> You asked the question using a 2-headed arrow <-> but there are 2 
> translations involved.

Right.

> SFOL -> SCL is trivial as SFOL *is already* SCL.

It is NOT in case we use the "holds" encoding: in this case
only a subset of SFOL is in SCL, while SFOL formulas containing
other predicates are not.

> I think this is important and needs to be preserved in our account: 
> SFOL is a subset of SCL.

As you see, I tend to look at it differently: holds/app converted SCL is 
a subset of SFOL.
I tend read SCL as a "macro language" which has to be converted to SFOL.
In case one does not like the macro language approach, then
one moves dangerously close to higher order logics with SCL.

Now, I have no ideological imperative inside me to claim
that SCL certainly must be seen as a subset of SFOL.

I'd be happy to accept the opposite - SFOL a subset of SCL - in case
we had a clear translation algorithm between these two,
at least in the crucial SCL->SFOL direction.

The translation algorithm is what I am personally after
as an ATP hacker. The question which one is inside the other
is less important.

>   SCL -> SFOL is therefore an embedding, and requires use of the 
> holds/app embedding to cover all of SCL syntax.  The result, if we 
> round-trip, is that SFOL->SCL->SFOL  amounts to the SFOL->SFOL mapping 
> which you get by rewriting SFOL in SFOL using the holds/app embedding 
> (which of course has always been an option, though unmotivated.)

> Actually we could define the SCL->SFOL mapping in two ways, as you 
> point out. One way is to leave any SFOL syntax alone and to embed only 
> non-FOL SCL using holds/app. The other is to apply the holds/app 
> uniformly, which is what I was assuming above. I can see the merits of 
> both ways of defining the translation, but like you, lean towards the 
> uniform technique as a 'standard'.


Well, this would be nice in my viewpoint, but a few paragraphs earlier
 you wrote that you would NOT agree to the uniform hold/app translation, 
since
you think that the translation could be done better than that.

> However, we could observe that if you start in FOL, then the SCL 
> results and standards apply to you without change, so there is 
> actually no need to apply any complex self-embeddings in order to use 
> a FOL engine on SCL that happens to be FOL already.

> On re-reading this I see it may be confusing. What I mean is that we 
> should indeed define a mapping from full SCL to FOL along the lines 
> you suggest, ie simple and applying uniformly to the entire syntax. 
> However, I think we can also observe that SFOL is a well-defined 
> sublanguage of SCL - I expect we will have several such sublanguages - 
> and that it is perfectly OK to work entirely within this sublanguage 
> and still be using SCL correctly. 

What do you mean by "we can also observe that SFOL is .... and that it 
is perfectly OK to work
entirely within this sublanguage and still be using SCL correctly"?

I can of course understand the obvious point that if we do not have any 
variables in
predicate/function positions, then the holds/app transformation would not be
necessary and the result of such a translation preserves 
satisfiability/unsatisfiability.

However, this observation does not make the meaning of your passage clear.

What we have to think about is what would a real implemented sem web
system and the internal prover do with the various SCL and SFOL files
it gets.

The expected situation in everyday life is that a system will several
files in several languages and it is asked to answer a query on these.

Let us take an example with an internal SFOL prover
in such a sem web system. For me this example represents
the the very core of the issue.  I'd be happy with any
solutions which lets us go through the example in
a well-implementable-and-usable manner.

The whole system gets a file F1.SCL in SCL and
a file F2.SFOL in SFOL. It is asked whether a formula Q.SFOL is
derivable from the conjunction of F1.SCL and F2.SFOL: ie, is

F1.SCL & F2. SFOL => Q.SFOL valid or not.

Such a question obviously requires that F1.SCL, F2.SFOL and Q.SFOL
are first transformed to a common language, in a clearly
specified way: otherwise the question itself is absurd.

Now, suppose that F1.SCL does not contain any variables
in predicate and function places. Would you say that F1.SCL
does not need any transformations at all and the formula

F1.SCL & F2. SFOL => Q.SFOL

can be considered to be IMMEDIATELY in a uniform
language SFOL?

If we do that, and then, after a little while, our system
gets a slightly modified file F1prim.SCL, where
there is a variable in a function/predicate position,
then we suddenly cannot use the F1prim.SCL directly.
We are forced to first convert it using holds/app, giving
us a final question

convertwithholdsapp(F1prim.SCL) & F2. SFOL => Q.SFOL

Observe that the relations between F1.SCL and F2.SFOL
on one hand, and convertwithholdsapp(F1prim.SCL) and
F2.SFOL, on the other hand, are EXTREMELY different.

Even in case the modification introduced to F1.SCL
to get F1prim.SCL is a small, useless formula bearing
no relations to anything in F2.SFOL and Q.SFOL,
the transformation has to be applied and the validity
of the implication may well be completely different
from the validity of the original case, where we
could avoid the transformation.

The same kinds of problems appear, probably in a more
aggravated form, if we consider the needs to keep
(cache) formulas deduced during answering earlier
questions to the same conjunction:

F1.SCL & F2. SFOL

Suppose that the first question asked is whether
Q1.SFOL is derivable  from the conjunction
above and the second question
asked is whether Q2.SCL is derivable. Now it
may well happen that everything derived while answering
the first question was done WITHOUT transforming
F1.SCL using holds/app, while we had to transform
F1.SCL for the second question (if Q2.SCL
contains variables in pred/app position,
then the whole implication does). Hence the
derivations done from the conjunction while
answering the first question cannot be
reused while searching for the answer to
the second question! This would be real bad.
In case of a uniform translation we could
always REUSE old temporary results, which
is IMHO highly important.


> So to conform to the SCL spec while using FOL is not to necessarily 
> use the full-SCL -> FOL embedding mapping. That is an option for 
> someone who has FOL tools and wishes to offer a full-SCL service, for 
> example: but then they would need to pay attention to matters like the 
> one you raise, of how to handle the 'extra' vocabulary introduced by 
> the embedding. No doubt a full writeup of the final document suite 
> should refer to this and discuss it in some detail, but I don't see it 
> as being a show-stopper or requiring us to do anything as drastic as 
> introducing two kinds of equality.
>
>> C) Make up your mind on the mapping
>>    "SCL with equality" <-> "SFOL with equality"
>>    and please tell your standpoint in an answer
>>    to this email.
>
>
> I think that with the current version of the model theory, the above 
> applies to the with-= case just as it does to the without-= case.

Maybe it does. However, once we consider the holds/app transformation
(not a standalone semantics) then the question about equality is not
automatically solved. For the holds/app transformation
we do need to do something to avoid problems with
Horrocks formulas.

>
>>
>>    I'll give a brief explanation of the approach
>>    taken in the proposal mentioned at the beginning
>>    of this email (please look there for the
>>    details).
>>
>>    We assume that initially we have SFOL without equality.
>>    We get equality by explicitly axiomatising a
>>    predicate symbol "=".
>
>
> Ah, but that is a different matter. We have been talking about using a 
> logic-with-=, not about axiomatizing equality in a logic-without-=. 
> Different issues arise.

I am not so sure. Namely, I have a bit hard time having intuitions
about SFOL with a kind of built-in equality, as opposed to
axiomatisation.

While using equality axiomatisation directly during proof
search is a bad idea, the axiomatisation is a necessary tool
while designing strategies etc for provers: thinking about
the axiomatisation gives a way to understand the effects
of strategies, modifications of the calculi, etc.

In any way, the approach that "we have a logic with built
in equality and everything is fine there, BUT WE DO NOT
KNOW HOW TO AXIOMATISE THIS EQUALITY"
won't work. We have to be able to say clearly how the
equality we have should be axiomatised.

Hence I do not agree to dismiss the question of how
to axiomatise equality.

>>    However, if we look at simple SCL formulas
>>    (example, "forall x. p(x)") which SEEMINGLY
>>    do not need "app" and "holds" in the SFOL
>>    translation, then we have a tendency to overlook
>>    that the substitution axioms for "holds" and
>>    "app" will be created. These axioms are exactly
>>    the source of confusion from Horrock formulas!
>
>
> You seem to be making several assumptions at once here. First, that we 
> are not actually using the logic with-= , but are axiomatizing SFOL+= 
> inside SFOL (without =).  If we use an actual logic with =, then I 
> don't see any problem.  


Maybe there isn't, but we have to be able to axiomatise this
equality anyway, as said earlier. Thus the problem persists.

> On re-reading I think I may see your point. Suppose we claim that 
> users of SFOL who wish to use SCL *must* go through an SFOL->SCL 
> conversion and then use our SCL->SFOL mapping to enable their 
> FOL-based tools to apply to SCL. I think this would be a serious 
> mistake, but lets suppose we do. In that case, 'normal' SFOL syntax 
> will be implicitly mapped into the holds/app syntax, and then the 
> 'normal' way of axiomatizing equality will miss the extra axiom 
> instances needed for the holds/app vocabulary; so following the 
> 'normal' rules on the *original* SFOL syntax to figure out the needed 
> equality schema instances will fail. Is that the issue? 

Yes. The axiomatisation (parametric to vocabulary with holds/app only)
done AFTER the holds/app transformation will be stronger than the
holds/app transormation of the axiomatisation (parametric to the 
original vocabulary) done before.

The Horrock confusion appears because the axiomatisation done AFTER 
holds/app transformation
is different from the holds/app transformation of the original 
axiomatisation. These two
operations (axiomatisation of equality for a vocabulary and holds/app 
transformation) do not commute.

Hence the proposal of two different equalities.

> Because if so, I think that we can easily handle this by allowing 
> people to just declare that they are using the FOL subset of SCL 
> syntax and that FOL reasoners will apply.  

I had serious counterarguments to this approach above.

> And by adding that any use of the holds/app embedding would require 
> that appropriate instances of the equality substitution schema be 
> added to any target equality axiomatization (if that really needs to 
> be said: of COURSE they do, right?) 

Now I'd ask: what are these appropriate instances? Please bring some 
examples
or an algorithm for constructing them. We cannot just say "appropriate"
without specifying what is appropriate.

When you do this,  I am pretty confident that you will soon have to
tackle the Horrocks confusion and bringing out different versions of
equality may start looking like a nice cure :)

>>    QUESTION: Would you agree with the mentioned proposal
>>    or not?
>
>
> Not.
>
>> If not, please give your arguments and ideas
>>    for alternative solutions.
>
>
> 1.  I think the idea of two different equalities is semantically 
> incoherent.
> 2. Chris' most recent tweak to the MT has eliminated the Horrocks 
> sentences as a problem
> 3. This problem, if I follow it, has to do with axiomatizing equality 
> in FOL-without-equality, so is peripheral to our concerns for either 
> case. (I don't mean to say we should completely ignore it, only that 
> it is not central or fundamental. I think we can give a useful 'user 
> guide' for how to best handle axiomatizations of equality in various 
> subsets of SCL.)

To summarise the equality issue,  I'd be happy if we could avoid bringing in
two equalities (nothing cool about two different equalities) but I have 
no inclinations
 to believe this can be avoided unless:

- Somebody writes an SCL->SFOL embedding algorithm and
- Axiomatises equality

So that the Horrocks problems do not arise and we have access to the 
ordinary SFOL
equality.

A standalone MT and a claim that equality never needs to be axiomatised
is not sufficient for practical usability of SCL.

>
> Sorry again for the long delay in responding.
>
> BTW, will you be at the SW meeting in Florida in a couple of weeks? 

Yes. Hopefully we could arrange a small SCL meeting on site!

Regards,
            Tanel Tammet