--- title: "A Mechanization of Type Theory" authors: - "Gérard P. Huet" doi: "" url: "https://ijcai.org/proceedings/1973/19" pdf: "https://ijcai.org/proceedings/1973/0019.pdf" venue: "Proceedings of the Third International Joint Conference on Artificial Intelligence" year: 1973 pages: "139-145" track: "Theorem Proving and Logic: 2" keywords: --- # A Mechanization of Type Theory Gérard P. Huet *Proceedings of the Third International Joint Conference on Artificial Intelligence*, pages 139-145. ## Abstract A refutational system of lo gi c for a l a nguage of orde r w is presented . This langage :i.s a s li ght modif i ca t i on of Church 1 s A-calculus wi th types . The system i s comp lete , in the sense th at a refutation of a set of sentences exists i f and on l y if this set does not possess a general Henk in mode l . Th e main rul e of i nference is a generalizat ion of Robi nson ' s resol u t io n to typ e theo ry , which all ows us to get ri d of the substitut i on r ule. ## Full text ## 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.