ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System

ACL2 Ve i ica ion o Simplicial Degene acy P og ams in he Kenzo Sys em F ancisco-Jesus Ma ´ın-Ma eos1, Julio Rubio2, and Jose-Luis Ruiz-Reina1 1Compu a ional Logic G oup Dep . o Compu e Science and A ificial 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 { jesus,j uiz}@us.es 2Dep . o Ma hema ics and Compu a ion, Uni e si y o La Rioja Edificio Vi es, Luis de Ulloa s/n. 26004 Log o˜no, Spain [email p o ec ed] Abs ac . Kenzo is a Compu e Algeb a sys em de o ed o Algeb aic Topology, and w i en in he Common Lisp p og amming language. I is a descendan o a p e ious sys em called EAT ( o Effec i e Algeb aic Topology). Kenzo shows a much be e pe o mance han EAT due, among o he easons, o a sma encoding o degene acy lis s as in ege s. In his pape , we gi e a comple e au oma ed p oo o he co ec ness o his encoding used in Kenzo. The p oo is ca ied ou using ACL2, a sys- em o p o ing p ope ies o p og ams w i en in (a subse o ) Common Lisp. The mos in e es ing idea, om a me hodological poin o iew, is ou use o EAT o build a model on which he e ifica ion is ca ied ou . Thus, EAT, which is logically simple bu less efficien han Kenzo, ac s as a ma hema ical model and hen Kenzo is o mally e ified agains i . 1 In oduc ion The Kenzo sys em [8] is a Common Lisp p og am, de eloped by F. Se ge ae and de o ed o Algeb aic Topology. I was w i en mainly as a esea ch ool and has go ele an esul s which ha e no been confi med no e u ed by any o he means. Being a compac p og am (a ound 16000 lines o Common Lisp, implemen ing complica ed algo i hms), he ques ion o Kenzo eliabili y (beyond es ing) came up in a na u al way. Se e al app oaches based on Fo mal Me hods ha e been used o unde ake his p oblem, anging om he Algeb aic Specifica ion o i s da a s uc u es ([12], [7], and ecen ly compu e aided wi h Coq [6]) o he applica ion o P oo Assis an s o s udy he co ec ness o algo i hms implemen ed in Kenzo. In his second line, he mos impo an con ibu ions ha e been he Isabelle/HOL p oo o he Basic Pe u ba ion Lemma [3] and he p ojec by Coquand and Spiwack which is based on Cons uc i e Type Theo y and Coq [5]. As i is well-know, Coq This wo k has been suppo ed by Minis e io de Educaci´on y Ciencia, p ojec MTM2006-06513. p oo s ca y hei co esponding p og ams, and also some wo k has been done o p oduce unning code om Isabelle/HOL p oo s in his con ex [4]. Ne e heless, he ex ac ed p og ams a e no compa able wi h he eal Kenzo sys em, bo h om he efficiency and he p og amming languages poin s o iew (OCaML o ML code ins ead o Common Lisp). Due o his d awback o he app oaches based on Isabelle and Coq, a new esea ch line was launched, ocused on he ACL2 heo em p o e . ACL2 is o ien- ed o p o e p ope ies o Common Lisp p og ams, and hus i could seem, a fi s sigh , e y p omising o e i y Kenzo. Ne e heless, since he ACL2 logic is fi s -o de , he ull e ifica ion o Kenzo is no possible, since i uses in ensi ely highe o de unc ional p og amming ( o encode, in pa icula , opological spaces o infini e dimension). This obse a ion, howe e , does no close he possibili y o e i ying fi s o de agmen s o Kenzo wi h ACL2. Some p elimina y wo ks in his line ha e been published in [1] and [2]. I is wo h no ing ha in hose pape s we unde ake he p oblem o e i ying some Common Lisp p og ams abou simplicial opology (in pa icula , algeb aic manipula ion and simplicial p ope ies o Kenzo algo i hms), bu ha no ac ual Kenzo agmen was s udied. In his pape we p esen o he fi s ime he e ifica ion o a Kenzo agmen wi hin he ACL2 heo em p o e . The e ified agmen is small in numbe o lines, bu i is cen al o he efficiency go by Kenzo. This is compa ed o he p e- decesso o Kenzo, ano he Common Lisp sys em called EAT [15], based on he same Se ge ae ’s ideas, bu whose pe o mance was much poo e han ha o Kenzo. One o he easons why Kenzo pe o ms be e han EAT is because o a sma encoding o degene acy lis s. These combina o ial objec s a e usually p e- sen ed in he Simplicial Topology li e a u e as dec easing lis s o na u al num- be s, and so hey we e encoded in EAT. On he con a y, in Kenzo degene acy lis s a e encoded as na u al numbe s. Since o gene a e and compose degene acy lis s a e ope a ions which appea in an exponen ial manne in mos Kenzo calcu- la ions ( h ough he Eilenbe g-Zilbe heo em [14]), i is clea ha he benefi s o ha ing a be e way o s o ing and p ocessing degene acy lis s is e y impo an . Bu , on he nega i e side, he algo i hms a e somehow obscu ed in Kenzo, wi h espec o he clean and comp ehensible app oach in EAT. The e o e, o p o e he co ec ness o he implemen a ion o degene acy algo i hms in Kenzo seems o be a good es -bed o apply compu e -aided o mal me hods. A comple e ACL2 p oo o he co ec ness o he degene acy p og ams in Kenzo is desc ibed in his pape . The main me hodological con ibu ion o he p oo is, in ou opinion, using EAT o build a model wi h espec o he e i- fica ion is ca ied ou . Thus, EAT, which is logically simple (i.e., easie o be e ified) bu less efficien han Kenzo, ac s as a ma hema ical model and hen Kenzo is o mally e ified agains i . The o ganiza ion o he es o he pape is as ollows. In Sec ion 2, we in- oduce b iefly bo h Simplicial Topology and he ole o degene acy ope a o s in i . In Sec ion 3, we gi e a b ie in oduc ion o he ACL2 sys em. E en i a fi s o de agmen o Kenzo (and EAT) has been chosen, he Kenzo unc ions canno be di ec ly defined in ACL2 (due o Common Lisp ea u es, like loops o des uc i e upda es, which a e no a ailable in ACL2). Thus, in Sec ion 4 we explain how o ob ain ac ual ACL2 unc ions om Kenzo and EAT degene acy p og ams, in a sa e and eliable way. Sec ions 5 and 6 a e de o ed o he desc ip- ion o he ACL2 p oo o co ec ness and o he impo an p ope ies. Finally we commen some conclusions and poin ou possible u he wo k. Due o he lack o space, we will no gi e he e de ails abou he p oo s ob ained and some unc ion defini ions will be omi ed. The in e es ed eade may consul [13], whe e he comple e de elopmen is a ailable. 2 The Role o Degene acy Ope a o s in Simplicial Topology Simplicial Topology [14] is a suba ea o Topology de o ed o eplace opologi- cal spaces by combina o ial models, in o de o ease hei s udy. The simples combina o ial model o a opological space is a simplicial complex.Le Vbe a se oge he wi h a pa ial o de <on i . A n-simplex is a lis [ 0, 1,..., n] whe e 0< 1< ... < na e elemen s o V. Fo each index iwe conside he i- ace ope a o ∂i ha gi en a n-simplex cons uc s a (n−1)-simplex dele ing he elemen a posi ion i.Asimplicial complex K(o e (V,<)) is a se o simplices closed wi h espec o he ace ope a o s. Each n-simplex can be ealized as an affine geome ical simplex ( o ins ance, a 0-simplex is ealized as a poin , a 1-simplex as a segmen , a 2-simplex as a i- angle, a 3-simplex as a e ahed on and so on). Thus, simplicial complexes a e models o iangula ed spaces, which a e a class o opological spaces sufficien ly la ge o de elop much o he gene al and algeb aic opology. Ne e heless, simpli- cial complexes ha e a se e e d awback: one needs many simplices o model ela- i ely simple spaces. Fo ins ance, o model a sphe e wi h a e ahed on we need 4 e ices, 6 edges and 4 iangles. Since he opological no ions a e qui e flexi- ble, we could use a much mo e efficien way o ep esen ing a sphe e: by means o a iangle whe e all he edges and e ices a e collapsed o jus one poin . The p oblem wi h his new ep esen a ion is he “dimension jump”: he e is one ele- men o dimension 2 ( he iangle) and one elemen o dimension 0 ( he poin ), and hen his se o simplices is no closed wi h espec o he ace ope a o s. The solu ion o his p oblem is o mo e om simplicial complexes o sim- plicial se s. In addi ion o he ace ope a o s, new ope a o s o degene acy a e conside ed. These ope a o s c ea e “a ificial” simplexes (wi h no geome ical meaning) bu allowing “jumping” among dimensions. To gi e an idea o his so- phis ica ed ins umen le us commen b iefly on how a simplicial complex can be iewed as a simplicial se . The ick is o accep simplexes ha a e o de ed bu no necessa ily s ic ly o de ed; ha is, epea ed elemen s a e allowed. Then o each index iwi h 0≤i≤n, we define he i-degene acy ope a o ηi ha gi en an-simplex cons uc s a (n+1)-simplex epea ing he elemen a posi ion i. Based on his idea, we define a simplicial se as a g aded se {Kq}q∈No abs ac simplexes (i.e. no necessa ily lis s o elemen s) wi h he i- ace and i-degene acy ope a o s, sa is ying he ollowing simplicial iden i ies (see [14] o de ails): ∀i<j ∂ i∂j=∂j−1∂i ∀i≤jη iηj=ηj+1ηi(1) ∀i<j ∂ iηj=ηj−1∂i ∀i, j ∂iηi=Id =∂j+1ηj ∀i>j+1 ∂iηj=ηj∂i−1 A simplicial se ep esen s a opological space in a much less expensi e manne han a simplicial complex. Fo ins ance, a sphe e o dimension ncan be ep esen ed wi h jus wo non-degene a e simplices: one in dimension nand o he in dimension 0 (geome ically, all he aces on he affine n-simplex a e collapsed o e a unique poin , p oducing a opological sphe e; hink in a seg- men whe e he wo ex emes a e iden ified, p oducing a ci cle, a 1-sphe e). A simplex is degene a e i i is ob ained as he applica ion o some ope a o ηi. I could be p o ed ha gi en a simplex x he e exis s a unique non-degene a e simplex yand a unique s ic ly dec easing lis o na u al numbe s [i0,i 1,...,i n] such ha ηi0ηi1...η in(y)=x. (This undamen al esul o Simplicial Topology has been p o ed in ACL2 as documen ed in [2]). We call his lis o indices [i0,i 1,...,i n]adegene acy lis and we say ha xis ob ained applying he de- gene acy lis [i0,i 1,...,i n] oy. In gene al, he applica ion o degene acy lis s o simplexes is a e y common ope a ion in Kenzo, e en o degene a e simplexes. Le us no e ha he appli- ca ion o a degene acy lis [i0,...,i n] o an degene a e simplex x, ha is he esul o applying ano he degene acy lis [j0,...,j m] o a non-degene a e sim- plex y, is he esul o applying he composi ion o he wo degene acy lis s, [i0,...,i n]◦[j0,...,j m], o y.Thecomposi ion o wo degene acy lis s is de- fined as he composi ion o he degene acy ope a o s: [i0,...,i n]◦[j0,...,j m]= ηi0...η inηj0...η jm; epea edly applying equa ion (1) abo e, his could be ans- o med again in o a degene acy lis . The implemen a ion in Kenzo o his com- posi ion ope a ion is cen al in he sys em as a whole. Fo example, he com- posi ion o he degene acy lis s [3,1] and [5,3,0] is η3η1η5η3η0, and applying epea edly he equa ion ηiηj=ηj+1ηi,wheni≤j, we successi ely ob ain η3η6η1η3η0,η3η6η4η1η0,η7η3η4η1η0and finally η7η5η3η1η0, ha is, he degene- acy lis [7,5,3,1,0]. The s a egy Se ge ae de ised was o in e p e a degene acy lis [i0,...,i n] as a bina y ep esen a ion o an in ege . He s o es he degene acies as in ege s (wi h he co esponding memo y sa ing) and implemen s he composi ion o degene acy lis s by using e y efficien Common Lisp p imi i es dealing wi h bina y numbe s (like logxo ,ash, and so on). This is one o he easons why Kenzo imp o es d ama ically he pe o mance o i s p edecesso EAT. Ne e he- less, his efficien composi ion ope a o called dgop*dgop in Kenzo has a mo e obscu e seman ics han i s co esponding in EAT, called cmp-ls-ls.Thispape is de o ed o desc ibe he ce ifica ion in ACL2 o he co ec ness o dgop*dgop, using cmp-ls-ls as a o mal specifica ion, and hen p o ing addi ional p ope - ies like equa ion (1) o simplicial se s o associa i i y o dgop*dgop. 3 An In oduc ion o he ACL2 Sys em ACL2 ([10],[11]) 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 . Thus, he sys em cons i u es an en i onmen in which algo i hms can be defined and execu ed, and hei p ope ies can be o mally specified and p o ed wi h he assis ance o a mechanical heo em p o e . As a p og amming language, i is an ex ension o an applica i e subse o Common Lisp1[16]. The logic conside s e e y unc ion defined in he p o- g amming language as a fi s -o de unc ion in he ma hema ical sense. Fo ha eason, he p og amming language is es ic ed o he applica i e subse o Common Lisp. This means, o example, ha he e a e no side-effec s, no global a iables, no des uc i e upda es and no highe -o de ea u es. E en wi h hese es ic ions, he e is a close connec ionbe weenACL2andCommonLisp:ACL2 p imi i es ha a e also Common Lisp p imi i es beha e exac ly in he same way, and his means ha , in gene al, ACL2 p og ams can be execu ed in any complian Common Lisp. The ACL2 logic is a fi s -o de logic, in which o mulas a e w i en in p efix no a ion; hey a e quan ifie – ee and he a iables in i a e implici ly uni e sally quan ified. The logic includes axioms o p oposi ional logic (wi h connec i es implies,and,. . . ), equali y (equal) and hose desc ibing he beha io o a sub- se o p imi i e Common Lisp unc ions. Rules o in e ence include hose o p oposi ional logic, equali y and ins an ia ion o a iables. The logic also p o- ides a p inciple o p oo by induc ion ha allows o p o e a conjec u e spli ing i in o cases and induc i ely assuming some ins ances o he conjec u e ha a e smalle wi h espec o some well– ounded measu e. An in e es ing ea u e o ACL2 is ha he same language is used o define p og ams and o speci y p ope ies o hose p og ams. E e y ime a unc ion is defined wi h de un, in addi ion o define a p og am, i is also in oduced as an axiom in he logic (whene e i is p o ed o e mina e o e e y inpu ). Theo ems and lemmas a e s a ed in ACL2 by he de hm command, and his command also s a s a p oo a emp in he ACL2 heo em p o e . The main p oo echniques used by ACL2 in a p oo a emp a e simplifica ion and induc ion. 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: e y o en non- i ial p oo s a e no ound by he sys em in a fi s a emp and hen i is needed o guide he p o e by adding lemmas, sugges ed by a p econcei ed hand p oo o by inspec ion o ailed p oo s. These lemmas a e hen used as ew i e ules in subsequen p oo a emp s. This kind o in e ac ion wi h he sys em is called “The Me hod” by i s au ho s. 4F omKenzoandEAT oACL2 Be o e gi ing he ACL2 defini ion o he composi ion o degene acy lis s (and he s a emen s o he heo ems we ha e p o ed), le us p esen he Kenzo code o 1In his pape , we will assume amilia i y wi h Common Lisp. ha ope a ion. As we ha e said be o e, Kenzo deals wi h degene acy lis s using a sma encoding. Basically, e e y degene acy lis can be seen as he na u al numbe whose bina y no a ion ep esen s he cha ac e is ic unc ion o he se o elemen s o he lis . Le us explain his wi h an example: he degene acy lis [5,3,0] can equi alen ly be seen as he bina y lis [1,0,0,1,0,1] in which 1 is in posi ion ii he numbe iis in he degene acy lis , 0 o he wise. This lis , seen as a bina y numbe in he e e se o de , is he na u al numbe 41. Thus, Kenzo encodes he abo e degene acy lis as 41. Le us now explain how Kenzo implemen s composi ion o degene acy lis s. This is be e unde s ood i we hink fi s in he bina y ep esen a ion. Le us conside he composi ion o he degene acy lis s [3,1] and [5,3,0]. Applying epea edly he equa ion ηiηj=ηj+1ηi,wheni≤j,weob ain[7,5,3,1,0]. Using bina y no a ion, his means ha he composi ion o [0,1,0,1] and [1,0,0,1,0,1] is [1,1,0,1,0,1,0,1]. In gene al (al hough i is no ob ious), composi ion be ween wo degene acy lis s in bina y no a ion can be desc ibed as sequen ially eplacing he 0’s in he fi s lis by he successi e elemen s o he second lis , un il one o he lis s is exhaus ed; and hen comple ing he esul wi h he emaining elemen s o he o he lis . As we ha e said be o e, Kenzo does no di ec ly use he bina y no a ion: i uses he na u al numbe ha his bina y no a ion ep esen s. Common Lisp logical ope a ions on numbe s, like logxo and ash, a e used o eflec he co es- ponding manipula ions on bina y lis s. The ollowing is he eal Common Lisp code o Kenzo o composi ion o degene acy lis s2: (de un dgop*dgop (dgop1 dgop2) (decla e ( ype ixnum dgop1 dgop2)) (le ((dgop 0) (bma k 0)) (decla e ( ixnum dgop bma k)) (loop (when (ze op dgop1) ( e u n- om dgop*dgop (logxo dgop (ash dgop2 bma k)))) (when (ze op dgop2) ( e u n- om dgop*dgop (logxo dgop (ash dgop1 bma k)))) (cond ((e enp dgop1) (when (oddp dgop2) (inc dgop (2-exp bma k))) (se dgop2 (ash dgop2 -1))) ( (inc dgop (2-exp bma k)))) (se dgop1 (ash dgop1 -1)) (inc bma k)))) This defini ion ecei es as inpu wo fixnum na u al numbe s dgop1 and dgop2 (encoding wo degene acy lis s) and execu es a loop ha uses wo local a iables dgop and bma k s o ing espec i ely he (pa ially compu ed) esul , and he numbe o elemen s o dgop al eady scanned. When one o he degene acy lis s is exhaus ed, i s ops and e u ns he conca ena ion o dgop and he emaining elemen s o he o he lis . O he wise, i upda es he wo local a iables (acco ding o he alues o he fi s elemen s o dgop1 and dgop2) and execu es again he body o he loop, emo ing he fi s elemen o dgop1, and e en ually he fi s elemen o dgop2. 2In he ollowing, o dis inguish ACL2 code om gene al Common Lisp code, we will use i alics o he la e . Since he unc ion dgop*dgop deals wi h na u al numbe s, we emphasize again ha logical ope a o s a e used o ea hem as bina y lis s. Fo example, com- pu ing (logxo dgop (ash dgop2 bma k)) is equi alen o “conca ena e” dgop and dgop2 (since bma k is he leng h o dgop). O , o example, (ash dgop1 -1) is equi alen o emo e “ he fi s elemen ” o dgop1. These logical ope a o s on fixnum numbe s a e usually compu ed in Common Lisp e y efficien ly, and his is one o he easons why Kenzo pe o ms much be e han EAT. On he nega i e side, he o mal e ifica ion o dgop*dgop seems a ha d ask. In he es o his sec ion, we p esen a defini ion o dgop*dgop in ACL2 ( ying o keep as close as possible o i s o iginal Common Lisp defini ion) and we s a e he heo em we wan o p o e in o de o inc ease ou confidence in he way Kenzo deals wi h degene acy lis s. 4.1 De ini ion o dgop*dgop in ACL2 Since he ACL2 p og amming language is a subse o Common Lisp, he defi- ni ion o dgop*dgop in ACL2, based on he abo e Common Lisp code, is qui e di ec . Ne e heless, due o he applica i e na u e o ACL2, he e a e some hings ha ha e o be defined in a diffe en (bu equi alen ) way. In pa icula , he only way o i e a e in ACL2 is by means o ecu sion. Thus, we use an auxilia y ecu - si e defini ion implemen ing he in e nal loop, ying o be as ai h ul as possible o he o iginal e sion. Also, since des uc i e upda es a e no allowed in ACL2, we conside he local a iables dgop and bma k as ex a inpu pa ame e s. Fi- nally, since ACL2 unc ions ha e o be o al, we ha e o define a esul jus in case he inpu s we e no o he in ended ype (( ype ixnum dgop1 dgop2)). Taking all hese conside a ions in o accoun , he ollowing is he ACL2 defini ion o he loop3: (de un dgop*dgop-loop (dgop1 dgop2 dgop bma k) (i (and (na p dgop1) (na p dgop2)) (cond ((ze op dgop1) (logxo dgop (ash dgop2 bma k))) ((ze op dgop2) (logxo dgop (ash dgop1 bma k))) ((e enp dgop1) (dgop*dgop-loop (ash dgop1 -1) (ash dgop2 -1) (i (oddp dgop2) (+ dgop (ash 1 bma k)) dgop) (+ bma k 1))) ( (dgop*dgop-loop (ash dgop1 -1) dgop2 (+ dgop (ash 1 bma k)) (+ bma k 1)))) 0)) Finally, he ACL2 defini ion o dgop*dgop is a call o he abo e auxilia y unc ion, wi h sui able ini ial ze o alues o dgop and bma k: (de un dgop*dgop (dgop1 dgop2) (dgop*dgop-loop dgop1 dgop2 0 0)) We claim ha he ACL2 e sion is ai h ul wi h he o iginal Kenzo defini ion, since we ha e ied o keep i as simila as possible. As we ha e said, he ac ha 3(2-exp n) e u ns 2n, hesameas(ash 1 n); we will commen mo e on his in he conclusions. ACL2 is a subse o Common Lisp makes his ansla ion almos di ec . Anyway, we s eng hened ou claim by an in ensi e es ing. Since bo h defini ions can be execu ed on any complian Common Lisp, i was e y easy o (success ully) es ha hey e u n he same esul o all pai s o inpu s nand m,wi h n, m ≤10000. 4.2 S a ing he Co ec ness P ope y o dgop*dgop We now desc ibe how we s a e he main heo em abou he co ec ness o he abo e ACL2 defini ion. I is clea ha we would like o p o e ha he unc ion compu es, using he na u al numbe encoding, he composi ion o wo degene- acy lis s. Degene acy lis s ha e been defined in Sec ion 2 as s ic ly dec easing lis s o na u al numbe s. The e o e, he fi s hing we ha e o define in ACL2 is he composi ion o degene acy lis s, ep esen ed as s ic ly dec easing lis s. Tha will be ou “specifi- ca ion” o he in ended beha io o any implemen a ion o composi ion o degene- acy lis s. No e ha , in p inciple, he compu a ion ca ied ou by dgop*dgop has no hing o do wi h he defini ion gi en in sec ion 2. While he o iginal defini ion is based on successi e applica ions o degene acy ope a o s on o a degene acy lis , he unc ion dgop*dgop makes some kind o “me ge” be ween he bina y ep esen a ion o degene acy lis s. As we ha e said be o e, he EAT sys em ( he Kenzo p edecesso ) used s ic ly dec easing lis s o na u al numbe s o ep esen degene acy lis s. Thus, i seems a good idea o p o e he equi alence (modulo he change o ep esen a ion) o he Kenzo unc ion wi h he co esponding EAT unc ion. In EAT, he composi ion o degene acy lis s is defined as an i e a i e appli- ca ion o he equa ion ηiηj=ηj+1ηi,wheni≤j. The ollowing is he eal code o he EAT defini ion o composi ion. No e ha he auxilia y unc ion cmp-s-ls implemen s he applica ion o a degene acy ope a o o a degene acy lis ; his unc ion is i e a i ely used by he main unc ion cmp-ls-ls o define composi ion: (de un cmp-s-ls (s ls) (decla e ( ype ixnum+ s) ( ype lis ls)) (do ((p ls (cd p)) ( sl (lis ) (cons (1+ (ca p)) sl))) ((endp p) (n e e se (cons s sl))) (decla e ( ype lis p sl)) (when (> s (ca p)) ( e u n (n econc (cons s sl) p))))) (de un cmp-ls-ls (ls1 ls2) (decla e ( ype lis ls1 ls2)) (do ((p ( e e se ls1) (cd p)) ( sl ls2 (cmp-s-ls (ca p) sl))) ((endp p) sl) (decla e ( ype lis p sl)))) We ha e defined ACL2 e sions o hese unc ions, ying o keep as ai h ul as possible wi h he o iginal code. Analogously o he p e ious subsec ion, a do loop has o be eplaced by auxilia y ecu si e unc ions. These a e ou ACL2 defini ions o composi ion o degene acy lis s: (de un cmp-s-ls-do (s p sl) (cond ((endp p) ( e e se (cons s sl))) ((> s (ca p)) (n econc (cons s sl) p)) ( (cmp-s-ls-do s (cd p) (cons (1+ (ca p)) sl))))) (de un cmp-s-ls (s ls) (cmp-s-ls-do s ls nil)) (de un cmp-ls-ls-do (p sl) (cond ((endp p) sl) ( (cmp-ls-ls-do (cd p) (cmp-s-ls (ca p) sl))))) (de un cmp-ls-ls (ls1 ls2) (cmp-ls-ls-do ( e e se ls1) ls2)) Again, he ansla ion om he eal Common Lisp code o EAT o he ACL2 e sion is qui e s aigh o wa d. Bu in o de o s eng hen e en mo e ou confi- dence in his “model”, we did in ensi e es ing, checking ha hey compu e he same esul s o 100000 inpu s andomly gene a ed. We now ha e o define unc ions ela ing he encoding used by Kenzo and he ep esen a ion o degene acy lis used by EAT. Fi s , he unc ion dgop-ex -in ans o ms a degene acy lis ep esen ed as a s ic ly dec easing lis o na u al numbe s (checked by he unc ion dgl-p) o i s co esponding ep esen a ion as a na u al numbe . No e he use o logical a i hme ic ope a o s: (de un dgop-ex -in (ex -dgop) (i (dgl-p ex -dgop) (i (endp ex -dgop) 0 (logxo (ash 1 (ca ex -dgop)) (dgop-ex -in (cd ex -dgop)))) 0)) We also define he unc ion dgop-in -ex , i s in e se. Fo ha , we use an auxilia y ecu si e defini ion ha simula es a do loop, wi h he inpu a iables sl and bma k, ha wo k as ex a pa ame e s o s o ing espec i ely he esul (pa ially) compu ed and he numbe o bina y digi s analyzed. The main unc ion simply calls his auxilia y defini ion wi h sui able ini ial alues o he ex a pa ame e s. This is ou ACL2 defini ion: (de un dgop-in -ex -do (dgop sl bma k) (i (na p dgop) (i (ze op dgop) sl (i (oddp dgop) (dgop-in -ex -do (ash dgop -1) (cons bma k sl ) (1+ bma k)) (dgop-in -ex -do (ash dgop -1) sl (1+ bma k)))) nil)) (de un dgop-in -ex (dgop) (i (na p dgop) (dgop-in -ex -acc dgop nil 0) nil)) I should be emphasized ha hese defini ions a e defined ying o be as close as possible o he co esponding Kenzo defini ions o hese ope a ions (al hough due o he lack o space we do no include he e his pa o he Kenzo code). We ha e now defined all he unc ions ha we need o s a ing he co ec ness p ope y o dgop*dgop. This p ope y exp esses ha o e e y pai o degene acy Acknowledgemen s In memo iam o Mi ian And ´es, ou colleague and, much mo e impo an , ou iend. Re e ences 1. And ´es, M., Lamb´an, L., Rubio, J.: Execu ing in Common Lisp, P o ing in ACL2. In: Kaue s, M., Ke be , M., Mine , R., Winds eige , W. (eds.) MKM/ CALCULEMUS 2007. LNCS, ol. 4573, pp. 1–12. Sp inge , Heidelbe g (2007) 2. And ´es, M., Lamb´an, L., Rubio, J., Ruiz-Reina, J.L.: Fo malizing Simplicial Topo- logy in ACL2. In: ACL2 Wo kshop 2007, Uni e si y o Aus in, pp. 34–39 (2007) 3. A ansay, J., Balla in, C., Rubio, J.: A Mechanized P oo o he Basic Pe u ba ion Lemma. Jou nal o Au oma ed Reasoning 40, 271–292 (2008) 4. A ansay, J., Balla in, C., Rubio, J.: Ex ac ing Compu e Algeb a P og ams om S a emen s. In: Mo eno D´ıaz, R., Pichle , F., Quesada A encibia, A. (eds.) EUROCAST 2005. LNCS, ol. 3643, pp. 159–168. Sp inge , Heidelbe g (2005) 5. Coquand, T., Spiwack, A.: Towa ds Cons uc i e Homological Algeb a in Type Theo y. In: Kaue s, M., Ke be , M., Mine , R., Winds eige , W. (eds.) MKM/ CALCULEMUS 2007. LNCS, ol. 4573, pp. 40–54. Sp inge , Heidelbe g (2007) 6. Dom´ınguez, C.: Fo malizing in Coq Hidden Algeb as o Speci y Symbolic Compu- a ion Sys ems. In: Au exie , S., Campbell, J., Rubio, J., So ge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS, ol. 5144, pp. 270–284. Sp inge , Heidelbe g (2008) 7. Dom´ınguez, C., Lamb´an, L., Rubio, J.: Objec O ien ed Ins i u ions o Speci y Symbolic Compu a ion Sys ems. Rai o - Theo e ical In o ma ics and Applica- ions 41, 191–214 (2007) 8. Dousson, X., Rubio, J., Se ge ae , F., Si e , Y.: The Kenzo P og am, Ins i u Fou ie (1999), h p://www- ou ie .uj -g enoble. /~se ge a /Kenzo/ 9. He as, J., Pascual, V., Rubio, J.: Media ed Access o Symbolic Compu a ion Sys- ems. In: Au exie , S., Campbell, J., Rubio, J., So ge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS, ol. 5144, pp. 446–461. Sp inge , Heidelbe g (2008) 10. Kau mann, M., Manolios, P., Moo e, J.S.: Compu e -Aided Reasoning: An Ap- p oach. Kluwe Academic Publishe s, Do d ech (2000) 11. Kau mann, M., Moo e, J.S.: ACL2 Home Page, h p://www.cs.u exas.edu/use s/moo e/acl2 12. Lamb´an, L., Pascual, V., Rubio, J.: An Objec -O ien ed In e p e a ion o he EAT Sys em. Applicable Algeb a in Enginee ing, Communica ion and Compu ing 14, 187–215 (2003) 13. Ma ´ın–Ma eos, F.J., Ruiz–Reina, J.L., Rubio, J.: ACL2 e ifica ion o simplicial degene acy p og ams in he Kenzo sys em, h p://www.cs.us.es/~ ma in/acl2/kenzo 14. May, J.P.: Simplicial Objec s in Algeb aic Topology. Van Nos and (1967) 15. Rubio, J., Se ge ae , F., Si e , Y.: EAT: Symbolic So wa e o Effec i e Homology Compu a ion, Ins i u Fou ie (1997), p:// p- ou ie .uj -g enoble. /pub/EAT 16. S eele J ., G.L.: Common Lisp The Language, 2nd edn. Digi al P ess (1990)