Mechanizing a Particularly Expressive Many Sorted Logic

1. INTRODUCTION

A problem arising in many AI systems is that of matching two structures. The simplest form of matching is a purely 'syntactic' comparison of nested patterns organised hierarchically, see (s]. Tips of the patterns are either constants (which match only if equal) or variables (which match any pattern in which they do not occur), We consider matching processes which utilise sort information; these are still relatively simple and syntactic (and thus cheap) but offer considerable selectivity, since the mismatch of sorts can prevent unifications which lead to useless inferences (contrast, e.g., KRL [1] where 'matching' covers arbitrarily complex inferencing). Moreover, it is sometimes pos­ sible to infer the truth value of an expression merely on the basis of the sorts of some of its subexpressions, E.g., if cis female then FATHER(c) is definitely false,

2, ASSIGNING SORTS TO EXPRESSIONS ____ ....;..;...;;.;;;.;;;...;;..;.;.;;..

Mechanized sorted logics are not new (e.g., (2], (a], but typically their expressive power has been limited by the restrictions on how expres­ sions may be sorted; in particular, variables must usually be quantified over a si~e sort thus precludingpolymorphism (though LBJ allows a very limited polymorphism).

Defining polymorphic functions is a common and useful style of programming. We want to use polymorphism in axiomatisations. Hayes (4] des­ cribes a logic allowing polymo~hically sorted relations and functions. (In L7] Strachey dis­ tinguishes 'parametric polymorphism' in which, e.g., maplist has sort (a +8) + list(8), from

'adhoc polymorphism' or overloading; our imple­ mentation only handles overloading), Rather than variables having sorts, each relation and function h has an associated sorting function h' which specifies which sorts are legal arguments and for each legal combination of argument sorts, the sort of the value of the function, [s] makes heavy use of this logic,

Thus the sort restrictions are specified once only for every non-logical symbol and the sorts a variable may have in any wff are determined by context. This is more convenient than specify­ ing the sorts locally in every wff.

As a simple example consider the following naturally polymorphic relation spouse: ( MANxWOMAN + U)+( WOMANxMAN + '\1) (the choice of 'L as the range is explained in sec. 4).

In a monomorphically sorted logic, we must de­ fine spouse: HUMANxHUMAN+ V.

which fails to capture all the constraints of our earlier definition; alternatively, if we allow a partial ordering on sorts (see sec. 3) then it it possible to define SPOUSE in terms of WIFE and HUSBAND with tighter sort restrictions, at the expense of forcing a two way split in the search space, depending on whether we assume WIFE(x,y) or HUSBAND(x,y). Our implementation allows the or-branching implicit in a polymor­ phic function to be maintained internally in a single derivation rather than forcing a spli t into several derivations, increasing the search­ space branching rate,

However, contrary to Hayes' claim in [4], mecharr izing such a sort structure is not trivial, E.g., if g:(SlxS2 +Sl)+(S2xSl+S2) then {P(g(x,y),g(y,x)),P(u,u)} should fail to unify,

MECHANIZING A PARTICULARLY EXPRESSIVE MANY SORTED LOGIC

Anthony Cohn Department of Computer Science University of Essex, U.K.

as should {Q(y,g(x,y),g(w,x)),Q(u,v,g(v,u))}, because the resulting terms (g(x,x) in the former and g(g(x,y),x) in the latter) both violate g's sort constraints. The difficulty occurs when merging two variables, because the checks cannot be kept local to the part of the proof tree being operated upon, as the scope of a variable is that of the whole proof tree. E.g., merging x/u would mean the erstwhile legal proof tree containing the terms g(x,y), g(y,z) and g(z,u) would become illegal; locally each terms looks correct; inconsistency is only de­ tected when the three terms, which may be widely separated in the proof tree, are considered together.

We need to be able to check the sort restric­ tions globally. For every well formed expres­ sion (wfe) b, we can define a partial function B:F+S where F=V+S, V is the set of variables and S the set of (for the moment) disjoint sorts, such that B(f) is defined and gives the correct sort for the wfe for the combination of sorts on variables specified by f. We can regard fc F as specifying an environment in which every variable is bound to some sort. B then speci­ fies which environments are permissible for b, and what the sort of b would be in that environ­ ment.

In our implementation, we choose to represent B as an n-dimensional square array called a sort array(SA), with as manr rows and columns as there are sorts and n=IVI. Thus every position represents an f~ F. We define domB={f:B(f)' S}. If sorts are being used to good-effect then ldomBI will be small and thus the array sparse. Ir-QomB=~ then no combination of sorts of variables is legal: b is illformed.

We can compute the SA for a proof tree incremen­ tally as the tree is built; the operations on SAs that we need to perform mirror the opera­ tions on the tree: substituting for variables and attaching new expressions to the proof. The primitive building blocks are the SAs represent­ ing the sorting functions of nonlogical symbols.

The following example illustrates two of the basic operations that we need to perform on SAs. Suppose the SA for term g(x,y) is as in Fig. 1, then binding x to g(u,v) gives the SA for g(g(u,v),y) in Fig. 2. Binding a variable to a a term with k new variables increases the dimen~ sionality of the SA by k-1. Merging two varia­ bles decreases the dimensionality by one, by taking a diagonal slice through the array. So substituting u/y picks out the rows on the y=u diagional, giving the SA for g(g(y,v),y) (see Fig. 3). Binding v to a constant c of sort Sl gives a vector with no defined entries; thus g(g(y,c),y)) . is not a wfe.

.,

3. NON-DISJOINT SORTS

A sort specifies a subset of objects in the uni­ verse. If we allow non-empty intersections then we naturally induce a partial ordering (i.e,, set inclusion) on S. Matching the sorts of two terms when unifying is then set intersection,

Inclusion induces a partial ordering on F and F+S in the usual way, e.g.:

Vfl,f2€ F fl ~ f2 : V vc V fl(v) 2 f2(v) We require B in F+S to be monotonic: fl ~ f2 => B(fl) 2 B(f2) and sensible:

Vd a domB, d + ~: lz = Ud => Jy = U{B(f): f( d}. With these (natural) restrictions, the implemen­ tation sketched above can be extended to the case of non-disjoint sorts. Considerable com­ putational and space savings follow from the observation that one can often calculate some entries in a SA, given others, Thus only part of each SA already sparse - needs to be explicitly stored in memory. Details of such normal SAs are in [3] ·

4. SORTING WFFS,

The value of a wff is true or false, Defining a single sort U = {true,false} leads to problems: we can only sort MOTHER and FATHER loosely as ( HUMANxHUMAN+ U) to make sense of Vx,y PARENT(x,y) : MOTHER(x,y) y FATHER(x,y) otherwise x.: MANu WOMAN! We shall define the functionality of SAs for wffs as F+BOOL where BOOL = {tp ,F' ,U.} and F = {false} and tf = {true}. We can induce a lower semi-lattice on BOOL as we did on S. We now sort MOTHER and FATHER as (MANxHUMAN+ F )+(WOMANxHUMAN+U) and ( MANxHUMAN+ \L) +( WOMANxHUMAN+ F ) respectively.

An advantage of this technique is that charac­ teristic predicates need no special treatment by the inference machine; e.g., we can sort MAN: (MAN+"f}+(J.\MAN+QW).

To demonstrate a second advantage let r={B(f): fC F} where b is some wff; if r = {f'} then b is a contradiction (e.g., MOTHER(John,x)) and if r = {"f} then b is a tautology (e.g., ,MOTHER(John,x)), Similarly if we are trying to prove V x,y MOTHER(x,y) and we resolve against the above assertion then we need only resolve away the subgoal PARENT(x,y) since FATHER(x,y)

can be inferred false by the sort structure. This technique generalises the concept of insig­ nificant literal in [2],

5, !!!E_ EFFECT .Q[ ~ ~!.!!, ~

We can only sketch this interaction: full de­ tails and proofs, including completeness and soundness results will be found in [3],

Every SA represents a set of axioms which would otherwise have to be explicitly asserted; e.g., if b: (SlxS2+S3)+(S4xS5+S6) then the missing axioms are (assuming disjoint sorts): \/x,y S3(b(x,y)) : Sl(x) 1\ S2(y) and Vx,y S6(b(x,y)) E S4(x) and SS(y) We must take account of these implicit axioms if we are to prove (say) S2(c), for a proof of S3(b(c,y)) would imply S2(c), That a given SA B is correct may be shown by proving that the equivalent axioms follow from the sort lattice axioms, the primitive SAs for all the nonlogical symbols and from b itself,

The axioms which define the structure of the sort lattice are eliminated in two ways, (l) Use of lattice theoretic operations (e.g. ), U) on SAs (see definitions below), (2) By extending resolution in the following way. We must allow Si(c) to match with any positive literal Sj(t) (where Sj usc Si, t unifies with c, Sc, Si, Sj C S and Sc(c)), This includes the conventional case where Sj=Si, It must also match Sj(t) where Sj usc 1: Si provided we also prove ,(Sj Si)(c)a, where a is the sub­ stitution unifying t and c, Similar but dual techniques apply when trying to prove ,Si(c),

We now present a formal definition of how to compute the new SA D after substituting e for x in a proof tree b, We need only consider the modified SA B for which {B(f):f· domB}:{\L} . -- . Slnce for all other f c domB we can already infer b 1 s truthvalue, So clearly if f c. domD then D( f)= W. , There are two cases to consider (1) e is a variable then Yfc domB 3z=f(x) j,l f(e) =>

(Av,v=e+z, vfx-+f(v))« doaD (2) e is not a variable-­ '#fc domB, gc domE f(x)' E(l) =>

(Av,vfx+(f+iJTv>h! domD If necessary b and e must be standardised apart before computing D, Subsequently the erstwhile shared variables must be remerged, diagonalizing in each case,

~oth the above operations have to be modified slightly to propogate normality~ Definition (2) only allows a term to match a variable of a lesser sort, though we can remove this restric­ tion by replacing the left hand side with 1 3 z=f( x)" E(g) 1 , providin1 that we &lao prove that e is of the more restricted sort; the resulting logic is more expressive (noticed first by Plotkin), E.g., suppose we wish to prove J xP(x) where P is only defined on abelian groups. If we know that R(g) and that ~~R(x)=>P(x) (where R is defined on groups and g is some group) then we can complete the proof providing we also prove that g is abelian (clearly abelian-group~ group). Polymorphism complicates the precise definition of- this ex­ tension so we do not give it here.

6, CONCLUSION

The difficulty experienced in mechanizing a theoxy or language is usually proportional to its gen­ erality or expressiveness, We have proposed a particularly general many sorted logic: allow­ ing polymorphic functions and a partially ordered sort space; furthermore, the sort of an expression may someti~s be determined solely from sort information,

A pilot implementation which works for the basic theory is currently being extended. At present SAs have to be ground instances, i,e,, sort meta­ variables, allowing parametric polymorphism are not permitted, It is hoped to include this facility,

7, ACKNOWLEDGEMENTS

Phil Collier and Jon Cunningham made useful comments on a draft; I am particularly indebted to Pat Hayes for his help and guidance.