Formalization of a normalization theorem in simplicial topology

Fo maliza ion o a no maliza ion heo em in simplicial opology Lau eano Lambán · F ancisco-Jesús Ma ín–Ma eos · Julio Rubio · José-Luis Ruiz–Reina Abs ac In his pape we p esen a comple e o maliza ion o he No maliza ion Theo em, a esul in Algeb aic Simplicial Topology s a ing ha he e exis s a homo opy equi alence be ween he chain complex o a simplicial se , and a smalle chain complex o he same simplicial se , called he no malized chain complex. E en i he No maliza ion Theo em is usually s a ed as a highe -o de esul (wi h a Ca ego y Theo y la o ) we manage o gi e a i s -o de p oo o i . To his aim i is ins umen al he in oduc ion o an algeb aic da a s uc u e called simplicial polynomial. As a demons a ion o he alidi y o ou echniques we de eloped a o mal p oo in he ACL2 heo em p o e . Keywo ds Au oma ed easoning · Fo maliza ion o ma hema ics · ACL2 · Algeb aic opology · No maliza ion heo em This wo k is dedica ed o ou colleague and iend Mi ian And és. She s a ed his esea ch bu passed away a he age o only 29 due o a ca acciden . Mi ian, he bes iend o you iends, we do no o ge you. Pa ially suppo ed by Minis e io de Ciencia e Inno ación, p ojec MTM2009-13842, and by Eu opean Commission FP7, STREP p ojec Fo Ma h, n. 243847. L. Lambán ·J. Rubio (B) Depa men o Ma hema ics and Compu a ion, Uni e si y o La Rioja, Edi icio Vi es, Luis de Ulloa s/n. 26004, Log oño, Spain e-mail: [email p o ec ed] L. Lambán e-mail: [email p o ec ed] F.-J. Ma ín–Ma eos ·J.-L. Ruiz–Reina Compu a ional Logic G oup, Depa men o Compu e Science and A i icial In elligence, Uni e si y o Se ille, A da. Reina Me cedes, s/n. 41012, Se illa, Spain F.-J. Ma ín–Ma eos e-mail: [email p o ec ed] J.-L. Ruiz–Reina e-mail: [email p o ec ed] In oduc ion The No maliza ion Theo em is an impo an esul in Algeb aic Simplicial Topology explaining ha , in o de o ob ain he homology g oups o a space, one can wo k wi h a chain complex (called no malized) smalle han he s anda d chain complex cons uc ed om all he simplexes o he space. In his pape we p esen a comple e o mal p oo o he No maliza ion Theo em. As a demons a ion o he soundness o ou app oach we ha e w i en a comple e de elopmen o he o mal p oo in he ACL2 heo em p o e . The in e es o his wo k s ems om h ee sou ces. Fi s , i cons i u es a good example o using e icien ly i s -o de logic in a con ex whe e a highe -o de app oach could seem mo e na u al, due o he cha ac e o he ma hema ics o - malized. Second, ou p oo alida es some o mulas ound expe imen ally, gi ing an explici e sion o he No maliza ion Theo em, unknown in he li e a u e (up o ou knowledge). And hi d, he No maliza ion Theo em is he basis o some design decisions in he Kenzo compu e algeb a sys em, a p og am o compu ing in Algeb aic Topology. This las poin is u he explained in he nex pa ag aphs. The o igin o his wo k comes om a Compu e Algeb a sys em called Kenzo [8], a Common Lisp p og am c ea ed by F. Se ge ae a ound 1990 and de o ed o compu ing homology g oups o opological spaces. In o he wo ds, Kenzo is a sys em de o ed o Algeb aic Topology, he b anch o ma hema ics dealing wi h algeb aic s uc u es (g oups, ings,...) associa ed o opological spaces. Usually, he opological spaces a e p esen ed unde a combina o ial o m as simplicial complexes o simplicial se s. The objec i e o Algeb aic Topology is o classi y o o dis inguish opological spaces by obse ing he algeb aic s uc u es associa ed o hem, which a e, in p inciple, amenable o a sys ema ic ea men (algeb a would be conside ed, in his sense, easie han opology). One ea u e o Algeb aic Topology is ha , in o de o ge in o ma ion om spaces o ini e dimension, i is equi ed o pass h ough some in ini e dimensional spaces (as loop spaces o ins ance; see [19] o de ails). This explains why Se ge ae chose Common Lisp as implemen a ion language o Kenzo: he used unc ional p og amming o encode in ini e se s needed in Algeb aic Topology cons uc ions. Al hough Kenzo is a e y eliable sys em which has been in ensi ely es ed, and is in p oduc ion se e al yea s ago, i u ns ou ha Kenzo was able o compu e new esul s (“new” in he sense ha no known heo e ical esul can be used o con i m i ; see [24]). Then, some conc e e ou pu s o he p og am canno be es ed, ha is, compa ed wi h any expec ed alue. This is he eason why a p ojec o apply o mal me hods o he s udy o Kenzo as a so wa e sys em was launched some yea s ago [6, 12]. E en ually, his esea ch line a i ed o he o maliza ion o some pa s o Algeb aic Topology and Homological Algeb a by using p oo assis an s as Isabelle/HOL [2, 3]o Coq [7]. A di e en app oach o using Coq o implemen in cons uc i e ype heo y some ea u es o Kenzo can be ound in [4]. When alking abou mechanized heo em p o ing and Kenzo, i is easy o hink abou ACL2 [11]. ACL2 is, a he same ime, a p og amming language, a logic o speci ying and p o ing p ope ies o he p og ams de ined in he language and a he- o em p o e suppo ing mechanized easoning in he logic. The ACL2 p og amming language is an ex ension o an applica i e subse o Common Lisp, and he logic is i s -o de , in which o mulas do no ha e quan i ie s and all he a iables in hem a e implici ly uni e sally quan i ied. I includes axioms o p oposi ional logic, equali y and o a numbe o p ede ined Common Lisp unc ions and da a ypes. Rules o in e ence o he logic include hose o p oposi ional calculus, equali y, ins an ia ion and induc ion. The p e ious discussion on Kenzo howe e shows he limi a ions o an ACL2 app oach o e i y Kenzo p ope ies, since Kenzo uses highe o de unc ional p og amming, while ACL2 is, essen ially, a i s o de ool. This cons ain has no been an obs acle o us o e ec i ely use ACL2 o s udy i s o de agmen s o Kenzo [10,18]. The ACL2 p oo o he No maliza ion Theo em desc ibed in his pape (a p elimina y e sion o his wo k was p esen ed in [13]) di e s om p e ious ACL2 o maliza ions in wo aspec s. The i s peculia i y o his pape is ha he o malized algo i hm is no di ec ly used in Kenzo. I is a he a p econdi ion o Kenzo, because only no malized chain complexes a e deal wi h in ha sys em. Thus, ou ACL2 p oo ce i ies ha he encoding s a egy applied in Kenzo is eliable. In addi ion, i in some u u e de elopmen he non-no malized chain complex is needed, hen ou ACL2 p oo will p o ide a ce i ied ans e o he Kenzo coding s yle ( o a di e en bu ela ed p oblem, whe e algo i hms in ol ing non-no malized objec s a e needed, see [22], pp. 102–104). The second di e en ial ea u e o he p oblem ackled in his pape is ha , in p inciple, i is a highe o de esul , because i quan i ies o e e e y simplicial se (which, in gene al, would be cha ac e ized by p edica es). The key poin o his pape is ha , o his conc e e esul , i s o de is enough. I is no due o a simula ion o highe o de logic in ACL2 by means o encapsula es [11] (al hough his echnique will be also used in ou de elopmen , in o de o p esen ou s a emen s in a s anda d ma hema ical e minology). A symbolic se ing is in oduced in which he heo em can be p o ed by using only simpli ica ion and induc ion on lis s, he kind o p oo s ACL2 was designed o . We hink ha his app oach could be use ul in o he ela ed esul s, because i is based on some ea u es o he simplicial ca ego y. Thus, his wo k could be conside ed a i s miles one o o malize simplicial opology in a i s o de ame. The o ganiza ion o he pape is as ollows. In Sec ion 2we in oduce bo h he p oblem (including he minimal ma hema ical machine y needed o s a e and unde s and he main heo em) and he s a egy o he solu ion we a e p oposing o i . The symbolic amewo k based on simplicial polynomials is hen desc ibed in Sec ion 3. I is applied o gi e a p oo o he No maliza ion Theo em in Sec ion 4. The s a emen o he No maliza ion Theo em in Sec ion 4is exp essed in e ms o he i s o de concep s in oduced in Sec ion 3; hen, in Sec ion 5we e o mula e i by using ACL2 encapsula es, p o iding a s a emen mo e eadable om he poin o iew o s anda d ma hema ical ex books. Sec ion 6is de o ed o pu he p oo in con ex , illus a ing ha ou app oach is no so-o iginal: highe o de logic is a oided due o wo king wi h a conc e e ca ego y o p e-shea es. The las sec ion in he pape deals wi h conclusions and u he wo k. In addi ion, we include wo appendices. In Appendix Awe gi e a sho ecipe allowing an in e es ed eade o check on his own compu e he o malized p oo , e en i he is no an ACL2 use . Appendix Bcon ains a sample ACL2 session showing he li e al ou pu o an au oma ic p oo o one o malized heo em. 2 P esen a ion o he p oblem and he solu ion In his sec ion we in oduce he ma hema ical p elimina ies equi ed o unde s and he p oblem, and we gi e some clues abou he na u e o he o maliza ion de el- oped. Mo e conc e ely, he mos impo an simplicial concep s needed o s a e he main heo em a e p esen ed in Sec ions 2.1–2.5. (Mo e de ails on simplicial opology can be ound, o ins ance, in [19].) Sec ions 2.6 and 2.7 explain he big lines o he p oo and some o maliza ion issues, espec i ely. Finally, in Sec ion 2.8, an example o a (simple) p oo is desc ibed, in o de o illus a e ou me hods. 2.1 Simplicial se s De ini ion 1 Asimplicial se K is a g aded se {Kn}n∈N oge he wi h unc ions: ∂n i:Kn→Kn−1,n>0,i=0,...,n, ηn i:Kn→Kn+1,n≥0,i=0,...,n, subjec o he ollowing equa ions: ∂n−1 i∂n j=∂n−1 j∂n i+1i i≥j,(1) ηn+1 iηn j=ηn+1 j+1ηn ii i≤j,(2) ∂n+1 iηn j=ηn−1 j−1∂n ii i<j,(3) ∂n+1 iηn j=ηn−1 j∂n i−1i i>j+1,(4) ∂n+1 iηn i=∂n+1 i+1ηn i=idn(5) The unc ions ∂n iand ηn ia e called ace and degene acy maps, espec i ely. The unc ion idndeno es he iden i y unc ion on Kn. The elemen s o Kna e called n-simplexes (o simplexes o dimension n).An- simplex xis degene a e i x=ηn−1 iy o some simplex y, and o some degene acy map ηn−1 i;o he wisexis non degene a e. Al hough we ha e no enough oom he e o illus a e he no ion o simplicial se , le us y o explain whe e he iden i ies come om. I we hink ha n-simplexes a e non-dec easing in ege lis s o leng h n+1, and we in e p e a ace ope a o ∂n i as e asing he elemen a posi ion iin a lis ( he i s elemen is ha a index 0), and a degene acy ope a o ηn ias epea ing he elemen a posi ion i, he equali ies ob ained a e exac ly hose o De ini ion 1. Wi h his in e p e a ion, non-degene a e simplexes a e hose lis s s ic ly inc easing, while he degene a e simplexes ha e some epe i ion. This kind o simplicial se (whose simplexes a e lis s) is called simplicial complex [5]. I can be conside ed ha a simplicial se is an abs ac ion o a simplicial complex, whe e simplexes a e no mo e lis s, bu wha e e elemen s. I no con usion can a ise, usually we emo e he supe index in he ace and degene acy ope a o s, w i ing simply ∂iand ηi, espec i ely. 2.2 Chain complexes and homology g oups A simplicial se is a combina o ial model o a opological space. Algeb aic Topology associa es algeb aic objec s o opological spaces. This is he eason o he ollowing de ini ions. Le Kbe a simplicial se . Fo each n∈N, le us conside Z[Kn], he ee Abelian g oup gene a ed by he n-simplexes Kn, deno ed by Cn(K). Then, he elemen s o such a g oup a e o mal linea combina ions  j=1λjxj,whe eλj∈Zand xj∈ Kn,∀j=1,..., . These linea combina ions a e called chains o simplexes o , in sho , chains. Now, i n>0, we in oduce a homomo phism dn:Cn(K)→Cn−1(K), i s de ining i o e each gene a o , and hen ex ending i by linea i y. Gi en x∈Kn, de ine dn(x)=n i=0(−1)i∂i(x). I can be p o ed ha (1) in he de ini ion o simplicial se implies ha dn◦dn+1=0,∀n∈N. Tha is o say, he amily {dn}n∈Nde ines a di e en ial (o bounda y) homomo phism on he g aded g oup {Cn(K)}n∈N. O , s ill in o he wo ds, he amily o pai s {(Cn(K), dn)}n∈Nis he chain complex associa ed o he simplicial se K, deno ed by C(K). Le C={(Cn,dn)}n∈Nbe a gene al chain complex ( ha is, each Cnis an Abelian g oup, and each dnis a homomo phism such ha he bounda y condi ion holds). The bounda y p ope y dn◦dn+1=0implies Im(dn+1)⊆Ke (dn), and since we a e wo king wi h Abelian g oups, i is possible o conside he quo ien g oup Ke (dn)/Im(dn+1). I is called he n- h homology g oup o he chain complex C, deno ed by Hn(C). In he pa icula case whe e C=C(K)(Kbeing a simplicial se ) we call i he (simplicial) n- h homology g oup o K, deno ed by Hn(K). Much e o is de o ed in Algeb aic Topology o s udy and de e mine such homology g oups. And i is also he main objec o be compu ed by means o Kenzo. 2.3 No malized chain complexes The e is an al e na i e way o associa e a chain complex o a simplicial se K. Gi en n∈N, le us deno e by KD nand KND n he se s o degene a e and non-degene a e n- simplexes o K, espec i ely (no e ha his gi es a disjoin pa i ion o he whole se Kn). We now conside he ollowing Abelian ee g oups: Dn(K)=Z[KD n], ha is o say he Abelian g oup eely gene a ed by degene a e simplexes. Condi ions (3)– (5) in De ini ion 1 imply ha he di e en ial dnis well de ined on D(K)( ha is, i we ake a combina ion c=m j=1λjxjwhe e e e y xjis degene a ed, hen dn(c)∈ Dn−1(K)). Thus, he chain complex D(K)is a subcomplex o C(K), and we can ob ain he quo ien chain complex C(K)/D(K), which is deno ed by CN(K)and is called he no malized chain complex o he simplicial se K. The e exis s an al e na i e isomo phic desc ip ion o he no malized chain com- plex CN(K). I consis s o de ining as CN n(K) he ee Abelian g oup Z[KND n] gene a ed by non-degene a e simplexes. Then, o ge an ac ual chain complex, i is necessa y o ede ine he di e en ial map dnby e asing, in he image, he gene a o s which a e degene a e. Wi h his desc ip ion he g oup CN n(K)is no mo e a quo ien , bu a subg oup o Cn(K). Obse e howe e ha CN(K)is no in gene al a chain subcomplex o C(K)(because some aces o a non-degene a e simplex can be degene a e simplexes). 2.4 The no maliza ion heo em Wi h any o he wo desc ip ions o he no malized chain complex CN(K), he e ex- is s a canonical epimo phism :C(K)→CN(K).I CN(K)is conside ed a quo ien , he map is no hing bu he canonical p ojec ion. I CN(K)is desc ibed as a ee g aded g oup, hen ( j=1λjxj)consis s simply o e asing in he combina ion he e ms λjxjwhe e xjis a degene a e simplex. No e ha he map espec s in bo h cases he di e en ials; ha is o say, n−1◦ dn=dN n◦ n,∀n>0,whe edNdeno es he di e en ial o CN(K). O s ill in o he wo ds, is a chain mo phism. This canonical chain mo phism p ese es he homological in o ma ion, and his is es ablished by he no maliza ion heo em. Theo em 1 (No maliza ion heo em) Fo all simplicial se K, he canonical homomo phism :C(K)→CN(K)induces g oup isomo phisms Hn(C(K)) ∼ = Hn(CN(K)), ∀n∈N. The heo em explains ha , om he compu a ional poin o iew, i is he same o wo k wi h C(K)o wi h CN(K). This jus i ies Se ge ae ’s decision o wo king in Kenzo only wi h he smalle chain complex CN(K) o compu e homology g oups o a simplicial se K. One p oo o he No maliza ion Theo em can be ound in [14], pp. 236–237. I consis s o il e ing he big g oup Cn(K)by conside ing sequen ially n-simplexes o he o m ηn−1x, hen o he o m ηn−2xo ηn−1x, and so on. In each s ep, he homological in o ma ion is p ese ed. And inally is desc ibed as he composi ion o all hese homology-p ese ing maps. 2.5 S a emen o he heo em o o malize I is no di icul o gi e a mo e p ecise p oo (and s a emen ) o he no maliza ion heo em using he no ion o educ ion. (In [22], pp. 102–104, a p oo simila o Mac Lane’s one is con e ed in o an algo i hm cons uc ing a educ ion, in a sligh ly di e en con ex .) De ini ion 2 A educ ion is a 5- uple (C,C, ,g,h) C ++ h55C g kk whe e C=(M,d)and C=(M,d)a e chain complexes, :C→Cand g:C→C a e chain mo phisms, h=(hi:Mi→Mi+1)i∈Nis a amily o homomo phisms (called homo opy ope a o ), which sa is y he ollowing p ope ies o all i∈N: (a) i◦gi=idM i, (b)di+2◦hi+1+hi◦di+1+gi+1◦ i+1=idMi+1, (c) i+1◦hi=0, (d)hi◦gi=0, (e)hi+1◦hi=0 This concep p ecisely desc ibes a si ua ion whe e he homological in o ma ion is p ese ed. Mo e conc e ely, i (C,C, ,g,h)is a educ ion, hen ninduces an isomo phism o g oups (wi h gnde ining he co esponding in e se) be ween Hn(C) and Hn(C), ∀n>0. The e o e he ollowing s a emen desc ibes a s onge e sion o he no maliza- ion heo em. Theo em 2 (No maliza ion educ ion) Fo all simplicial se s K, he e exis s a educ- ion (C(K), CN(K), ,g,h)whe e is he canonical chain epimo phism. 2.6 Plan o he o malized p oo Ins ead o ying a p oo based on Mac Lane’s ideas, we o malized a di e en p oo , wi h he addi ional goal o applying i o s udy an expe imen al esul p esen ed in [23]. The e, a e unning se e al examples, i was conjec u ed ha some possible o mulas o he No maliza ion Theo em could be: •gm=(−1)p i=1ai+biηap...η a1∂b1...∂ bp whe e he indexes ange o e 0≤a1<b1<...<ap<bp≤m,wi h0≤p≤ (m+1)/2. •hm=(−1)ap+1+p i=1ai+biηap+1ηap...η a1∂b1...∂ bp whe e he indexes ange o e 0≤a1<b1<...<ap<ap+1≤bp≤m,wi h0≤ p≤(m+1)/2. We will p o e in ACL2 ha , wi h some ecu si e e sions o hese o mulas, he equali ies (a), (b) and (c) in De ini ion 2 hold. This esul is he mos di icul one in all ou o maliza ion. To s ess he complexi y o his ask, le us obse e ha he sum o gmhas 2m e ms, while ha o hmhas 2m+1−1 e ms. Le us call p e educ ion o a 5- uple (C,C, ,g,h)as in he de ini ion o educ ion, bu whe e equali ies (d) and (e) a e possibly no sa is ied.1Then, he ollowing esul can be used o cons uc , om ou p e ious explici o mulas, a educ ion linking C(K)and CN(K). 1One o he anonymous e e ees obse ed ha , o be a p e educ ion, i is enough o he uple (C,C, ,g,h) o sa is y he p ope ies (a) and (b), because he o mula h1:= (1−g )h(1−g )gi es he p ope ies (c) and (d) o h1. In ou conc e e si ua ion, he de ini ions o and hsa is y al eady P ope y (c), h=0, and hus ou weake esul is enough in ou case. Theo em 3 Le (C,C, ,g,h0)be a p e educ ion. Then, an algo i hm p oduces a educ ion (C,C, ,g,h). Le us explain he p oo o his las heo em, because i will se e us la e o illus a e how ACL2 can be e ec i ely used in his kind o highe -o de easoning (obse e ha Cand Ccan be suppo ed by in ini e se s, de ined by p edica es, and ha he cons uc ion o h om ( ,g,h0)would equi e highe o de unc ional p og amming). Fi s , we de ine: h1:= h0−h0g . This new homomo phism o deg ee +1sa is ies condi ions (a)-(b)-(c) in he de ini ion o educ ion. Fo ins ance: dh1+h1d= d(h0−h0g )+(h0−h0g )d=dh0−dh0g +h0d−h0g d=dh0−dh0g +h0d− h0dg =dh0+h0d−(dh0+h0d)g =id −g −(id −g )g =id −g −g +g g = id −g −g +g =id −g , and so condi ion (b) is sa is ied o he new homo opy h1. In addi ion: h1g=(h0−h0g )g=h0g−h0g g=h0g−h0g=0. Now, wi h his kind o simple ew i ings, i is easy o e i y ha all he p ope ies o a educ ion a e ob ained wi h he ollowing homo opy ope a o : h:= h1dh1. 2.7 Fo maliza ion issues Summa izing he p e ious subsec ion, ou p oblem is o p o e in ACL2 he No mal- iza ion Theo em (in i s s ong e sion p o iding a educ ion, as in Theo em 2). In addi ion, ou p oo should be based on he explici o mulas expe imen ally ound in [23]. As al eady men ioned, he s a emen in Theo em 2 is clea ly o second-o de . I quan i ies o e all simplicial se s. Bu a simplicial se is gi en by a collec ion o p edica es (de ining, ∀n∈N, hese o n-simplexes, ha can be an in ini e se ) and o unc ions ∂n i,ηn i. To deal wi h hese s uc u es as i s -class ci izens ( o pass hem as a gumen s o unc ions, and o p oduce hem as ou pu s o unc ions) Kenzo uses highe -o de unc ional p og amming. Highe o de can be simula ed in ACL2 by means o encapsula es,amechanism o in oduce abs ac unc ions wi h cons ain s. Fo ins ance, a gene ic de ini ion o a educ ion can be encoded in an encapsula e. Then, p ope ies ob ained om ha encapsula e can be applied o any educ ion. In Sec ion 5we will use his echnique o p oduce in ACL2 a p esen a ion o he No maliza ion Theo em close o he one usually ound in ex books. Fu he mo e, we p o e he e Theo em 3, by guiding he heo em p o e . Howe e , o gi e a p oo o Theo em 2, a g ea e deg ee o au oma ion would be desi able, because he ma hema ical p oo is much mo e complica ed han ha o Theo em 3. To his aim, we ha e de ised an ACL2 p oo ee o encapsula es. Tha is o say, a pu ely i s o de p oo . The idea is as ollows. Le us de ine a simplicial ope a o as any sequence o ace and degene acy maps. Fo ins ance, ∂5η3∂1∂2η4is such a simplicial ope a o . Obse e ha , as dimensions a e d opped ( he e a e no supe indexes), his exp ession deno es a unc ional objec in each alid dimension (a leas dimension 5in he example), and o e e y simplicial se on which i is applied. Now, i equali ies in De ini ion 1 a e conside ed as ew i ing ules ( eading hem om le o igh ) hen he e exis s a canonical o m o each simplicial ope a o (see [1] o a comple e de elopmen o his idea, o malized in ACL2). Le us show his con e sion o canonical o m s ep by s ep in ou unning example: ∂5η3∂1∂2η4=η3∂4∂1∂2η4=η3∂1∂5∂2η4=η3∂1∂2∂6η4=η3∂1∂2η4∂5= η3∂1η3∂2∂5=η3η2∂1∂2∂5. Thus any simplicial ope a o can be encoded, in a unique way, as a pai o lis s o na u al numbe s: he i s lis being a s ic ly dec easing lis o na u al numbe s, and he second one s ic ly inc easing. In ou example: ((3 2) (1 2 5)).Le uscall such pai s simplicial e ms, using a e minology bo owed om algeb aic polynomial heo y (see, o ins ance, he o maliza ion in [20]). No e ha al hough a simplicial e m is a simplicial ope a o , we call i in a special way o emphasize he ac ha i is in canonical o m. Simplicial e ms can be composed (by using again he simplicial iden i ies o De ini ion 1) and so hey a e endowed wi h a monoid s uc u e ( he uni y being he pai wi h wo emp y lis s). Now, le us obse e ha he o mulas o gmand hmin he p e ious subsec ion can be in e p e ed as linea combina ions o simplicial e ms. Thus i is sensible o y he p oo in he ing eely gene a ed by simplicial e ms. We will call he elemen s o his ing simplicial polynomials. The ACL2 o maliza ion o simplicial polynomials p esen ed he e is simila o he o maliza ion o polynomials o e he a ional ield de eloped in [20]. Simplicial polynomials can be in e p e ed unc ionally only o e a single chain complex C(K). This implies, o ins ance, ha he canonical p ojec ion canno be ep esen ed inside his amewo k (since i links wo di e en chain complexes, namely C(K)and CN(K)). In Sec ion 4, we manage o e o mula e he p ope ies o a educ ion in he simplicial polynomials se ing. Then, in Sec ion 5,weuse he encapsula ion p inciple o eco e he s anda d s a emen o he esul s (in e ms o unc ional objec s). 2.8 An example a wo k The in ui i e idea unde lying ou app oach is ha i we p o e a esul by only using he simplicial equali ies o De ini ion 1, hen he scope o he p oo is he whole ca ego y o Simplicial Se s. Le us see i in ac ion wi h he ollowing example. (In Appendix Bwe gi e an ACL2 session co esponding o his same heo em.) Theo em 4 dn◦dn+1=0,∀n∈N. Le us s a om he de ini ion: dn+1= n+1  i=0 (−1)i∂n+1 i=(−1)n+1∂n+1 n+1+ n  i=0 (−1)i∂n+1 i. Now, we do a o bidden ope a ion: emo e he supe indexes in he las exp es- sion. This allows us a ecu si e de ini ion o he di e en ial: dn+1=(−1)n+1∂n+1+ n i=0(−1)i∂i=(−1)n+1∂n+1+dn. Analogously: dn=(−1)n∂n+dn−1. By applying he o mal p ope ies o he simplicial ing, we ob ain: dn◦dn+1=[(−1)n∂n+dn−1][(−1)n+1∂n+1+dn]=−∂n∂n+1+(−1)n∂ndn+ (−1)n+1dn−1∂n+1+dn−1dn. And hen, using he induc ion hypo hesis dn◦dn+1= −∂n∂n+1+(−1)n∂ndn+(−1)n+1dn−1∂n+1. I is no di icul o p o e, also by induc ion, he ollowing auxilia y esul . Lemma 1 ∂ndn=(−1)n∂n∂n+1+dn−1∂n+1. clea ha ano he es ic ion we mus impose on a simplicial polynomial, in o de o being able o in e p e i as a unc ion on chains, is ha all i s e ms mus ha e he same deg ee (wha we will call a uni o m polynomial). We ha e o malized in ACL2 hose es ic ions by means o h ee unc- ions alid-sp,uni o m-sp and deg ee-sp, whose de ini ions we omi he e: alid-sp(p,m) checks whe he all he simplicial e ms in pa e alid o dimen- sion m,uni o m-sp(p) checks i all he e ms in pha e he same deg ee and deg ee-sp(p) is he common deg ee o he e ms o a uni o m polynomial (o 0 i i is he ze o polynomial). We will say ha a polynomial is well- o med o dimension mwhen i is alid o mand uni o m. I is impo an o no e ha well- o medness is no needed o p o e he ing p ope ies o simplicial polynomials, which a e ue o e e y polynomial, well- o med o no . Bu i will be needed in Sec ion 5, whe e we will in e p e simplicial polynomials as unc ions on chains. 4 Fo mal p oo s in he polynomial amewo k As ske ched in Sec ion 2, ou main goal is o p o e he No maliza ion Theo em (in i s s ong e sion), by explici ly gi ing a educ ion (C(K), CN(K), ,g,h). Un o una ely, we canno di ec ly s a e his heo em in he simplicial polynomial amewo k. The e a e se e al easons o his. Fo example, is de ined o be he canonical chain epimo phism, om C(K) o CN(K). This unc ion can be desc ibed as he ope a ion o e asing all he degene a e simplexes o a chain ( ecall om Sec ion 2.1: a linea combina ion o simplexes wi h in ege coe icien s). Since a simplicial polynomial does no ha e an explici men ioning o he a gumen s on which he unc ion ha i ep esen s is supposed o be applied, his epimo phism canno be desc ibed as a simplicial polynomial. Also, we should no o ge ha in ou polynomial se ing we d opped any explici men ioning o he dimensions o he ace and degene acy maps in ol ed, and hese dimensions a e explici in he de ini ion o simplicial se (De ini ion 1). Bu o una ely, we can do mos o he wo k (o a leas , he ha d pa ) using simplicial polynomials in a con enien way, as we will desc ibe. The idea is o de ine polynomial e sions o he di e en ial dand o gand h, and p o e, in he simplicial polynomial ing, hei main p ope ies. 4.1 The polynomials dm,gmand hm Fi s , le us ecall he de ini ions (pa ame e ized by m∈N) o he di e en ial dm and o he conjec u ed de ini ions o gmand hm, gi en in Sec ion 2: •dm=m i=0(−1)i∂i •gm=(−1)p i=1ai+biηap...η a1∂b1...∂ bp, whe e he indexes ange o e he aiand bisuch ha 0≤a1<b1<...<ap<bp≤m,wi h0≤p≤(m+1)/2. •hm=(−1)ap+1+p i=1ai+biηap+1ηap...η a1∂b1...∂ bp, whe e he indexes ange o e 0≤a1<b1<...<ap<ap+1≤bp≤m,wi h0≤p≤(m+1)/2. No e ha , iewed as symbolic exp essions, he abo e de ine h ee amilies o simplicial polynomials. In o de o ansla e hem o ACL2, we ound an essen ial hind ance: ACL2 does no admi i e a i e de ini ions, and he e o e i is manda o y o wo k wi h an equi alen ecu si e de ini ion. A he end o he way, i will gi e o ou p oo a ecu si e la o , and so di e ences wi h he abo e men ioned Mac Lane’s p oo [14] could be unno iced. Howe e , ou p oo was di ec ly inspi ed by hese summa ions, and ca ied ou ollowing combina o ial clues gi en by hem. (In ac , a e ou o maliza ion was comple ed, we ound he pape [9], whe e Da id Eps ein ga e o mulas e y close o ou ecu si e e sions o he summa ions.) We i s in oduce he ecu si e polynomials ( ha is, he polynomial o mwill be de ined in e ms o he polynomial o m−1) and hen explain wi h some de ail he ansla ion om he summa ions o he ecu si e polynomials. The case o he unc ion di -pol, de ining he di e en ial dm, is easy and does no dese e a hough ul explana ion: De ini ion: [dm] di -pol(m):= i m∈ N+ hen ∂0 else (−1)m·∂m+di -pol(m−1) Fo he de ini ion o gm,le pi,jdeno e he polynomial ηi∂j,wheni<j. Conside he ollowing ecu si e de ini ion: De ini ion: [gm] G-pol(m):= i m∈ N+ hen id else G-pol(m−1)·(id −pm−1,m) Some explana ion is needed o show why his de ini ion can be conside ed as a ecu si e e sion implemen ing he explici o mula conjec u ed in [23], ha we epea he e o ease he eading: gm=(−1)p i=1ai+biηap...η a1∂b1...∂ bp,whe e he indexes ange o e he aiand bisuch ha 0≤a1<b1<...<ap<bp≤m,wi h 0≤p≤(m+1)/2. Le us i s obse e ha , by applying he simplicial iden i ies: ηap...η a1∂b1...∂ bp=ηa1∂b1...η ap∂bp=pa1,b1...pap,bp The e o e, gmis he simplicial polynomial whose monomials a e (up o sign, +1 o −1) all he simplicial e ms which a e a p oduc o disjoin e ms pi,j(we called wo e ms pi1,j1and pi2,j2disjoin e ms i i1<j1<i2<j2) wi h subindexes less o equal han m. This is he idea allowing us o de ine ou ecu si e e sion o gm,as explained below. The composi e e ms pa1,b1...pap,bpcan be g ouped in o wo disjoin amilies, exp essing gmas a sum o wo polynomials: – P oduc s whe e bp<m, whose addi ion gi es ise o gm−1(including p=0), and – P oduc s whe e i s las ac o is pα,m,wi hα∈{0,...,m−1}. Then we claim ha he co esponding polynomial ob ained by adding all he ac o s in his amily is equal o −gm−1pm−1,m.Tha is,i α=m−1 he p oduc has he adequa e shape, and he sign changes because 2m−1is an odd numbe ; i α<m−1we can w i e pα,m=pα,m−1pm−1,m, and he sign changes because he second subindex has been dec eased by one. Thus, gm=gm−1−gm−1pm−1,m=gm−1(Id−pm−1,m)which is he implemen ed ecu si e de ini ion. Fo example, his is he esul ob ained when we compu e g3using he abo e de ini ion: idT−η0∂1+η0∂2−η0∂3−η1∂2+η1∂3−η2∂3+η2η0∂1∂3. Fo he ecu si e de ini ion o hm, we i s de ine a new amily o pa ame e ized polynomials, deno ed qm,in he ollowingway: De ini ion: [qm] Q-pol(m):= i m∈ N+ hen 0 else −Q-pol(m−1)·pm−1,m+(−1)m−1·ηm·gm−1·pm−1,m Now we de ine hmin he ollowing ecu si e way: De ini ion: [hm] H-pol(m):= i m∈ N+ hen η0 else H-pol(m−1)+(−1)m·ηm+qm Le us p o e he e ha his ecu si e de ini ion is equi alen o hm= (−1)ap+1+p i=1ai+biηap+1ηap...η a1∂b1...∂ bp, whe e he indexes ange o e 0≤a1< b1<...<ap<ap+1≤bp≤m,wi h0≤p≤(m+1)/2( he o mula conjec u ed in [23]). Asin hecaseo gm, we can desc ibe hmas he polynomial ha ing monomials ex ac ed (up o sign) om he exp essions: ηap+1pa1,b1...pap,bp,whe e0≤a1< b1<...<ap<ap+1≤bp≤m. Again, we ha e wo disjoin amilies o monomials: – P oduc s whe e bp<m, whose addi ion co esponds o hm−1+(−1)mηm(in- cluding p=0), and – P oduc s whe e i s las ac o is pα,m. Le us add all he polynomials in he second amily p oducing a polynomial called ˆ qm. The polynomial ˆ qmcan be, in u n, decomposed in o wo amilies: monomials s a ing om ηm(acco ding o he discussion on gm, hey co espond o ηm(gm− gm−1)=−ηmgm−1pm−1,m) and monomials s a ing om ηkwi h k<m, which can be exp essed as −ˆ qm−1pm−1,m(since ηk...pα,m=ηk...pα,m−1pm−1,m, p o ided ha ηk...pα,m−1appea s in ˆ qm−1; obse e ha he sign changes due o he dec easing o he subindex). This discussion p o es ha ˆ qmis equal o he polynomial qmde ined abo e, and shows he alidi y o he exp ession hm=hm−1+(−1)mηm+qm. As an example, he ollowing is he compu a ion o h3using he abo e de ini ion: η0−η1+η1η0∂1−η1η0∂2+η1η0∂3+η2+η2η0∂2−η2η0∂3−η2η1∂2+η2η1∂3−η3+ η3η0∂3−η3η1∂3+η3η2∂3−η3η2η0∂1∂3. 4.2 The main heo ems Ha ing de ined he unc ions, he ollowing a e he ACL2 heo ems es ablishing he main p ope ies ( ega ding he No maliza ion Theo em) o hose polynomials: Theo em: cmp-di -pol-di -pol=0 m∈N→dm·dm+1=0 Theo em: G-pol-on-degene a e=0 (m∈N∧i∈N∧i<m)→gm·ηi=0 Theo em: G-pol-and-di -pol-commu e m∈N→dm·gm=gm−1·dm Theo em: H-pol-p ope y-b m∈N+→dm+1·hm+hm−1·dm=id −gm We emphasize he ac ha in hese o mulas, +and · espec i ely deno e addi ion and composi ion o simplicial polynomials. Tha is, we p o e ha he abo e equali ies hold in he ing o simplicial polynomials. These p ope ies a e polynomial e sions o some o he esul s we need o p o e Theo em 2. In pa icula , cmp-di -pol-di -pol=0 is he polynomial e sion o he esul es ablishing ha dmis a di e en ial homomo phism; heo em G-pol-on-degene a e=0 gi es he beha io o gmon degene a e simplexes; G-pol-and-di -pol-commu e is he polynomial e sion o he esul ha s a es ha gmis a chain mo phism; and H-pol-p ope y-b will be essen ial o p o e p ope y (b) equi ed in he de ini ion o educ ion. These ou heo ems, al hough wi h subs an ial di e ences in i s di icul y, ha e been p o ed in a simila way: we apply induc ion on he na u al numbe s and use he p ope ies o he simplicial polynomial ing and he simplicial iden i ies, o p o e he induc i e case. To illus a e his, we desc ibe in he ollowing subsec ion a ske ch o he p oo o he heo em G-pol-and-di -pol-commu e.2We hope his desc ip ion will gi e he eade a la o o how we p o e p ope ies in he ing o simplicial polynomials. The p oo o he heo em H-pol-p ope y-b is by a he mos di icul , and we omi i s desc ip ion he e due o he lack o space. We u ge he in e es ed eade o consul he sou ce iles. 4.3 A ske ch o a p oo o dm·gm=gm−1·dm Le us i s gi e some lemmas ha will be used in he p oo . Fi s , he ollowing lemma es ablishes ha gmand ∂kcommu e when m<k: Lemma: G-pol-and- aces-commu e (m∈N∧k∈N∧m<k)→∂k·gm=gm·∂k This p ope y is easily p o ed by induc ion on m, and expanding he de ini ion o gm. Now we p o e a lemma ha es ablishes how we can commu e dmand pi,jwhen m<i<j. Again, his p ope y is easily p o ed by induc ion on m, and expanding he de ini ion o dm: Lemma: pij-pol-and-di -pol-commu e (n∈N∧i∈N∧j∈N∧m<i∧i<j)→pi−1,j−1·dm=dm·pi,j 2A ske ch o he p oo o he heo em cmp-di -pol-di -pol=0 was also gi en in Sec ion 2 and i s conc e e ACL2 ealiza ion is p esen ed in Appendix B. Le us now desc ibe he p oo o G-pol-and-di -pol-commu e,whichis p o ed by induc ion on m: •Base case: m=0.Thisis i ial,sinced0·id =id ·d0. •Induc i e case: suppose m>0and dm−1·gm−1=gm−2·dm−1. We will see how we can ew i e dm·gm o gm−1·dm. Fi s , we expand he de ini ions o gmand dm, and apply ing p ope ies: dm·gm=dm·gm−1·(id −pm−1,m)=(dm−1+(−1)m∂m)·gm−1·(id −pm−1,m) =dm−1·gm−1·(id −pm−1,m)+(−1)m·∂m·gm−1·(id −pm−1,m) We apply lemma G-pol-and- aces-commu e abo e and he induc ion hy- po hesis, ew i ing he las exp ession: gm−2·dm−1·(id −pm−1,m)+(−1)m·gm−1·∂m·(id −pm−1,m) No e ha using he simplicial iden i y (5), i is easy o p o e ∂m·(id −pm−1,m)= 0; using his iden i y and hen applying dis ibu i i y, we ob ain: gm−2·dm−1·(id −pm−1,m)=gm−2·(dm−1−dm−1·pm−1,m) Expanding he second occu ence o dm−1and applying dis ibu i i y, we ha e: gm−2·(dm−1−(−1)m−1·∂m−1·pm−1,m−dm−2·pm−1,m) Now, by he lemma pij-pol-and-di -pol-commu e, we ha e ha dm−2· pm−1,mis equal o pm−2,m−1·dm−2; and applying he simplicial iden i y (5)we p o e ∂m−1·pm−1,m=∂m. So we can simpli y he las exp ession (con ac ing also he de ini ion o dm) o he ollowing: gm−2·(dm−pm−2,m−1·dm−2) Finally, i is no di icul o p o e (using he simplicial iden i ies) ha pm−2,m−1· dm−2is equal o pm−2,m−1·dm; applying his o he las exp ession and ac o ing ou dmwe ob ain: gm−2·(id −pm−2,m−1)·dm=gm−1·dm The mechanical p oo o G-pol-and-di -pol-commu e is ca ied ou in ACL2 in a e y simila way o he hand p oo desc ibed abo e, guiding he p o e wi h he app op ia e lemmas and applying he same ew i ing s eps (al hough no necessa ily in he same di ec ion). As poin ed ou in Sec ion 3, he polynomial ing p ope ies, used as ew i ing ules, a e an essen ial componen in his p oo . 5 Re o mula ing he s a emen As we ha e seen, simplicial polynomials gi e us a con enien amewo k o ea- soning abou he simplicial maps and how hey combine acco ding o he simplicial iden i ies. In his amewo k we ha e p o ed non- i ial p ope ies abou hose combina ions, needed o he p oo o he No maliza ion Theo em. Ne e heless, being symbolic exp essions, wha we ha e p o ed is no a comple e and ai h ul o maliza ion o he s anda d o mula ion o his heo em in Simplicial Topology. Fo example, we ha e no de ined no ions like simplicial se s, chain complexes o degene a e simplexes. In his sec ion we show a o maliza ion o he No maliza ion Theo em in ACL2, as close as possible o he s anda d ma hema ical o mula ion p esen ed in Sec ion 2. We will also show how he heo ems p o ed in he polynomial amewo k can be ansla ed and used in his o maliza ion. 5.1 Simplicial se s and chain complexes I is clea ha he i s s ep in ou o maliza ion has o be he de ini ion o he no ion o simplicial se , as p esen ed in De ini ion 1. Since he heo em we wan o p o e is a esul on any simplicial se , we in oduce a gene ic simplicial se using he ACL2 encapsula ion p inciple. A simplicial se can be de ined by means o h ee unc ions K,dand n.The unc ion Kis a p edica e wi h wo a gumen s, wi h he idea ha K(m,x) holds i and only i x∈Km. The unc ions dand nha e bo h h ee a gumen s and hey ep esen he ace and degene acy maps, espec i ely. The in ended meanings o d(m,i,x)and n(m,i,x) a e espec i ely ∂m i(x)and ηm i(x). To be gene ic, he only assumed p ope ies abou K,dand na e hose s a ing well-de ineness and he simplicial iden i ies. They a e in oduced ia encapsula e: Assump ion: d-well-de ined (x∈Km∧m∈N+∧i∈N∧i≤m)→∂m i(x)∈Km−1 Assump ion: n-well-de ined (x∈Km∧m∈N∧i∈N∧i≤m)→ηm i(x)∈Km+1 Assump ion: simplicial-id1 (x∈Km∧m∈N∧i∈N∧j∈N∧j≤i∧i<m∧1<m) →∂m−1 i(∂m j(x)) =∂m−1 j(∂m i+1(x)) Assump ion: simplicial-id2 (x∈Km∧m∈N∧i∈N∧j∈N∧i≤j∧j≤m) →ηm+1 i(ηm j(x)) =ηm+1 j+1(ηm i(x)) Assump ion: simplicial-id3 (x∈Km∧m∈N∧i∈N∧j∈N∧i<j∧j≤m) →∂m+1 i(ηm j(x)) =ηm−1 j−1(∂m i(x)) Assump ion: simplicial-id4 (x∈Km∧m∈N∧i∈N∧j∈N∧j+1<i∧i−1≤m) →∂m+1 i(ηm j(x)) =ηm−1 j(∂m i−1(x)) Assump ion: simplicial-id5 (x∈Km∧m∈N∧i∈N∧j∈N∧i≤j≤i+1∧i≤m) →∂m+1 j(ηm i(x)) =x These assump ions a e a o maliza ion o he s anda d de ini ion o simplicial se , as gi en in any ex book, and cons i u e he basis whe e we will s a e he No maliza ion Theo em. To di e en ia e om he polynomial amewo k, we will call his he “s anda d amewo k”. The nex s ep is o de ine chain complexes in his s anda d amewo k. Since chains a e linea combina ions o simplexes o a gi en dimension, i is na u al o ep esen hem as lis s whose elemen s a e (do ed) pai s o med by an in ege and a simplex. As wi h simplicial polynomials, we will conside only chains in canonical o m: hei elemen s mus ha e non-null coe icien s and ha e o be inc easingly o de ed wi h espec o a s ic o de ing. The ollowing unc ion sc-p de ines chains in a gi en dimension m. I uses he unc ion ss-p ecognizing he do ed pai s o med by a non-null in ege and a m-simplex, and he unc ion ss-< implemen ing a s ic o de ing be ween such pai s (no e ha hese unc ions ake he dimension mas an a gumen ): De ini ion: ss-p(m,s):=(consp(s)∧ca (s)∈Z−{0}∧cd (s)∈Km) De ini ion: sc-p(m,c):= i endp(c) hen c=nil elsei endp(cd (c)) hen ss-p(m, i s (c)) ∧ es (c)=nil else ss-p(m, i s (c)) ∧ss-<(m, i s (c),second(c)) ∧ sc-p(m, es (c)) As wi h polynomials, he main ad an age o conside ing chains in canonical o m is ha we can check i s equali y using equal. The main ope a ions on chains a e addi ion and scala p oduc by an in- ege , o each dimension m. The ACL2 unc ions o hese ope a ions a e add-sc-sc(m,c1,c2)andscl-p d-sc(m,k,c). We omi hei de ini ions he e, be- cause hey a e e y simila o he co esponding ope a ions on polynomials. In his pape we will use c1+c2and k·c, espec i ely, o hose ope a ions on chains. No e ha , o he sake o eadabili y, we omi he dimension and ha we abuse o he no a ion using he same no a ion as wi h polynomials. Anyway, he p ecise meaning o e e y use o hese symbols will be clea om he con ex . We ha e p o ed ha he se o chains o a gi en dimension is an Abelian g oup wi h espec o addi ion, whe e he iden i y in his g oup is he ze o chain ( ep esen ed as nil and deno ed he e as 0). I is wo h men ioning ha , as we did in he case o polynomials, hese de ini ions and heo ems abou chains we e au oma ically gene a ed as a pa icula ins ance o a mo e gene ic heo y abou he ee Abelian g oup gene a ed by a gene ic basis. Simplicial maps can be linea ly ex ended on chains. Fo example, his is he de ini ion o c-d, he ace map ex ended o chains: De ini ion: [∂m i(c)] c-d(m,i,c):= i endp(c) hen c else cons(ca ( i s (c)),∂m i(cd ( i s (c)))) +c-d(m,i, es (c))) No e ha his unc ion is no a simple “mapca ” on he simplexes o a chain, since he esul is e u ned in canonical o m. In a simila way, we de ine c-n, he ex ension o he degene acy map o chains. We will use he same no a ion (∂m i(c)and ηm i(c)) o deno e hese maps bo h on simplexes and on chains. 5.2 E alua ion o simplicial polynomials As we ha e said be o e, ou in en ion is o ansla e he heo ems desc ibed in Sec ion 3 om he polynomial amewo k o he s anda d amewo k. The key poin he e is o in e p e a simplicial polynomial as a unc ion on chains o a gi en dimension. Recall om Sec ion 3.3 ha his will be only possible when he polynomial is well- o med o ha dimension. To de ine he unc ional beha iou o a simplicial polynomial, we simply apply he ope a ions indica ed in he symbolic exp ession. Fo example, he ollowing unc ion e al-ld is he e alua ion o a lis o aces ld on a chain co dimension m(whe e ld is expec ed o be alid o dimension m): De ini ion: e al-ld(ld,m,c):= i endp(ld) hen c else c-d(m-len( es (ld)), i s (ld), e al-ld( es (ld),m,c))) In a simila way, we can de ine he e alua ion o a lis o degene acies o a gi en dimension. Ex ending hese, we de ine he e alua ion o simplicial e ms (e al-s ) and he e alua ion o monomials (e al-sm). Finally, we de ine e al-sp, he e alua ion o a polynomial on a chain in a gi en dimension: De ini ion: e al-sp(p,m,c):= i endp(p) hen 0 else e al-sm( i s (p),m,c)+e al-sp( es (p),m,c)) The key p ope ies o he e alua ion unc ion we ha e jus de ined is ha o a gi en dimension, i beha es consis en ly wi h espec o he ope a ions o he ing o simplicial polynomials, whene e he inpu polynomials a e well- o med o ha dimension: Theo em: e al-sp-add-sp-sp (p1∈P∧p2∈P∧m∈N∧c∈Cm(K)∧uni o m-sp(p1)∧ uni o m-sp(p2)∧ alid-sp(p1,m)∧ alid-sp(p2,m)∧ (endp(p1)∨endp(p2)∨deg ee-sp(p1)=deg ee-sp(p2))) →e al-sp(p1+p2,m,c)=e al-sp(p1,m,c)+e al-sp(p2,m,c)) Theo em: e al-sp-scl-p d-sp (p∈P∧m∈N∧c∈Cm(K)∧uni o m-sp(p)∧ alid-sp(p,m)∧k∈Z) →e al-sp(k·p,m,c)=k·e al-sp(p,m,c) Theo em: e al-sp-cmp-sp-sp (p1∈P∧p2∈P∧m∈N∧c∈Cm(K)∧uni o m-sp(p1)∧ uni o m-sp(p2)∧ alid-sp(p1,m+deg ee-sp(p2)) ∧ alid-sp(p2,m)) →e al-sp(p1·p2,m,c)= e al-sp(p1,m+deg ee-sp(p2),e al-sp(p2,m,c)) These p ope ies allow us o ansla e in a con enien way he p ope ies p o ed in he polynomial amewo k o he co esponding p ope ies in he s anda d amewo k. We can illus a e his by showing how we p o e he di e en ial p op- e y. Recall ha he p ecise de ini ion (wi hou emo ing he supe indexes) o he di e en ial homomo phism is dm(c)=m i=0(−1)i∂m i(c). The ollowing is he co esponding ACL2 de ini ion in he s anda d amewo k. No e ha we need an auxilia y unc ion di -aux o deal p ope ly wi h he supe index: De ini ion: di -aux(m,i,c):= i i∈ N+ hen ∂m 0(c) else (−1)i·∂m i(c)+di -aux(m,i−1,c)) De ini ion: [dm(c)] di (m,c):=di -aux(m,m,c) The ollowing heo em es ablishes he connec ion be ween he di e en ial poly- nomial and he di e en ial unc ion, ia e al-sp: Theo em: e al-sp-di -pol (m∈N+∧c∈Cm(K)) →e al-sp(dm,m,c)=dm(c) Now, om he heo em cmp-di -pol-di -pol=0 in Sec ion 3,using he heo em e al-sp-cmp-sp-sp and p e iously p o ing ha dmis a polynomial well- o med o dimension mand wi h deg ee −1, we can easily p o e he di e en ial p ope y o he unc ion dm: Theo em: di -di =0 (m∈N+∧c∈Cm+1(K)) →dm(dm+1(c)) =0 5.3 The no malized chain complex We now desc ibe he o maliza ion o he no malized chain complex CN(K). Fi s o all we de ine degene a e simplexes, hose ha can be ob ained applying a degene acy map o ano he simplex: De ini ion: [x∈KD m] Kd(m,x):=∃y,i(i∈N∧i<m∧y∈Km−1∧ηm−1 i(y)=x) The exis en ial quan i ie in his de ini ion is in oduced using de un-sk,which is he way ACL2 p o ides suppo o i s -o de quan i ica ion. This mac o allows (by means o a choice axiom) o de ine unc ions whose body has an ou e mos quan i ie . Ha ing de ined degene a e simplexes, we de ine non-degene a e simplexes simply as he nega ion o ha p ope y: De ini ion: [x∈KND m] Kn(m,x):=x∈Km∧x∈ KD m Since no malized chains a e linea combina ions o non-degene a e simplexes o a gi en dimension, we ep esen hem in he same way as we ep esen gene al chains, bu in his case equi ing non-degene a e gene a o s. As wi h gene al chains, he heo y o no malized chains is ob ained as an ins ance o he gene ic heo y o eely gene a ed g oups. Tha is, his ins an ia ed heo y con ains he de ini ions and p ope ies showing ha no malized chains oge he wi h addi ion is an Abelian g oup. We also p o ed ha i is a subg oup o Cm(K)so i makes sense o deno e c1+c2 he addi ion o wo no malized chains c1and c2;andk·c he scala p oduc o an in ege kand a no malized chain c. Since in ou ep esen a ion an elemen x o CN m(K)is also an elemen o Cm(K)( ha is o say, he e is a canonical implici inclusion om CN m(K) o Cm(K), as se s), hen any unc ion de ined on Cm(K)can also be conside ed de ined on CN m(K); analogously, any unc ion anging o e CN m(K) will be in e p e ed, implici ly, as anging o e Cm(K), oo. We de ine he canonical epimo phism :C(K)→CN(K)as he unc ion ha , gi en an elemen o Cm(K), e u ns he no malized chain ob ained elimina ing i s degene a e addends. In ou o maliza ion, he ollowing unc ion F-no m de ines (he e SSn-P checks he p ope y o being a non-degene a e addend, and i uses he unc ion Kn abo e): De ini ion: [ m(c)] F-no m(m,c):= i endp(c) hen 0 elsei SSn-P(m, i s (c)) hen i s (c)+F-no m(m, es (c))) else F-no m(m, es (c)) A key p ope y ela ing he canonical chain epimo phism and he di e en ial on C(K)is he ollowing: m−1(dm( m(c))) = m−1(dm(c)). In ui i ely, his means ha i we apply no maliza ion on he esul o he di e en ial o a chain, we ob ain he same esul as i we apply he same ope a ion p e iously no malizing he chain. A ske ch o he p oo o his esul is he ollowing: gi en a chain c∈Cm(K),wecan w i e i as he esul o summing i s no maliza ion and a linea combina ion o de- gene a e simplexes: c= m(c)+kλk·ηm−1 ik(y). Thus, dm(c)=dm( m(c)) +kλk· dm(ηm−1 ik(y)). F om he de ini ion o dmand applying he simplicial iden i ies, i can be p o ed ha dm(ηm−1 j(y)) is s ill a linea combina ion o degene a e simplexes ( his is he essen ial p ope y p o ing ha he degene a e chain complex D(K), in oduced in Sec ion 2.1, is a chain subcomplex o C(K)). Thus, kλk·dm(ηm−1 ik(y)) is a linea combina ion o degene a e simplexes and he e o e m−1(dm(c)) = m−1(dm( m(c))). The ollowing heo em es ablishes his esul : Theo em: di -n-F-no m (m∈N+∧c∈Cm(K)) → m−1(dm( m(c))) = m−1(dm(c)) Le us now de ine he di e en ial ope a ion o he no malized chain complex CN(K), deno ed as dN m(c). We will de ine i as he esul o applying he di e en ial dm, and a e ha , no malizing wi h m−1. De ini ion: [dN m(c)] di -n(m,c):= m−1(dm(c)) The di e en ial p ope y o din C(K)( heo em di -di =0 in he las subsec ion), oge he wi h he p ope y di -n-F-no m, allows us o p o e he di e en ial p ope y o dNin CN(K), since o all c∈CN m(K),dN m(dN m+1(c)) = m−1(dm( m(dm+1(c)))) = m−1(dm(dm+1(c))) = m−1(0)=0. The ollowing heo em es ablishes i : Theo em: di -n-di -n=0 (m∈N+∧c∈CN m+1(K)) →dN m(dN m+1(c)) =0 6.2 The no malized chain complex In ou app oach o he p oblem, in o de o build o each simplicial se Ka educ ion ( ,g,h):C(K)→CN(K), we ha e de ined, by means o explici o mulas, wo amilies o simplicial polynomials gmand hm(see Sec ion 4.1).Fo hesakeo simplici y, le us deno e by Gin his subsec ion he unc ion de ined on C(K)by gm. Obse e ha he exp ession o G(as in he case o he homo opy ope a o h)is independen om he simplicial se K(and om he e alua ion o simplicial ope a- o s o e simplexes), while ( he canonical p ojec ion) equi es o i s de ini ion a es unc ion, de e mining whe he a gi en simplex is degene a e o no . This implies ha depends on K, and, as a consequence, i canno be ep esen ed as a simplicial polynomial. This is he eason why in he o mal p oo he mo phism does no appea un il Sec ion 5. Howe e , he e y de ini ion o CN(K)as a quo ien in he ca ego y o chain complexes ( ecall: CN(K)=C(K)/D(K)) es ablishes ha o de ine a chain mo phism om CN(K) o ano he chain complex Camoun s o de ining a chain mo phism o m C(K) o Cwhich is null on D(K). In pa icula , he mo phism G:C(K)→C(K)is null on degene a ed simplexes (i has been p o ed in ACL2 by using he G-pol-on-degene a e=0 p ope y) and i allows us o de ine g: CN(K)→C(K)as he unique chain mo phism such ha g◦ =G, iden i ying wi h he canonical quo ien map. Le us no e ha , in Sec ion 5, a e sion sligh ly di e en has been used, conside ing CN(K)as a e ac o C(K)in he ca ego y o g aded Abelian g oups. In o he wo ds, we ake as de ini ion CN n(K)=Z[KND n]. In his case, we ha e he diag am C(K) --CN(K), i llwi h an explici de ini ion o , in oducing dN:= ◦d◦iand checking ha G=G◦i◦ , we ob ain a chain mo phism g:= G◦i. Wi h his p esen a ion he equi ed p e educ ion p ope ies ollow easily om o he s p o ed in he simplicial amewo k. 6.3 Simplicial e ms and dimension The equi alence be ween na u al ans o ma ions and simplicial polynomials de- sc ibed in Sec ion 6.1 allowed us o educe he ini ial p oblem o deal wi h simplicial polynomials plus one dimension. Ou ACL2 p oo , desc ibed in Sec ion 4,was howe e ca ied ou o e simplicial polynomials wi hou any dimension in o ma ion. The eason o his hi d, and las , simpli ica ion is now explained. Le us in e p e i(which skips he elemen i∈N)andδj(which co e j∈N wice) as o de - p ese ing maps om N o N. We deno e by N he monoid o maps gene a ed (by composi ion) om {i,δj;∀i,j∈N}. The elemen s o Na e exac ly he o de - p ese ing maps om N o Ncon aining a ini e amoun o in o ma ion: hey s abilize om a gi en numbe ( ha is, a unc ion γ:N→Nsuch ha he e exis s 0∈N sa is ying γ( +1)=γ( )+1,∀ > 0). The elemen s in Ncan be ep esen ed in canonical o m as explained o mo phisms o he ca ego y . This p o es ha , as monoids, he e is a canonical isomo phism be ween Nand ou monoid o simplicial e ms ( he isomo phism being simply induced by con a a iance). In Sec ion 4we ha e wo ked wi h simplicial e ms wi hou dimension, ha is o say wi h maps in Nand no in . We can now hink in Nas a (monoidal) ca ego y wi h only one objec , and mo phisms he elemen s o he monoid. We can conside he unc o (−)#:→Nwhich comple es each mo phism α:[n]→[m]o ,by s abilizing i in he ollowing way: α#(k)=α(k)i k≤nand α#(k)=m+(k−n)i k>n. This is ac ually a unc o ; in pa icula , (α ◦β)#=α#◦β#. Mo eo e (−)#is ai h ul, ha is o say: gi en wo mo phisms α, β :[n]→[m]such ha α#=β# hen α=β. In o he s wo ds, equa ional easoning abou simplicial ope a o s can be sa ely simula ed o e simplicial e ms, wi hou any e e ence o he dimensions whe e he simplicial ope a o s apply. The same a gumen can be used in he ing o simplicial polynomials (de ined as he ee Abelian g oup on he monoid o simplicial e ms), showing ha any chain o equali ies deduced om combina ions o e mo phisms o he monoidal ca ego y Nalso holds in he alid dimensions. Thus, he comple e p oo o he No maliza ion Theo em can be de eloped in a i s o de se ing by using equa ional easoning on simplicial polynomials wi hou explici dimensions, as i has been done in ACL2 in Sec ion 4, and i can be exp essed as in Sec ion 5by simply adding he alidi y condi ion among e ms and dimensions. 7 Conclusions and u he wo k In his pape we ha e o malized he No maliza ion Theo em, an impo an esul in simplicial opology es ablishing a link be ween he wo chain complexes ha can be na u ally associa ed o a simplicial se . An ou s anding ea u e o ou o maliza ion is ha i has been ca ied ou in a i s -o de logic, e en hough in p inciple a highe - o de se ing could be conside ed mo e na u al o s a e i . As a demons a ion o his cha ac e is ic we ha e implemen ed he whole p oo in he ACL2 heo em p o e (we hope he echniques in oduced ha e been explained in his pape wi h enough de ail o be e-p oduced in o he induc i e easoning en i onmen s, oo). Ano he in e es ing bene i ob ained om ou p oo is ha i was inspi ed by some explici o mulas expe imen ally ound in [23], showing he alidi y o he o mulas, which kep up o now unp o en. To quan i y he p oo e o , he comple e o maliza ion con ains 100 de ini ions and 532 lemmas and heo ems (wi h 89 non i ial p oo hin s explici ly gi en), which gi es an idea o he deg ee o au oma ion o he p oo . As o he o maliza ion de elopmen , we ollowed a s anda d in e ac ion wi h he heo em p o e . Tha is, we i s had an o iginal hand p oo o he esul ha sugges ed he main de ini ions and lemmas. Some o hese lemmas we e no p o ed in a i s a emp and new lemmas a e hen sugges ed om he inspec ion o he ailed a emp s. I is also wo h poin ing ou ha he whole de elopmen has bene i ed om he use o ou ins an ia ion ool o gene ic heo ies desc ibed in [17]. Tha allowed us o ob ain in an au oma ed way, he de ini ions and heo ems p o ing he ing o simplicial polynomials and he Abelian g oup o chains and no malized chains, as ins ances o gene ic heo ies (we ha e no included hese au oma ically gene a ed de ini ions and lemmas in he s a is ics abo e). The planned u u e wo k is ying o ex end he echniques in oduced he e (based on simplicial polynomials) o o he p oblems in simplicial opology. Ou nex objec i e is he Eilenbe g–Zilbe Theo em [9,19]. I is a e y impo an esul gi ing a educ ion be ween he chain complex o a Ca esian p oduc o simplicial se s, CN(A×B), and he enso p oduc o he co esponding chain complexes o he ac- o s, CN(A)⊗CN(B). The associa ed algo i hm (in i s mos explici e sion, a ows ,g,ha e desc ibed by explici o mulas; see he Appendix in [21]) is e y impo an in Kenzo, being esponsible o a g ea pa o he (exponen ial) complexi y o many Kenzo p og ams. Thus he ask o o malizing i can be conside ed a good nex s ep o ou p ojec . The esul s in Sec ion 6show ha he e a e ca ego ical easons o hink ha he Eilenbe g–Zilbe Theo em could be ackled in a i s o de se ing. F om he ACL2 poin o iew, he challenge is ha in he Eilenbe g–Zilbe Theo em he e a e wo simplicial se s in ol ed, and hen he scope o ou echniques should be signi ican ly ex ended o be applied in ha case. Acknowledgemen s We hank he anonymous e e ees o hei ca e ul e ision and use ul eed- back. Appendix A: Checking he o malized p oo To check ou o malized p oo in ACL2, he sys em has o be p ope ly ins alled and he books ha come wi h he dis ibu ion ce i ied. De ails abou he ins alla ion o ACL2 can be ob ained in sec ion Ob aining and Ins alling a he web page h p://www.cs.u exas.edu/use s/moo e/acl2/. The comple e sou ce iles wi h he ACL2 o maliza ion o he No maliza ion Theo em a e accessible a : h p://www.glc.us.es/ ma in/acl2/ an is in a ile named an is . gz. This ile should be expanded wi h he command: ...> a -xz an is . gz This command builds he di ec o y an is wi h he whole o maliza ion. To ce i y he o maliza ion, he ollowing command should be execu ed in he an is di ec o y: ...> cd an is .../ an is > make -s all This command ce i ies all he books. I gene a es iles .o,.ce and .da e o e e y book in he dis ibu ion. A ile .log is also c ea ed con aining he ACL2 ce i ica ion ou pu co esponding o e e y book. Appendix B: ACL2 p oo o CMP-DIFF-POL-DIFF-POL=0 ACL2 !>(DEFTHM CMP-DIFF-POL-DIFF-POL=0 (IMPLIES (NATP N) (EQUAL (CMP-SP-SP (DIFF-POL N) (DIFF-POL (1+ N))) (ADD-SP-SP-ID))) :HINTS (("Goal" :IN-THEORY (ENABLE (DI))))) [No e: A hin was supplied o ou p ocessing o he goal abo e. Thanks!] By he simple: de ini ion NATP and he :execu able-coun e pa o ADD-SP-SP-ID we educe he conjec u e o Goal’ (IMPLIES (AND (INTEGERP N) (<= 0 N)) (EQUAL (CMP-SP-SP (DIFF-POL N) (DIFF-POL (+ 1 N))) NIL)). This simpli ies, using he :compound- ecognize ules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER, he:de ini ion DIFF-POL, p imi i e ype easoning, he : ew i e ules |1-1+N|, ADD-SP-SP-COMMUTATIVE, CMP-SP-SP-ADD-SP-SP-DISTRIBUTIVE-R, COMMUTATIVITY-2-OF-+, DIFF-POL-SP, SCL-PRD-SP-CMP-SP-SP-2, SP-P-DI and SP-P-SCL-PRD-SP and he : ype-p esc ip ion ule EXP-1, o Goal’’ (IMPLIES (AND (INTEGERP N) (<= 0 N)) (NOT (ADD-SP-SP (CMP-SP-SP (DIFF-POL N) (DIFF-POL N)) (SCL-PRD-SP (EXP-1 (+ 1 N)) (CMP-SP-SP (DIFF-POL N) (DI (+ 1 N))))))). Name he o mula abo e *1. Pe haps we can p o e *1 by induc ion. Th ee induc ion schemes a e sugges ed by his conjec u e. Subsump ion educes ha numbe o one. We will induc acco ding o a scheme sugges ed by (DIFF-POL N). This sugges ion was p oduced using he :induc ion ule DIFF-POL. I we le (:P N) deno e *1 abo e hen he induc ion scheme we’ll use is AND (IMPLIES (AND (NOT (ZP N)) (:P (+ -1 N))) (:P N)) (IMPLIES (ZP N) (:P N))). This induc ion is jus i ied by he same a gumen used o admi DIFF-POL. When applied o he goal a hand he abo e induc ion scheme p oduces ou non au ological subgoals. Subgoal *1/4 (IMPLIES (AND (NOT (ZP N)) (NOT (ADD-SP-SP (CMP-SP-SP (DIFF-POL (+ -1 N)) (DIFF-POL (+ -1 N))) (SCL-PRD-SP (EXP-1 (+ 1 -1 N)) (CMP-SP-SP (DIFF-POL (+ -1 N)) (DI (+ 1 -1 N)))))) (INTEGERP N) (<=0N)) (NOT (ADD-SP-SP (CMP-SP-SP (DIFF-POL N) (DIFF-POL N)) (SCL-PRD-SP (EXP-1 (+ 1 N)) (CMP-SP-SP (DIFF-POL N) (DI (+ 1 N))))))). Bu simpli ica ion educes his o T, using he :compound- ecognize ules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER, he :de ini ions ADD-SP-SP, DIFF-POL and SCL-PRD-SP, he :execu able-coun e pa s o ADD-SP-SP-ID, CONSP, SP-P and ZIP, linea a i hme ic, p imi i e ype easoning, he : ew i e ules |1-1+N|, ADD-SP-SP-COMMUTATIVE, ADD-SP-SP-COMMUTATIVE-2, ADD-SP-SP-NOT-CONSP, CMP-DIFF-POL-DIFF-POL=0-LEMMA-INDUCT-CASE, CMP-SP-SP-ADD-SP-SP-DISTRIBUTIVE-L, CMP-SP-SP-ADD-SP-SP-DISTRIBUTIVE-R, DIFF-POL-SP, EXP-1-PRODUCT-CONSECUTIVE, EXP-1-PRODUCT-EQUAL, EXP-1-SUM-CONSECUTIVE, SCL-PRD-SP-1, SCL-PRD-SP-1-INVERSE, SCL-PRD-SP-ADD-SP-SP-DISTRIBUTIVE-L, SCL-PRD-SP-ADD-SP-SP-DISTRIBUTIVE-R, SCL-PRD-SP-ASSOCIATIVE, SCL-PRD-SP-CMP-SP-SP-1, SCL-PRD-SP-CMP-SP-SP-2, SIMPLICIAL-EQ1, SP-P-ADD-SP-SP, SP-P-CMP-SP-SP, SP-P-DI and SP-P-SCL-PRD-SP and he : ype-p esc ip ion ule EXP-1. Subgoal *1/3 (IMPLIES (AND (NOT (ZP N)) (< (+ -1 N) 0) (INTEGERP N) (<=0N)) (NOT (ADD-SP-SP (CMP-SP-SP (DIFF-POL N) (DIFF-POL N)) (SCL-PRD-SP (EXP-1 (+ 1 N)) (CMP-SP-SP (DIFF-POL N) (DI (+ 1 N))))))). Bu we educe he conjec u e o T, by he :compound- ecognize ule ZP-COMPOUND-RECOGNIZER and p imi i e ype easoning. Subgoal *1/2 (IMPLIES (AND (NOT (ZP N)) (NOT (INTEGERP (+ -1 N))) (INTEGERP N) (<=0N)) (NOT (ADD-SP-SP (CMP-SP-SP (DIFF-POL N) (DIFF-POL N)) (SCL-PRD-SP (EXP-1 (+ 1 N)) (CMP-SP-SP (DIFF-POL N) (DI (+ 1 N))))))). Bu we educe he conjec u e o T, by he :compound- ecognize ule ZP-COMPOUND-RECOGNIZER and p imi i e ype easoning. Subgoal *1/1 (IMPLIES (AND (ZP N) (INTEGERP N) (<= 0 N)) (NOT (ADD-SP-SP (CMP-SP-SP (DIFF-POL N) (DIFF-POL N)) (SCL-PRD-SP (EXP-1 (+ 1 N)) (CMP-SP-SP (DIFF-POL N) (DI (+ 1 N))))))). Bu simpli /ica ion educes his o T, using he :compound- ecognize ule ZP-COMPOUND-RECOGNIZER, he :execu able-coun e pa s o <, ADD-SP-SP, BINARY-+, CMP-SP-SP, DI, DIFF-POL, EXP-1, INTEGERP, NOT, SCL-PRD-SP and ZP and linea a i hme ic. Tha comple es he p oo o *1. Q.E.D. ... Time: 0.56 seconds (p o e: 0.51, p in : 0.03, o he : 0.02) CMP-DIFF-POL-DIFF-POL$=$0 Re e ences 1. And és, M., Lambán, L., Rubio, J., Ruiz-Reina, J.L.: Fo malizing simplicial opology in ACL2. In: P oceedings ACL2 Wo kshop 2007, pp. 34–39. Uni e si y o Aus in (2007) 2. A ansay, C., Balla in, C., Rubio, J.: A mechanized p oo o he basic pe u ba ion lemma. J. Au om. Reason. 40(4), 271–292 (2008) 3. A ansay, C., Balla in, C., Rubio, J.: Gene a ing ce i ied code om o mal p oo s: a case s udy in homological algeb a. Fo m. Asp. Compu . 22(2), 193–213 (2010) 4. Coquand, T., Spiwack, A.: Towa ds cons uc i e homological algeb a in ype heo y. In: Calcule- mus 2007, Lec u e No es in A i icial In elligence, ol. 4573, pp. 40–54. Sp inge (2007) 5. De Loe a, J.A., Rambau, J., San os, F.: T iangula ions. S uc u es o Algo i hms and Applica- ions. Sp inge (2010) 6. Domínguez, C., Lambán, L., Rubio, J.: Objec -o ien ed ins i u ions o speci y symbolic compu- a ion sys ems. Rai o-Theo . In o m. Appl. 41, 191–214 (2007) 7. Domínguez, C., Rubio, J.: Compu ing in coq wi h in ini e algeb aic da a s uc u es. In: Calcule- mus 2010, Lec u e No es in A i icial In elligence, ol. 6167, pp. 204–218. Sp inge (2010) 8. Dousson, X., Se ge ae , F., Si e , Y.: The Kenzo P og am. Ins i u Fou ie , G enoble (1999) h p://www- ou ie .uj -g enoble. /~se ge a /Kenzo/ 9. Eps ein, D.B.A.: Semisimplicial objec s and he Eilenbe g–Zilbe heo em. In en . Ma h. 1, 209– 220 (1966) 10. He as, J., Pascual, V., Rubio, J.: P o ing wi h ACL2 he co ec ness o simplicial se s in he Kenzo sys em. In: LOPSTR 2010, Lec u e No es in Compu e Science, ol. 6564, pp. 37–51. Sp inge (2010) 11. Kau mann, M., Manolios, P., Moo e, J S.: Compu e -Aided Reasoning: An App oach. Kluwe (2000) 12. Lambán, L., Pascual, V., Rubio, J.: An objec -o ien ed in e p e a ion o he EAT Sys em. Appl. Algeb a Eng. Commun. Compu . 14(3), 187–215 (2003) 13. Lambán, L., Ma ín–Ma eos, F.J., Rubio, J., Ruiz–Reina, J.L.: Applying ACL2 o he o maliza- ion o algeb aic opology: simplicial polynomials. In: In e ac i e Theo em P o ing 2011, Lec u e No es in Compu e Science, ol. 6898, pp. 200–215. Sp inge (2011) 14. Mac Lane, S.: Homology. Sp inge (1963) 15. Mac Lane, S.: Ca ego ies o he Wo king Ma hema ician. Sp inge (1971) 16. Mac Lane, S., Moe dijk, I.: Shea es in Geome y and Logic. Sp inge (1992) 17. Ma ín–Ma eos, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz–Reina, J.L.: A gene ic ins an ia ion ool and a case s udy: a gene ic mul ise heo y. In: P oceedings o he Thi d In e na ional ACL2 Wo kshop and i s Applica ions, pp. 188–201 (2002) 18. Ma ín–Ma eos, F.J., Rubio, J., Ruiz–Reina, J.L.: ACL2 e i ica ion o simplicial degene acy p og ams in he Kenzo sys em. In: Calculemus 2009, Lec u e No es in A i icial In elligence, ol. 5625, pp. 106–121. Sp inge (2009) 19. May, J.P.: Simplicial Objec s in Algeb aic Topology. Van Nos and (1967) 20. Medina–Bulo, I., Palomo–Lozano, F., Ruiz–Reina, J.L.: A e i ied common lisp implemen a ion o Buchbe ge ’s algo i hm in ACL2. J. Symb. Compu . 45(1), 96–123 (2010) 21. Real, P.: Homological pe u ba ion heo y and associa i i y. Homol. Homo opy Appl. 2(5), 51–88 (2000) 22. Rome o, A.: E ec i e homology and spec al sequences. PhD Thesis. Uni e sidad de La Rioja (2007). A ailable a : h p://www.uni ioja.es/cu/an ome o/ esis.pd 23. Rubio, J., Se ge ae , F.: Suppo s acycliques and algo i hmique. As é isque 192, 35–55 (1990) 24. Rubio, J., Se ge ae , F.: Cons uc i e algeb aic opology. Bull. Sci. Ma h. 126, 389–412 (2002)