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)