Formal Correctness of a Quadratic Unification Algorithm

Fo mal Co ec ness o a Quad a ic Uni ica ion Algo i hm Jos´e–Luis Ruiz–Reina, F ancisco–Jes´us Ma ´ın–Ma eos, Jos´e–An onio Alonso and Ma ´ıa–Jos´e Hidalgo Compu a ional Logic G oup Dep . o Compu e Science and A i icial In elligence, Uni e si y o Se ille E.T.S.I. In o m´a ica, A da. Reina Me cedes, s/n. 41012 Se illa, Spain E-mails: {j uiz, jesus,jalonso,mjoseh}@us.es Abs ac . We p esen a case s udy using ACL2 [5] o e i y a non- i ial algo i hm ha uses e icien da a s uc u es. The algo i hm ecei es as inpu wo i s -o de e ms and i e u ns a mos gene al uni ie o hese e ms i hey a e uni iable, ailu e o he wise. The e i ied implemen a ion s o es e ms as di ec ed acyclic g aphs by means o a poin e s uc u e. I s ime complexi y is O(n2) and i s space complexi y is O(n), and i can be execu ed in ACL2 a a speed compa able o a simila C implemen a ion. We epo he main issues encoun e ed o achie e his o mally e i ied implemen a ion. 1. In oduc ion I is gene ally accep ed ha he e is a ade-o be ween he e iciency o an implemen a ion and he simplici y o i s o mal co ec ness p oo : ha ing mo e sophis ica ed con ol and da a s uc u es inc eases he e o needed o p o e i s co ec ness. Tha is he eason why mos o he p oo s abou well-known algo i hms ha ha e been ca ied ou using heo em p o e s a e done easoning abou non-e icien nai e implemen a ions. Ne e heless, he ACL2 sys em [5] has al eady been demons a ed capable o e icien implemen a ions o mic oa chi ec u al le el p o- cesso models (see [4], o example) ha can be execu ed a C–like pe o mance. In his way, in addi ion o ha ing a high-speed simula ion model one has he addi ional bene i o being able o p o e o mal p ope ies o ha model. The co e o he implemen a ion is a “nex s a e” unc ion ha ecei es as inpu a da a s uc u e ep esen ing he cu en s a e o he machine and e u ns an upda ed machine s a e. A single- h eaded objec (s obj in he ollowing) is usually employed o ep esen he machine s a e. These da a s uc u es in ACL2 allow cons an ime access and des uc i e upda es, while main aining an applica i e seman ics o easoning abou i . In ligh o his, and gi en ou p e ious expe ience in he de elop- men o o mal heo ies ela ed o symbolic compu a ion sys ems [8], we decided o apply ACL2 o ob ain a o mally e i ied and e icien 2 implemen a ion o some non- i ial algo i hm in his a ea. Ou goal was wo old: compa e he execu ion e iciency ob ained in ACL2 wi h o he implemen a ions done in o he languages, and explo e he main issues encoun e ed du ing he e i ica ion e o o he co ec ness o ha implemen a ion. Fo his case s udy, we ha e chosen he implemen a ion o a syn ac ic uni ica ion algo i hm. The algo i hm ecei es as inpu wo i s -o de e ms and i e u ns a mos gene al uni ie o hese e ms i hey a e uni iable, ailu e o he wise. Uni ica ion algo i hms a e bo h heo e i- cally in e es ing and p ac ically impo an , since hey a e a he hea o many symbolic compu a ion sys ems [2]. The e i ied implemen a ion s o es e ms as di ec ed acyclic g aphs (dags in he ollowing) by means o a poin e s uc u e s o ed in an a ay ield o a s obj. In his way, we ob ain a ime complexi y o O(n2) and a space complexi y o O(n). We ollowed qui e closely a Pascal implemen a ion o he algo i hm desc ibed in Sec ion 4.8 o [1], which in u n is based on he exposi ion by Co bin and Bidoi [3]. I should be no ed ha we do no p o e he complexi y o ou implemen a ion in ACL2; a hand-p oo o his complexi y can be ound in [1]. The main ea u e o ou o mal p oo o he co ec ness o he algo i hm is a clea sepa a ion be ween he logic o he p ocess o uni ica ion, he da a s uc u es used, he speci ic execu ion con ol o he algo i hm and he de ails ela ed o i s execu ion in ACL2. To cope wi h he complexi y o he whole o mal p oo , we in oduce each o hese aspec s in successi e e inemen s eps. The desc ip ion p esen ed he e is guided and mo i a ed by hese s eps. This pape is a e ised e sion o [10], p esen ed a he ACL2 Wo k- shop 2004. We do no p esen he e de ails o he p oo s, and some o he unc ion de ini ions will be omi ed. We u ge he in e es ed eade o consul [11], whe e he comple e sou ce code o he de elopmen (wi h de ailed commen s) is a ailable. 2. An ACL2 O e iew We now gi e a b ie o e iew o he ACL2 sys em. ACL2 s ands o “A Compu a ional Logic o an Applica i e Common Lisp.” Roughly speaking, ACL2 is a p og amming language, a logic and a heo em p o e . I s p og amming language is an ex ension o an applica i e subse o Common Lisp [12] (we will assume he eade amilia wi h his language). The ACL2 logic desc ibes he p og amming language, wi h a o mal syn ax, axioms and ules o in e ence: he applica i e subse o Common Lisp is a model o he ACL2 logic. Finally, he 3 heo em p o e p o ides suppo o mechanized easoning in he logic. Thus, he sys em cons i u es an en i onmen in which p og ams can be de ined and execu ed, and hei p ope ies can be o mally speci ied and p o ed wi h he assis ance o a heo em p o e . The logic is a i s -o de logic wi h equali y. The syn ax o i s e ms is ha o Common Lisp and he e o e uses p e ix no a ion. Fo mulas a e quan i ie - ee and hei a iables a e conside ed o be uni e sally quan i ied. Fo example, he ollowing o mula may be ead as “ o all na u al numbe s nand x, wi h xe en and n > 0, xnis e en”: (de hm e enp-exp (implies (and (na p n) (> n 0) (na p x) (e enp x)) (e enp (exp x n))) The logic includes axioms o p oposi ional logic and o a numbe o p imi i e Common Lisp unc ions and da a ypes. Rules o in e ence include hose o p oposi ional calculus, equali y, ins an ia ion and a p inciple o p oo by induc 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 ACL2 heo em p o e is an in eg a ed sys em o ad hoc p oo echniques, including simpli ica ion and induc ion among hem. Sim- pli ica ion is a p ocess combining e m ew i ing wi h some decision p ocedu es (linea 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 ea u es in ACL2. 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 condi ional ew i ing ule). Fo example he abo e heo em e enp-exp , once p o ed, would allow he p o e o ew i e an ins ance o he e m (e enp (exp x n)) o he boolean cons an ( ue), p o ided ha he co esponding ins an ia ed condi ions o he ule can be es ablished. The heo em p o e is au oma ic in he sense ha , once de hm is submi ed, he use can no longe in e ac wi h he sys em. Howe e , in some sense, i is in e ac i e. O en, non- i ial esul s can no be p o ed on a i s a emp , and hen he ole o he use is impo an : she has o guide he p o e by a sui able collec ion o de ini ions and lemmas, used in subsequen p oo s as ew i ing ules. These lemmas a e sugges ed by a p econcei ed hand p oo (a a highe le el) o by inspec ion o ailed p oo s (a a lowe le el). This kind o in e ac ion 4 is called “The Me hod” by he au ho s o he sys em [5]. We ollowed “The Me hod” o ob ain he esul s p esen ed in his pape . A ele an ea u e o ACL2 is execu abili y: since i s axioms and ules o in e ence desc ibe a subse o Common Lisp, mos g ound exp essions in he logic a e di ec ly execu able in he hos Lisp (as opposed o deducing hei alues ia he axioms). Ne e heless, his simple ela ionship is complica ed by he ac ha no all Common Lisp unc ions a e de ined on all inpu s: he Common Lisp s anda d in oduces he no ion o “in ended domain” o a p imi i e unc ion. Ou side his in ended domain he beha io o a unc ion is no speci- ied. In con as , in he ACL2 logic unc ions a e o al: ha is, e e y applica ion o a unc ion de ined has a comple ely speci ied esul . ACL2 o malizes he no ion o in ended domain by means o gua ds. The gua d o a unc ion (p imi i e o de ined) is a o mula desc ibing i s in ended domain. Gua d e i ica ion is he p ocess o p o ing ha i a unc ion is called on an inpu sa is ying i s gua d, hen he e alua ion o his call will p oceed wi hou any gua d iola ion. Roughly speaking, he p oo obliga ions gene a ed by he gua d e i ica ion p ocess s a e ha he gua d o a unc ion implies he gua ds o i s de ini ion body. Gua ds ha e no e ec om he logical poin o iew, bu hey p o ide a means o ( o mally suppo ed) di ec execu ion in he hos Common Lisp, Fo mo e in o ma ion on ACL2, he bes e e ence is [5]. Fo a de ailed and upda ed desc ip ion o all he sys em de ails, we also ecommend isi ing he ACL2 home page [6] and he use ’s manual in i . 3. Syn ac ic Uni ica ion Le us ecall in his sec ion some basic concep s and esul s abou syn- ac ic uni ica ion o i s -o de e ms, ou a ge example. A comple e desc ip ion o he heo y o uni ica ion can be ound in [2]. An equa ion is an o de ed pai o i s -o de e ms, deno ed as 1≈ 2, and a sys em o equa ions is a ini e se o equa ions. A subs i u ion σis a solu ion o he equa ion 1≈ 2i σ( 1) = σ( 2). We say ha a subs i u ion is a solu ion o a sys em o equa ions Si i is a solu ion o e e y equa ion in S. We say ha he sys em is sol able i i has a solu ion. Usually, a sol able sys em has mo e han one solu ion, bu we will be in e es ed in mos gene al solu ions. Gi en wo subs i u ions σ and δ, we say ha σis mo e gene al han δi he e exis s a subs i u ion γsuch ha δ=γ◦σ, whe e ◦deno es unc ional composi ion. We say 5 ha a solu ion o Sis a mos gene al solu ion (mgs in he ollowing) i i is mo e gene al han any o he solu ion o S. As a pa icula case, we say ha wo e ms 1and 2a e uni iable i he e exis s a solu ion (called uni ie ) o he sys em { 1≈ 2}. A mos gene al uni ie (mgu in he sequel) o 1and 2is a mos gene al solu ion o ha sys em. Finally, a (syn ac ic) uni ica ion algo i hm is an algo i hm ha decides whe he wo gi en e ms a e uni iable, and in ha case i e u ns a mos gene al uni ie . In he li e a u e, i is qui e common o desc ibe syn ac ic uni ica ion algo i hms by means o he ela ion ⇒ugi en by he ans o ma ion ules p esen ed in Figu e 1. This se o ules is known as he Ma elli- Mon ana i ans o ma ion sys em. The ules ac on pai s o sys ems o equa ions o he o m S;U( he symbol ⊥ ep esen s uni ica ion ailu e). In ui i ely, he sys em Scan be seen as a se o equa ions o be sol ed, and he sys em Uas a (pa ially) compu ed uni ie . We call he pai S;Uauni ica ion p oblem. No e ha we a e iden i ying a sys em o equa ions o he o m {x1≈ 1,...,xn≈ n}, whe e he xi a e a iables, wi h he subs i u ion {x17→ 1,...,xn7→ n}. I none o he xiappea in any o he j, we say ha he sys em is in sol ed o m. No e ha e e y sys em in sol ed o m is an mgs o i sel . The in ui i e idea is ha , in o de o ind a mos gene al solu ion o a sys em o equa ions S, we can i e a i ely apply (in a “don’ ca e” nonde e minis ic manne ) he ules o ⇒u, s a ing wi h he uni ica ion p oblem S;∅, un il ei he a uni ica ion p oblem o he o m ∅;Uo ⊥is ob ained. I can be p o ed ha his p ocess mus e mina e and ha Sis sol able i and only i ⊥is no de i ed; in ha case Uis a mos gene al solu ion o S. No e ha he ans o ma ion ela ion ⇒udoes no desc ibe any con- c e e uni ica ion algo i hm. Roughly speaking, a uni ica ion algo i hm can be designed by using a da a s uc u e o ep esen i s -o de e ms and subs i u ions, and choosing a s a egy o apply he ules, s a ing wi h he pai o sys ems { 1≈ 2};∅(whe e 1and 2a e he wo gi en inpu e ms). This ans o ma ion based speci ica ion o he uni ica ion p ocess allows us o concen a e on i s logical p ope ies wi hou he bu den o da a s uc u es o con ol issues. 4. Fo maliza ion o he Uni ica ion T ans o ma ion Rela ion The i s s ep is o o malize in ACL2 he ans o ma ion ela ion ⇒u and p o e i s main p ope ies. I u ns ou ha hese p ope ies a e mo e easily p o ed i we conside a “na u al” ep esen a ion o i s - o de e ms and subs i u ions, e en hough his ep esen a ion may 6 Dele e: { ≈ } ∪ R;U⇒uR;U Occu -check: {x≈ } ∪ R;U⇒u⊥i x∈ V( ) and x6= Elimina e: {x≈ } ∪ R;U⇒uθ(R); {x≈ } ∪ θ(U) i x∈X,x /∈ V( ) and θ={x7→ } Decompose: { (s1, ..., sn)≈ ( 1, ..., n)} ∪ R;U⇒u {s1≈ 1, ..., sn≈ n} ∪ R;U Clash: { (s1, ..., sn)≈g( 1, ..., m)} ∪ R;U⇒u⊥ i n6=mo 6=g O ien : { ≈x} ∪ R;U⇒u{x≈ } ∪ R;Ui x∈X, /∈X Figu e 1. Ma elli–Mon ana i ans o ma ion sys em no be he mos e icien . In pa icula , in his i s s age e ms a e ep esen ed in p e ix no a ion, using lis s (excep a iables, which a e ep esen ed by a omic objec s). Fo example, he e m (x, g(y), h(x)) is ep esen ed by he lis ( x (g y) (h x)). Subs i u ions a e ep e- sen ed as associa ion lis s, and sys ems o equa ions as lis s o do ed pai s o e ms. A uni ica ion p oblem is a lis wi h wo elemen s: a sys em and a subs i u ion. The ailu e ⊥is ep esen ed as nil. In he sequel, his ep esen a ion o e ms and subs i u ions in p e ix o m, using lis s, will be e e ed o as p e ix ep esen a ion o p e ix no a ion. Le us now b ie ly desc ibe how we ha e o malized in ACL2 he ela ion ⇒u. No e ha one s ep o ans o ma ion o ⇒uis de e - mined by he ule applied and he equa ion whe e ha ule is applied. To o malize his in ui i e idea in ACL2, we de ine ⇒uby means o ope a o s. In his con ex , an ope a o is a do ed pai o he o m (name .i)whe e name is one o he ule names in Figu e 1 and i is a na u al numbe , co esponding o he i- h equa ion o he sys em. Thus, he ans o ma ion ⇒ucan be seen as applying one ope a o o a uni ica ion p oblem. No e e y ope a o can be applied o e e y uni ica ion p oblem, since ules ha e some condi ions ha ha e o be me . Fo example, he ope a o (elimina e . 5) can be applied o a uni ica ion p oblem only i i has a leas i e equa ions o be sol ed and i s i h equa ion is o he o m x≈ ,xbeing a a iable and no occu ing in . These conside a ions lead us o o malize in ACL2 he ela ion ⇒uby means o wo unc ions: −(uni -legal-p upl op), checking he condi ions equi ed o ap- ply a gi en ope a o op o a uni ica ion p oblem upl (in p e ix no a ion). −(uni - educe-one-s ep-p upl op), e u ning he ans o med uni ica ion p oblem (in p e ix no a ion) a e applying op o upl. 7 Wi h his ope a o -based ep esen a ion, we p o ed in ACL2 he main p ope ies o ⇒u: 1. The se o solu ions o a uni ica ion p oblem is p ese ed in each ans o ma ion s ep. 2. I he second sys em o a uni ica ion p oblem is in sol ed o m, hen he ans o med uni ica ion p oblem has i s second sys em in sol ed o m. 3. The ans o ma ion ela ion is e mina ing. Fo example, hese a e he ACL2 heo ems es ablishing p ope y 1 abo e: (de hm mm-p ese es-solu ions-1 (implies (and (uni -legal-p upl op) (solu ion sigma (bo h-sys ems upl))) (solu ion sigma (bo h-sys ems (uni - educe-one-s ep-p upl op))))) (de hm mm-p ese es-solu ions-2 (implies (and (uni -legal-p upl op) (uni - educe-one-s ep-p upl op) (solu ion sigma (bo h-sys ems (uni - educe-one-s ep-p upl op)))) (solu ion sigma (bo h-sys ems upl)))) (de hm mm-p ese es-solu ions-3 (implies (and (uni -legal-p upl op) (no (uni - educe-one-s ep-p upl op))) (no (solu ion sigma (bo h-sys ems upl))))) Ha ing p o ed he main p ope ies o one-s ep ans o ma ions, we can easily ex end hese p ope ies o ini e sequences o ans o ma- ions1. In pa icula we p o e ha gi en wo e ms 1and 2and a subs i u ion σ, i { 1≈ 2};∅∗ ⇒u∅;σ, hen σis an mgu o 1and 2, and i { 1≈ 2};∅∗ ⇒u⊥, hen 1and 2a e no uni iable. This esul is he key o p o e he co ec ness o a gi en uni ica ion algo i hm: i su ices o show ha he esul s compu ed by he algo i hm can be desc ibed by he i e a i e applica ion o a sequence o ope a o s (al hough he algo i hm does no necessa ily ha e o deal explic ly wi h ope a o s). Mos o he esul s abou he ela ion ⇒uha e been eused om a p e ious o maliza ion o he main p ope ies o he la ice o i s -o de 1No e ha in ou o maliza ion, a sequence o ans o ma ions can be iden i ied wi h a lis o ope a o s. Each o hese ope a o s has o be applicable o he esul ob ained by he p e ious one. 8 e ms wi h espec o subsump ion [9]. As pa o ha wo k, we had de ined and e i ied a uni ica ion algo i hm based on he ans o ma ion sys em ⇒uac ing on e ms in p e ix no a ion. Fo a de ailed desc ip ion o he p oo s and a p ecise s a emen o he p ope ies men ioned abo e, we e e he eade o he suppo ing ma e ials. 5. Rep esen ing Te ms as Di ec ed Acyclic G aphs Using he p e ix ep esen a ion, a uni ica ion algo i hm may ha e expo- nen ial complexi y in some si ua ions, bo h in ime and space. Conside , o example, he ollowing s anda d pa ame e ized uni ica ion p oblem, which we will call Un: p(xn,...,x2, x1)≈p( (xn−1, xn−1),..., (x1, x1), (x0, x0)) An mgu o his p oblem is {x17→ (x0, x0), x27→ ( (x0, x0), (x0, x0)),...} mapping each a iable xi o a comple e bina y ee o heigh i. This mgu is ob ained by epea edly applying he Elimina e ule o ⇒u. Using he p e ix ep esen a ion o e ms, i would be necessa y o econs uc he ins an ia ed sys ems o equa ions, o each applica ion o he ule. The s anda d app oach o deal wi h his p oblem is o use e m dags, a kind o poin e s uc u es ep esen ing e ms whe e a iables can be sha ed. Fo example, he g aph below ep esen s he equa ion (x, g( , h(x)), h(y)) ≈ (h(u), g(y, ), z). Nodes a e labeled wi h unc- ion and a iable symbols, and ou going edges connec e e y node wi h dags ep esen ing i s immedia e sub e ms. We can na u ally iden i y he oo node o a e m dag wi h he whole e m. No e also ha he e is a ce ain amoun o s uc u e sha ing, a leas o he epea ed a iables: g x hy h h gz u 9 To implemen a uni ica ion algo i hm wi h his e m ep esen a ion, he main idea is ne e o build new e ms bu only c ea e poin e s. In pa icula , he Elimina e ule can be implemen ed in oducing a poin e linking he a iable wi h he e m o which his a iable is bound; in ha way no econs uc ion o he e m is equi ed in he applica ion o a subs i u ion. In he g aph abo e, hese poin - e s a e ep esen ed by dashed a ows. The binding o a a iable can be de e mined by ollowing he poin e s a e sing he g aph dep h i s , om le o igh . In his case, he subs i u ion ep esen ed is {x7→ h(u), y 7→ h(h(u)), z 7→ h(h(h(u))), 7→ h(h(u))}, which is an mgu o (x, g( , h(x)), h(y)) and (h(u), g(y, ), z). In ACL2, we ha e ep esen ed a e m dag as a lis o nodes. In pa icula , i gis a lis ep esen ing a e m dag, each o i s elemen s ep esen s a node in he g aph, uniquely iden i ied by i s posi ion index. The nodes s o e in o ma ion abou i s label and i s successo s, in he ollowing way: −I node i ep esen s an unbound a iable x, hen (n h ig) ( ha is, he i- h elemen o g) is a do ed pai o he o m (x. )2. −I node i ep esen s a bound a iable, hen (n h ig) is an index npoin ing o he oo node o he e m o which he a iable is bound. −I node iis he oo node o a non- a iable e m ( 1, . . . , n), hen (n h ig) is a do ed pai o he o m ( .l), whe e lis he lis o he indices co esponding o he oo nodes o 1, . . . , n. Fo example, we can ep esen he e m equ( (x, g( , h(x)), h(y)), (h(u), g(y, ), z)) by a lis wi h he ollowing elemen s ( o a be e unde s anding, we ma ked each elemen wi h i s posi ion index): 0 8 9 (Y . T) (EQU . (1 9)) (F . (2 3 7)) 1 2 (X . T) 3 (G . (4 5)) 4 (V . T) 5 (H . (6)) 6 2 7 (H . (8)) (F . (10 12 15)) (H . (11)) 10 1211 (U . T) 13 (G . (13 14)) 14 8 4 15 (Z . T) Al hough wi h he abo e con en ions one can ep esen e e y i s - o de e m as a lis o nodes, he con e se is no ue. Thus, we need 2We could ha e used any non-lis alue as he second elemen in his do ed pai o dis inghish i om he ep esen a ion o non- a iable e ms. 16 (de un uni -legal-q-iden i y (i j g) (and (na p i) (< i (len g)) ( e m-dag-non- a iable-p i g) (na p j) (< j (len g)) ( e m-dag-non- a iable-p j g) (no (equal i j)) (equal (dag-as- e m i g) (dag-as- e m j g)))) (de un uni - educe-one-s ep-q-iden i y (i j S sol g) (lis S sol (upda e-n h i j g))) The unc ions uni -legal-q and uni - educe-one-s ep-q de ine he ex ended ans o ma ion ela ion. No e ha his ex ended ela ion is de ined on a e m dag ep esen a ion and includes all he ans o - ma ion ules o ⇒uas well as iden i ica ions: (de un uni -legal-q (upl op) (i (equal ( i s op) ’iden i y) (uni -legal-q-iden i y (second op) ( hi d op) ( hi d upl)) (uni -legal-d upl op))) (de un uni - educe-one-s ep-q (upl op) (i (equal ( i s op) ’iden i y) (uni - educe-one-s ep-q-iden i y (second op) ( hi d op) ( i s upl) (second upl) ( hi d upl)) (uni - educe-one-s ep-d upl op))) The ollowing heo ems es ablish he main p ope ies o his ex- ended ans o ma ion ela ion: (de hm uni - educe-one-s ep-q-p ese es-well- o med-upl (implies (and (well- o med-upl upl) (uni -legal-q upl op)) (well- o med-upl (uni - educe-one-s ep-q upl op)))) (de hm uni - educe-one-s ep-q- o -iden i ica ions (implies (and (well- o med-upl upl) (uni -legal-q upl op) (equal ( i s op) ’iden i y)) (equal (upl-as-pai -o -sys ems (uni - educe-one-s ep-q upl op)) (upl-as-pai -o -sys ems upl)))) Tha is: −Well- o medness o he dag uni ica ion p oblem is p ese ed. No e again ha his esul is no i ial: i means ha upda ing a node by a legal iden i ica ion do no c ea e cycles in he g aph. −An iden i ica ion does no change he uni ica ion p oblem in p e- ix o m ep esen ed by he dag uni ica ion p oblem. Tha is, no “ha m” is done by iden i ica ions, om he poin o iew o he uni ica ion p oblem. 17 F om hese heo ems and he esul s o he p e ious sec ion, i is no di icul o p o e ha o e e y sequence o hese ans o ma ion s eps (including iden i ica ions) pe o med a he dag le el, he e exis s a sequence o ans o ma ion s eps o ⇒upe o med a he co esponding p e ix ep esen a ion. The e o e, e e y algo i hm whose compu a ion can be desc ibed as he i e a i e applica ion o hese ules on dag uni ica ion p oblems is a co ec uni ica ion algo i hm. 8. An Imp o ed Occu Check Be o e de ining he quad a ic uni ica ion algo i hm in he nex sec ion, we mus ix ano he echnical de ail ha could cause exponen ial be- ha io . Assume ha a some poin o he uni ica ion p ocess, a a iable is bound o a e m o exponen ial size, bu his e m is s o ed in he e m dag in linea size because i s sub e ms a e sha ed. I we ha e o check he occu ence o a a iable in his e m, we should a oid isi ing hese sha ed subg aphs epea edly. This exponen ial beha io may appea wi h he nai e implemen a- ion o occu check de ined by he unc ion occu -check-d gi en in Sec ion 5: we do no ake ca e o epea ed isi s o he same subg aph. To op imize his implemen a ion, we ollow he idea gi en in [1]. We will use a s amp lis o in ege s: he numbe in posi ion io his lis ep esen s he las ime node io he e m dag was isi ed o occu check. We also use a ime coun e ha will be inc emen ed e e y ime he uni ica ion p ocedu e calls o he occu check unc ion. Be o e isi ing a subg aph o check he occu ence o a a iable, we check i i s s amp in o ma ion is equal o ime. I ha is he case we simply e u n nil, wi hou a e sing he subg aph; o he wise we a e se he subg aph, upda ing he s amp in o ma ion i he a iable does no occu in he subg aph. The de ini ion below implemen s in ACL2 his imp o ed occu check. No e ha i e u ns a lis o wo elemen s: he i s is a boolean indica ing occu ence and he second is he (possibly modi ied) s amp lis . (de un occu -check-q ( lg x h g s amp ime) (i (dag-p g) (i lg (le ((p (n h h g))) (i (in ege p p) (occu -check-q lg x p g s amp ime) (le ((a gs (cd p))) (cond ((equal a gs ) (lis (equal x h) s amp)) ((equal (n h h s amp) ime) (lis nil s amp)) ( (le * ((bool-s amp 18 (occu -check-q nil x a gs g s amp ime)) (bool ( i s bool-s amp)) (s amp (second bool-s amp))) (i bool bool-s amp (lis nil (upda e-n h h ime s amp))))))))) (i (endp h) (lis nil s amp) (le * ((bool-s amp (occu -check-q x (ca h) g s amp ime)) (bool ( i s bool-s amp)) (s amp (second bool-s amp))) (i bool bool-s amp (occu -check-q nil x (cd h) g s amp ime))))) (lis ’unde s amp))) The ollowing heo em es ablishes ha he esul compu ed by he imp o ed unc ion occu -check-q is consis en wi h he esul com- pu ed by he unc ion occu -check-d. (de hm occu -check-d-occu -check-q (implies (occu -check-in a ian x h g s amp ime) (equal ( i s (occu -check-q x h g s amp ime)) (occu -check-d x h g)))) The unc ion occu -check-in a ian in his heo em desc ibes an in a ian condi ion ha we will p o e ha is me in e e y s ep o ou implemen ed uni ica ion algo i hm. Roughly speaking, all he numbe s in he s amp lis ha e o be s ic ly smalle han he ime coun e . 9. A Quad a ic Uni ica ion Algo i hm I is ime o de ine ou implemen a ion o a quad a ic uni ica ion algo- i hm. Tha is, ha ing p o ed he main p ope ies o he ule-based speci ica ion o he uni ica ion p ocess on e m dags, we deal wi h con ol issues. No su p isingly, we simply choose a ce ain s a egy o apply he ules o he ex ended ans o ma ion ela ion: in ou case, we always selec he i s equa ion o be sol ed. To a oid exponen ial complexi y, we need some echnical de ails in o de o do iden i ica- ions p ope ly and also we use he imp o ed occu check de ined in he p e ious sec ion. The unc ion dag- ans o m-mm-q de ines he indi idual s eps o ans o ma ion pe o med by he algo i hm. This is he main compo- nen o he algo i hm. Roughly speaking, he implemen ed algo i hm will apply his unc ion un il he e a e no equa ions o be sol ed o ailu e is de ec ed. 19 (de un dag- ans o m-mm-q (ex -upl) (le * ((ex -S ( i s ex -upl)) (equ ( i s ex -S)) (R ( es ex -S)) (U (second ex -upl)) (g ( hi d ex -upl)) (s amp ( ou h ex -upl)) ( ime ( i h ex -upl))) (i (equal ( i s equ) ’id) (le ((g (upda e-n h (second equ) ( hi d equ) g))) ;;; IDENTIFY (lis R U g s amp ime)) (le (( 1 (dag-de e (ca equ) g)) ( 2 (dag-de e (cd equ) g))) (i (equal 1 2) (lis R U g s amp ime) ;;; DELETE (le ((p1 (n h 1 g)) (p2 (n h 2 g))) (cond ((dag- a iable-p p1) (le * ((bool-s amp (occu -check-q 1 2 g s amp ime)) (bool ( i s bool-s amp)) (s amp (second bool-s amp))) (i bool nil ;;; OCCUR-CHECK (le ((g (upda e-n h 1 2 g))) (lis R (cons (cons (dag-symbol p1) 2) U) g s amp (1+ ime)))))) ;;; ELIMINATE ((dag- a iable-p p2) (lis (cons (cons 2 1) R) U g s amp ime)) ;;; ORIENT ((no (equal (dag-symbol p1) (dag-symbol p2))) nil) ;;; CLASH1 ( (le * ((pai s-bool (pai -a gs (dag-a gs p1) (dag-a gs p2))) (pai s ( i s pai s-bool)) (bool (second pai s-bool))) (i bool (lis (append pai s (cons (lis ’id 1 2) R)) U g s amp ime) ;;; DECOMPOSE nil)))))))))) ;;; CLASH2 This unc ion ecei es as inpu wha we call an ex ended uni ica ion p oblem. An ex ended uni ica ion p oblem is a lis wi h i e elemen s: an ex ended indices sys em, an indices subs i u ion, a e m dag, a s amp lis and a ime coun e . An ex ended indices sys em is an indices sys em ha could include also some iden i ica ion ma ks o he o m (id i j). In his unc ion, he ans o ma ion s ep o apply is de e mined by he i s elemen o he ex ended indices sys em. I his i s elemen is an o dina y equa ion be ween indices, hen he co esponding ule o ⇒uis applied. I i is an iden i ica ion ma k o he o m (id i j), hen an iden i ica ion o he nodes iand jis applied. In o de o gua an ee ha iden i ica ions a e always done wi h oo nodes o al eady uni ied sub e ms, iden i ica ion ma ks a e included a e e y applica ion o he 20 Decompose ule, jus a e he equa ions pai ing4 he a gumen s o he nodes o be uni ied. In his way, ex ended indices sys ems can be seen as a s ack: when an iden i ica ion ma k is a he op o he s ack, we a e su e ha he nodes o be iden i ied ha e success ully been uni ied. The unc ion dag- ans o m-mm-q has o be i e a i ely applied un il he sys em o equa ions o be sol ed is emp y o un il nil (un- sol abili y) is ob ained. The ollowing unc ion sol e-upl-q does his job: (de un no mal- o m-sys (ex -upl) (no (and (consp ex -upl) (consp ( i s ex -upl))))) (de un sol e-upl-q (ex -upl) (decla e (xa gs :measu e (uni ica ion-measu e-q ex -upl))) (i (uni ica ion-in a ian -q ex -upl) (i (no mal- o m-sys ex -upl) ex -upl (sol e-upl-q (dag- ans o m-mm-q ex -upl))) ’unde )) The condi ion (uni ica ion-in a ian -q ex -upl) in he abo e de ini ion is needed o e mina ion. Among many o he p ope ies, i includes he dag-p condi ion. Te mina ion o sol e-upl-q is no i ial a all, and a lexicog aphic measu e has o be supplied o in- s uc he p o e in he e mina ion p oo . This measu e (gi en by he unc ion uni ica ion-measu e-q, omi ed he e) is mainly based on he measu e ha jus i ies he e mina ion o ⇒u. In addi ion, he unc ion uni ica ion-in a ian -q de ines he p ope ies needed o ensu e ha he unc ion dag- ans o m-mm-q is applying a legal ans o ma ion s ep o he ex ended ans o ma ion e- la ion5. No e ha his is i ial o he case o non-iden i ica ion ans- o ma ions, because he applicabili y condi ions a e explici ly checked. Ne e heless, ha is no he case o iden i ica ions. Recall ha an iden i ica ion can be applied only when he e ms poin ed by he iden- i ied nodes a e equal. Bu his applicabili y condi ion is no checked (and ha is essen ial o he e iciency o he algo i hm). The key poin is ha , due o he way he successi e ans o ma ion s eps a e ca ied ou , i is gua an eed ha e e y ime an iden i ica ion s ep is pe o med, his iden i ica ion is legal. In o he wo ds, he e is some “well- o medness” condi ions on he ex ended uni ica ion p oblem ha can be seen as an in a ian o he uni ica ion p ocess, and his in a ian condi ion implies ha e e y ans o ma ion s ep pe o med 4Gi en wo lis s (l1. . . ln)and (m1. . . mk) he auxilia y unc ion pai -a gs e u ns he lis (((l1.m1)... (ln.mk)) ) i n=k,(nil nil) o he wise. 5And also ha we can sa ely use he imp o ed occu check unc ion. 21 by dag- ans o m-mm-q is a legal ans o ma ion s ep wi h espec o he ex ended ans o ma ion ela ion de ined in Sec ion 7. The ollowing heo ems es ablish his ac 6: (de hm uni ica ion-in a ian -q-p ese ed (implies (and (no (no mal- o m-sys ex -upl)) (uni ica ion-in a ian -q ex -upl)) (uni ica ion-in a ian -q (dag- ans o m-mm-q ex -upl)))) (de hm ans o m-mm-q-applies-a-legal-ope a o (implies (and (no (no mal- o m-sys ex -upl)) (uni ica ion-in a ian -q ex -upl)) (uni -legal-q (ex -upl- o-upl ex -upl) (dag- ans o m-mm-q-op ex -upl)))) (de hm ans o m-mm-q-applies-an-ope a o (implies (uni ica ion-in a ian -q ex -upl) (equal (ex -upl- o-upl (dag- ans o m-mm-q ex -upl)) (uni - educe-one-s ep-q (ex -upl- o-upl ex -upl) (dag- ans o m-mm-q-op ex -upl))))) We sa e he eade om he de ini ion o he unc ion uni ica- ion-in a ian -q. I is a e y long de ini ion (mo e han 300 lines o code) including well- o medness p ope ies such as acyclici y o he e m dag, he occu -check in a ian and he co ec placemen o he iden i ica ion ma ks in he ex ended indices sys em s ack. Due o his, he abo e heo em uni ica ion-in a ian -q-p ese ed u ns ou o be he mos di icul o p o e o all he e i ica ion e o . In he abo e heo ems, he unc ion dag- ans o m-mm-q-op e- u ns he co esponding “wi ness” ope a o jus i ying ha dag- ans- o m-mm-q is applying a ule o he ex ended ans o ma ion ela ion. This means ha he exhaus i e i e a ion o dag- ans o m-mm-q, as implemen ed by sol e-upl-q, is a co ec uni ica ion p ocedu e. Thus, we a e almos done. Bu be o e we need o deal wi h some echnical issues ela ed o he execu ion o he algo i hm in ACL2. 10. Execu ion o he Algo i hm in ACL2 The unc ion sol e-upl-q in he p e ious sec ion can be execu ed in ACL2. Bu om he p ac ical poin o iew, his execu ion is comple ely un easible, mainly o wo easons: 6The unc ion ex -upl- o-upl emo es he iden i ica ion ma ks, he s amp lis and he ime coun e o an ex ended dag uni ica ion p oblem. 22 −The e m dag is s o ed in a lis . This means ha accessing (wi h n h) and upda ing (wi h upda e-n h) he in o ma ion o he nodes a e no done in cons an ime. Mo eo e , upda es a e no des uc- i e and need copying. −As we ha e seen, some o he ecu si e unc ions implemen ed ha e expensi e well- o medness condi ions (like dag-p o uni ica- ion-in a ian -q) in hei bodies, needed o e mina ion. And hese condi ions would be e alua ed in e e y ecu si e call. Fo una ely, we can ix hese wo p oblems. To deal wi h he i s , we will use a single- h eaded objec . In ACL2, i is possible o decla e some objec s in he language as single- h eaded (s objs) and pe o m des uc- i e upda es on hem. When an objec is decla ed o be single- h eaded, ACL2 en o ces ce ain syn ac ic es ic ions on i s use, ensu ing ha in e e y momen , only one copy o he objec is needed. Wi h hese es ic ions, he des uc i e upda es a e consis en wi h he applica i e unc ional seman ics o ACL2. Using s objs we can combine e icien impe a i e implemen a ions wi h he seman ic o unc ional languages o eason abou hem. The ollowing c ea es a s obj called e ms-dag wi h wo esizable a ay ields o s o e he e m dag and he s amp: (de s obj e ms-dag (dag : ype (a ay (0)) : esizable ) (s amp : ype (a ay in ege (0)) :ini ially -1 : esizable )) The e ec o his ACL2 o m is o in oduce he s obj e ms-dag and i s associa ed ecognize s, c ea o , accesso s, upda e s, and leng h and esize unc ions o he a ay ields. In pa icula , gi en an in- dex i, he exp essions (dagi i e ms-dag) and (upda e-dagi i e ms-dag) espec i ely access and upda e (wi h alue ) he i- h cell o he dag a ay. Simila ly, unc ions s ampi and upda e-s ampi a e in oduced. These ope a ions a e execu ed in cons an ime and he upda e is des uc i e (a he p ice o syn ac ic es ic ions on he use o e ms-dag). Now, we edo all he de ini ions o he implemen ed algo i hm, ak- ing in o accoun ha he e m dag is s o ed in his s obj. I is wo h poin ing ou ha he syn ac ic equi emen s needed o ensu e he single- h eadedness o he ACL2 unc ions ha use s objs a e na u ally me in his algo i hm. The unc ion dag- ans o m-mm-s below is he s obj coun e pa o dag- ans o m-mm-q. The key poin is ha om he logical poin o iew, he dag and s amp a ays o he s obj a e lis s. Thus i is s aigh o wa d o ansla e he al eady p o ed p ope ies abou he lis e sion o he algo i hm o he s obj e sion. 23 (de un dag- ans o m-mm-s (S U e ms-dag ime) (decla e (xa gs :s objs e ms-dag) ...) (le * ((equ (ca S)) (R (cd S))) (i (equal (ca equ) ’id) ;;; IDENTIFY (le (( e ms-dag (upda e-dagi (second equ) ( hi d equ) e ms-dag))) (m R U e ms-dag ime)) (le * (( 1 (dag-de e -s (ca equ) e ms-dag)) ( 2 (dag-de e -s (cd equ) e ms-dag)) (p1 (dagi 1 e ms-dag)) (p2 (dagi 2 e ms-dag))) (cond ((= 1 2) (m R U e ms-dag ime)) ;;; DELETE ((dag- a iable-p p1) (m -le (oc e ms-dag) (occu -check-s 1 2 e ms-dag ime) (i oc ;;; OCCUR-CHECK (m nil nil nil e ms-dag nil) (le (( e ms-dag (upda e-dagi 1 2 e ms-dag))) (m R (cons (cons (dag-symbol p1) 2) U) e ms-dag (1+ ime)))))) ;;; ELIMINATE ((dag- a iable-p p2) (m (cons (cons 2 1) R) U e ms-dag ime)) ;;; ORIENT ((no (eql (dag-symbol p1) (dag-symbol p2))) (m nil nil nil e ms-dag nil)) ;;; CLASH1 ( (m -le (pai s bool) (pai -a gs-m (dag-a gs p1) (dag-a gs p2)) (i bool (m (append pai s (cons (lis ’id 1 2) R)) U e ms-dag ime) ;;; DECOMPOSE (m nil nil nil e ms-dag nil))))))))))) ;;; CLASH2 Ano he op imiza ion o execu ion ha is wo h poin ing ou is he use o mul i alues in unc ions ha e u ned se e al alues in a lis , such as occu -check-q o pai -a gs. In he s obj e sion o he algo i hm, we used m and m -le o handle his (see [6] o de ails on mul i alues). Again, he e is no di e ence om he logical poin o iew, since acco ding o he logic, m e u ns a lis . Ne e heless, a lis is ne e c ea ed o s o ing mul iple e u n alues du ing execu ion, making i mo e e icien . Le us now deal wi h he second p oblem, o how o ge id o he expensi e well- o medness condi ions in he bodies o some o he ecu - si e unc ions o ou implemen a ion. These condi ions a e only needed o he logical de ini ions: hey can be sa ely emo ed in execu ion because hey a e p ese ed in each ecu si e call. Fo ha pu pose, we use de exec and mbe: his ACL2 ea u e allows us o associa e an “execu able body” wi h a (possibly di e en ) “logical body”. This associa ion will be allowed by he sys em a e p o ing ha on he 24 in ended domain o he unc ion he execu able body and he logical body a e equal. Le us explain his in mo e de ail. In he logic, he exp ession (mbe :logic logic body :exec exec body)is equal o logic body; he alue o exec body is igno ed. Ne e heless, o execu ion in he hos Lisp his o m mac oexpands simply o exec body. The gua d e i ica ion mechanism plays a key ole he e. Roughly speaking, he gua d p oo obliga ions gene a ed by he abo e call o mbe a e (equal logic body exec body)along wi h hose gene a ed by he execu able body. The e- o e, whene e a unc ion de ined using mbe is called on an inpu sa is- ying i s gua d, hen exec body may be sa ely used in he hos Common Lisp o ob ain a esul , since i is p o ably equal in he ACL2 logic o logic body. In addi ion, de exec gene a es a p oo obliga ion ensu ing ha he execu able body e mina es on i s in ended domain. Fo example, he ollowing is he comple e de ini ion o he unc- ion sol e-upl-s , he s obj coun e pa o he unc ion sol e-upl-q de ined in he p e ious sec ion7. No e ha he expensi e uni ica ion- -in a ian -q condi ion is emo ed in he execu able body. (de exec sol e-upl-s (S U e ms-dag ime) (decla e (xa gs :s objs e ms-dag :gua d (and ( ue-lis p S) (uni ica ion-in a ian -q (lis S U (dag-componen -s e ms-dag) (s amp-componen -s e ms-dag) ime))) ...)) (mbe :logic (i (uni ica ion-in a ian -q (lis S U (dag-componen -s e ms-dag) (s amp-componen -s e ms-dag) ime)) (i (endp S) (m S U e ms-dag ime) (m -le (S1 U1 bool e ms-dag ime1) (dag- ans o m-mm-s S U e ms-dag ime) (i bool (sol e-upl-s S1 U1 e ms-dag ime1) (m S U nil e ms-dag ime)))) (m S U nil e ms-dag ime)) :exec (i (endp S) (m S U e ms-dag ime) (m -le (S1 U1 bool e ms-dag ime1) (dag- ans o m-mm-s S U e ms-dag ime) 7The unc ions dag-componen -s and s amp-componen -s collec s in a lis he con en s o he dag and s amp a ays o he s obj. 25 (i bool (sol e-upl-s S1 U1 e ms-dag ime1) (m S U nil e ms-dag ime)))))) The gua d e i ica ion o his unc ion is no i ial. We ha e o p o e ha he p ope y uni ica ion-in a ian -q is p ese ed in e e y ecu si e call. Bu essen ially, ha is he heo em uni ica ion- -in a ian -q-p ese ed discussed in he p e ious sec ion. In gene al, we used de exec and mbe in he de ini ion o all he ecu si e unc ions ha need well- o medness condi ions in hei logical bodies whene e hese condi ions can be sa ely emo ed o execu ion. In pa icula , in de e e encing, in occu checking and in he unc ion ha builds a e m in p e ix o m om he con en s o a e m dag. Finally, he op le el unc ion o ou implemen ed algo i hm is called dag-mgu. This unc ion ecei es as inpu wo e ms 1 and 2 in p e- ix no a ion and compu es i s mos gene al uni ie (o ailu e) in he ollowing way (see he suppo ing ma e ials o he de ini ions): 1. I c ea es e ms-dag as a local s obj, esizing he dag and s amp a ays acco ding o he sizes o 1 and 2. 2. I s o es bo h e ms in he dag a ay, as di ec ed acyclic g aphs, building an ini ial dag uni ica ion p oblem. 3. Applies he unc ion sol e-upl-s o he ini ial uni ica ion p ob- lem. 4. I ailu e is de ec ed, i e u ns (m nil nil); o he wise, i e- u ns (m σ), whe e σis he mos gene al uni ie (in p e ix no a ion) ob ained om he inal indices subs i u ion compu ed by sol e-upl-s . I is wo h poin ing ou ha he inpu and ou pu o his op le el unc ion a e in p e ix no a ion, al hough he main p ocess o he algo i hm is pe o med wi h he dag ep esen a ion. The gua d o he unc ion dag-mgu is qui e simple, and only checks ha he wo inpu e ms a e in p e ix o m. In con as , he gua ds o he in e - media e unc ions a e qui e complica ed and expensi e, including he well- o medness condi ions and in a ian s desc ibed in he p eceding sec ions. Bu since gua ds a e e i ied hese in e media e gua ds a e ne e e alua ed. The ollowing h ee heo ems es ablish he co ec ness o he imple- men ed uni ica ion algo i hm, showing ha i compu es a mos gene al uni ie o wo gi en e ms, whene e hey a e uni iable, and ailu e o he wise: