Multiset Relations: A Tool for Proving Termination

Multiset Relations: a To ol for Proving Termination ? J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo and F.-J. Martn f jruiz,jalonso,mjoseh,fjesus g ia.es Departamento de Cienias de la Computaion e Inteligenia Artiial. Faultad de Informatia y Estadstia, Universidad de Sevilla Avda. Reina Meredes, s/n. 41012 Sevilla, Spain Abstrat. We present in this pap er a formalization of multiset relations in ACL2, and we show how multisets an b e used to prove non-trivial termination prop erties in ACL2. Intuitively, multisets are sets that admit multiple o urrenes of elements. Every relation on a set A indues a relation on nite multisets over A and it an be shown that the multiset relation indued by a well-founded relation is also well-founded. We proved this prop erty in the ACL2 logi, and used it by funtional instantiation in order to provide well-founded relations to the admissibility test of reursive funtions. We also develop ed a maro defmul , to dene well-founded multiset relations in an easy way. Finally, we present three ase studies where multisets are used to prove non-trivial termination prop erties: a tail-reursive version of Akermann's funtion, a denition of MCarthy's 91 funtion and a pro of of Newman's lemma for abstrat redution relations. Intro dution We present in this pap er a formalization of multiset relations in ACL2, and we show how these relations an b e used to prove non-trivial termination prop erties, providing a to ol for dening relations on nite multisets and showing that these relations are well-founded. Suh well-founded relations are used in the admissibility test for reursive funtions, allowing the user to provide a partiular multiset measure in order to prove termination of reursively dened funtions. Multisets are usually dened in an informal way as \sets with rep eated elements". Dershowitz and Manna [4℄ proved that every well-founded relation on a set A indues a well-founded relation on the set of nite multisets of elements taken from A . We have formalized this theorem using ACL2, and stated it in an abstrat way. This allows to instantiate the theorem to show well-foundedness of onrete multiset relations. We have also develop ed a maro defmul in order to easily make denitions of indued multiset relations. Besides dening the multiset relation indued by a given relation, this maro proves, by funtional instantiation, well-foundedness of the de- ned multiset relation, provided that the original relation is well-founded. The rst setion of this pap er presents how we have formalized and proved wellfoundedness of multiset relations indued by well-founded relations. The seond se- tion presents the maro defmul and it is shown how it an b e used to dene multiset well-founded relations. In the three setions after that, three ase studies of inreasing omplexity are presented, showing how multisets an b e used to prove non-trivial termination prop erties. The rst one is a tail-reursive denition of Akermann's funtion. The seond one shows admissibility of an iterative version of MCarthy's 91 funtion. The third one is a pro of of Newman's lemma ab out abstrat redution relations: terminating and lo ally onuent redution relations are onuent. ? This work has been supp orted by DGES/MEC: Pro jets PB96-0098-C04-04 and PB96-1345 We will assume the reader has a working knowledge of ACL2. The b est intro du- tion to ACL2 is [5℄. Due to the lak of spae, we will skip details of the mehanial pro ofs and we will not mention guards or guards veriation. The omplete b o oks are available on the web in http://www-s.us.es/~jruiz/al2-mul/ . 1 Formalization of multiset relations in ACL2 1.1 Multisets: denitions and prop erties A multiset M over a set A is a funtion from A to the set of natural numb ers. This is a formal way to dene \sets with rep eated elements". Intuitively, M ( x ) is the numb er of opies of x 2 A in M . This multiset is nite if there are nitely many x suh that M ( x ) > 0. The set of all nite multisets over A is denoted as M ( A ). We will use standard set notation to represent multisets. For example, if A = f a; b;  g , an example of multiset over A is M = f a; b; b; b g , an abbreviation of the funtion M ( a ) = 1, M ( b ) = 3 and M (  ) = 0. Thus, f a; b; b; b g is idential to the multiset f b; b; a; b g , but distint from the multiset f a; b; b g . Basi op erations on multisets are dened to generalize the same op erations on sets, taking into aount multiple o urrenes of elements: x 2 M means M ( x ) > 0, M  N means M ( x )  N ( x ), for all x 2 A , M [ N is the funtion M + N and M n N is the funtion M :  N (where x :  y is x  y if x  y and 0 otherwise). For example, f a; b; b; a g [ f ; ; a; b g is the multiset f a; a; a; b; b; b; ;  g and f a; b; b; a g n f ; ; a; b g is the multiset f a; b g . Any ordering dened on a set A indues an ordering on multisets over A : given a multiset, a smaller multiset an b e obtained by removing a non-empty subset X and adding elements whih are smaller than some element in X . This onstrution an b e generalized to binary relations in general, not only for partial orderings. This is the formal denition: DEFINITION 1. Given a relation < on a set A , the multiset relation indued by < on M ( A ), denoted as < mul , is dened as N < mul M i there exist X ; Y 2 M ( A ) suh that ; 6 = X  M ; N = ( M n X ) [ Y and 8 y 2 Y 9 x 2 X ; y < x . For example, if A = f a; b; ; d; e g and b < a , d <  , then f a; b; b; b; b; d; d; d; d; d; e g < mul f a; a; b; ; d; e g by replaing X = f a;  g by Y = f b; b; b; d; d; d; d g . It an b e easily shown that if < is a strit ordering, then so is < mul . In suh ase we talk ab out multiset orderings . A relation < on a set A is terminating if there is no innite dereasing 1 sequene x 0 > x 1 > x 2 ::: . An imp ortant prop erty of multiset relations on nite multisets is that they are terminating when the original relation is terminating, as stated by the following theorem: THEOREM 1. Let < b e a terminating relation on a set A , and < mul the multiset relation indued by < on M ( A ). Then < mul is terminating. The ab ove theorem provides a to ol for showing termination of reursive funtion denitions, by using multisets: show that some multiset measure dereases in eah reursive all omparing multisets with resp et to the relation indued by a given terminating relation. In the following subsetion, we explain how we formalized theorem 1 in the ACL2 logi. 1 Although not expliitly, we will supp ose that the relations given here represent some kind of \smaller than" relation. 1.2 Formalization of well-founded multiset relations in ACL2 Let us deal with formalization of terminating relations in ACL2. A restrited notion of terminating relations is built into ACL2 based on the following meta-theorem (axiom of hoie needed): a relation < on a set A is terminating i there exists a funtion F : A ! O r d suh that x < y ) F ( x ) < F ( y ), where O r d is the lass of all ordinals. In this ase, we also say that the relation is wel l-founded . Note that we are denoting the relation on A and the ordering b etween ordinals using the same symb ol < . An arbitrary well-founded relation rel dened on a set of ob jets satisfying a prop erty mp an b e dened in ACL2 as shown b elow (dots are used to omit tehnial details, as in the rest of the pap er): (enapsulate ((mp (x) booleanp) (rel (x y) booleanp) (fn (x) e0-ordinalp)) ... (defthm rel-well-founded-relation-on-mp (and (implies (mp x) (e0-ordinalp (fn x))) (implies (and (mp x) (mp y) (rel x y)) (e0-ord-< (fn x) (fn y)))) :rule-lasses :well-founded-relation)) The prediate mp reognizes the kind of ob jets (alled measures ) that are ordered in a well-founded way by rel . The embedding funtion fn is an order-preserving funtion mapping every measure to an ordinal. One a relation is proved to satisfy these prop erties and the theorem is stored as a well-founded relation rule, it an b e used in the admissibility test for reursive funtions. We all the theorem rel-well- -founded-relation-on-mp ab ove the wel l-foundedness theorem for rel , mp and fn . In ACL2, every partiular well-founded relation has to b e given by means of three funtions (a binary relation, a measure prediate and an emb edding funtion) and the orresp onding well-foundedness theorem for suh funtions. As a partiular ase, when mp is t we an omit any referene to mp in the statement of the orresp onding well-foundedness theorem. See well-founded-relation in the ACL2 manual [6℄. The ab ove notion of termination is restrited: sine only ordinals up to " 0 are formalized in the ACL2 logi, a limitation is imp osed on the maximal order typ e of well-founded relations that an b e formalized. Consequently, our formalization suers from the same restrition (nevertheless, our pro ofs do not dep end on partiular prop erties of " 0 , exept well-foundedness). Let us now deal with formalization of multisets relations. We represent multisets in ACL2 as true lists. Given a prediate (mp x) desribing a set A , nite multisets over A are desrib ed by the following funtion: (defun mp-true-listp (l) (if (atom l) (equal l nil) (and (mp (ar l)) (mp-true-listp (dr l))))) Note that this funtion dep ends on the partiular denition of the prediate mp . With this representation, dierent true lists an represent the same multiset: two true lists represent the same multiset i one is a p ermutation of the other. Thus, the order in whih the elements app ear in a list is not relevant, but the numb er of o urrenes of an element is imp ortant. This must b e taken into aount, for example, when dening multiset dierene in ACL2 (the funtion remove-one , omitted here, deletes one o urrene of an element from a list, whenever p ossible): (defun multiset-diff (m n) (if (atom n) m (multiset-diff (remove-one (ar n) m) (dr n)))) The denition of < mul given in the preeding subsetion is quite intuitive but, due to its many quantiers, diÆult to implement. Instead, we will use a somewhat restrited denition, based on the following theorem: THEOREM 2. Let < b e a strit ordering on a set A , and M ; N two nite multisets over A . Then N < mul M i M n N 6 = ; and 8 n 2 N n M ; 9 m 2 M n N ; suh that n < m . From the omputational p oint of view, the main advantage of this alternative denition is that the we do not have to searh the multisets X and Y of the original denition b eause we an take M n N and N n M , resp etively. It should b e remarked that this equivalene is true only when < is a strit partial ordering. Take for example, the relation S dened on A = f a; b; ; d g , suh that dS  , S b and bS a . In this ase we have f b; ; d g S mul f a; b;  g , taking X = f a; b;  g and Y = f b; ; d g . Nevertheless, d 2 f b; ; d g n f a; b;  g , f a g = f a; b;  g n f b; ; d g and it is not true that dS a . Anyway, this is not a severe restrition. Moreover, well-foundedness of < mul also holds when this restrited denition is used, even if the relation < is not transitive, as we will see. Thus, given a dened (or onstrained) binary relation rel , we dene the indued relation on multisets based on this alternative denition: (defun exists-rel-bigger (x l) (ond ((atom l) nil) ((rel x (ar l)) t) (t (exists-rel-bigger x (dr l))))) (defun forall-exists-rel-bigger (l m) (if (atom l) t (and (exists-rel-bigger (ar l) m) (forall-exists-rel-bigger (dr l) m)))) (defun mul-rel (n m) (let ((m-n (multiset-diff m n)) (n-m (multiset-diff n m))) (and (onsp m-n) (forall-exists-rel-bigger n-m m-n)))) Finally, let us see how we an formalize in the ACL2 logi the theorem 1 ab ove, whih states well-foundedness of the relation mul-rel . As said b efore, in order to establish well-foundedness of a relation in ACL2, in addition to the relation ( mul-rel in this ase), we have to give the measure prediate and the emb edding funtion, and then prove the orresp onding well-foundedness theorem. Sine mul-rel is intended to b e dened on multisets of elements satisfying mp , then mp-true-listp is the measure prediate in this ase. Let us supp ose we have dened a suitable emb edding funtion alled map-fn-e0-ord . Then theorem 1 is formalized as follows: (defthm multiset-extension-of-rel-well-founded (and (implies (mp-true-listp x) (e0-ordinalp (map-fn-e0-ord x))) (implies (and (mp-true-listp x) (mp-true-listp y) (mul-rel x y)) (e0-ord-< (map-fn-e0-ord x) (map-fn-e0-ord y)))) :rule-lasses :well-founded-relation) In the next subsetion we show a suitable denition of map-fn-e0-ord and desrib e some asp ets of the ACL2 pro of of this theorem. 1.3 A pro of of well-foundedness of the multiset relation In the literature [1℄, theorem 1 is usually proved using Konig's lemma: every innite and nitely branhed tree has an innite path. Nevertheless, we have to nd a dierent pro of in ACL2, dening an order-preserving emb edding funtion map-fn-e0-ord from mp-true-listp ob jets to e0-ordinalp ob jets. Thus, our pro of is based on the following result from ordinal theory: given an ordinal  , the set M (  ) of nite multisets of elements of  (ordinals less than  ), ordered by the multiset relation indued by the order b etween ordinals, is order-isomorphi to the ordinal !  and the isomorphism is given by the funtion H where H ( f  1 ;::: ; n g ) = !  1 + ::: + !  n . This result an b e proved using Cantor's normal form of ordinals and its prop erties. As a by-pro dut, an interesting prop erty ab out multiset well-founded relations an b e dedued. Sine   " 0 implies !   ! " 0 = " 0 , this means that one an always prove, in the ACL2 logi, well-foundedness of the multiset relation indued by a given well-founded ACL2 relation (i.e., using emb eddings in the ordinal " 0 ). This is not the ase, for example, of lexiographi pro duts, sine the maximal ordinal typ e of a lexiographi pro dut of two ACL2 well-founded relations may b e greater than " 0 . The isomorphism H ab ove suggests the following denition of the emb edding funtion map-fn-e0-ord : given a multiset of elements satisfying mp , apply fn to every element to obtain a multiset of ordinals. Then apply H to obtain an ordinal less than " 0 . If ordinals are represented in ACL2 notation, then the funtion H an b e easily dened, provided that the funtion fn returns always a non-zero ordinal: the funtion H simply has to sort the ordinals in the multiset and add 0 as the nal dr . These onsiderations lead us to the following denition of the emb edding funtion map-fn-e0-ord . Note that the non-zero restrition on fn is easily overome, dening (the maro) fn1 equal to fn exept for integers, where 1 is added. In this way fn1 returns non-zero ordinals for every measure ob jet and it is order-preserving if and only if fn is. (defun insert-e0-ord-< (x l) (ond ((atom l) (ons x l)) ((not (e0-ord-< x (ar l))) (ons x l)) (t (ons (ar l) (insert-e0-ord-< x (dr l)))))) (defun add1-if-integer (x) (if (integerp x) (1+ x) x)) (defmaro fn1 (x) `(add1-if-integer (fn ,x))) (defun map-fn-e0-ord (l) (if (onsp l) (insert-e0-ord-< (fn1 (ar l)) (map-fn-e0-ord (dr l))) 0)) One map-fn-e0-ord has b een dened, let us now deal with the ACL2 me- hanial pro of of the well-foundedness theorem for mul-rel , mp-true-listp and map-fn-e0-ord as stated at the end of subsetion 1.2 by multiset-extension-of- -rel-well-founded . The rst part of the theorem, whih establishes that (map-fn- -e0-ord x) is an ordinal when (mp-true-listp x) , it is not diÆult, and an b e proved in ACL2 with minor help form the user. The hard part of the theorem is to show that map-fn-e0-ord is order-preserving. Here is an informal pro of sketh: Pro of sketh: Let us denote, for simpliity, the funtions fn1 and map-fn-e0-ord , as f and f mul , and the relation rel , mul-rel and e0-ord-< as < r el , < mul and < , resp etively. Let M and N b e two multisets of mp elements suh that N < mul M . We have to prove that f mul ( N ) < f mul ( M ). We an apply indution on the numb er of elements of N . Note that M an not b e empty, and if N is empty the result trivially holds. So let us supp ose that M and N are not empty. Let f ( x ), f ( y ) b e the biggest elements of f [ N ℄ and f [ M ℄, resp etively. Note that f ( x ) and f ( y ) are the ar elements of f mul ( N ) and f mul ( M ), resp etively. Sine f ( x ) and f ( y ) are ordinals, three ases may arise: 1. f ( x ) < f ( y ). Then, by denition of < , we have f mul ( N ) < f mul ( M ). 2. f ( x ) > f ( y ). This is not p ossible: in that ase x is in N n M and by the multiset relation denition, exists z in M n N suh that x < r el z . Consequently f ( z ) > f ( x ) > f ( y ). This ontradits the fat that f ( y ) is the biggest element of f [ M ℄. 3. f ( x ) = f ( y ). In that ase, x 2 M , sine otherwise it would exist z 2 M n N suh that x < r el z and the same ontradition as in the previous ase app ears. Let M 0 = M n f x g and N 0 = N n f x g . We have N 0 < mul M 0 and, in addition, f mul ( N 0 ) and f mul ( M 0 ) are the dr of f mul ( N ) and f mul ( M ), resp etively. Indution hyp othesis an b e applied here to onlude that f mul ( N 0 ) < f mul ( M 0 ) and therefore f mul ( N ) < f mul ( M ) : ut To lead ACL2 to the ab ove informal pro of sketh, an indution sheme must b e supplied as hint. This is a funtion suggesting suh indution sheme (the funtion max-fn1-list , omitted here, returns the element of a given list with the greatest value of fn1 ): (defun indution-multiset (n m) (delare (xargs :measure (al2::len n))) (ond ((atom n) (if (atom m) 1 2)) ((atom m) 3) (t (let* ((max-m (max-fn1-list m)) (max-n (max-fn1-list n)) (fn1-max-m (fn1 max-m)) (fn1-max-n (fn1 max-n))) (ond ((equal fn1-max-m fn1-max-n) (if (member max-n m) (indution-multiset (remove-one max-n n) (remove-one max-n m)) 5)) ((e0-ord-< fn1-max-n fn1-max-m) 6) ((e0-ord-< fn1-max-m fn1-max-n) 7) (t 8)))))) Using this indution sheme we proved the following theorem, whih is the hard part of the theorem multiset-extension-of-rel-well-founded . (defthm map-fn-e0-ord-order-preserving (implies (and (mp-true-listp n) (mp-true-listp m) (mul-rel n m)) (e0-ord-< (map-fn-e0-ord n) (map-fn-e0-ord m))) :hints (("Goal" :indut (indution-multiset n m))))) The pro of of this result was not easy: lemmas to handle eah of the ases generated by the ab ove indution sheme have to b e proved, obtaining a mehanial pro of very lose to the previous pro of sketh. See the b o ok multiset.lisp in the web page for details ab out the mehanial pro of. Well-foundedness of mul-rel has b een proved in an abstrat framework, without assuming any partiular prop erties of rel , mp and fn , exept those onerning well-foundedness. This allows us to funtionally instantiate the theorem in order to establish well-foundedness of the multiset relation indued by any given well-founded ACL2 relation. We develop ed a maro named defmul in order to mehanize this pro ess of funtional instantiation. The following setion desrib es the maro. 2 The defmul maro and the multiset b o ok We dened a maro defmul in order to provide a onvenient way to dene the multiset relation indued by a well-founded relation, and to delare the orresp onding wellfounded relation rule. We explain now how defmul is used. Let us supp ose we have a previously dened (or onstrained) relation my-rel , whih is known to b e well-founded on a set of ob jets satisfying the measure prop erty my-mp and justied by the emb edding funtion my-fn . That is to say, the following theorem, using variables x and y , has b een proved (and stored as a well-founded relation rule): (defthm theorem-name (and (implies ( my-mp x ) (e0-ordinalp ( my-fn x ))) (implies (and ( my-mp x ) ( my-mp y ) ( my-rel x y )) (e0-ord-< ( my-fn x ) ( my-fn y )))) :rule-lasses :well-founded-relation)) In order to dene the (well-founded) multiset relation indued by my-rel , we write the following maro all: (defmul ( my-rel theorem-name my-mp my-fn x y )) The expansion of this maro generates a numb er of ACL2 forms. You may use the ACL2 trans1 ommand in order to view the translated form of a defmul all. The main non-lo al events generated by this maro all are: { the denitions needed for the multiset relation indued by my-rel : funtions existsmy-rel -bigger , forall-existsmy-rel -bigger , and mulmy-rel analogous to the funtions given in subsetion 1.2. { the denition of the multiset measure prop erty, my-mp -true-listp . { the denition of mapmy-fn -e0-ord , the emb edding funtion from multisets to ordinals. { the well-foundedness theorem for mulmy-rel , my-mp -true-listp and mapmy- -fn -e0-ord . This theorem is proved by funtional instantiation from multiset- -extension-of-rel-well-founded and is named multiset-extension-ofmy- -rel -well-founded We exp et defmul to work without assistane from the user. After the ab ove all to defmul , the funtion mulmy-rel is dened as a well-founded relation on multisets of elements satisfying the prop erty my-mp , indued by the well-founded relation my-rel . From this moment on, mulmy-rel an b e used in the admissibility test for reursive funtions to show that the reursion terminates. To know the list of names we need to supply to a defmul all, we have develop ed a to ol to extrat the information from the ACL2 world and print it. This maro is simply alled in this way: (defmul-omponents my-rel ) This is only an informative to ol, not a event. This maro lo oks up the ACL2 world, and returns the list of names that are needed in the defmul all for my-rel . We have divided the results and to ols ab out multisets into two b o oks. The b o ok multiset.lisp ontains the pro of of the theorem multiset-extension-of-rel- -well-founded shown in subsetion 1.3. Names in this b o ok are dened in the pakage MUL . The b o ok defmul.lisp ontains the maro denitions of defmul and defmul- -omponents and inludes the multiset b o ok. See the web page for details. We have also inluded some non-lo al rules in multiset.lisp , whih help ed us to prove the three examples presented in this pap er, and we think they are general enough to assist in other ases. Two relevant examples of these additional results and to ols are: { We have dened the funtion equal-set as an equivalene relation. This funtion implements equality for sets, not for multisets, but it turned out useful in our ase studies b eause it an b e proved to b e a ongruene with resp et to b oth arguments of forall-existsmy-rel -bigger : (defun equal-set (x y) (and (subsetp x y) (subsetp y x))) (defequiv equal-set) (defong equal-set iff forall-existsmy-rel -bigger l m 1) (defong equal-set iff forall-existsmy-rel -bigger l m 2) Sine the latter two ongruene rules dep end on the partiular denition of my-rel , they are generated by every partiular all to defmul . { We also dene a meta rule to deal with dierene of multisets represented by lists with nal ommon suÆx. This rule rewrites expressions of the form (multiset-diff (list* x 1 x 2 : : : x m l) (list* y 1 y 2 : : : y k l)) to the following equivalent expression (with resp et to equal-set ): (multiset-diff (list x 1 x 2 : : : x m ) (list y 1 y 2 : : : y k )) This meta rule is very useful 2 when proving that a partiular multiset measure dereases in every reursive all of a funtion: it is \usual" that the multiset obtained measuring the arguments of a reursive all is a list with the same nal part than the multiset obtained measuring the arguments in the original all. 3 Case studies using multiset relations In the next subsetions, we show three examples where well-founded multiset relations play an imp ortant role in the ACL2 pro of of non-trivial termination prop erties. The rst example is taken from [4℄. We use a multiset relation to show termination of a tail-reursive version of Akermann's funtion. In the seond example, also taken from [4℄, we use a multiset relation to admit an iterative version of MCarthy's 91 funtion. The third example is a pro of of Newman's lemma for abstrat redution systems: every terminating and lo ally onuent redution relation has the ChurhRosser prop erty. This last example is part of a larger pro jet develop ed by the authors in order to formalize some asp ets of equational reasoning using ACL2 [8, 9℄. All the examples show one funtion whose termination is proved using a wellfounded multiset relation and a multiset measure funtion. When the funtion is presented for the rst time, its o de is ommented (using semiolons), to emphasize that a suitable measure has still to b e given in order to pass the admissibility test. 3.1 A tail-reursive version of Akermann's funtion The following is the standard denition of Akermann's funtion in ACL2: (defun ak (m n) (delare (xargs :measure (ons (+ (nfix m) 1) (nfix n)))) (ond ((zp m) (+ n 1)) ((zp n) (ak (- m 1) 1)) (t (ak (- m 1) (ak m (- n 1)))))) We now try to dene the following iterative program to ompute Akerman's funtion: ; (defun ak-it-aux (S z) ; (if (endp S) ; z ; (let ((head (first S)) 2 Due to a bug in ACL2 version 2.5, this meta rule fails to b e applied. This is not the ase in version 2.4, where we originally develop ed this work. The problem in version 2.5 an b e xed by inluding a path that will b e inluded in Version 2.6. Thanks to Matt Kaufmann for the path. ;;; (a) A well-founded partial order: (enapsulate ((rel (x y) t) (fn (x) t)) ... (defthm rel-well-founded-relation (and (e0-ordinalp (fn x)) (implies (rel x y) (e0-ord-< (fn x) (fn y)))) :rule-lasses (:well-founded-relation :rewrite)) (defthm rel-transitive (implies (and (rel x y) (rel y z)) (rel x z)))) ;;; (b) A terminating and loally onfluent redution relation: (enapsulate ((legal (x u) boolean) (redue-one-step (x u) element) (reduible (x) boolean) (transform-loal-peak (x) proof)) .... (defun proof-step-p (s) (let ((elt1 (elt1 s)) (elt2 (elt2 s)) (operator (operator s)) (diret (diret s))) (and (r-step-p s) (implies diret (and (legal elt1 operator) (equal (redue-one-step elt1 operator) elt2))) (implies (not diret) (and (legal elt2 operator) (equal (redue-one-step elt2 operator) elt1)))))) (defun equiv-p (x y p) (if (endp p) (equal x y) (and (proof-step-p (ar p)) (equal x (elt1 (ar p))) (equiv-p (elt2 (ar p)) y (dr p))))) (defthm terminating (implies (legal x op) (rel (redue-one-step x op) x))) (defthm loally-onfluent (let ((valley (transform-loal-peak p))) (implies (and (equiv-p x y p) (loal-peak-p p)) (and (steps-valley valley) (equiv-p x y valley)))))) Fig. 1. Assumptions of Newman's lemma partiular shap es ( val leys and loal peaks ): loal-peak-p reognizes pro ofs of the form v x ! u and steps-valley reognizes pro ofs of the form v  ! x  u . To deal with the assumption of lo al onuene, note that a redution is lo ally onuent i for every lo al p eak pro of there is an equivalent valley pro of. Therefore, in order to state lo al onuene of the general redution relation dened, we assume the existene of a funtion transform-loal-peak whih returns a valley pro of for every lo al p eak pro of. See again item (b) in gure 1 for a statement of this assumed prop erty. Having established the assumptions, in order to prove Newman's lemma we must show onuene of this general redution relation assumed to b e terminating and lo ally onuent. Instead of onuene, we prove the Churh-Rosser prop erty, whih is equivalent. Therefore, we must prove that for every pro of there exists an equivalent valley pro of, i.e., we have to dene a funtion transform-to-valley and prove that (transform-to-valley p) is a valley pro of equivalent to p . This is the statement of Newman's lemma: (defthm Newman-lemma (let ((valley (transform-to-valley p))) (implies (equiv-p x y p) (and (steps-valley valley) (equiv-p x y valley))))) A suitable denition of transform-to-valley and a pro of of this theorem in ACL2 is shown in the following subsetion. The hard part of the pro of is to show termination of transform-to-valley . It will b e done with the help of a well-founded multiset relation. An ACL2 pro of of Newman's lemma: The pro of ommonly found in the literature [1℄, is done by well-founded indution on the terminating redution relation. Our approah is more onstrutive and is based on a pro of given in [7℄. We have to dene a funtion transform-to-valley whih transforms every pro of in a equivalent valley pro of. For that purp ose, we an use the funtion transform-loal-peak , assumed to transform every lo al p eak pro of in a equivalent valley pro of. Thus, the funtion we need is dened to iteratively apply replae-loal-peak , (whih replaes the rst lo- al p eak subpro of by the equivalent subpro of given by transform-loal-peak ) until there are no lo al p eaks (heked by exists-loal-peak ). The following is the de- nition of transform-to-valley (we omit here the denition of replae-loal-peak and exists-loal-peak ): ;(defun transform-to-valley (p) ; (if (not (exists-loal-peak p)) ; p ; (transform-to-valley (replae-loal-peak p)))) This funtion is not admitted without help from the user. The reason is that when a lo al p eak in a pro of is replaed by an equivalent valley subpro of, the length of the pro of obtained may b e larger than the length of the original pro of. Nevertheless, the key p oint here is that every element of the new subpro of is smaller (w.r.t. the well-founded relation rel ) than the greatest element of the lo al p eak. If we measure a pro of as the multiset of the elements involved in it, then replaing a lo al p eak subpro of by an equivalent valley subpro of, we obtain a pro of with smaller measure with resp et to the well-founded multiset relation indued by rel . The funtion proof-measure returns this measure for a given pro of: it ollets the elt1 elements of every pro of step in a pro of. (defun proof-measure (p) (if (endp p) nil (ons (elt1 (ar p)) (proof-measure (dr p))))) Using defmul , we dene the well-founded relation mul-rel , indued by the wellfounded relation rel intro dued in the previous subsetion: (defmul (rel rel-well-founded-relation-on-mp t fn x y)) The main result we proved states that the pro of measure dereases (with resp et to the well-founded relation mul-rel ) if a lo al-p eak is replaed by an equivalent valley subpro of: (defthm transform-to-valley-admission (implies (exists-loal-peak p) (mul-rel (proof-measure (replae-loal-peak p)) (proof-measure p))) :rule-lasses nil) With this theorem, admission of the funtion transform-to-valley is now p ossible, giving a suitable hint: (defun transform-to-valley (p) (delare (xargs :measure (proof-measure p) :well-founded-relation mul-rel :hints (("Goal" :use (:instane transform-to-valley-admission))))) (if (not (exists-loal-peak p)) p (transform-to-valley (replae-loal-peak p)))) One transform-to-valley is admitted (whih is the hard part of the theorem), the following two theorems are proved, and this trivially implies Newman's lemma as stated at the end of subsetion 3.3. (defthm equiv-p-x-y-transform-to-valley (implies (equiv-p x y p) (equiv-p x y (transform-to-valley p)))) (defthm valley-transform-to-valley (implies (equiv-p x y p) (steps-valley (transform-to-valley p)))) The mehanial pro of of Newman's lemma is the most diÆult of the three examples presented here. Lemmas have to b e proved to simplify the multiset dierenes app earing in the onjeture generated by the termination pro of of transform-to- -valley . See the le newman.lisp in the web page for details. We also provide b o oks proving deidability of the equivalene relation generated by a terminating and lo ally onuent redution relation. To see how this result an b e exp orted to the study of equational theories, see [9℄. 4 Conlusions We have presented a formalization of multiset relations in ACL2, showing how they an b e used as a to ol for proving non-trivial termination prop erties of reursive fun- tions in ACL2. We have dened the multiset relation indued by a given relation and proved a theorem establishing well-foundedness of the multiset relation indued by a well-founded relation. This theorem is formulated in an abstrat way, so that funtional instantiation an b e used to prove well-foundedness of onrete multiset relations. We have presented also a maro named defmul , implemented to provide a onvenient to ol to dene well-founded multiset relations indued by well-founded relations. This maro allows the denition of these multiset relations in a single step. Three ase studies are presented, to show how this to ol an b e useful in obtaining pro ofs of non-trivial termination prop erties of funtions dened in ACL2. The rst ase study is the denition of a tail-reursive version of Akermann's funtion. The seond is the admissibility of a denition of MCarthy's 91 funtion, and a study of its prop erties. The third is a pro of of Newman's lemma for abstrat redution relations. This work arose as part of a larger pro jet, trying to formalize prop erties of abstrat redution relations, equational theories and term rewriting systems [8, 9℄. In that work, ACL2 is used as a meta-logi to study prop erties of a formal pro of system, namely equational logi. Newman's lemma is a key result needed to prove deidability of equational theories given by omplete term rewriting systems [1℄. One formalized multiset relations and used in the pro of of Newman's lemma, we deided to make a to ol ( defmul ) whih allowed to exp ort the results on multisets to other ontexts. To test this implementation, we applied it to two examples desrib ed in [4℄: Akermann's funtion and MCarthy's 91 funtion. Further work has to b e done to provide a go o d library of lemmas to handle multisets and their op erations. We plan also to improve the use of defmul , in order to provide only the name of the well-founded relation, avoiding to give the funtions, variables and event asso iated with it. Up dated versions of the b o oks will b e in the web page. The examples presented here are all of a theoretial nature. Nevertheless, a remark given at the end of setion I I I in [4℄, p ointing an heuristi pro edure for proving termination of lo ops using multisets, suggests that this kind of orderings ould b e applied to a wider lass of termination problems and that the searh for a suitable multiset measure ould b e mehanized to some extent. Another appliation of multisets orderings is to provide the basis for some pro ofs of termination of term rewriting systems [1℄. We intend to make further researh following these two lines. Referenes 1. Baader, F., and Nipkow, T. Term rewriting and al l that . Cambridge University Press, 1998. 2. Brok, B. defstruture for ACL2 version 2.0. Tehnial Rep ort, 1997. 3. Cowles, J. Knuth's generalization of MCarthy's 91 funtion. In Computer-Aided Reasoning: ACL2 Case Studies , M. Kaufmann, P. Manolios, and J S. Mo ore, Eds. Kluwer Aademi Publishers, 2000, h. 17. 4. Dershowitz, N., and Manna, Z. Proving termination with multiset orderings. In Annual International Col loquium on Automata, Languages and Programming (1979), H. Maurer, Ed., no. 71 in LNCS, Springer-Verlag, pp. 188{202. 5. Kaufmann, M., Manolios, P., and Moore, J S. Computer-Aided Reasoning: An Approah . Kluwer Aademi Publishers, 2000. 6. Kaufmann, M., and Moore, J S. ACL2 version 2.5. http://www.s.utexas.edu/users/mo ore- /al2/al2-do .html, 2000. 7. Klop, J. Term rewriting systems. Handbook of Logi in Computer Siene (1992). 8. Ruiz-Reina, J., Alonso, J., Hidalgo, M., and Mart  n, F. http://www-s.us.es/ ~ jruiz/al2rewr. Formalizing equational reasoning in the ACL2 theorem prover, 2000. 9. Ruiz-Reina, J., Alonso, J., Hidalgo, M., and Mart  n, F. Formalizing rewriting in the ACL2 theorem prover. In Proeedings of AISC'2000 (Fifth International Conferene Artiial Intel ligene and Symboli Computation) (to app ear), LNCS, Springer Verlag.