[SCL] Concrete embedding proposal to TFOL (GOFOL, SFOL)
pat hayes
phayes at ai.uwf.edu
Wed Jun 4 16:09:52 CDT 2003
>Hi,
>
>While Pat and Chris are busy working out the finer points of the
>semantics of SCL, I have been a bit worried about the practical
>usability of SCL by ordinary TFOL (GOFOL) theorem provers.
>
>In my understanding these systems do need an embedding
>(transmogrifying, as Chris put it :-) of SCL to TFOL.
>
>In order to check out whether my intuitions about SCL
>coincide with other people I wrote such an embedding
>of SCL to TFOL (named SFOL for "standard FOL" in
>the following).
>
>The embedding is nothing fancy: it is completely
>traditional and intuitive, except for (perhaps) the
>details of translating equality, where we have had
>(and probably still have) different viewpoints.
>
>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.)
>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.
>
>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. 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). 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.
Pat
>Mapping SCL formulas to SFOL
>--------------------------------------------------
>
>In order to facilitate the use of standard first order predicate
>calculus (SFOL
>in the following) for proving theorems presented in SCL, we define a mapping
>M from SCL to SFOL.
>
>This mapping holds both in cases a syntactically correct SCL formula F
>is also a syntactically correct SFOL formula and in cases where F is not
>a syntactically correct SFOL formula (for example, if F is a formula
>"forall x. x(x)" then F is a correct SCL formula but not a correct
>SFOL formula).
>
>In other words, the mapping treates SFOL formulas in the same way as
>any other SCL formulas: SFOL formulas are simply a subset of SCL formulas.
>
>The result of the mapping is intended to be usable by SFOL theorem
>provers. Obviously, the provers may (and do) use their own conversion
>mechanisms and special machinery (equality handling is a typical example).
>Such further modifications by provers are OK if the crucial
>properties detected
>by the provers (for example, satisfiability and (for some provers)
>also the size of models)
>are preserved.
>
>Observe that the mapping automatically defines a standard FOL semantics
>for SCL formulas. The important points of the semantics defined by the mapping
>(satisfiability, size of models, etc) coincides with a "standard FOL" reading
>of SCL formulas. In particular, if an SCL formula F is a syntactically correct
>SFOL formula, then F is satisfiable iff the outcome of mapping M(F)
>is satisfiable.
>Essentially, the mapping M(F) changes only the signature of F, not
>the important
>logical properties of F.
>
>The mapping M defined in the following is normative for SCL: this is
>THE mapping
>of any SCL formula to SFOL. Mappings which are different from M are
>not correct
>SCL mappings. Using only the correct SCL mapping is crucial for compatibility
>of various SCL concrete syntaxes, ordinary SFOL formulas and translated
>forms of various other logic-based languages to SCL. The correct mapping
>guarantees that in a conjunction of formulas translated from
>different languages
>the subformula components are interpreted correctly.
>
>We will present the mapping M in two parts: the first part defines a mapping
>M' from SCL formulas without equality, while the second part extends the
>definition of M' to the mapping M, covering also formulas with equality.
>
>The approach used in the mapping for the equality predicate is axiomatic.
>Equality predicates are considered to have no intrinsic meaning: their
>meaning is explicitly given by the axioms constructed by the mapping.
>
>M': mapping SCL formulas without equality to SFOL
>- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>
>SCL contains two distinguished predicate symbols for equality, "=" and "scl=",
>(their difference is explained in the following section).
>
>Although the mapping M' in the current section is defined also for the
>case where a mapped SCL formula F contains predicates "=" or "scl=",
>the mapping M' is incomplete in such cases. If F contains "=" and "scl=",
>then the complete mapping M defined in the next section adds the
>necessary axioms to the result of M'(F).
>
>In case a mapped formula F in SCL does not contain "=" or "scl=", then M(F)
>is equal to M'(F).
>
>Observe that in SCL formulas the terms p and f in the following atoms
>p(t_1,....,t_n) and terms f(t_1,....,t_n) may be arbitrary terms of SCL,
>not just symbols as in SFOL.
>
>For any atom p(t_1,....,t_n) in SCL:
>
>if p is not a symbol "scl=" then:
> M'(p(t_1,....,t_n)) := holds_n+1(M'(p),M'(t_1),....,M'(t_n))
>if p is a symbol "scl=" then:
>M'(p(t_1,....,t_n)) := scl=(M'(t_1),....,M'(t_n))
>
>For any term f(t_1,....,t_n) in SCL:
>
>M'(f(t_1,....,t_n)) := app_n+1(M'(f),M'(t_1),....,M'(t_n)))
>
>For any formula c(a_1,....,a_n) in SCL where c is a logical connective from
>the set {implies, and, or, not, equivalent} and a_1,...,a_n are atoms:
>
>M'(c(a_1,....,a_n) ) := c(M'(a_1),....,M'(a_n))
>
>For any q(x,a) in SCL where q is a quantifier from
>the set {exists, forall}, x is the variable bound by q and
>a is the formula in the scope of q:
>
>M'(q(x,a)) := q(x,M'(a))
>
>For any q(x,p,a) in SCL where q is a quantifier from
>the set {exists, forall}, x is the variable bound by q,
>p is a restriction predicate symbol on x and
>a is the formula in the scope of q:
>
>M'(q(x,p,a)) := q(x,M'(p(x)) implies M'(a)
>
>
>M: mapping SCL formulas with equality to SFOL
>- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>
>SCL contains two distinguished predicate symbols
>denoting equality:
>
>(1) =
>(2) scl=
>
>Intuitively, "=" is the equality predicate used in SFOL
>formulas, while "scl=" is a special, strong equality predicate of SCL.
>
>Thus, in case an SCL formula F with equality is also considered to
>be an SFOL formula (in other words, if we tract a standard FOL
>formula in the SCL context), then F contains only = as an equality predicate.
>No SCL formula G containing scl= cannot be considered to
>be a correct SFOL formula.
>
>The following defines an extension M of the mapping M' to
>the case where a formula F in SCL contains an equality (either
>"=" or "scl=")
>
>M(F) := M'(F) & M'(equalityaxioms(=,F)) & equalityaxioms(scl=,M'(F))
>
>where equalityaxioms(e,f) is a set of axioms for a distinguished
>equality predicate e in an SFOL formula f, computed for e and f in
>a traditional way from the signature of f (signature meaning the set of
>all predicate and function symbols in f). equalityaxioms(e,f) consist of
>three subsets: equivalence axioms, substitution axioms for function symbols,
>substitution axioms for predicate symbols.
>
>Equivalence axioms:
>
>forall x. e(x,x).
>forall x,y. e(x,y) implies e(y,x)
>forall x,y,z. (e(x,y) and e(y,z)) implies e(x,z).
>
>Substitution axioms for function symbols present in the formula f
>contain n axioms for each function symbol fsymb in f, where n is
>arity of fsymb
>and the position of the variable x (resp y) in
>fsymb(z_1,...,x,....z_n) (resp fsymb(z_1,...,y,....z_n))
>is iterated from 1 to n, so that for each fsymb and each position in
>the set {1,...,n} there is
>exactly one substitution axiom of the following form:
>
>forall x,y,z_1,...,z_n. e(x,y) implies e(fsymb(z_1,...,x,....z_n),
>fsymb(z_1,...,y,....z_n))
>
>Substitution axioms for predicate symbols present in the formula f
>contain n axioms for each function symbol psymb in f, where n is
>arity of psymb
>and the position of the variable x (resp y) in
>psymb(z_1,...,x,....z_n) (resp psymb(z_1,...,y,....z_n))
>is iterated from 1 to n, so that for each position in the set
>{1,...,n} there is
>exactly one substitution axiom of the following form:
>
>forall x,y,z_1,...,z_n. e(x,y) implies (psymb(z_1,...,x,....z_n)
>implies psymb(z_1,...,y,....z_n))
>
>We note that in the definition of a mapping M
>
>M(F) := M'(F) & M'(equalityaxioms(=,F)) & equalityaxioms(scl=,M'(F))
>
>the translation M(F) in equalityaxioms(scl=,M'(F)) cannot contain any
>function symbols except app_i for several arities i, and it cannot contain
>any predicate symbols except scl= and holds_i for several arities i.
>
>---------------
>
>
>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 ai.uwf.edu http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu for spam
More information about the Scl
mailing list