A Mechanization of Type Theory

1. Constrained resolution.

Let E 1 = A/B 1 and E 2 = AJB 2 be two

non-terminal CCs.

let {x 1 ,x 2 , ··· , xn} be all the variables that appear free 1n both E 1 and E 2 , and {w 1 , w 2 , ··· , w} be neW variables of the same types which donnot appear in either E 1 or E 2 ·

We define the substitution :

NOw we distinguish p positive literals in A 1 and q negative literals in A 2 · That is, using ~ to denote disjoint union :

We say that the CC :

follows by constrained resolution from CCs E 1 and E 2 ·

2 . ~~~~~~~!!~ ·

Let E = A/C be any non- terminal CC, such that 1 contains a literal L whose predicate is a variable ; i . e . A= B W !L} . We have the following cases

1 0 if L is a positive literal :

if L is a negative literal ; i.e. L = I M

2- 2 Deduce E 2 = B LJ(q}/C U{ !M,lq}}

where q is a new variable of type o .

Any of the above CCs is said to be deducible from E by splitting.

completeness in w-order logic . The trick is to interpret predicate variables of type (a ~ o) ~or i nst ance ) over domains whi ch may be proper subsets of 2 ~a , where ~a is the domain of interpretation of objects of type a · We only impose that these domains be closed under opera­ tions corresponding to the different constructs of the language (for instance complementation, projection, etc ··· ) . In the same way ~( a- ~) may be a proper subset of ~a ~ ~~ ·

Tnis enlarged semantic characterization (general Henkin models) permits us to restrict validity to just those formulas which are deri­ vable in the logic .

I n the following, we shall therefore use satisfiable as an abbreviation for "has a gene­ ral Henkin model" .

Definition A property r of finite sets of propositions is called an analytic consistency property if and only if, for any finite set g of propositions, we have (y 1 ) to Cy 7 ) below.

• (y1) if r (g) , then there i s no literal 0 such that a E g and l a E g ,

• (y 7 ) if r(g U {l 1t a}) , then r(g U{la(X)}) for ru1y constantaor variable X of type a which does not occur free in a or S.

We are interested i n analytic consistency proper­ ties because they provide a sufficient condition for satisfiability, as expressed by the follo­ wing lemma from Andrews 1 , which extends results by Smullyan ·

o) . Lemma I . If r is any analytic consistency property ru1d 3 is a finite set of propositions such that r(g) , then g is satj.sfiable .

RulJs 1- 3 and 2- 3 depend on some arbitrary type a · I n practice we shall implement ,them by restricting a to some small initial segment of types .

3. Unification.

Let E = ¢/C be a terminal CC. If C is unifiable, we can deduce 0 from E.

This rule too is not directly mechanizable, since in the general case unification is net decidable. We can make it so by putting a bound on the number of steps of our unification algo­ rithm. For this reason our method may ultimate ­ ly lead to a double enumeration .

For any set ~of propositions , let ~· be the set of sentences (closed propos itions) obtained from ~ by replacing free variables by new cons­ tants in a one to one fashion . Obviously i f ~ is unsatisfiable then ~ · is unsatisfiable too , Now we define the following property r of sets of propositions :

r(~) if and only if ~ ~ is not refutable .

SOUNDNESS AND COMPLETENESS Lemma II . r is an analytic consistency property. The proof of this lemma is given in Hue t ' 0 · The idea is to prove eaxh of Cy 1 ) to (y 7 ) by proving the contrapositive statement about refu­ t a tion8 . For instance , to prove (y 1 ), let us assume that there exists a l iteral a such that a E g and l a E g · This implies that i n the clause form of 3 1 there are clauses (0 1 } and {10 '} . It i s well known that higher- order logic is Therefore from g ' we can deduce CC ¢/((o',a'}},

not compl e te , under the usual semantic characte- from which we deduce 0 by trivial unification. rization (Godel models) . However, Henkin 9 has S' being refutable, we have not r(g) by defini­ shown that a different characterization yields tion of r . Taking the contrapositive statement

we. get ( y 1 ).

Now let g be tences. By J£mma by definition of any unsatisfiable set of sen­ I and Lemma II : not r(g) and r, g is refutable.

This gives us the completeness of our system:

Theorem 1. Let ~es . If g is ~le. g be any finite set of senten­ unsat~sfiable then it is refuta-

The soundness is obtained by mapping refuta­ tions in our system i nto refutations in Andrews ' R system (Andrews 1 ), which is known to be sound if one assumes the axiom schema of choice . Let us call axiom of choi ce for type a the formula :

where the types of the variables are :

.=--~~::--:2=-::. Let g be any finite se t of senten­ g is refutable, then there exists a inite set e of axioms of choice such that U e is unsatisfiabl e .

Remarks.

In our formal presentation of the rules of infe­ rence, we have supposed that we wer e not trying to unify at all when r esol ving, instead we just generated constraints . The processi ng of the literals wl;i .ch are candidates for unification and the checking for consistency of the cons­ traints obtained is not necessary in theory, and it was more convenient to use this formali sm for our proofs . However , as was shown in our example above , it is highly desirable in prac­ tice to do some amount of processi ng when apply­ ing constrained resolution. Of course , this does not affect the soundness of completeness of the modified system, as long as we suppress only clauses with ununifiabl e constraints . There i s a trade- off here between many useless but fast derivations and few useless but slow ones , and it is difficult to estimate how much processi ng of constr a i nts should be done until the system is implemented.

In the case where the set of initial clauses is first - order, it is pos sible to process com­ pletely every constraint, and splitting i s not applicable . Our modified system reduces exactly to resolution in this case .

It should be noted that we have not assumed extensionality so far s ince Henkin models may not be extensional, as shown by Andrews · · However we have i n option a unification algo­ rithm which assumes the weak extensionality axiom :

We shall now present a few examples'of refutations . We have replaced the cumbersome existential parameters E(:\x ·O') by the usual Skolem functions X( y 1 , ··· , y ) , where the y. ' s are the free variables of a nand X is a n~w constant of the appropri ate type.

~~!:~~ 1.

Cantor ' s theorem : NN i s no t denumerabl e .

I.et ~ be the type "integer", n , f and h be vari ables , with types ~(n) = ~, -r(f)=C~- ~) and ~(h) = c ~. ~- ~).

We shall refute the negation of Cantor's theo­ rem : "it is possi ble to enumerate the functions of i nteger to integer", i.e.

After reduction to normal form we get , using N and H as Skolem functions, ~(N) = ( ( ~-+ ~)-+ ~), ~cH) = c~ . ~ -~) :

We shall need the followi ng property of equa­ lity

and the existence of a successor function S satisfying

The refutation goes as follows

R( 1, 2) 4

H(Nf , n) = fn

R( 4, 3) 5 ¢J1fn, SH( Nf , n)}

Note that the constraints coming from the first constr a i ned resolution can be completely processed , so that C = ¢. This short proof (3 steps) is due to a 4 conc i se representation of the problem. In particular, the use of type ~ for i ntegers gives us implicitly restricted quantification over integers without havi ng to carry additional literals .

The pigeonhole principl e : i f we distribut e m objects into n hol es., with m > n , there is at least one hole which contains more than one object .

We choose type a for the set A of objects and type ~ for the set B of holes. The hypo­ thes i s is :

1 0 \B\ < \A\ : there exists a one- one mapping from B to A, not onto.

20 \A\ < w : every one- one mapping from A to A is onto .

The conclusion is : there is no one- one

mapping from A to B.

Using the following atoms

'L"(=) = (a , a ..... o) or(~ . ~ ..... o) accordi ng to the context, we get , after reduction to normal form :

• 5 X y , Gx I Gy G is one- one A -+ B

We get the following refutation :

• R(3, 2) 6 Xh I Yh/{hZ(h, E) , Fu 1 } c6
• R( 4, 2) 7 hXh hYh/C 6
• R( 7, 1 ) 8 u v/C 6 + {hXh, Fu} + { hYh, Fv}
• R(8, 5) 9 X yjC 6 + {hXh, FGx} + {hYh,FGy}
• R( 9, 6) 10 ¢/{hZ(h, E) , Fu 1 } ,{ hXh, FGXh'} , {hYh,FGYh 1 }, {h 1 Z(h 1 ,E),Fu"}
• U( 10) 11 0 by substitution : {h <· A:x: ·FGx, ul~ GZ (t..x · FGx, E) , h 1 same as h , u" same as u 1 } .

When the theorem prover gets a refutation, it is trivial to gi ve the user a more natural proof in Andrew5 system, chai ning back the substitutions.

We shall demonstrate this technique here ; now S(n) means substitution i n clausen and C(n, m) means cut of clause n and clause m. H is an abbreviation for t..x ·FGx .

• S(2) 6 1 FGZ(H, E) I E
• S(3) 7' XH I YH, FGZ(H,E) E
• C( 6', 7') 8 ' XH I YH
• S( 4) 9 1 FGXH = FGYH, FGZ(H, E) = E
• C(6 1 ,9')10 1 FGXH = FGYH
• S( 1) 11' GXH = G YH, FGXH I FG YH
• C(10 1 ,11') 12 1 GXH = GYH
• S(5) 13 1 XH = YH, GXH I GYH

c (12 ~ J3 1 ) 1 4 I XH = YH

c ( 8 I J 14 1 )15 I ~

We shall now give a completely detailed refuta­ tion of a less trivial proposition. We are going to prove Knaster- Tarski 1 s theorem : "Any function monotone over a complete lattice possesses a fixpoint" . Let (A,E;;) be the comple­ te lattice considered .

We use the types : o for truth values

• for the elements of A.

We represent a subset of A by its characteris­ tic function, of type ( ~ ..... o). We use the follo­ wi ng axioms

(vxh)[ (hx :::> (1 h E;; X) & (( VY)(hy :::> X Y)::>X

[every subset h of A possesses a glb (1 h]

We want to prove :

(vf)[(vxy)(x E;;Y :::> fx E;; fy) :::> (~z)(fz = z)] The types of our atoms are, respectively :

x , y , z : ~

We negate the theorem and put all the proposi­ tions i n clause form . We use again the usual form of Skolem functions , replacing

by F , where Y and F are new constants of tJJJeS respectively ( L, ( L-+ o) -+L) and (L-+L) .

This gives us the following set of clauses

• X ~ X
• 2 I X E;; y , l Y ~ x , X y
• 3 l x E;; y, l Y E;; z , X E;; Z
• 4 l hx, n h E;; x
• 5 hY(x, h) , XE;;(1 h
• 6 l x E;; Y(x, h) , x ~ n h
• 7 l x E;; y, Fx E;; Fy
• 8 lFx =X

First we resolve 2 (on its last literal) and B. As the constraint {x = y, Fx 1 = x 1 } possesses a most general unifier {x ~ Fx 1 , y ~x 1 } we just substitute without generating any constrai nt,to get :

R(2 , 8) 9 l Fx E;; x, l x E;; Fx

Similarly, resolving 4 on its second literal with 9 on i ts second literal, we get

RC 4, 9) 10 l F n h E;; n h · l hF n h

[The last literal is a shorthand forl (h(F(n (h))lH

Next , we resolve the second literal of 7 with the second of 10. Here we do not know a most general way of unifying the two literals, and a constraint is added to the resolvent :

R( 7, 1 0) 11 l F (1 h E;; (1 h , l x ~ :w'{hF (1 h , Fx E;; Fy}

(This constr ai nt i d obviously unifiable , for i nstance by { h ~ 1\u. Fx ~ Fy} ).

We shall now resolve both literals of 11 with the second literal of 6. We have to unify :

• . firstly {F (1 h, x, x 1 }
• secondly {n h, y, (1h ' l and again we know a most general unifier

Notice that the substitution has been effected i n the constraint from 11 as we ll as i n the li­ terals . We shall denote this new constraint by

c.

The re s t of the refutation is pretty straight­ forward , no new constraints be i ng gener ated

This last CC is the analogue of 12, 5 and 6 having one literal in common due to the initial reduction to clause form .

Next we resolve both literals of 15 with 16, ob­ taini ng therefore a terminal CC :

R(16, 15) 17 ¢/C 1 where C 1 consists of the following constrai nts :

We then apply our uni fication process to C 1 , which terminates with answer "yes", correspon­ ding to the unifier :

The refutation is now completed, and it is tri­ vial to go back in the proof , substituti ng a and the substitutions derived f rom it by compo­ sition with the unifi ers already detected, to

get a ground refutation.

In particular, we shall substitute n AU· Fu ~ u for x in B. which gives u·s explicitly a fixpoi nt of F , name ly n( (ujFu ~ u} ), which is precise­ ly its least f ixpoint .

Notice that splitting was not necessary here either , and that the refutation is pretty short and does not i nvolve huge constraints .

CONCLUSION

It is.difficult to make any efficiency assertion from searchless exampl es . However , one of the mos t important heuristic rules to use in this system would be to throw out clauses with constraints which are obviously not unifia­ ble . In practice of course most clauses will be recogni zed as such, thereby reducing sharply the number of possible derivations .

Types i n this logic play a multiple role . First, they permit us to have A normal forms for all terms . Second , they can be used to sort objects of different nature , and so we ge t res­ tricted quantification without adding cumbePsome additional literals . Finally, as a consequence they restrict the search for unifiers .

This system uses the constraints mechanism to delay as much as possi ble the process of unifi­ cation . This has two advantages . First , the dee­ per we go in a refuta tion, the more information we gather about the structure of the terms we need to substitute . This reduce s our search space for unifiers (intuitively, the more argu­ ment - value pairs we know, the less functions exist whose graphs contain these pairs~

Second, we just need to check for the exis­ tence of some unifier , we do not need most gene­ r al ones . This permits us never to consider the unifica tion of two terms whose heads are varia­ bles , such as :

These cases are the most difficult ones to mnsider for most general unification , but they are trivial when we need only check for exis­ tence of unifiers (take any constant funct ion) . Actually we need to compose only two elementary unification processes (called i mitati on and projection) , whereas to get most general uni­ fiers Pietrzykowski and Jensen'~ need four , the other two be i ng the most prolific ones i ndeed . This i s because when we consider a pair such as f(A 1 , A 2 , ··· ,A ) and F(B 1 , B 2 , ··· , B ) , we know something defiBite about the structRre of the common instance (it must begi n w~th an F) and so we have a "handle " on the uni fication pro­

cess .

A di sadvantage of the delaying of unifica­ tion i s that we may generate clauses whose cons - traints cannot be satisfied and thi s i s why some processing of these constrai nts i s neces­ sary. In many cases we will know a most general uni f i er of some constraint and thi s unifi er should be applied to the cl ause . In other case s we may know that no substitution will uni fy the constraints, and then we should de lete the clause . There is a trade - off here i n the amount of unifying while searching which should be done .

Automatic theorem proving i s undoubtedly more difficult here than in first - order logic . However our higher- order language permits us to state many theorems in a more concise way, and refutations tend to be a lot shorter . For i nstance , i n our examples , we used set vari a­ bles i n a very natural way (us i ng their charac­ teristi c predicates) . We coul d get all the propert i es of E wi th application, of complementat ion with l and of union with V · Also the abstraetion mechanism of A- calculus replaces in a ni ce way cumbersome comprehension axioms.

However we might still need use some axioms of descript i ons , to assert the existence of

certai n functions :

When we need to substitute non- atomic propo­ sitions for predicate variables (vi a splittingl refutations tend to become messy and unnatural. The system should be improved on thi s point , maybe by replacing splitting by rules closer to natural deduction . This woul d also allow us to get r i d of the i nitial r educti on to clause form, which is not always desirable , and to use we l l ­ known techniques to decr ease the complexity of refutations (Ernst 7 ) . Only then can we hope to deal with proofs by induction in a satisfactory way.

In conclusion, we have presented in this paper a system of logic which is a generaliza­ tion to Church 's type theory of Robinson ' s reso­ lution. This system seems well suited to mecha­ niz i ng proofs which require complex substituti­ tions for function variables , as shown i n a few hand-simulated examples . Substitutions on non­ atomic propositions for prredi cate variables are not dealt with in a very satisfactory way yet , and some improvement is needed there . Our sys­ tem without extensionality is equivalent to Andrews ' system. However it i s amenable to auto­ matic treatment because the substitution ru~e has disappeared . Our system with extensionality ought to be equivalent to Pietrzykowski 's sys­ tem, and it i s conj ectured that it is more effi­ cient . A partial implementat i on is i n progress at IRIA, mechanizing constrained resolution without spli tting . The emphasis will be put on the heuristic rules for processing constraints duri ng the r efutation.

ACKNOWLEDGEMENTS

This paper presents results contained i n the author 's Ph . D. thesis at Case Western Reser­ ve University, under the direction of Pr. G.W. Ernst . This research was supported by the National Science Foundation under Grant N° GJ- 1135 .

The author wishes to thank the referees for their helpful comments .

BIBLIOGRAPHY

• Andrews P. B. ( 1971) Resolution i n type theory Journal of Symbolic Logic 36, 3 pp .414-432 .
• 2 Andrews P.B. (1972) General models and extensionality. Journal of Symbolic Logic 37,2 pp . 395- 397 .
• 3 Church A. (1940) A formulation of the simple theory of types . Journal of Symbolic Logic 5,1 pp. 56- 68 .
• 4 Church A. ( 1941) The calculi of lambda-conversion. Annals of Ma thematical Studies no.6 . Princeton University Press.
• 5 Curry H. B. and Feys R. (1958) Combinatory Logic (Vol 1) North Holland , Amsterdam.

6 Ernst G.W. (1971)

A matching procedure for type theory .

Computing and Information Sciences,

Case Western Reserve University.

• 7 Ernst G.W.( 1971) The utility of independent subgoals in theorem proving . Information and control 18, 3 pp. 237- 252 .
• 8 Gould W.E(1966) A matching procedure for t.t1- order logic. Scientific Report N°4, AFCRL 66- 781 (Contract AF 19 (628) - 3250) AD-646 560 .
• 9 Henkin L. (1950) Completeness in the the ory of types . Journal of Symbolic Logic 15,2 pp . 81 - 91.
• 10 Huet G.P. (1972) Constrained resolution : A complete method for higher order logic . Ph .D. Thesis , Case Western Reserve Univ . Jennings Computing Center Report 1117 .
• 11 Huet G. P. (1973) The undecidability of unification in third order logic . Information and Control 22, 3 pp . 257- 267 .
• 12 Pietrzykowski T. (1971) A complete mechanization of second order logic . Report CSRR 2038, Department of Applied Analysis and Computer Science, University of Waterloo . Also Journal of Assoc. for Camp . M·ach. 20, 2 pp . 333- 364.
• 13 Pietrzykowski T. and Jensen D. ( 1972) A complete mechanization of w-arder type theory . Report CSBR 2060, Department of Applied Analysis and Computer Science , Uni versity of Waterloo. Also Assoc . for Camp. Mach . National Conf . (1972) . Vol 1, pp . 82- 92.
• 14 Robinson J . A. (1965) A machine-oriented logic based on the resolution principle . Journal of Assoc. for Camp. Mach. 12, 1 pp . 23-41.
• 15 Robinson J.A. ( 1968) New directions i n theorem proving . Proceedings of IFIP Congress Edinburgh August 1968 i n Information processi ng 68, Vol 1 pp. 63- 67, North-Holland, Amsterdam.
• 16 Robinson J . A. (1969). Mechanizing higher order l ogic . Machine Intelligence 4, pp . 151-1 70. American Elsevier , New York.