[SCL] SCL basic consensus badly needed
pat hayes
phayes at ihmc.us
Thu Oct 2 11:52:16 CDT 2003
>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 will try to produce a sketch soon (This weekend?? Hmmm.)
>
>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.
Thanks for that, it is very encouraging. It
suggests to me that it would in fact be
relatively easy to modify the code of such a
system to use SCL syntax directly, without the
app/holds transformation being necessary. I now
have some hope that once we publish SCL, such
systems may appear fairly quickly.
In the meantime however we must continue to hoe this row.
>
>>> 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:
I meant that SFOL syntax is a special case of SCL
syntax, and the SCL MT applied to it (now) gives
the very same semantics as a FOL MT does, even
with =. So just ignoring any encodings, we can
assert that SFOL as it stands is a genuine
sublanguage of SCL. The encodings introduce new
issues, I agree.
>in this case
>only a subset of SFOL is in SCL, while SFOL formulas containing
>other predicates are not.
In that case, indeed. The embedding of SCL into SFOL also embeds SFOL.
>
>>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.
Well, I understand. But I think that as an ATP
hacker you can choose to take either stance. YOu
can say: I am conforming to SCL specs by working
strictly in FOL; or you can say: I can handle all
of full SCL (in a lower voice:) by encoding it
all into FOL using the holds/app style. Now, in
the second case, *someone* indeed has to pay
attention to the encoding and its complications,
including those involving = . If you want to
claim full SCL performance while keeping the
encoding secret, as it were, then you need to pay
attention to those details: if you want to just
deal with FOL then you might require that your
users supply you with the encoded axioms. But
either way, someone has to not drop the ball,
indeed.
>
>> 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.
I meant that we should not define the
relationship between SCL and FOL in this way as a
primary defining relationship. That suggests that
FOL users of SCL must use this translation in
order to conform, which would be misleading.
>
>>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.
Let me explain my thinking. We are trying to
write a very general specification. It is of the
nature of specifications that they define
conformance, and we anticipate that there will be
various kinds of SCL sublanguage and various
kinds of conformance. In particular, someone can
declare that they are conforming to a sublanguage
of SCL, such as SFOL, in the sense that they
provide full SFOL inference and parsing (using
the SCL grammar for conformance and
intercommunciation with other SCL systems) but do
not undertake to accept any expressions outside
the SFOL sublanguage. Other systems might only
accept Horn clauses, or whatever. Accepting
conformance to the entire SCL grammar is a larger
commitment, but all this app/holds stuff arises
in order to make it possible for someone with a
conventional ATP system to declare *full* SCL
compliance without having to mess with his code.
This is a rather special (though I agree
important) case, and as long as we give a
reasonable road-map of how to do this, I think we
will have discharged our duty. We do not need to
base the entire SCL spec on this particular case,
however.
>
>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.
Yes, but in the context of what its owner is
claiming it can do. Different claims may require
different strategies.
>
>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.
True. I would anticipate that this scenario would
require that the files identify which subset of
SCL they are written in (and which concrete
syntax, by the way.)
>
>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?
I see where you are going, and agree there is an
issue here. However this is an issue in SW
design, viz. how some published content can as it
were advertise what language it is written in.
Your point is that if we rely on existing ATP
technology to do SW inference when content is
written in a mixture of SFOL and full SCL,
relying on the holds/app transform to reduce it
all to the ATP's native FOL, then we never know
when we might need to later transform something
that we previously treated as just being FOL,
thereby rendering all our entailments suspect or
at least requiring a lot of work to be done.
True, if that is how SCL got deployed on the Web
then we might have that issue. However I think we
are a long way from that scenario arising in that
level of detail, to be frank. Most of the
deployed SW content is going to be written in
sub-FOL languages like RDF and OWL and maybe a
few Horn-rules languages, and we can provide
standard embeddings of these into SCL and if
necessary into the SFOL subset (using embeddings
where we say so) which will suffice to handle a
lot of the existing traffic for the immediate
future. If your issue ever gets to be a serious
problem I think the SW will by then have evolved
techniques for indicating markup style and for
negotiating mutually acceptable encodings for
transferring content.
>
>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.
Different, but we know how to map between them. I
bet it would in fact be fairly easy to keep that
mapping inside the ATP code so that it could move
between them as required, for an ATP adapted to
this style of SW use. It is easy to see how to
adapt an MGU to match SCL with holds/app-embedded
SCL, right? (Just flush the holds/app stuff from
the subexpressions and don't require the relation
name to be an atom.)
>
>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
Yes, caching is always an issue if we have nay
kind of re-coding going on, obviously. BUt again,
I don't think this is unsurmountable, even in the
worst case; and I suspect that the problem will
be solved before we get to it, in practice, by
existing and emerging SW markup conventions.
>
>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 don't think it really has to do with the
Horrocks stuff any more. It is all to do with the
embedding.
>
>>
>>>
>>> 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.
Oh, sure; but it is easy to axiomatize SCL =y in
SCL; and its also easy to axiomatize h/a-embedded
SCL =y in the SFOL subset. Your issue, I think,
is that the h/a-embedding of the first is not
exactly the same as the second, right? Well, OK,
so it isn't, so one has to be little careful
about = when doing the embedding.
>Hence I do not agree to dismiss the question of how
>to axiomatise equality.
I don't mean to dismiss it, but I think it is
fundamentally straightforward, modulo the above
embedding point.
>
>>> 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.
I think that if the declaration is made part of
the SW content - and I agree we have not
discussed how to do this, but for example in the
XML syntax it could be in the file header as an
attribute value - then I think there is no
fundamental problem here.
>
>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.
One needs instnaces of the substitution schema
for all of the vocabulary. If the vocabulary of
your theory uses holds/app then you need those
instances.
>
>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 :)
OK, I take that as a challenge to give more
details. I will try to do that soon. It is time
that the whole SCL->SFOL holds/app embedding was
written up in FULL detail anyway.
>
>>> 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.
Yes, we need to do that. OK, I will try.
>
>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.
Great! Chris will be also and maybe some others.
Maybe we should wear hats with SCL written on
them, or something.
>Hopefully we could arrange a small SCL meeting on site!
Indeed.
Pat
>Regards,
> Tanel Tammet
>
>
>
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl
--
---------------------------------------------------------------------
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 ihmc.us http://www.ihmc.us/users/phayes
More information about the Scl
mailing list