Incorporating Generalization Heuristics into Verification of Prolog Programs

INCORPORATING GENERALIZATION HEURISTICS

INTO VERIFICATION OF PROLOG PROGRAMS

Hirohisa SEKI

Mitsubishi Eleetrie Corporation Central Research Laboratory Tsukaguehi-Honmaehi 8-1-1 Amagasaki,Hyogo,JAPAN 661

ineorporated into the verifleation of Prolog programs.

ABSTRACT

This paper is eoneerned with the problem of generaliza­ tion heuristics, whieh are ineorporated into our verifleation sys­ tem for Prolog programs. Two kinds of generalisation are dis­ eussed, that is, a meebanical generali1ation and an intelligent generalization. We show that the meehanieal generalisation used in Boyer-Moore's theorem prover (BMTP) ean be per­ formed by the simplifleation rule of our verifleation aystem, as weil as in the ease of eross-fertilization. To the intelligent generalization heuristie, whieh is not employed in BMTP, we give a generalization seheme whieh is naturally ineorporated into our inferenee system of the extended-exeeution style of the Prolog interpreter, and whieh proves to be eft'eetive also for flawed induetion aehemea.

I. INTRODUCTION

This paper is eoneerned with a verifleation ayatem for Prolog programs whieh is eurrently under development, aa one of the subprojeeta of the FGCS ·Intelligent Programming System" [1].

Logie programming ia often advoeated aa a deairable choiee for the verifleation problem beeause of ita elear aeman­ ties (e.g., [2]). In the design of our verifleation system, we have tried to take advantage of Prolog'· eharaeteristiea and present flrst order inferenee in an extended exeeution style of a Prolog interpreter [3]. Not only flrst order inferenee but induetion is indispensable aa a meana of proving interesting properties of Prolog programs such as termination and eorreetness. In the case of funetionallanguage, Boyer-Moore's theoremprover (BMTP) [4] is famous for ita automatie applieation of indue­ tion and many aophistieated heuriatiea eonstrueting induetive proofs. Into our verifleation system, various kinda of heuristiea have been integrated, moat of whieh are inspired by BMTP and are developed to auit the verifleation of Prolog programa (e.g.,[S]).

In this paper, speeial attention ia paid to ·Generalization Heuristies" which are applied when a theorem to be proved ia too weak and it is neeessary and easier to prove a theorem that is stronger than the original weak one. We deal with two kinda of generalization heuristies. The flrst generalization heuristie (we call it mecbanical generalitation in thia paper) eorresponda to the one used in BMTP, and the aeeond (ealled intelligent generalization ) is one that ia not employed in BMTP but ia left to the user. Some work has been done with respeet to funetional language to meehanize the intelligent generalisation heuristie (e.g.,[6],[7]). Our main purpoae lies in an attempt to elarify how these two kinds of generalization heuristies ean be After summarizing some preliminary materials in seetion ß, we present our verifleation methods for Prolog programs in aeetion m. In seetion IV, we explain two kinds of generalization heuriaties ; flrst, we illustrate that the meehanieal generaliza­ tion ia naturally ineorporated by the simplifleation rule of our verifleation system ; seeondly, we show some examples whieh eannot be proved by simply applying flrst order inference and induction, and therefore motivate us to incorporate the intelligent generalization heuristic. In section V, we discuss in detail how the intelligent generalization is performed in the framework of our veriflcation system of Prolog programs. Lastly in aection VI, we discuss the relation to other work and aome implementation issuea.

ß. FORMULATION OF VERIFICATION

In this aection, we give our formulation of the veriflcation of Prolog programa. In the following, we follow the syntax of DEC-10 Prolog [8] and assume some familiarity to the ter­ minology of Prolog and flrst order logic(see e.g.,[9], [10]).

In our veriflcation system, we treat only pure Prolog, i.e., we impoae the following 3 conditions on Prolog programs :

• (i) no negative clausea and no ·not" in programs.

(ii) no executable primitives.

(iii) no ·cut" symbol (!).

On the other band, our speciflcation language is a sub­ claal of first order logic formulas. That ia, a specification is expressed by a closed formula which can be transformed into the following prenex form (we eall it an S-formula) :

'VXt · ··'VXm3Yt · ··3Y,. F (m, n~O),

where F eontains no quantiflers.

Let S be a apeeifleation and P be a Prolog program and p· be the eompletion of P in the sense of Clark [11]. Then we adopt a formulation that verilication of S with respect to P provea that p·1-s. This means that S is a logieal eonsequence of p· by flrst order inferenee and induction, which are explained in the next section.

We use the following definitions and notations. First, we use the notion of polarity (see [9], [10]). The positive and negative subformulaa are deflned as follows :

• (i) F is a positive subformula of F .
• (ii) When .,Gis a positive (negative) subformula of F, then G ia a negative (positive) subformula of F .

• (iii) When GIIH or GVH is a positive (negative) subformula of F, then G and H are positive (negative) subformulas of F.
• (iv) When G-::>H isapositive (negative) subformula of F, then Gis a negative (positive) subformula of FandHis a positive (negative) subformula of F.

Next, variables which appear in a specification are distin­ guished in the following way. Let F be a closed first order formula. When 'VXG is a positive subformula or 3XG is a negative subformula of F, then X is called a free variable of F. On the other hand, when 'rfY H is a negative subformula or 3Y H is a positive subformula of F, then Y is called an un­ decided variable of F. In other words, when F is transformed into prenex normal form, free variables arevariables quantified universally, and undecided variables are those quantified exist­ entially.

A goal formula is a formula which is obtained from an S-formula by replacing each undecided variable Y with ?Y and deleting all quantifications. Furthermore, a Substitution t1 for a goal formula G is called a deciding substitution when t1 instantiates no free variable in G.

Example : An S-formula :

'VX(li6t(X)-::>'rfY3Z append(X, Y, Z))

is represented by a goal formula :

list(X)-::>append(X, Y, !Z),

where list(X) is negative and append(X, Y, ? Z) is positive.

A replacement of an occurrence of a term t in a formula F by s is denoted by F1[s), and a replacement of all occurrences of a term t in a formula F by s is denoted by Ft(s). Formula F is said to be in a reduced form [10) with respect to logical constants true and false, if Fis either (i) true or (ii) falu, or (iii) if neither true nor false occur in F. The reduced form of a formula F is denoted by F l.

III. INFERENCE RULES

In this section, we give a briet description of our verification procedure for a specification (for a detailed ex­ planation, see [3)).

A. Extended Execution

Since a specification is not restricted in a Horn clause but is expressed in an S-formula, we need some extension of the usual Prolog interpreter. For this purpose, our verification system uses the following four inference rules.

(1) Ca·e Spllttlns

Let G be a goal formula and H either (i) an outermost positive subformula of the form H1ll · ··1\H,. or (ii) an out­ ermost negative subformula of the form H1 V· ··V H,.(l: > 1). Then, if each undecided variable appearing in Hi ap­ pears only in Hi(1~i~l:), we generate new 1: AND-goals GH[Hl),···,G!l[H,.J.

The following two rules are an extension of a Prolog in­ terpreter using polarity.

(2) DeiDlte Clau1e IDterenee (DCI)

Let A be a positive atom in a goal formula G and Iet ·s :- B11 ···, Bm · be any definite clause in P. When Ais unifiable with B by a deciding m.g.u.(most general unifier) t1, we generate new OR-goals for allsuch definite clauses : t1(GA[B1II · ··!IBm)) l (t1(GA[true)) l when m=o ) . All newly introduced variables are treated as fresh undecided variable·.

(3) Nesatlon ·· Fallure IDterenee(Nfl)

Let A be a negative atom in a goal formula G and Iet · B :- B1, ···, Bm · be any definite clause in P. When A is not unifiable with a head of any definite clause in P, we generate a goal: GA[/alle)l. When Ais unifiable with B of adefinite clause by an m.g.u. tl, we generate new AND­ goala for all such definite clauses : t1(GA[B1!1 · ··!IBm)) l (t1(GA[true)) l when m=o ). All newly introduced vari­ ables are treated as fresh free variables.

(·) Slmpllleatlon

Let G be a goal formula. When A1, ···,Am are positive atoms and Am+ 11 ···, A,. are negative atoms unifiable to A by a deciding m.g.u. tl, we generate new AND-goals : t~(�)A(true) l and ti{G)A(/alse) l .

These four inference rules are repeatedly applied to a given goal formula until it is reduced to true or false . Ir these rules cannot be applied any more, then we appeal to the following induction.

B. lnduction

Our verification system utilizes inductive proofs which are based on structural induction schemes. Those induction schemes are also used in [12),[13),[14) for the verification of Prolog programs. For example, the following is an induction acheme for Iist X :

where Q(X) ia a theorem to be proved, QQ )) is a base case, and 'VA, X (Q(X) -::> Q([AIXJ)) ia an induction step.

IV. GENERALIZATION HEURISTICS

In the following, we discuss two kinds of generalization heuristics incorporated into our verification system.

A. Mechanical Generalization

The generalization empioyed in BMTP is a heuristic by which a term in a formula ia replaced by a variable under an appropriate condition [4). For example, when the generaliza­ tion heuristic is applied to a formula in functional language :

then the following formula ia obtained :

re11erse(N)=L-::> re11er se(append(N, [X)))=[XILJ, where term rever~e(L) in the firat formula ia replaced by a new variable N and thus a more general formula ia obtained. On the other hand, Iet G be a goal formula :

When we apply the simplification rule to the above un­ derlined positive · and negative rever~e(L, M) in G, then we generate the following AND-goala :

which are immediately reduced to :

and true, respectively. This inference exactly corresponds to the above-mentioned generalization heuristic employed in BMTP.

Likewise, the inference of cross-fertilization in BMTP also correspoiids to the one performed bysimplification [3]. In this way, generalization and cross-fertilization, which are treated as dilferent heuristics in BMTP, are performed in a unified way by the simplification rule in our verification aystem.

Furthermore, the heuristic of eliminating destructors in BMTP can be considered as a kind of generalization heuristic. For example, selecton for data structure like c:or(L) and c:dr(L) appearing in the goals of BMTP are eliminated and replaced by variables. In Prolog programs, we usually don't use such selectors explicitly ; we do without them by using unification. Hence, Prolog programming style sometimes makes unnecea­ sary such a generalization heuristic as eliminating destructora.

B. Intelligent Generalization .

The second generalization heuristic dilfera from the above one, and BMTP intentionally does not employ it because it requires ·creative· insight (chap.Xll in [4]). In the nrification or Prolog programs, however, there arealso some cases where, in proving an induction step goal, we cannot use ita induction hypothesis because of mismatcbing with ita conclusion. Aa an example or such a case, conaider the proof of the following theorem.

theorem( rever ae-rever 1e ).

"VXY reverse(X,[ ], Y)::>rever~e(Y,[ ],X) · ·· (G0) end.

where program reveru ia defined aa followa :

First, we try to prove the above theorem by induction and the induction scheme in aection 01-B ia generated for lilt: X, where Q(X) is Wrever~e(X,[ ],Y):::>rever~e(Y,[ ],X).

The proof of its baae case, Q([ ]), is trivial. The proof of the induction atep goal, however, ia not easily performed becauae or thoae underlined mismatched literals ahown below :

[induction atep] (Q(X) :::> Q([AIXJ))

(rever~e(X, [ ], !Y0 ) :::> rever u(!Y0 , [ ], X)) :::>(revem([AIXJ,[ ], Y):::>revme(Y,[ ], [AIXJ)) ! NFI for revem([AIX], [ ], Y) (rever~e(X,[ ], !Yo):::>reverse(!Yo,[ ],X)) :::> (revem(X, [A), Y)::> revem(Y, [ ], [AIXJ))

Here, since we cannot apply simplification because of mis­ matching between ·[ ]· and ·[A]· in the above underlined parta, there is no way to use the induction hypothesis. These ·phenomena· often happen to the verification of Prolog pro­ grams containing a ·accumulator· [6] like the second argu­ ment of rever~e, which, though they make the computation linear order, cause at the aame time mismatching between an induction hypothesis and its conclusion. Hence, in order to aolve theae kinds of mismatching, it is neceaaary to incorporate some heuristics in order to generate a generalized goal. Our verification aystem generates the following goal mechanically :

end.

We call auch kind of generalization an ·intelligent generalisation. · It ia easily known that the above theorem is actually a generalized goal of G0 and its proof can be rather straightrorwardly performed.

V. INTELLIGENT GENERALIZATION HEURISTIC

In this aection, we atate how the intelligent generalization heuristic ia applied to the proof of an induction step goal and give the intelligent generalization scheme which mechanically generates its generalized goal. We then go on to show that its scheme is also elfective for fiawed induction achemea [4].

A. Intelligent Generalization Scheme

At first, for ease of underatanding, we illustrate the intel­ ligent generalization heuristic by uaing the previous example.

The first step of intelligent generalization is to find those mismatcbing arguments which make it impossible to use the induction hypothesis. In the above example, those mismatch­ ing arguments are ·[ ]· and ·[A]· in rever~e(X, [ ], !Yo) and rever~e(X, [A], Y), respectively.

Next, we replace the mismatching arguments in the in­ duction conclusion by new variables. In the above, ·[A]· is replaced by a new variable, say, T. We call those variables contained in the mismatching arguments ·mismatcbing vari­ able·,· and those arguments in the induction conclusion which contain mismatching variables are called ·arguments relating to miamatcbing.· In thia case, · A· is a miamatching variable and ·[AIX]· ia an argument relating to mismatching. These argument1 relating to mismatching are also replaced by new distinet variables. In this ease, we replace ·[AIXJ· by a new variable, say, U,and the induction conclusion becomes the fol­ lowing rormula :

Clearly, the above goal G1 is not a correct speciflcation but an "over-generalized" goal of the original theorem G0, and an appropriate constraint condition should be imposed on G1 in order to obtain a correct generalized goal. Hence, we u­ sume some ·constraint relation" between freshly introduced variables and those variables which appear in arguments relat­ ing to mismatching. In this case, a constraint relation, aay, R(T,X, U), is imposed, because T and U are newly introduced variables and X is a variable which appeara in the argument relating to mismatching, i.e., [AIX]. We aasume the following goal as a generalized goal of the original one :

where R(T,X, U) is some relation whose precise form ia not determined yet ; and we call such a goal that containa an unspecified relation a ·temporar.r goal. ·

The third step is to infer the constraint relation mentioned above. Our current system infers such a relation from the following two conditions. The flrst interring condition ia called a ·generaliJation condition," which is a necessary condition for a temporary goal to be actually a generalized goal of the original one. In this case, by comparing G0 and G2, it followa that X equals U when T is [ ], which imposes the following constraint on Jl(T, X, U) :

The second interring condition is that derived from "pseudo verilication," which meana that we apply the inference rule mentioned in section W to the temporary goal. For ex­ ample, if we apply induction on G2, we get the following verification process for the induction atep : VAX P(X) :::> P((AIX]), where P(X) ia :

WTU rever~e(X, T, Y)I\Jl(T,X, U):::>rever~e(Y,( ], U).

(reverse(X, !To, !Yo)I\R(!To,X, !Uo):::>rever~e(!Yo,[ ], !Uo)) :::>(reverse([AIX], T, Y)I\R(T, (AIX], U):::>revem(Y ,[ ], U)) ~ NFI for reveru([AIX], T, Y)

(reverse(X, !To, !Yo)I\R(!To,X, !Uo):::>rever·e(!Yo,[ ], !Uo)) :::>(revem(X, [AlT], Y)I\Jl(T, (AIX], U):::>revem{Y,[ ], U)) ~ simpliflcation w.r.t ~ rever~e(X, !T0 , !Y0) and rever~e(X, [AlT], Y) (R([AIT],X, !Uo):::>revem(Y,[ ], !Uo)) ::>(R(T, (AIX], U):::>revme(Y,[ ], U)) ~ aimplification w.r.t ~ rever~e(Y, [ ], !U0) and rever u(Y, [ ], U) R(T, [AIX], U):::>.ll([AIT],X, U). · ·· (CR2)

Similarly, aa for the baae caae of the induction acheme for P(X), we obtain the following constraint relation :

Then, from theae constraint relationa, (CR1), {C~) and (CR3 ), we try to identify the unkDown relation Jl(T,X, U). Our veriflcation system aearches for an already deflned Prolog program which satisfles thoae constraint relations. Actually, we rewrite those constraint relations into formulas in Horn clausea;

and then find a definite clause which can be ·unifled" with those (CRi)'s whose heads are the unknown constraint rela­ tion. Ir there are no auch clausea deflned in the system, we conaider all the permutations of the arguments of the con­ atraint relation. That is, for example in this case, we con­ aider all the permutations of {T, X, U} and check each case for Jl(T, U,X), Jl(U, T,X), Jl(U,X, T), etc. In the above ex­ ample, from (CRi) and (CRi), we can find that

and it is easily conflrmed to satisfy (CR1 ). From G2 and Ga, we finally obtain the generalized goal G 1 ,,. mentioned in aection IV-B.

To aum up, the intelligent generalization scheme consists or the following 4 stepa :

1. Find out mismatching arguments in literals to which the induction haa been applied.
2. Replace those arguments relating to the mismatching by new variables in the induction conclusion (and obtain an ·over-generalized goal").
3. On the over-generalized goal, impose an appropriate constraint relation by generalization condition and by the paeudo veriflcation.
4. From the reatrictiona derived in (3), infer the constraint relation.

Aa for the inference method in step {4) above, our cur­ rent implementation deals only with those constraint relations which can be reduced into Horn clauses as mentioned in the examples.

B. Application to Flawed lnduction Schemes

The application of the intelligent generalization scheme is not restricted to the above-mentioned proofs, but it is some­ times eft'ective also for a "flawed" induction scheme [4] . For example, consider the following example which is a corollary of the associativity of append.

theorem( corollarJI-O f -append-aa ·ociativit!l) VX DR append(X, X, D)l\append(X, D, R) :::>append(D, X, R) end.

From the deflnition of append, we note that the predi­ cate append(X, Y, Z) recursively changes its flrst and third argument and leavea its aecond argument flxed. Ir we use the terminology of BMTP, the flrst and third arguments are changing variables and the second argument is an unebang­ ing variable. The above example shows a case where an in­ duction acheme auggested by an atom and another induction acheme auggested by a dift'erent atom, are mutually flawed. That ia, the induction scheme suggested by append(X, D, R) recursively changes X, which is an unebanging variable in append(D, X, R), while the induction acheme auggeated by append(D,X,R) recursively changes D, which ia an unebang­ ing variable in append(X, D, R) ( and note that the induction scheme suggested by append(X, X, D) ia flawed by itself).

In this case, our intelligent generaliution acheme generates the following generalized goal :

where append(V, V, U) is a constraint relation obtained ; we know that the above goal is easily proved by an ·unflawed· induction.

VI. CONCLUDING REMARKS 111: RELATED WORK

This paper has shown how generalization heuristics are incorporated into the veriflcation system of Prolog programs. ·Two kinds of generalization, mechanical generalization and in­ telligent generalization, are discussed. We have shown that the mechanical generalization used in BMTP can be performed by simpliflcation in our verifl.cation system, as weil as in the case of cross-fertilization. To the intelligent generalization heuristic we have given a generalization scheme which is naturally in­ corporated into our inference system of the extended-execution style, and which has proved to be etrective also for fl.awed in­ duction schemes.

We owe our heuristics to BMTP and other related work by Moore [6] and Au bin [7], although there is a ditrerence in target languages and deduction methods. As for the interring con­ straint relation mentioned in section V, we find some relevance to Shapiro's [15] Model Inference System which is a general theory to infer a Prolog predicate satisfying given facts. Our intelligent generalization scheme ditren in that it gives a Prolog predicate some constraint relations to be satisfied.

The generalization heuristiCs presented here have been ex­ amined by numerous hand proofs and their first versiona haTe been implemented in DEC-10 Prologon DEC-2060 aa one of the heuristics of our verification system for Prolog programa. We intend to implement our verification system on PSI [16) aa a basis for ·Intelligent Programming Environment· for Prolog programming on which we can perform various kinds of ex­ periments such as program transformation and aynthesis.

Acknowledgments

The author appreciates K. Fuchi(Director of ICOT) , K. Furukawa (Chief of ICOT 2nd Laboratory) and T. Yokoi(Chief of ICOT 3rd Laboratory) for the chance of doing this research. He is greatly indebted toT. Kanamori for valuable comments, especially on the extended execution. He would also like to thank A. Fusaoka, H. Fujita and K. Suzuki for their useful discussions and help.

Heferences

1. Furukawa, K and T. Yokoi, "Basic Software System· In Proc FGCS-84. Tokyo, Japan, November, 1984, pp. 3757.
2. Bowen, K. A. "Programming with Full First-Order Logic·
3. In Machine Intelligente 10 (1982) 421-440.
4. Kanamori, T. -verifl.cation of Prologprograms Using an Extension of Execution, · ICOT Technical Report, TR-096, 1984.
5. Boyer, R. S. and J. S. Moore. Computational Logic, New York: Academic Press, 1979.
6. Kanamori, T. et al. "Formulation of Induction Formulas in Verification of Prolog Programs,· ICOT Technical Report, TR-094,1984.
7. [6) Moore, J . S., "Introducing iteration into the pure LISP theorem prover.· IEEE Trans. Software Eng. 1:3 (1975) 328-338.
8. Aubin, R. ·some Generalization Heuristics in Proofs by Induction· In Proc. IRIA Colloq. on Proving and Improving Programs. Are et Senans, France, July, 1975, pp. 197-208.
9. Pereira, L. M., F . C. Pereira and D. H. Warren "User's Guide to DECsystem-10 PROLOG,· Techical Report, Univ. of Edinburgh, September 1978.
10. Prawih, D. Natural Deduction, A Proof-Theoretical-Study Stockholm: Almqvist 111: Wiksell, 1965.
11. [10) Murray, N. V., ·completely Non-Clausal Theorem Proving·, Artificial Intelligence, 18:1 (1982) 67-85.
12. Clark, K. L. "Negation as Failure· In Logic and Database, Gallaire. H and J . Minker. Eds., (1978) 293-322.
13. Clark, K. L. and S-A. Tärnlund "A First Order Theory of Data and Programs· In~. Toronto, Canada, August, 1977, pp. 939-944.
14. Clark, K. L. ·Predicate Logic as a Computational Formalism: Technical Report 59, Imperial College, December 1979.
15. Stering, L. and A. Bundy "Meta-Level Inference and Program Verification· In 6th Conf on Automated Deductjon Lecture Notes in Computer Science 138 1982 pp. 144-150. ' '
16. Shapiro, E. Y. "An Algorithm that Infers Theories from Facts· In Proc IJCAI-81. Vancouver, Canada, August, 1981, pp. 446-451.
17. Yokoi, T., S. Uchida, et al. "Sequentialinference Machine : SIM· In Proc FGCS-84 Tokyo, Japan, November, 1984, pp. 70-81.