Type Inference in Prolog and Its Application

1. IDtroduetloa

It gives usefull information not only to programmers but also to meta-proceaaing systems to infer characteristics of execution-time behavior from program texts. Especially in Prolog, it is usefull to Jmow of what type a variable in a query is when the query succeeds. We call such a task type inlerence [8}. In this paper we present a type inference method for Prolog programs. After aummarising preliminary materiala in aection 2, we describe type inference algorithma for Prolog programs in aection 3. An application to verification is shown in aection 4. See [7) for more details.

2. Prellmlaarle1

In the followings, we assume familiarity with the basic terminologies of first order logic such as term,atom,substitution and most general unifier(mgu). We also assume Jmowledge about semantics of Prolog 1uch aa Herbrand univene H ,Her brand interpretation I,minimum Herbrand Model Mo and transfor­ mation T of Herbrand interpretation aasociated with Prolog programs (see [1},[4)). We follow the syntax of DEC-10 Prolog [10} . Anatom p(X1,X2 , ... ,X,.) ia said tobe in generalform when xl, X:a, ... , X,. are distinct variables. A Substitution u ia called substitution away from an atom A when u in­ stanciates each variable X in A to a term t such that every variable in t is a fresh variable not in A.

2.1. DeflDltloa of Data Type.

We iatroduce t)'pe iato Prolog to separate definite clauaes for data structures from others for procedures,e.g.,

t)'pe defines a unary relation by definite clauses. The head ofthedefinite clause takes a term defl.ning a data struc­ ture as the argument, either a constant b called bottom ele­ ment or a term of the form c(t1, t 2 , · .. , t,.) where c is called constructor. The body showa a type condition about the proper subterms of the argument.

Here note the set of ground terma prescribed by type predicatea. The set of all ground terma t auch that !-p(t) succeeda is called type of p and denoted by !!:

Example 2.1. Let the defl.nition of a data type number be t)'pe.

number(O). number(s(X)) :- number(X). ead.

Then number ia a aet {0, ·(0), 1(1(0)), . .. }.

Suppose there are defined k data types Pl,P:t , . . . ,p,. and p1,p2 , ·· · ,p1 are disjoint. We denote the aet of all ground terms contained in no p; by other1 and consider it like one of types. Then the Herbrand universe His divided into k + 1 disjoint sets as follows.

Procedures are defl.ned following the syntax of DEC-10 Prolog [10},e.g.,

Throughout this paper, we use P as a finite set of definite clauses defl.ning data types and procedures. We asaume vari­ ables in each definite clause are renamed at each use so that there occurs no variable names con1lict.

2.2. A fundamental Theorem for Tfpe IDtereaee Ia Prolo&

Let I and J be Herbrand interpretations. I is aaid to cover success set under a restriction J when it contains the intersection of the minimum Herbrandmodel Mo and J .

An Herbrand interpretation J is aaid to be closed witb respect to P when for any ground instance of definite clause in P such that the head is in J, any ground atom in the body is also in J. This means M0 n J is computable within it.

Theorem If J is closed with respect to P, T(I) ~ T'(I) and T'(I) n J ~ I, then I covers success set under J .

Proof. T(I) n J ~ I from T(I) ~ T' (I). Let T J be a monotone transformation of Herbrand interpretations such that TJ(I) is T(I) n J for any I . TJ has a least fixpoint nTJ(I)~I I by the Knaster-Taraki fixpoint theorem ([1} p.843, Theorem 2.1). Becauae J is cloaed, Mon J is a fl.xpoint ofTJ. Moreover it is the least fl.xpoint, aince Mo n J = U:.o T~(0) ([1) p.843,Theorem 2.2). Therefor MonJ ~ I for any I satisfying TJ(I) ~ I.

Our goal of type inference ia to deacribe an Herbrand interpretation I covering aucceaa aet under a restriction J in terms of the typea. Thia is performed by defl.ning an appropriate transformation T' aatisfying the theorem above.

3. Type IDferenee 1n Prolo&

In thia section, we ahow how to describe a claas of Herbrand interpretationa in terma of the typea fl.rat. Then we defl.ne an appropriate tranaformation aatiafying the con­ dition in the theorem in 2.2. The baaic computation method and the incremental version are preaented in 3.4 and 3.5.

3.1. Interpretation by Type

(1) Type Set

A set of ground terms represented by a union of types is called type set. Type aeta are denoted by t !!_, ~ ·... etc.

Example 3.1.1. number U lidisatype set. 0 isatype set,too. P1 UP2 U ... UP1 U other· ia a type aet.We denote it by anv. (anv 18 not a type but an abbreviation of a type aet.) -

(2) Type Substitution

An assignment of type sets to variables

is called type substitution. Atype assigned to a variable X by E is denoted by E(X) . We assume E(X) = anv for any variable X not appearng explicitly in the domain of E. A type substitution E =< X1{:::t1,X2{:::t:~, ... ,X,.{:::t,. > is considered the same as a set of lübatituiions -

Example 3.1.2. < L{:::li&t > isatype aubstitution. This is considered the same as a set of substitution { < L{:::t >I t is any ground term in list }. The empty substitution < > is a type SUbstitution assigning GnV to any variable.

The union of two type substituions E1 and E2 is a type substitution E such that E(X) = E1(X) U E2(X) for any X and denoted by E1 U E:~ . The intersection of two type substituions E1 and E:~ is a type substitution E such that E(X) = E 1 (X) n E:~(X) for any X and denoted by E 1 n E:~.

(3) Interpretation by Type

Let Bo be a head of adefinite clause "Bo :- B1, B:~, .. . , Bm" in P and E be a type substitution. Then E(Bo) is conaidered a set of ground atoms {cr(Bo) I er E E}. An Herbrand inter­ pretation I represented by a union of all such forms,i.e.

is called interpretation by type.

Example 3.1.3. Let I be an Herbrandinterpretation

< > (append([ ], K, K)) U < L{:::0, M{:::0,N{:::0 > (append([XIL), M, [XIN))).

Then I is an interpretation by type. Thia ia an Herbrand interpretation { append([ ),t,t) I t is any ground term }.

3.2. Reatrtetlon by Type

An Herbrand interpretation J of the form U; E;(A;) is called restriction by type, where each A; is not necessarily a head of definite clauses in P.

Example 3.2. J =< > (append(N, [A), M)) U < > (re11er·e (L, M)) is a reatriction by type.

3.3. A Tranllformatlon for Type IDferenee

(1) Computation of Type Set of Superterm and Subterm

When each variable X in a term t ia instanciated to a ground term in E(X), we compute a type set containing all ground instances oft aa followa and denote it by t/E.

Example 3.3.1. Let t be [XILJ and E be < L {:::list > . Then t/E is list. Let t be [XILJ and E be < > . Then t/E is anv.

When a term t containing an occurrence of a variable X is instanciated to a ground term in t we compute a type set containing all ground instancea of the occurrence of X as follows and denote it by X/ < t{:::!_ >.

when t isavariable X; when t is of the form c(t1 , t2, ... , t,.),!. is p, c is a constructor of p, Xis in t; and t; is a type aet assigned to the i-th argument t;; otherwise.

Example 3.3.2. Let t be [XILJ and t. be list. Then X/< [XIL){:::list >= anv, L/ < [XIL){:::list >= list. Let t be [XILJ and !. be number. Then X/< [XIL){:::number >= 0, L/ < {XIL){:::number >= 0.

(2) Computation of Covering Type Substitution

Let B1, B:~, .. . , Bm be a sequence of atoms and I be an interpretation by type. A type substitution is called cover­ ing type substitution with respect to B1, [h, .. . , Bm and I when it contains every substitution u such that all ground instances u(Bt), u([h), ... , u(Bm) are in I . A transformation T' is defl.ned using the covering type substitutions.

Let I be an interpretation by type U; E;(A;) and B1, B2, . .. , Bm be a sequence of atoms. When B11 [h, .. . , Bm are unifl.able with A; 11 A; 1 , ... ,A;., by an mgu r, we defl.ne a type substitution E on variables in B1, B:~, .. . , Bm as fol­ lows. Note that we can assume without loss of generality that t contains no variable in B1, B2, ··. , Bm when a variable X in B11 B:~, .. . , Bm is instanciated to t by r, because the unifl.ability shows there is no cycle.

When m > 0 then

• (a) Let t be a term containing variable· in A; 1 and X be a variable in B; . If r substitutes t for X, then we aasigns t/E; 1 to X .
• (b) Let t be a term containing an occurrence of X in B; and Y be a variable in A; 1 · If r aubstitutes t for Y, then we assigns X/ < H=E; 1 (Y) > to the occurrence of X.

Then E assigns the intenection ni !f to X when !!_, !!· ... are computed as type sets at different occurrencea of X in B1 ,B~, ... ,Bm. (When E assigna 0 to some variable in B1, B~, .. . , Bm, we assume E assigns 0 to any variables.)

By r 818 "j"" 8 ml, we denote the union of E for every possible combination of Ä; 1 ,Ä; 1 , ·· · ,A;". and ita mgu r.

Example 3.3.3. Let I be a type interpretation

<> (append([],K,K))U

< L~0,M~0,N~0 > (append((XIL),M,(XIN)))

and B1 be a seqence of atoms (though it ia only one atom)

append(A, B, C).

Then There are two possibitity of unification. One is r1 = < A~[], B~K, C~K > and the corresponding type Substitu­ tion is < A~li&t >. Another is r~ =< A~[XIL],B~M. C~[XINJ > and < ..4.~0. B~0. C~0 > is the correspond­ ing type substitution. Hence by taking their union,we have r .. ,, ... 1A,s.c>l =< A~tilt >

(3) A Transformation T'

We define T' as folows .

It is obvious that T(I) t;;; T'(I) and T' is monotone for interpretations by type.

3.f. Computatlon of Type lnterence

An interpretation by type covering success set under a restriction J is called type inference under J. The theorem in 2.2 holds for interpretations by type as weil. We already have an appropriate transformation T' so that we can compute a type inference under a closed restriction J. The outlock or the basic algorithm for type inference is similar to the bottom-up computation of minimum Herbrand models.

Figure 1. Computation of Type Inference

In order to compute type inference under a closed restriction J, we need T'(I) n J ,which is obtained by using r 818 ·j··Bml (Bo)nr~HBo). r~l(.Bo) is common to all repetitions of the type inference process and can be computed once and for all before the repetitions.

3.5. lncremental Type lnterenee

An atom A is said to be closed witb respect to P when for any ground instance of the definite clause in P such that the head is a ground instance of A, any recunive call in the body is also a ground instance of A. (Hence any non-recursive definite clause and any definite clause with a head nonunifiable with A are negligible.) This means the set of ground atoma in Mo of the form of instance of A is computable by some instances of definite clauses. Note that p(X1 ,X~, . . . ,X,.) in generalform is alwaya closed.

Example 3.5.1. Anatom append(N, (X], M) is closesd. This means {append(t1, [t2], ta)!t1, t2 and ta are ground terms} n Mo is computable by

The closedness of an atom A can be checked as follows .

• (a) Check whether the head Bo is unifl.able with A by a substitution for A away from A (see section 2). If it is, decompose the mgu to u o r0 where u is the restriction to variables in Bo and r0 is the restriction to variables in A. If it is not,neglect the definite clause.
• (b) Check whether each instance of the recursive call in the body u(B;) is an instance of A and if it is,compute the instanciation r; . If it is not,A is not closed.

The set of all instances of definite clauses by u is called instanciated program for A.

Example 3.5.2. Let the atom A be append(A, (U), C) . Then the first head append([J, L, L) is unifl.able with append(A, (U), C)by< L~(Y) > o < A~[),U~Y,C~[Y) > . Thesecond head append([XIL], M, [X IN)) is unifiable with append(A, (U), C) by < M~[Y] > o < A{=[XIL), U~Y,C~[XINJ and the instance append(L, [Y), N) in the body is also an inatance ofappend(A,[U),C) by < A~L,U~Y,C~N >.

append([ ),[Y),[Y)) .

append((XIL),[Y),(XIN)) :- append(L,[Y),N) .

is the instancated program for append(A, (U], C) .

An atom satisfying the following condition is called closure of A with reapect to P and denoted by A.

• (a) Ais closed with respect to P,
• (b) Ais an instance of A and
• (c) Ais an instance of any X satisfying (a) and (b) .

Example 3.5.3. rever·e(A, B') is a closure of reverse(A, (VIB)) .

The closure is unique up to renaming and A is closed iff A = A modulo renaming. (See (7) for the proof of uniqueness and the algorithm to compute the closure.)

Now suppose we would like to compute type inference about p under a restriction by type < > p(t1, t 2 , .. . , t,.) and denote it by T(p(t1, t2, .. . , t,.)) . Let A1, A2 , ··· , ÄJ be non-recunive calls in the bodies of instanciated program for p(t1, t2, ... , t,.). (If some B; = q(11, 12, .. . , ·m) and B; = q(& 1 1, B~, .· · , ·~), we distinguish the predicate symbols by q1 and cn and assume both of them have the same definite clause program as q.) Then we compute T (p(t1, t2, . . . , t,.)) by initializing Io to T(At) bj T(A;) bl · · · l!J T(Aj), where each T(Ai) is computed recursively.

Figure 2. lncremental Type lnference

Ir there is no mutual recunion,thi1 proce11 1top1. The base case is the type inference for predicate1 which call no other predicate,e.g. append.

Example 3.5.4. Suppose we compute T(re11er.e(L, M)). The computation proceeds by initializing Io to T(append(N, [X], M)) as follows .

< L{::!lli., N {=Iid > (append([XIL], [Y], [X IN]))

10 = < > (append([], [Y], [Y]) U

/1 = IoU <> (re11me([],[])U

1'1. = Io U < > (re11me([ ], []) U < L{::!lli., M{::lilt > (re11em([XIL], M))

< X{::0,L{::0,M{::0 > (re11me([XIL],M)),

and !3 = I':J.. Hence the type inference of re11er~e is

< > (re11me([ ], []) U

< L{::!lli., M {::liat > (ret~er~e([XIL], M))

Recursive computation of T(AJ is 1ometime1 unnecea­ sary. For example,when A; is an atom q(Xl,X':l., .. . , Xm) in general form and T(q(X1,X'1., . . . ,Xm)) is already com­ puted before, then recomputing it all the way alows down the whole computation. A1 another example, when some A; = q(11 , 1'1., . . . , Im) and A; = q(·'1, 1'':1., ·.. , ·~), we dia­ tinguish their predicate symbols by q1 and q':J.. But if q(·1, · 2 , ... , ·,.) = q(·~, ·~· ... , ·~) modulo renaming, it turn· out to compute the aame result twice and the distinction is useless. In order to avoid the defliciency and acceralate the convergence, we store the results computed before for each closed atom, or more preciaely for each instanciated program, and utilize them immediately if po11ible.

4. VerUleatloa of Prolo1 Propoam1 UsiDJ T)'pe IDtormatloa

Type inference is used effectively in our verill.cation sys­ tem (5],(6],(7] . In veriflcation we aometime1 simplify the theorem to be proved by aasuming that some atom is true or false. In such a caae,some information about variables left in the simplifled theorem may be lost and we need to retain it to prove the right theorem. This problem was ll.rst noticed by Boyer and Moore (2] in their theorem prover(BMTP) for pure LISP. The same problem arises in verill.cation of Prolog programs.

Example 4. Suppose we prove a theorem

VU, V, C(3Bret~er~e(C, [VIB]):::>3B'reuem((UIC], (VIB'])).

Because of the deflnition of re11er~e, it i1 transformed to

V U,A,V,C (3B revene(C,[VIB]) :::>

3B' ,D (reverse(C,D) 1\append(D,[U],[VIB'])))

Now Iet us decide D tobe (VIB] . This decision is sound and we have a new subgoal

V U,V,C,B (reverse(C,[VIB]) :::>

3B' (reverse(C,[VIB]) 1\append([VIB],[U],[VIB']))).

Here we can utilize the antecedant. Ir re11er~e(C, (VIB]) i1 false,the theorem is trivially true. Hence we can only need to consider the case re11er~e(C, (VIB]) is true. By replacing re11er~e(C, [VIB]) with true,we have a new subgoal

V U,V,B 3B' append([VIB],[U],[VIB'])

which is further transformed to

V U,B 3B' append(B,(U],B')

because append((VIB], lUJ, (VIB']) ur append(B, (U], B'). But this transformation has generated a too strong theorem and it is in factnot true. (For example, an instance VU3B' append(O, [U], B') is wrong.) In order to keep the theorem right, we need to add type information a1 antecedant1,i.e. when we derive a subgoal assuming re11er~e(C, (VIB]) true, we have information lilt(B). Our new subgoal 1hould be V U,V,B (list(B):::>3B 1 append([VIB],[U],[VIB'])) This is provable by induction and we complete the proof.

5. Dl1eU11loa1

Several works are done for type inference in Prolog (3],[8],(9] from different point of views. In our approach, both syntactical and 1emantical concepts appear. It is semantical whether a type inference I covers a succe11 set, while it is 1yntactical and closely related to the well-typedne11 in [3],(9] whether a restriction J ia closed. Moreover they are related atrongly through the crucial condition that J muat be closed for I to be computed. Though our approach ia still monomor­ hic, it is new in the following reapects.

• (a) Our type inference describes a supenet of the success set by associating a type substitutions with each definite clause, which gives some accuracy to the types infered.
• (b) Our approach solves the problem under it ayntactical reatriction, which is utilized to inter types more minutely.
• (c) Our type inference ia not reatricted tothat for arguments. Type inference can be done for any variables in any procedure call which is not nece11arily in general form.

I. Conelu1lon1

We have ahown a type inference method for Prolog pro­ grama and ita application to verifl.cation. Thia type inference method ia an element of our verill.cation aystem for Prolog programs developed in 1984.

Aeknowleqement1

Our verill.cation aystem is a subproject of the Fifth Generation Computer Syatem(FGCS) project. The authors would like to thank Dr.K.Fuchi (Director of ICOT) for the chance of this research and Dr.K.Furukawa(Chief of ICOT 2nd Laboratory) and Dr.T.Yokoi(Chief of ICOT 3rd Laboratory) for their advices and encouragements.

Referenee1

1. Apt,K.R. and M.H.van Emden, ·contribution to the Theory ofLogic Programming",J.ACM, Vol.29,No.3,pp 841-862,1982.
2. Boyer,R.S. and J.S.Moore, ·A Computational Logic· ,Chap. 6., Academic Press,l979.
3. (3] Bruynooghe,M., ·Adding Redundancy to Obtain More Reliable and More Readable Prolog Programs·, Proc.lst International Logic Programming Conference,pp.129-133,1982.
4. (4] van Emden,M.H. and R.A.Kowalski, ·The Semantics of Predicate Logic as Programing Language· ,J.ACM,Vol.23,No.4, pp.733-742,1976.
5. (5] Kanamori,T., ·verill.cation. of Prolog Programs Using An Extension of Execution· ,ICOT TR-096,1984.
6. (6] Kanamori, T .and H.Fujita, ·rormulation of Induction Formu­

las in Verill.cation of Prolog Programs· ,ICOT TR-094,1984.

• (7] Kanamori,T.and K.Horiuchi, ·Type lnference in Prolog and Its Applications· ,ICOT TR-095,1984.
• Mishra,P.,-Towards a Theory of Types in Prolog" ,Proc. 1984 International Symposium on Logic Programming,pp.289298,1984.
• (9] Mycroft,R.and R.A.O'Keefe, ·A Polymorphie Type System for Prolog", Artill.cial Intelligence 23,pp.295-307,1984.
• (10] Pereira,L.M.,F .C.N .Pereira and D.H.D.Warren, ·user's Guide to DECsystem-10 Prolog", Occational Paper 15,Dept.of Artiflcial lntelligence, Edinburgh,1979.