Formal proofs about rewriting using ACL2

Fo mal p oo s abou ew i ing using ACL2 José-Luis Ruiz-Reina, José-An onio Alonso, Ma ía-José Hidalgo and F ancisco-Jesús Ma ín-Ma eos Depa amen o de Ciencias de la Compu ación e In eligencia A i icial, Escuela Técnica Supe io de Ingenie ía In o má ica, Uni e sidad de Se illa, A da. Reina Me cedes, s/n. 41012 Se illa, Spain E-mails: {j uiz,jalonso,mjoseh, ma in}@cs.us.es We p esen an applica ion o he ACL2 heo em p o e o eason abou ew i e sys ems heo y. We desc ibe he o maliza ion and ep esen a ion aspec s o ou wo k using he i s - o de , quan i ie - ee logic o ACL2 and we ske ch some o he main poin s o he p oo e o . Fi s , we p esen a o maliza ion o abs ac educ ion sys ems and hen we show how his abs ac ion can be ins an ia ed o es ablish esul s abou e m ew i ing. The main heo ems we mechanically p o ed a e Newman’s lemma ( o abs ac educ ions) and Knu h–Bendix c i ical pai heo em ( o e m ew i ing). Keywo ds: heo em p o ing, ACL2, ew i ing, o mal e i ica ion 1. In oduc ion Fo mal, mechanically checked p oo s no only p o ide e i ica ion o ma hema ical esul s bu encou age close examina ion and deepe unde s anding o hose esul s. We epo in his pape he s a us o ou wo k on he applica ion o he ACL2 heo em p o e o eason abou abs ac educ ions and e m ew i ing sys ems heo y; con luence, local con luence, Noe he iani y, no mal o ms and o he ela ed concep s ha e been o mal- ized in he ACL2 logic and some esul s abou abs ac educ ions and e m ew i ing ha e been mechanically p o ed, including Newman’s lemma and Knu h–Bendix c i ical pai heo em. ACL2 [8] is bo h a logic and a mechanical heo em p o ing sys em suppo ing i , de eloped by J Moo e and M. Kau mann. The ACL2 logic is an exis en ially quan i ie - ee, i s -o de logic wi h equali y. ACL2 is also a p og amming language, an ap- plica i e subse o Common Lisp. The sys em e ol ed om he Boye –Moo e heo em p o e , also known as Nq hm. The no ion o ew i ing o simpli ica ion is a c ucial componen in symbolic com- pu a ion: simpli ica ion p ocedu es a e needed o ans o m complex objec s in o de o ob ain equi alen bu simple objec s and o compu e unique ep esen a ions o equi a- lence classes (see, o example, [5]). Since ACL2 is also a p og amming language, his wo k can be seen as a i s s ep o ob ain e i ied execu able (and e icien , i possible) This wo k has been suppo ed by DGES/MEC: P ojec TIC2000-1368-CO3-02. Common Lisp code o componen s o symbolic compu a ion sys ems and equa ional heo em p o e s. Al hough a ully e i ied implemen a ion o such a sys em is cu en ly imp ac ical, se e al basic algo i hms can be mechanically “ce i ied” and in eg a ed as pa o he whole sys em. We also show he e how a weak logic like he ACL2 logic (no quan i ica ion, no in ini e objec s, no highe o de a iables, e c.) can be used o ep esen , o malize, and mechanically p o e non i ial heo ems. In his pape , we place emphasis on desc ibing he o maliza ion and ep esen a ion aspec s o ou wo k and we also highligh some o he main poin s o he p oo e o . Due o he lack o space we will skip de ails o he mechanical p oo s and o he same eason some unc ion de ini ions will be omi ed. We u ge he in e es ed eade o see he comple e de elopmen , a ailable on he web a URL h p://www.cs.us.es/˜j uiz/acl2- ew . This pape is an ex ended and e ised e sion o [15,17]. The es o he pape is o ganized as ollows. Sec ions 1.1 and 1.2 p esen a b ie desc ip ion o ACL2 and an in o mal p esen a ion o he heo y o abs ac educ ions and e m ew i ing, espec i ely. In sec ion 2 we p esen a o maliza ion o abs ac e- duc ions in he ACL2 logic, including a p oo o Newman’s lemma. In sec ion 3 we desc ibe he ins an ia ion o he abs ac o maliza ion p esen ed in he p e ious sec ion o he case o e m ew i ing educ ions. We also p esen a p oo o Knu h–Bendix c i i- cal pai heo em and a p oo o decidabili y o equa ional heo ies desc ibed by comple e e m ew i ing sys ems. Finally, in sec ion 4, we d aw some conclusions and discuss u- u e wo k. 1.1. The ACL2 sys em We b ie ly desc ibe he e he ACL2 heo em p o e and i s logic. The bes in oduc- ion o ACL2 is [8]. To ob ain mo e backg ound on ACL2, see he ACL2 use ’s manual in [9]. A desc ip ion o he main p oo echniques used in Nq hm, also used in ACL2, can be ound in [3]. 1.1.1. The logic ACL2 s ands o A Compu a ional Logic o Applica i e Common Lisp. The ACL2 logic is a quan i ie - ee, i s -o de logic wi h equali y, desc ibing an applica i e subse o Common Lisp. The syn ax o e ms is ha o Common Lisp [19] (we will assume ha he eade is amilia wi h his language). The logic includes axioms o p oposi ional logic and o a numbe o Lisp unc ions and da a ypes. Rules o in e ence include hose o p oposi ional calculus, equali y, and ins an ia ion. By he p inciple o de ini ion,new unc ion de ini ions (using de un) a e admi ed as axioms only i he e exis s an o dinal measu e in which he a gumen s o each ecu si e call (i any) dec ease, hus p o ing i s e mina ion. This ensu es ha no inconsis encies a e in oduced by new de ini ions. The heo y has a cons uc i e de ini ion o he o dinals up o ε0, in e ms o lis s and na u al numbe s, gi en by he p edica e e0-o dinalp and he o de e0-o d-<.One impo an ule o in e ence is he p inciple o induc ion, ha pe mi s p oo s by induc ion on ε0. In addi ion o he de ini ion p inciple, he encapsula ion p inciple (using encap- sula e) allows he use o in oduce new unc ion symbols by axioms cons aining hem o ha e ce ain p ope ies. To ensu e consis ency, wi ness unc ions ha ing he same p ope ies ha e o be exhibi ed. Wi hin he scope o an encapsula e, p ope - ies s a ed wi h de hm need o be p o ed o he wi nesses; ou side, hose heo ems wo k as assumed axioms. The unc ions pa ially de ined wi h encapsula e can be seen as second o de a iables, ep esen ing unc ions wi h hose p ope ies. A de i ed ule o in e ence, unc ional ins an ia ion, allows some kind o second-o de easoning: heo ems abou cons ained unc ions can be ins an ia ed wi h unc ion symbols i hey a e known o ha e he same p ope ies (see [10]). 1.1.2. The heo em p o e The ACL2 heo em p o e is inspi ed by Nq hm, bu has been conside ably im- p o ed. The main p oo echniques used by he p o e a e simpli ica ion and induc ion. Simpli ica ion is a p ocess combining e m ew i ing wi h some decision p ocedu es (lin- ea a i hme ic, ype se easone , e c.). Sophis ica ed heu is ics o disco e ing an (o en sui able) induc ion scheme is one o he key poin s in he success o ACL2 and i s p e- decesso . A collec ion o de ini ions and p o ed heo ems is usually s o ed in a ce i ied ile o e en s (a book in he ACL2 e minology), ha can be included in o he books. The command de hm s a s a p oo a emp , and, i i succeeds, he heo em is s o ed as a ule (in mos cases, a ew i ing ule). The heo em p o e is au oma ic in he sense ha once de hm is in oked, he use can no longe in e ac wi h he sys em. Howe e , in a deepe sense, he sys em is in e ac i e. Ve y o en, non i ial p oo s a e no ound by he sys em in a i s a emp and hen he use has o guide he p o e by adding lemmas and de ini ions, used in subsequen p oo s as ules. Inspec ion o ailed p oo s is e y use ul o ind hose lemmas needed o “p og am” he sys em in o de o ge he mechanical p oo o a non i ial esul . This kind o in e ac ion is called “The Me hod” by he au ho s o he sys em (see [8]). Thus, he ole o he use is impo an : a ypical p oo e o consis s o o malizing he p oblem in he logic and helping he p o e o ind a p econcei ed hand p oo by means o a sui able se o ew i e ules. The mechanical p oo s o he esul s p esen ed he e we e ca ied ou ollowing “The Me hod”. 1.2. Abs ac educ ions and e m ew i ing sys ems This sec ion p o ides a sho in oduc ion o basic concep s and de ini ions om ew i ing heo y used in his pape . A comple e desc ip ion can be ound in [1]. An abs ac educ ion is simply a bina y ela ion →de ined on a se A. We will deno e as ←,↔,∗ →and ∗ ↔ espec i ely he in e se ela ion, he symme ic closu e, he e lexi e- ansi i e closu e and he equi alence closu e. The ollowing concep s a e de ined wi h espec o a educ ion ela ion →.Anelemen xis in no mal o m (o i educible) i he e is no zsuch ha x→z. We say ha xand ya e joinable (deno ed as x↓y) i he e exis s usuch ha x∗ →u∗ ←y. We say ha xand ya e equi alen i x∗ ↔y. An impo an p ope y o s udy abou educ ion ela ions is he exis ence o unique no mal o ms o equi alen objec s. A educ ion ela ion has he Chu ch–Rosse p op- e y i e e y wo equi alen objec s a e joinable. An equi alen p ope y is con luence: o all x,u, such ha u∗ ←x∗ → , henu↓ . In e e y educ ion ela ion wi h he Chu ch–Rosse p ope y he e a e no dis inc and equi alen no mal o ms. I in addi- ion he ela ion is no malizing (i.e., e e y elemen has a no mal o m, deno ed as x↓) hen x∗ ↔yi x↓= y↓. P o ided no mal o ms a e compu able and iden i y in Ais decidable, hen he equi alence ela ion ∗ ↔is decidable, by means o a es o equali y o no mal o ms. Ano he impo an p ope y is e mina ion: a educ ion ela ion is e mina ing (o Noe he ian) i he e is no in ini e educ ion sequence x0→x1→x2→ ···.Ob i- ously, e e y Noe he ian educ ion is no malizing. The Chu ch–Rosse p ope y can be localized when he educ ion is e mina ing. In ha case an equi alen p ope y is local con luence: o allx,u, such ha u←x→ , henu↓ . This esul is known as Newman’s lemma. An impo an ype o educ ion ela ion is de ined on he se T(,X)o i s o de e ms o a gi en language, whe e is a se o unc ion symbols, and Xis a se o a iables. In his con ex , an equa ion isapai o e msl= . The educ ion ela ion de ined by a se o equa ions Eis de ined as: s→E i he e exis l= ∈Eand a subs i u ion σo he a iables in l( he ma ching subs i u ion) such ha σ(l)is a sub e m o sand is ob ained om sby eplacing he sub e m σ(l) o σ( ). This educ ion ela ion is o g ea in e es in uni e sal algeb a because i can be p o ed ha E|= s= i s∗ ↔E . This implies decidabili y o e e y equa ional heo y de ined by a se o axioms Esuch ha →Eis e mina ing and locally con luen . To emphasize he use o he equa ion l= om le o igh as desc ibed abo e, we w i e l→ and alk abou ew i e ules.A e m ew i ing sys em (TRS) is a se o ew i e ules. Unless deno ed o he wise, Eis always a se o equa ions (equa ional axioms) and Ris a e m ew i ing sys em. Local con luence is decidable o ini e and no malizing TRSs: joinabili y has only o be checked o a ini e numbe o pai o e ms, called c i ical pai s, accoun ing o he mos gene al o ms o local di e gence (see [1] o a p ecise de ini ion). The c i ical pai heo em s a es ha a TRS is locally con luen i all i s c i ical pai s a e joinable. Thus, he Chu ch–Rosse p ope y o e mina ing TRSs is a decidable p ope y: i is enough o check i e e y c i ical pai has a common no mal o m. In ha case, he TRS is said o be comple e and can be used o decide i s equa ional heo y. I a e mina ing TRS has a c i ical pai wi h di e en no mal o ms, he e is s ill a chance o ob ain a decision p ocedu e o i s equa ional heo y, adjoining ha equa ion as a new e mina ing ew i e ule. This is he basis o he well-known comple ion algo i hm (see [1] o de ails). In he sequel, we desc ibe he o maliza ion o hese p ope ies in he ACL2 logic and some poin s o hei mechanical p oo . Fo he es o he pape , when we alk abou “p o e” we mean “mechanically p o e using ACL2”. 2. Fo malizing abs ac educ ions in ACL2 One possible way o ep esen abs ac educ ion ela ions in he ACL2 logic could be simply o de ine hem as bina y Boolean unc ions, using encapsula e o s a e hei p ope ies. Ne e heless, we adop ed a sligh ly di e en app oach, in o de o s ess he “ educ ion” poin o iew: i x→y, mo e impo an han he ela ion be ween xand yis he ac ha yis ob ained om xby applying some kind o ans o ma ion o ope - a o . In i s mos abs ac o mula ion, we can iew a educ ion as a bina y unc ion ha , gi en an elemen and an ope a o , e u ns ano he objec , pe o ming a one-s ep educ- ion. Think o example o equa ional educ ions: elemen s in ha case a e i s -o de e ms and ope a o s a e he objec s cons i u ed by a posi ion (indica ing he sub e m eplaced), an equa ion ( he ule applied) and a subs i u ion ( he ma ching subs i u ion). O cou se no any ope a o can be applied o any elemen . Thus, a second com- ponen in his o maliza ion is needed: a Boolean bina y unc ion o es i i is legal o apply an ope a o o an elemen . Finally, a hi d componen is in oduced: since com- pu a ion o no mal o ms equi es sea ching o legal ope a o s o apply, we will need a una y unc ion ha when applied o an elemen e u ns a legal ope a o , whene e i exis s, o nil o he wise (a educibili y es ).1 The abo e conside a ions lead us o o malize he concep o abs ac educ ions in ACL2, using h ee pa ially de ined unc ions: educe-one-s ep,legal and educible. This can be done wi h he ollowing encapsula e (do s a e used o omi local e en s2and echnical de ails, as in he es o he pape ): (encapsula e (( educe-one-s ep (x op) ) (legal (x op) ) ( educible (x) )) ... (de hm legal- educible-1 (implies ( educible x) (legal x ( educible x)))) (de hm legal- educible-2 (implies (no ( educible x)) (no (legal x op)))) ...) 1I is possible o p o e some o he heo ems p esen ed he e wi hou any e e ence o a educibili y es ( o example, Newman’s lemma). See he web page. 2The speci ic wi ness unc ions de ini ions a e i ele an o ou discussion, since ou side he encapsu- la e only he nonlocal p ope ies a e used. The i s pa o e e yencapsula e is a signa u e desc ip ion o he nonlocal unc ions pa ially de ined. No e ha ( educe-one-s ep x op) is he elemen ob ained applying he ope a o op o x. The unc ion legal is he applicabili y es , i.e., (legal x op) is no nil i i is legal o apply op o x.And educible is he educibili y es : ( educible x) is a legal ope a o applicable o xwhene e such ope a o exis s, nil o he wise (we a e assuming ha nil does no ep esen any ope a o ). The wo heo ems assumed abo e as axioms a e minimal equi emen s o e e y educ ion we de ined: i u he p ope ies ( o example, local con luence, con luence o Noe he iani y) we e assumed, hey ha e o be s a ed inside he encapsula e.Thisis a e y abs ac amewo k o o malize educ ions in ACL2. We hink ha hese h ee unc ions cap u e he basic abs ac ea u es e e y educ ion has. On he one hand, a p ocedu al aspec : he compu a ion o no mal o ms, applying ope a o s un il i educible objec s a e ob ained. On he o he hand, a decla a i e aspec : e e y educ ion ela ion desc ibes i s equi alence closu e. Rep esen ing educ ions in his way, we can de ine concep s like he Chu ch–Rosse p ope y, local con luence o Noe he iani y and e en p o e non i ial heo ems like Newman’s lemma, as we will see. To ins an ia e his gene al amewo k, conc e e ins ances o educe-one-s ep, legal and educible ha e o be de ined and he p ope ies assumed he e as axioms mus be p o ed o hose conc e e de ini ions. By unc ional ins an ia ion, esul s abou abs ac educ ions can hen be easily expo ed o conc e e cases (as we will see o he equa ional case). 2.1. Equi alence and p oo s Due o he cons uc i e na u e o he ACL2 logic, in o de o de ine x∗ ↔y,we ha e o include an a gumen wi h a sequence o s eps x=x0↔x1↔x2···↔xn=y. This is done by he unc ion equi -p de ined in igu e 1. (equi -p x y p) is i pis an abs ac p oo 3jus i ying ha x∗ ↔y. Thismeans ha pis a sequence o legal s eps connec ing xand y, whe e each p oo s ep is a s uc u e4 -s ep wi h ou ields: el 1,el 2 ( he elemen s ela ed by he s ep), di ec (a boolean alue indica ing i he s ep is di ec o in e se) and ope a o . A p oo s ep is legal (as de ined by p oo -s ep-p) i one o i s elemen s is ob ained by applying i s ope a o (which mus be legal) o he o he elemen , in he di ec ion indica ed by di ec .Two abs ac p oo s jus i ying he same equi alence will be said o be equi alen . The Chu ch–Rosse p ope y and local con luence can be ede ined wi h espec o he o m o abs ac p oo s (sec ions 2.2 and 2.3). Fo ha pu pose, we de ine (omi ed he e) unc ions o ecognize p oo s wi h pa icula shapes ( alleys and local peaks): local-peak-p ecognizes p oo s o he o m ←x→uand s eps- alley ecognizes p oo s o he o m ∗ →x∗ ←u. 3O simply a p oo i ha e minology does no a ise con usion wi h p oo s done using he ACL2 sys em. 4We used he de s uc u e ool de eloped by B. B ock [4]. (de s uc u e -s ep di ec ope a o el 1 el 2) (de un p oo -s ep-p (s) (le ((el 1 (el 1 s)) (el 2 (el 2 s)) (op (ope a o s)) (di ec (di ec s))) (and ( -s ep-p s) (implies di ec (and (legal el 1 op) (equal ( educe-one-s ep el 1 op) el 2))) (implies (no di ec ) (and (legal el 2 op) (equal ( educe-one-s ep el 2 op) el 1)))))) (de un equi -p (x y p) (i (endp p) (equal x y) (and (p oo -s ep-p (ca p)) (equal x (el 1 (ca p))) (equi -p (el 2 (ca p)) y (cd p))))) Figu e 1. De ini ion o p oo s and equi alence. 2.2. The Chu ch–Rosse p ope y and decidabili y We desc ibe how we o malized and p o ed he decidabili y o an equi alence e- la ion desc ibed by a Chu ch–Rosse and no malizing educ ion. Valley p oo s can be used o e o mula e he de ini ion o he Chu ch–Rosse p ope y: a educ ion is Chu ch– Rosse i o e e y abs ac p oo he e exis s an equi alen alley p oo . Since he ACL2 logic is quan i ie - ee, he exis en ial quan i ie in his s a emen has o be e- placed by a Skolem unc ion, which we call ans o m- o- alley. The concep o being no malizing can also be e o mula ed in e ms o abs ac p oo s: a educ ion is no malizing i o e e y elemen he e exis s an abs ac p oo o an equi alen i e- ducible elemen . This p oo is gi en by he (Skolem) unc ion p oo -i educible (no e ha we a e no assuming Noe he iani y ye ). P ope ies de ining a Chu ch–Rosse and no malizing educ ion a e encapsula ed as shown in igu e 2, i em (a). The unc ion -equi es s i no mal o ms a e equal. The no mal o m o an elemen xis de ined o be he las elemen o (p oo -i educible x): (de un no mal- o m (x) (las -o -p oo x (p oo -i educible x))) (de un -equi (x y) (equal (no mal- o m x) (no mal- o m y))) ;;; (a) De ini ion o Chu ch-Rosse no malizing educ ion: (encapsula e ((legal (x op) ) ( educe-one-s ep (x op) ) ( educible (x) ) ( ans o m- o- alley (x) ) (p oo -i educible (x) )) ..... (de hm Chu ch-Rosse -p ope y (le (( alley ( ans o m- o- alley p))) (implies (equi -p x y p) (and (s eps- alley alley) (equi -p x y alley))))) ..... (de hm no malizing (le * ((p-x-y (p oo -i educible x)) (y (las -o -p oo x p-x-y))) (and (equi -p x y p-x-y) (no ( educible y)))))) ;;; (b) Main heo ems p o ed: (de hm i -C-R-- wo-i educible-connec ed-a e-equal (implies (and (equi -p x y p) (no ( educible x)) (no ( educible y))) (equal x y))) (de hm -equi -sound (implies ( -equi x y) (equi -p x y (make-p oo -common-n- x y)))) (de hm -equi -comple e (implies (equi -p x y p) ( -equi x y)) Figu e 2. Chu ch–Rosse and no malizing implies decidabili y. To p o e decidabili y o a Chu ch–Rosse and no malizing ela ion, i is enough o p o e ha -equi is a comple e and sound algo i hm deciding he equi a- lence ela ion desc ibed by he educ ion ela ion. See igu e 2, i em (b).Wealso include he main lemma used, s a ing ha he e a e no dis inc equi alen i e- ducible elemen s. No e also ha soundness is exp essed in e ms o a Skolem unc- ion make-p oo -common-no mal- o m (de ini ion omi ed), which cons uc s a p oo jus i ying he equi alence. These heo ems a e p o ed qui e easily, wi hou much guidance om he use . The main poin he e is ha he induc ion scheme sugges ed by he unc ion equi -p (and mechanically gene a ed by he sys em), u ns ou o be e y use ul in p o ing p ope ies abou he ela ion ∗ ↔: i esembles he in ui i e idea o “induc ion on he numbe o s eps”. 2.3. Noe he iani y, local con luence and Newman’s lemma A ela ion is well ounded on a se Ai e e y nonemp y subse has a minimal elemen . A es ic ed no ion o well- oundedness is buil in o ACL2, based on he ol- lowing me a- heo em: a ela ion on a se Ais well- ounded i he e exis s a unc ion F:A→O d such ha x<y⇒F(x) < F(y),whe eO d is he class o all o di- nals. In ACL2, once a ela ion is p o ed o sa is y hese equi emen s (and he heo em is s o ed as a well- ounded- ela ion ule), i can be used in he admissibili y es o ecu si e unc ions. A gene al well- ounded pa ial o de el can be de ined in ACL2 as shown in igu e 3, i em (a). Since only o dinals up o ε0a e o malized in he ACL2 logic, a limi a ion is imposed in he maximal o de ype o well- ounded ela ions ha can be ep esen ed. Consequen ly, ou o maliza ion su e s om he same es ic ion.5 In igu e 3, i em (b) a gene al de ini ion o a Noe he ian and locally con luen e- duc ion ela ion is p esen ed.6Local con luence is easily exp essed in e ms o he shape o abs ac p oo s in ol ed: a ela ion is locally con luen i o e e y local peak p oo he e is an equi alen alley p oo . This alley p oo is assumed o be gi en by a unc ion named ans o m-local-peak. As o Noe he iani y, ou o maliza ion elies on he ollowing me a- heo em: a educ ion is Noe he ian i and only i i is con ained in a well- ounded pa ial o de ing. Thus, he gene al well- ounded ela ion el p e iously p esen ed is used o jus i y Noe he iani y o he gene al educ ion ela ion de ined: o e e y elemen xsuch ha a legal ope a o op can be applied o, hen applying op o xusing educe-one-s ep, p oduces an elemen less han x(wi h espec o el). The s anda d p oo o Newman’s lemma ound in he li e a u e [1], shows con- luence by Noe he ian induc ion based on he Noe he ian educ ion ela ion. Ne e - heless, he o mal p oo we ob ained is di e en , in luenced by ou abs ac p oo app oach. I is inspi ed by he one gi en by Klop in [11]. In ou o maliza ion, we show ha he educ ion ela ion has he Chu ch–Rosse p ope y7by de ining a unc ion ans o m- o- alley and p o ing ha o e e y p oo p,( ans o m- o- - alley p) is an equi alen alley p oo . This unc ion is de ined o i e a i ely ap- ply eplace-local-peak (which eplaces a local peak subp oo by he equi alen p oo gi en by ans o m-local-peak), un il he e a e no local peaks. This can be seen as a no maliza ion p ocess ac ing on abs ac p oo s. See de ini ion in igu e 3, i em (c). 5Ne e heless, no pa icula p ope ies o ε0a e used in ou p oo s, excep well- oundedness. 6Name con lic s wi h he unc ions p esen ed in he p e ious and nex sec ions a e a oided using Common Lisp packages. 7No e ha we do no need o deal wi h con luence since he Chu ch–Rosse p ope y, an equi alen concep , is p o ed wi h he same e o . ;;; (a) TRS wi h joinable c i ical pai s: (encapsula e ((RLC () ) ( ans o m-cp (l1 1 pos l2 2) )) ... (de hm RLC- ew i e-sys em ( ew i e-sys em (RLC))) (de hm RLC-joinable-c i ical-pai s (implies (and (membe (cons l1 1) (RLC)) (membe (cons l2 2) (RLC)) (posi ion-p pos l1) (no ( a iable-p (occu ence l1 pos)))) (le * ((cp- (cp- l1 1 pos l2 2)) ( alley-cp ( ans o m-cp l1 1 pos l2 2))) (implies cp- (and (eq-equi -p (lhs cp- ) ( hs cp- ) alley-cp (RLC)) (s eps- alley alley-cp))))))) ;;; (b) Theo em p o ed: (de un ans o m-eq-local-peak (p) ...) (de hm c i ical-pai - heo em (le (( alley ( ans o m-eq-local-peak p))) (implies (and (eq-equi -p 1 2 p (RLC)) (local-peak-p p)) (and (s eps- alley alley) (eq-equi -p 1 2 alley (RLC)))))) Figu e 5. The c i ical pai heo em. 3.5. Reduc ion o de ings In o de o o malize e mina ion p ope ies o e m ew i ing sys ems we ely on he well-known concep o educ ion o de ing, i.e., well- ounded o de ing being s able (closed unde ins an ia ion) and compa ible (closed unde eplacemen o sub e ms). We used he ollowing cha ac e iza ion: a e m ew i ing sys em R e mina es i he e exis s a educ ion o de  ha sa is ies l o all l→ ∈R. In igu e 6, encapsula ion is (encapsula e (( ed< ( 1 2) ) ( n- ed< ( e m) )) .... (de hm ed<-well- ounded- ela ion (and (e0-o dinalp ( n- ed< 1)) (implies ( ed< 1 2) (e0-o d-< ( n- ed< 1) ( n- ed< 2)))) : ule-classes :well- ounded- ela ion) (de hm ed<-s able (implies ( ed< 1 2) ( ed< (ins ance 1 sigma) (ins ance 2 sigma)))) (de hm ed<-compa ible (implies (and (posi ion-p pos e m) ( ed< 1 2)) ( ed< ( eplace- e m e m pos 1) ( eplace- e m e m pos 2)))) (de hm ed<- ansi i e (implies (and ( ed< x y) ( ed< y z)) ( ed< x z)))) (de un noe he ian- ed< (TRS) (i (endp TRS) (le (( ule (ca TRS))) (and ( ed< ( hs ule) (lhs ule)) (noe he ian- ed< (cd TRS))))) Figu e 6. A educ ion o de ed<. used o (pa ially) de ine a unc ion ed<, assumed o be a educ ion o de . The unc ion (noe he ian- ed< TRS) is de ined o es i ed< jus i ies e mina ion o TRS. Once ed< has been assumed o be a educ ion o de ing and he unc ion noe- he ian- ed< has been de ined, we p o ed ha he educ ion ela ion →Ris e mi- na ing, whene e Ris a TRS such ha (noe he ian- ed< R) ( his esul is needed o expo Newman’s lemma o he equa ional case): (de hm R-Noe he ian-i -subse p-o - ed< (implies (and (noe he ian- ed< R) (eq-legal e m op R)) ( ed< (eq- educe-one-s ep e m op) e m))) Al hough he (pa ial) de ini ion o he educ ion o de ing ed< gi en in igu e 6 wo ks well om a heo e ical poin o iew, he main d awback in his o maliza ion o educ ion o de ings is ha i can be di icul o p o e ha a pa icula o de ing ( o example, a pa h o de ing o a Knu h–Bendix o de ing [1]) is a educ ion o de ing, since an o dinal measu e n- ed< has o be gi en explici ly. 3.6. Comple e e m ew i ing sys ems and decidabili y As a consequence o he esul s p esen ed so a , and using unc ional ins an ia ion, we can o malize and p o e decidabili y o he equa ional heo y desc ibed by a comple e TRS. In he ollowing we desc ibe he assump ions needed o de ine a comple e TRS. Again using encapsula e we (pa ially) de ine a e m ew i ing sys em (RC) assumed o be comple e: (RC) is e mina ing (jus i ied by ed<) and e e y c i ical pai ob ained om ules in (RC) ha e a common no mal o m (see igu e 7). In his o maliza ion, he concep s o c i ical pai s and no mal o ms a e implemen ed by he unc ions cp- (desc ibed in sec ion 3.4) and RC-no mal- o m, espec i ely. The unc ion RC-no mal- o m is de ined o compu e no mal o ms wi h espec o he e m ew i ing sys em (RC). I i e a i ely applies he unc ion - educe un il a no mal o m is ound. The exp ession ( - educe e m TRS), whose de ini ion we omi he e, pe o ms one s ep o ew i ing, whene e i is possible. I a e ses e m o ind a sub e m subsumed by he le -hand side o a ule in TRS. When such a sub- e m is ound, i is eplaced by he co esponding ins ance o he igh -hand side o he ule. I i is no ound, hen - educe e u ns nil (and he e o e e m is in no mal o m). Those p ope ies o - educe we e mechanically e i ied. No e ha a e i ied subsump ion algo i hm is needed o ha pu pose. I is wo h poin ing ha a unc ion compu ing he no mal o m o a e m wi h espec o a TRS would no be admi ed in he ACL2 logic, since e mina ion is no assu ed in gene al. Ins ead, we assume (RC) o be e mina ing and we de ine no mal o m calcula ion wi h espec o (RC).10 Ha ing assumed he p ope ies o igu es 6 and 7, we can de ine a unc ion RC-equi alen ( es ing equali y o no mal o ms) and hen p o e ha i p o ides a comple e and sound algo i hm o decide he equa ional heo y o (RC): (de un RC-equi alen ( 1 2) (equal (RC-no mal- o m 1) (RC-no mal- o m 2))) (de hm RC-equi alen -comple e (implies (eq-equi -p 1 2 p (RC)) (RC-equi alen 1 2))) 10 Al hough his de ini ion is sui able om a o mal poin o iew, he main d awback is ha ha RC-no mal- o m is no execu able. Ne e heless, we can de ine an execu able unc ion (no mal- o m-n n e m R) ha applies (a mos ) n educ ion s eps o e m wi h espec o he TRS R. In p ac ice, his can be used o compu e no mal o ms. (encapsula e ((RC () )) ... (de hm RC- ew i e-sys em ( ew i e-sys em (RC))) (de hm RC-Noe he ian- ed< (noe he ian- ed< (RC))) (de un RC-no mal- o m ( e m) (decla e (xa gs :measu e e m :well- ounded- ela ion ed<)) (le (( ed ( - educe e m (RC)))) (i ed (RC-no mal- o m (unpack ed)) e m))) (de hm RC-common-n- -c i ical-pai s (implies (and (membe (cons l1 1) (RC)) (membe (cons l2 2) (RC)) (posi ion-p pos l1) (no ( a iable-p (occu ence l1 pos)))) (le ((cp- (cp- l1 1 pos l2 2))) (implies cp- (equal (RC-no mal- o m (lhs cp- )) (RC-no mal- o m ( hs cp- )))))))) Figu e 7. A comple e e m ew i ing sys em (RC). (de hm RC-equi alen -sound (implies (RC-equi alen 1 2) (eq-equi -p 1 2 (RC-make-p oo -common-n- 1 2) (RC)))) The p oo o he wo heo ems abo e is s aigh o wa d (al hough some elabo a ed) by means o unc ional ins an ia ion o he p e ious heo ems p esen ed. The ollowing is pa o he unc ional subs i u ion used in his ins an ia ion, associa ing o he unc ions desc ibing an abs ac educ ion he co esponding unc ions o he equa ional educ ion associa ed o (RC): ... ( educe-one-s ep eq- educe-one-s ep) ( educible (lambda ( e m) (eq- educible e m (RC)))) (legal (lambda ( e m op) (eq-legal e m op (RC)))) (equi -p (lambda ( 1 2 p) (eq-equi -p 1 2 p (RC)))) ... An impo an poin in his decidabili y heo em is ha he e i ied decision algo- i hm RC-equi alen does no deal wi h equa ional p oo s, equa ional p oo s eps o equa ional ope a o s. This is an example o composi ional easoning, o how o eason abou an implemen a ion by using ules ha ans o m some unc ions in o he unc ions (o en less e icien ) ha a e easie o eason abou . No e ha in his case he unc ions eq- educible and eq- educe-one-s ep p o ides a way o pe o m one s ep o ew i ing, whene e i is possible: gi en a e m and a TRS, apply eq- educible o ob ain an equa ional ope a o and, i non-nil, apply his ope a o o he e m using eq- educe-one-s ep.I heTRSis e mi- na ing, hen his me hod can be applied i e a i ely un il a no mal o m is ob ained. This de ini ion o no mal o m is app op ia e o easoning. Fo example, i u ns ou o be use ul when we de ine an equa ional coun e pa o p oo -i educible, a unc- ion ob aining an equa ional p oo connec ing e e y elemen o i s no mal o m, ha is needed o expo by unc ional ins an ia ion he decidabili y esul o sec ion 2.2. Ob- iously, his no mal o m calcula ion can be op imized in se e al ways. Fo example, a unc ion compu ing no mal o ms nei he needs o build an equa ional ope a o in e e y ew i ing s ep no a e se he e ms wice, sea ching o a legal equa ional ope a o , and hen applying he educ ion s ep. As we desc ibed abo e, - educe is a mo e e icien (al hough no op imal) e sion o one-s ep ew i ing. The main poin he e is ha we used he mo e heo e ical e sion o eason abou no mal o m calcula ion, which u ned ou o be simple . La e on, we p o ed heo ems ela ing he beha io o - educe wi h eq- educible and eq- educe-one-s ep, showing he equi alence wi h he imp o ed e sion o no mal o m calcula ion, and hen we s a ed he inal e sion o he heo em using - educe. 4. Conclusions and u he wo k We ha e p esen ed an applica ion o he ACL2 sys em o o malize and eason abou ew i e sys ems heo y. This is a case s udy o using he ACL2 sys em as a me a- language o o malize p ope ies o objec p oo sys ems (abs ac educ ions and equa- ional logic in his case) in i . Ou o maliza ion has he ollowing main ea u es: •Abs ac educ ion ela ions and hei p ope ies a e s a ed in a e y gene al ame- wo k, as explained in sec ion 2. Func ional ins an ia ion is ex ensi ely used o expo esul s om he abs ac case o he equa ional case. •The concep s o abs ac p oo s and equa ional p oo s a e key no ions in ou wo k, as i has been poin ed epea edly. P oo s a e ea ed as objec s ha can be ans o med o ob ain new p oo s and his poin o iew has g ea in luence bo h in o maliza ion and easoning. •Composi ional easoning is used, e i ying some unc ions by using ew i e ules ha ans o m hem in o he unc ions, o en less e icien , ha a e easie o eason abou . We hink ha he esul s p esen ed he e a e impo an o wo easons. F om a he- o e ical poin o iew, i is shown how a weak logic can be used o o malize p ope ies o TRSs. F om a p ac ical poin o iew, his is an example o how o mal me hods can help in he design o symbolic compu a ion sys ems. Usually, ew i ing echniques a e applied o he design o p oo p ocedu es in au oma ed deduc ion. We show how bene i s can be ob ained in he e e se di ec ion: au oma ed deduc ion used as a ool o “ce i y” componen s o symbolic compu a ion sys ems. Since ACL2 is also a p og amming language, compu ing and p o ing asks can be mixed. As a esul o his o maliza ion, we ob ained a numbe o basic unc ions in e m ew i ing, execu able and e i ied in ACL2; o example, ma ching, uni ica ion, compu a ion o c i ical pai s o applica ion o educ ion s eps wi h espec o a e m ew i ing sys em. We e i ied he gua ds o all hese unc ions, ensu ing in his way ha hey a e execu able in any complian Common Lisp (wi h he app op ia e iles loaded). I should be s essed ha p o ing non i ial esul s in a heo em p o e like ACL2 is no i ial. A use expe in bo h he heo em p o e and he subjec domain is needed (maybe ha is he eason why many o he published o mal p oo s a e abou o mal sys- ems). As claimed in [8], di icul ies come om “ he complexi y o he whole en e p ise o o mal p oo s”, a he han om he complexi y o ACL2. A ypical p oo e o con- sis s o o malizing he p oblem and guiding he p o e o a p econcei ed “hand p oo ”, by decomposing he p oo in o in e media e lemmas. Ne e heless, p oo s can be sim- ple i a good lib a y o p e ious esul s (books in he ACL2 e minology) is used. We hink ou wo k p o ides a good collec ion o books o be eused in u he e i ica ion e o s. The p oo desc ibed he e has been s uc u ed in h ee collec ion o books (see he web page), ch onologically de eloped in he ollowing o de (e e y book needs esul s om i s p edecesso ): 1. Books abou abs ac educ ions: abs ac -p oo s con ains basic de ini ions and p ope ies abou abs ac p oo s, con luence p o es he decidabili y o he equi alence ela ion desc ibed by a Chu ch–Rosse and no malizing educ ion, newman is he p oo o Newman’s lemma and local-con luence isap oo , by unc ional ins an ia ion, o decidabili y o he equi alence ela ion desc ibed by a e mina ing and locally con luen educ ion ela ion. 2. Books abou equa ional heo ies and ew i ing: equa ional- heo ies con ains he de ini ion and main p ope ies o he equa ional heo y gi en by a se o equa ional axioms and ew i ing de elops he no ions o educibili y, educ ion o de ings and one-s ep ew i ing. 3. The p oo o he c i ical pai heo em is in he book c i ical-pai s and decid- abili y o he equa ional heo y o a comple e TRS is p o ed in kb-decidabili y. Table 1 gi es some quan i a i e in o ma ion on he p oo . The i s column con ains he name o he book. The nex h ee columns show he numbe o lines (including commen s), he numbe o de ini ions and he numbe o heo ems in each book. These numbe s can gi e an idea o he g anula i y o ou p oo . We should say ha hese sizes can be educed, bu some imes we p e e ed o spli de ini ions and heo ems o he sake o cla i y. We also included a i h column wi h he numbe o heo ems ha needed hin s om he use : he es o he heo ems we e p o ed au oma ically by he sys em. Toge he wi h he numbe o heo ems, his can gi e an idea o he deg ee o au oma ion o he p oo s. Mos o he hin s gi en a e o disabling o enabling ules and o using ins ances o p e ious heo ems. I is clea om he able ha he main p oo e o was done o p o e Newman’s lemma and he c i ical pai heo em. I should be emphasized also ha , al hough no lis ed in he able, he books abou i s -o de e ms [14] and mul ise ela ions [16] a e c ucial in ou de elopmen . Some ela ed wo k has been done in he o maliza ion o abs ac educ ion e- la ions in o he heo em p o ing sys ems, mos ly as pa o o maliza ions on he λ-calculus. Fo example, Hue [7] in he Coq sys em o Nipkow [13] in Isabelle/HOL. A compa ison is di icul because ou goal was di e en and, mo e impo an , he logics in ol ed a e signi ican ly di e en : ACL2 logic is a much weake logic han hose o Coq o HOL. A mo e ela ed wo k is Shanka [18], using Nq hm. Al hough his wo k is on he conc e e educ ion ela ion o λ-calculus and he does no deal wi h he abs ac case, some o his ideas a e e lec ed in ou wo k. Table 1 Quan i a i e in o ma ion on he p oo s. Book Lines De ini ions Theo ems Hin s abs ac -p oo s 284 16 17 0 con luence 387 12 31 7 newman 993 15 53 10 local-con luence 464 19 14 6 equa ional- heo ies 543 11 29 8 ew i ing 720 13 38 9 c i ical-pai s 2129 43 112 26 kb-decidabili y 500 16 18 7 To al 6020 145 312 73 To ou knowledge, no o maliza ion o e m ew i ing sys ems has been done ye and, consequen ly, he o mal p oo s o hei p ope ies p esen ed he e a e he i s ones we know pe o med using a heo em p o e . In addi ion o ex end he lib a y o esul s abou e m ew i ing sys ems, he e a e also se e al ways in which he wo k p esen ed he e can be u he de eloped, mos ly de- o ed o imp o e e iciency o he e i ied algo i hms and o apply he esul s o conc e e equa ional heo ies: •In o de o ob ain ce i ied decision p ocedu es o some conc e e equa ional heo ies, wo k has o be done o o malize in ACL2 well-known e mina ing e m o de ings ( e- cu si e pa h o de ings, Knu h–Bendix o de ings, e c.). As commen ed in sec ion 3.5, maybe some p oblems will a ise due o he es ic ed no ion o Noe he iani y sup- po ed by ACL2. •The wo k p esen ed in [12] sugges s ano he applica ion o his wo k: o he heo em p o e s can be combined wi h ACL2 in o de o ob ain mechanically e i ied decision algo i hms o some equa ional heo ies. •Al hough a ully e i ied equa ional easoning sys em is cu en ly imp ac ical, i would be desi able o imp o e he e iciency o he algo i hms ( o example, using be e da a s uc u es). Composi ional easoning can be used o eason abou hese imp o ed algo i hms. •Ou o iginal mo i a ion when we began his o maliza ion (and now ou goal in he long e m) is o ob ain a ce i ied comple ion p ocedu e w i en in Common Lisp. We hink he wo k p esen ed he e is a good s a ing poin . Re e ences [1] F. Baade and T. Nipkow, Te m Rew i ing and All Tha (Camb idge Uni e si y P ess, Camb idge, 1998). [2] L. Bachmai , Canonical Equa ional P oo s (Bi khäuse , New Yo k, 1991). [3] R. Boye and JS. Moo e, A Compu a ional Logic Handbook, 2nd ed. (Academic P ess, New Yo k, 1998). [4] B. B ock, de s uc u e o ACL2 e sion 2.0, Technical Repo , Compu a ional Logic, Inc. (1997). [5] B. Buchbe ge and R. Loos, Algeb aic simpli ica ion, in: Compu e Algeb a, Symbolic and Algeb aic Compu a ion. Compu ing Supplemen um 4 (1982). [6] G. Hue , Con luen educ ions: abs ac p ope ies and applica ions o e m ew i ing sys ems, Jou nal o he ACM 27(4) (1980) 797–821. [7] G. Hue , Residual heo y in λ-calculus: a o mal de elopmen , Jou nal o Func ional P og amming 4 (1994) 475–522. [8] M. Kau mann, P. Manolios and JS. Moo e, Compu e -Aided Reasoning: An App oach (Kluwe Aca- demic, Do d ech , 2000). [9] M. Kau mann and JS. Moo e, ACL2 Ve sion 2.5 (2000) a ailable a h p://www.cs. u exas.edu/use s/moo e/acl2/acl2-doc.h ml. [10] M. Kau mann and JS. Moo e, S uc u ed heo y de elopmen o a mechanized logic, Jou nal o Au oma ed Reasoning 26(2) (2001) 161–203. [11] J.W. Klop, Te m ew i ing sys ems, in: Handbook o Logic in Compu e Science (Cla endon P ess, Ox o d, 1992). [12] W. McCune and O. Shumsky, I y: a p ep ocesso and p oo checke o i s -o de logic, in: Compu e -Aided Reasoning: ACL2 Case S udies (Kluwe Academic, Do d ech , 2000) chap e 16. [13] T. Nipkow, Mo e Chu ch–Rosse p oo s, Jou nal o Au oma ed Reasoning 26(1) (2001) 51–66. [14] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, Mechanical e i ica ion o a ule based uni ica ion algo i hm in he Boye –Moo e heo em p o e , in: AGP’99 Join Con e ence on Decla a- i e P og amming (1999) pp. 289–304. [15] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, A mechanical p oo o Knu h–Bendix c i ical pai heo em (using ACL2), in: FTP’2000 (Thi d Wo kshop on Fi s -O de Theo em P o ing), Technical Repo 5-2000, Fachbe ich e In o ma ik, Uni e si ä Koblenz-Landau (2000). [16] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, Mul ise ela ions: a ool o p o ing e - mina ion, in: Second ACL2 Wo kshop, Technical Repo TR-00-29, Compu e Science Depa amen , Uni e si y o Texas (2000). [17] J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo and F.J. Ma ín, Fo malizing ew i ing in he ACL2 heo- em p o e , in: AISC’2000 (Fi h In e na ional Con e ence A i icial In elligence and Symbolic Com- pu a ion), Lec u e No es in Compu e Science, Vol. 1930 (Sp inge , Be lin, 2001) pp. 92–103. [18] N. Shanka , A mechanical p oo o he Chu ch–Rosse heo em, Jou nal o he ACM 35(3) (1988) 475–522. [19] G.L. S eele, Common Lisp he Language, 2nd ed. (Digi al P ess, 1990).