Fo mal Reasoning abou Efficien Da a
S uc u es: A Case S udy in ACL2
Jos´e Luis Ruiz-Reina, Jos´e An onio Alonso-Jim´enez,
Ma ´ıa Jos´e Hidalgo, and F ancisco Jes´us Ma ´ın-Ma eos
Compu 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
h p://www.cs.us.es/{~j uiz,~jalonso,~mjoseh,~ ma in}
Abs ac . We desc ibe in his pape he o mal e ifica ion, using he
ACL2 sys em, o a syn ac ic unifica ion algo i hm whe e e ms a e ep-
esen ed as di ec ed acyclic g aphs (dags) and hese g aphs a e s o ed
in a single- h eaded objec (s obj). The use o s objs allows des uc i e
ope a ions on da a ( hus imp o ing he pe o mance o he algo i hm),
while main aining he applica i e seman ics o ACL2. We in end o show
how ACL2 p o ides an en i onmen whe e execu ion o algo i hms wi h
efficien da a s uc u es and o mal easoning abou hem can be ca ied
ou .
1 In oduc ion
The ACL2 sys em includes a p og amming language, a logic o o mal eason-
ing abou he p ope ies o he unc ions defined in he language, and a heo 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 a fi s -o de logic wi h equali y, wi hou quan ifie s (all he o mulas a e im-
plici ly uni e sally quan ified).
Since he p og amming language is applica i e, logical a gumen s abou he
co ec ness and e mina ion o algo i hms a e made as hey a e in o dina y ma h-
ema ics, wi hou he complica ions incu ed by conside a ion o s a e. No wi h-
s anding, i is possible o decla e some objec s in he language as single- h eaded
objec s (in he sequel, s objs) and pe o m des uc i e upda es on hem. When
an objec is decla ed o be single- h eaded, ACL2 en o ces ce ain syn ac ic e-
s ic ions on i s use, ensu ing ha in e e y momen only one copy o he objec
is needed. Wi h hese es ic ions, he des uc i e upda es a e consis en wi h
he applica i e seman ics o ACL2. Using s objs we can combine efficien im-
pe a i e implemen a ions wi h he seman ic o unc ional languages o eason
abou hese implemen a ions.
This wo k has been suppo ed by p ojec TIC2000-1368-C03-02 (Minis y o Science
and Technology, Spain) and FEDER unds.
In his pape we p esen a case s udy whe e we use ACL2 o implemen and
e i y a unifica ion algo i hm. A s anda d app oach in he implemen a ion o
unifica ion is o ep esen e ms as di ec ed acyclic g aphs (dags in he ollowing),
allowing some amoun o s uc u e sha ing; in his way, i is no needed o build
new e ms du ing he unifica ion p ocess, bu me ely upda e (des uc i ely) he
g aph, hus imp o ing he pe o mance o he algo i hm. In ou implemen a ion,
he dags will be s o ed using a s obj.
To achie e he o mal p oo , we ollow he well-known me hodology o compo-
si ional easoning. As a fi s s ep, we eason abou unifica ion a a e y abs ac
le el, wi hou en e ing in de ails ela ed o he con ol o he algo i hm o he
da a s uc u es used. By s epwise- efinemen , we finally ob ain he p oo o he
desi ed p ope ies o ou conc e e unifica ion algo i hm.
Ano he in e es ing poin in his case s udy is he use o a new ea u e in
ACL2 ( he mbe ea u e) ha associa es an “execu able body” wi h a (possibly
diffe en ) “logical body”. This associa ion will be allowed by he sys em a e
p o ing ha on he in ended domain o he unc ion, he execu able body and
he logical body a e equal. We desc ibe his new ea u e o ACL2, and explain
how i can be used o imp o e he execu ion efficiency o he e ified unifica ion
algo i hm.
Al hough we will no gi e an in oduc ion o ACL2, we will commen he
ele an ques ions in passing, when needed. An excellen in oduc ion o ACL2
is [5]. A de ailed desc ip ion o he sys em can be ound in he manual, a ailable
in [6]. We will assume he eade amilia wi h Common Lisp. 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. We u ge he in e es ed eade o consul [11], whe e
he comple e de elopmen (wi h a de ailed desc ip ion) is a ailable.
2DagUnifica ion
We b iefly e iew some basic concep s abou (syn ac ic) unifica ion, a unda-
men al p ocess upon which many me hods o au oma ed deduc ion a e based. A
comple e desc ip ion o he heo y o unifica ion can be ound in [2].
An equa ion is a pai o fi s -o de e ms, deno ed as 1≈ 2,andasys em
o equa ions is a fini e se o equa ions. A subs i u ion σis a solu ion o 1≈ 2
i σ( 1)=σ( 2) and i is a solu ion o a sys em o equa ions Si i is a solu ion
o e e y equa ion in S. Gi en wo subs i u ions σand δ,wesay ha σis mo e
gene al han δi he e exis s a subs i u ion γsuch ha δ=γ◦σ,whe e◦deno es
unc ional composi ion. We say ha a solu ion o Sis a mos gene al solu ion i
i is mo e gene al han any o he solu ion o S.Two e ms 1and 2a e uni iable
i he e exis s a solu ion (called uni ie ) o he sys em { 1≈ 2}.Amos gene al
uni ie (mgu in he sequel) o 1and 2is a mos gene al solu ion o ha sys em.
Auni ica ion algo i hm is an algo i hm ha decides whe he wo gi en e ms
a e unifiable, and in ha case i e u ns a mos gene al unifie .
Essen ially, he unifica ion algo i hm we ha e implemen ed is based on he
ela ion ⇒ugi en by he se o ans o ma ion ules p esen ed in Figu e 1 (known
Dele e: { ≈ }∪R;U⇒uR;U
Occu -check: {x≈ }∪R;U⇒u⊥i x∈V( )andx=
Elimina e: {x≈ }∪R;U⇒uθ(R); {x≈ }∪θ(U)
i x∈X,x/∈V( )andθ={x→ }
Decompose: { (s1, ..., sn)≈ ( 1, ..., n)}∪R;U⇒u{s1≈ 1, ..., sn≈ n}∪R;U
Clash: { (s1, ..., sn)≈g( 1, ..., m)}∪R;U⇒u⊥i n=mo =g
O ien : { ≈x}∪R;U⇒u{x≈ }∪R;Ui x∈X, /∈X
Fig. 1. Ma elli–Mon ana i ans o ma ion sys em
as he Ma elli-Mon ana i ans o ma ion sys em). This sys em ac s on pai s o
sys ems o equa ions o he o m S;U. In ui i ely, he sys em Scan be seen as a
se o pai s o e ms o be unified, and he sys em Uas a (pa ially) compu ed
unifie 1(we say ha he pai S;Uis a uni ica ion p oblem). The symbol ⊥
ep esen s unifica ion ailu e. S a ing wi h he pai o sys ems S;∅, hese ules
can be (non-de e minis ically) applied i e a i ely, un il ei he a pai o sys ems o
he o m ∅;Uo ⊥is ob ained. I can be p o ed ha his p ocess mus e mina e
and ha Shas a solu ion i and only i ⊥is no de i ed; in ha case Uis a mos
gene al solu ion o S. Thus, a unifica ion algo i hm can be designed choosing an
s a egy o apply he ules, s a ing wi h he pai o sys ems { 1≈ 2};∅,whe e
1and 2a e wo gi en inpu e ms.
In [10] we had defined and e ified a unifica ion algo i hm based on his se
o ans o ma ion ules, as pa o an ACL2 lib a y wi h o mal p oo s o he
la ice- heo e ic p ope ies o fi s -o de e ms. In ha lib a y, e ms a e ep e-
sen ed in p efix no a ion, using lis s (excep a iables, which a e ep esen ed by
a omic objec s). Fo example, he e m (x, g(y),h(x)) is ep esen ed by he lis
( x(gy)(hx)). Subs i u ions a e ep esen ed as associa ion lis s, and sys-
ems o equa ions as lis s o do ed pai s o e ms. In he sequel, his ep esen-
a ion o e ms and subs i u ions in p efix o m, using lis s, will be e e ed o
as p e ix ep esen a ion o p e ix no a ion.
Using he p efix ep esen a ion, a unifica ion algo i hm may be inefficien
in some si ua ions. Conside , o example, he ollowing s anda d pa ame e ized
unifica ion p oblem, which we will call Un:
p(xn,...,x
2,x
1)≈p( (xn−1,x
n−1),..., (x1,x
1), (x0,x
0))
A mgu o his p oblem is {x1→ (x0,x
0),x
2→ ( (x0,x
0), (x0,x
0)),...},
which maps each a iable xi o a comple e bina y ee o heigh i.Thismgu
can be ob ained by epea edly applying he Elimina e ule o ⇒u.I weuse he
p efix ep esen a ion o e ms, i will be necessa y o econs uc he ins an ia ed
sys em o equa ions, each ime he ule is applied.
1We will iden i y a sys em o equa ions o he o m {x1≈ 1,...,x
n≈ n},whe e
he xia e a iables, wi h he subs i u ion {x1→ 1,...,x
n→ n}.I noneo hexi
appea in any o he j, we say ha he sys em is in sol ed o m.No e ha e e y
sys em in sol ed o m is a mgu o i sel .
The s anda d app oach o deal wi h his p oblem is o use e m dags whe e
a iables a e sha ed. Fo example, he ollowing g aph ep esen s he equa ion
(h(z),g(h(x),h(u))) ≈ (x, g(h(u), )). Nodes a e labeled wi h unc ion and
a iable symbols, and ou going edges connec e e y node wi h dags ep esen -
ing i s immedia e sub e ms. We can na u ally iden i y he oo node o a e m
dag wi h he whole e m. No e also ha he e is a ce ain amoun o s uc u e
sha ing, a leas o he epea ed a iables2:
gg
hhh
To implemen a unifica ion algo i hm wi h his e m ep esen a ion, he main
idea is ne e o build new e ms bu only c ea e poin e s. In pa icula , he
Elimina e ule can be implemen ed adding a poin e linking he a iable wi h
he e m o which his a iable is bound; in ha way no econs uc ion o he
e m is equi ed in he applica ion o a subs i u ion. In he g aph abo e, hese
poin e s a e ep esen ed by dashed a ows. The binding o a a iable can be
de e mined by ollowing he poin e s a e sing he g aph dep h fi s , om le
o igh . In his case, he subs i u ion ep esen ed is {x→ h(z),u → h(z), →
h(h(z))}, which is a mgu o (h(z),g(h(x),h(u))) and (x, g(h(u), )).
3 An ACL2 Implemen a ion
The implemen a ion desc ibed he e is based on he Pascal implemen a ion gi en
in sec ion 4.8 o [1]. The main diffe ence is ha ins ead o a eco d wi h poin e s,
we use a single- h eaded objec . This s obj is a s uc u e called e ms-dag wi h
only one field: an a ay called dag (whose size can be modified dynamically).
This a ay is used o s o e he unifica ion p oblem in dag o m:
(de s obj e ms-dag
(dag : ype (a ay (0)) : esizable ))
The effec o his ACL2 e en is o in oduce he s obj e ms-dag and i s
associa ed ecognize s, c ea o , accesso s, upda e s, and leng h and esize unc-
ions o he a ay field. In pa icula , gi en an index i(a na u al numbe ) co -
esponding o a cell o he dag a ay, he exp essions (dagi i e ms-dag) and
(upda e-dagi i e ms-dag) access and upda e (wi h alue ) espec i ely
he i- h cell o he dag a ay. These ope a ions a e done in cons an ime and he
2I should be ema ked ha his is simply one possible ep esen a ion in which only
a iables a e sha ed; his is no he mos compac ep esen a ion, bu he one ha
se es as he basis o he e ified unifica ion algo i hm.
upda e is des uc i e. Ne e heless, om he logical poin o iew, he a ay can
be hough as a lis , wi h an applica i e seman ic ( ha is, as i in e e y upda e a
new objec we e c ea ed) . This is possible due o he ac ha in ACL2, he use
o s objs is syn ac ically es ic ed, ensu ing ha in e e y momen only one copy
o he objec is needed. Roughly speaking, hese syn ac ic es ic ions en o ce
ha he only e e ences o he s obj a e done ia i s name ( e ms-dag,in his
case). See [4, 6] o u he in o ma ion abou s objs in ACL2 and he es ic ions
on i s use.
Each node in he g aph is ep esen ed by a cell in he dag a ay o he s obj.
Thus, a node in he g aph can be iden ified wi h an a ay index. Each cell s o es
he label and he successo s o one node, in he ollowing way:
–I node i ep esen s an unbound a iable x, hen(dagi i e ms-dag) con-
ains a do ed pai o he o m (x. ).
–I node i ep esen s a bound a iable, hen (dagi i e ms-dag) con ains
an index npoin ing o he oo node o he e m o which he a iable is
bound.
–I node iis he oo node o a non- a iable e m ( 1,...,
n), hen (dagi i
e ms-dag) isado edpai o he o m( .l),whe elis he lis o he
indices co esponding o he oo nodes o 1,...,
n.
In his way, we can s o e a unifica ion p oblem using he e ms-dag s obj.
Fo example, i we s o e he e m equ( (h(z),g(h(x),h(u))), (x, g(h(u), ))) he
significan cells o he dag a ay a e:
6 8
1
(EQU . (1 9))
0
(F . (2 4))
7
(H . (8))
8
(U . T)
9
(F . (10 11))
32
(H . (3)) (Z . T)
10
4
(G . (5 7)) (X . T)
6
(H . (6))
5
1311
(G . (12 14)) (H . (13))
12
(V . T)
14
We can na u ally iden i y an a ay index wi h he e m whose oo node is
s o ed in he co esponding a ay cell. Taking ad an age o his idea, we can
define a unc ion (called dag- ans o m-mm-s , figu e 2) ha applies one s ep
o he ans o ma ion ela ion ⇒u o a unifica ion p oblem s o ed in e ms-dag.
Le us p ecise abou he beha io o dag- ans o m-mm-s . In addi ion o
he s obj, his unc ion ecei es as inpu a (non-emp y) sys em o equa ions S
o be unified and a pa ially compu ed subs i u ion U. The key poin he e is
ha Sand Uonly con ain indices poin ing o he e ms s o ed in e ms-dag.
In pa icula , Sis a lis o pai s o indices, and Uis a lis o pai s o he o m
(x.n)whe e xis a a iable symbol and nis he index o he node o which
he a iable is bound (we say ha Sis an indices sys em and Uan indices
subs i u ion). Depending on he pai o e ms poin ed o by he fi s equa ion
o S3, one o he ules o ⇒uis applied. The unc ion e u ns a mul i alue wi h
he ollowing componen s, ob ained as a esul o he applica ion o one s ep
o ans o ma ion: he esul ing indices sys em o equa ions o be sol ed, he
3No e ha he indices o he selec ed equa ion a e de e e enced using he unc ion
dag-de e -s , which ollows a chain o ins an ia ions un il i eaches an unbound
a iable o non- a iable node.

(de un dag- ans o m-mm-s (S U e ms-dag)
(decla e (xa gs :s objs e ms-dag))
(le * ((ecu (ca S))
( 1 (dag-de e -s (ca ecu) e ms-dag))
( 2 (dag-de e -s (cd ecu) e ms-dag))
(R (cd S))
(p1 (dagi 1 e ms-dag))
(p2 (dagi 2 e ms-dag)))
(cond
((= 1 2) (m R U e ms-dag))
((dag- a iable-p p1)
(i (occu -check-s 1 2 e ms-dag)
(m nil nil nil e ms-dag)
(le (( e ms-dag (upda e-dagi 1 2 e ms-dag)))
(m R (cons (cons (dag-symbol p1) 2) U) e ms-dag))))
((dag- a iable-p p2)
(m (cons (cons 2 1) R) U e ms-dag))
((no (eql (dag-symbol p1)
(dag-symbol p2)))
(m nil nil nil e ms-dag))
( (m -le (pai -a gs bool)
(pai -a gs (dag-a gs p1) (dag-a gs p2))
(i bool
(m (append pai -a gs R) U e ms-dag)
(m nil nil nil e ms-dag)))))))
Fig. 2. One s ep o ans o ma ion
esul ing indices subs i u ion, a boolean (i ⊥is ob ained, his alue is nil)and
he s obj e ms-dag. No e ha only when Elimina e is applied, he s obj is
upda ed, causing he co esponding a iable o poin o he co esponding e m.
Wi h dag- ans o m-mm-s as i s main componen , we can define he uni-
fica ion algo i hm. In sho , his unc ion, called dag-mgu, ecei es as inpu wo
e ms in p efix o m; a e s o ing hese e ms as di ec ed acyclic g aphs in he
s obj (p e iously esizing he dag a ay p ope ly), i i e a i ely applies he unc-
ion dag- ans o m-mm-s un il ei he non-unifiabili y is de ec ed o he e a e
no mo e equa ions o be sol ed. In his las case, he e u ned subs i u ion (in
p efix o m) is buil om he final con en s o dag, ollowing he poin e s o he
ins an ia ed a iables. The ollowing a e wo examples ob ained wi h dag-mgu.
No e ha he unc ion e u ns wo alues: he fi s one is a boolean indica ing
whe he he e ms a e unifiable o no , and, in case o unifiabili y, he second is
he mgu.
ACL2 !>(dag-mgu ’( (h z) (g (h x) (h u))) ’( x (g (h u) )))
(T ((V . (H (H Z))) (U . (H Z)) (X . (H Z))))
ACL2 !>(dag-mgu ’( y x) ’( (k x) y))
(NIL NIL)
I is wo h poin ing ou ha he syn ac ic equi emen s needed o ensu e he
single- h eadedness o he ACL2 unc ions ha use s objs a e na u ally me in
his algo i hm. See [11] o he defini ions o all he auxilia y unc ions used. Since
he ACL2 language is a subse o Common Lisp (and we ha e e ified gua ds4),
he defined algo i hm can be compiled and execu ed in e e y complian Common
Lisp, wi h he app op ia e ACL2 files loaded.
4 The Fo mal P ope ies o he Unifica ion Algo i hm
Once defined he unc ion dag-mgu, we use he ACL2 logic and i s heo em
p o e o o mally es ablish ha i compu es he mos gene al unifie o wo
e ms i and only i he e ms a e unifiable:
(de hm dag-mgu-comple eness
(implies (and ( e m-p 1) ( e m-p 2)
(equal (ins ance 1 sigma) (ins ance 2 sigma)))
( i s (dag-mgu 1 2))))
(de hm dag-mgu-soundness
(implies (and ( e m-p 1) ( e m-p 2)
( i s (dag-mgu 1 2)))
(equal (ins ance 1 (second (dag-mgu 1 2)))
(ins ance 2 (second (dag-mgu 1 2))))))
(de hm dag-mgu-mos -gene al-solu ion
(implies (and ( e m-p 1) ( e m-p 2)
(equal (ins ance 1 sigma) (ins ance 2 sigma)))
(subs-subs (second (dag-mgu 1 2)) sigma)))
The unc ion ins ance defines he applica ion o a subs i u ion o a e m,
and he p edica e subs-subs defines he ela ion “mo e gene al han” be ween
subs i u ions. The p edica e e m-p ecognizes hose ACL2 objec s ha ep-
esen fi s -o de e ms in p efix no a ion. No e ha he basic heo y used o
s a e he p ope ies is buil on he e ms ep esen ed in p efix no a ion. Fo a
de ailed desc ip ion o his heo y, see [10]. Also he inpu and he ou pu o he
unc ion dag-mgu a e e ms and subs i u ions in p efix no a ion. Bu i has o
be emphasized ha in e nally, he main p ocess is ca ied ou on e m dags.
The fi s heo em, dag-mgu-comple eness, es ablishes ha he algo i hm
e u ns (as i s fi s alue) i he inpu e ms a e unifiable5.The heo emdag-
-mgu-soundness es ablishes ha in ha case i e u ns (as i s second alue) a
unifie o bo h e ms. Finally, he heo em dag-mgu-mos -gene al-solu ion
es ablishes ha he e u ned subs i u ion is mo e gene al han any o he unifie
o bo h e ms. These h ee p o ed heo ems cons i u e a o mal p oo o he
co ec ness o he algo i hm.
4The no ion o gua d o a unc ion will be explained in sec ion 6.
5No e ha he a iable sigma, al hough implici ly uni e sally quan ified, can be seen
as exis en ially quan ified, since i only appea s in he hypo hesis o he heo em.
5 Commen s abou he P oo
In his sec ion, we gi e an o e iew o he p oo p ocess. To emphasize he “com-
posi ional easoning” me hodology ollowed, we ha e s uc u ed i in subsec ions.
Fi s we begin wi h he subsec ions desc ibing p ope ies o he algo i hm a a
mo e abs ac le el. These abs ac p ope ies can be g adually conc e ized o
finally ob ain he heo ems shown in he p e ious sec ion.
5.1 Reasoning abou he Reduc ion ⇒u
One s ep o ans o ma ion o ⇒uis de e mined by he ule applied and he
equa ion selec ed. To o malize his in ui i e idea in ACL2, we define ⇒uby
means o ope a o s. In his con ex , an ope a o is a do ed pai o he o m
(name .i)whe e name is one o he ule names in figu e 1 and iis a na u al
numbe , co esponding o he i- h equa ion o he sys em. Thus, he ans o -
ma ion ⇒ucan be seen as applying one ope a o o a unifica ion p oblem. This
ope a o can be applied whene e he condi ions o he pa icula ule applied
a e me . Fo example, he ope a o (elimina e . 3) can be applied o a uni-
fica ion p oblem i i s hi d equa ion is o he o m x≈ and xdoes no occu
in . The ollowing wo unc ions o malize his idea in ACL2:
•(uni -legal-p upl op), checking he condi ions needed o apply a gi en
ope a o op o a unifica ion p oblem upl (in p efix no a ion).
•(uni - educe-one-s ep-p upl op), e u ning he ans o med unifica-
ion p oblem (in p efix no a ion) a e applying op o upl.
Wi h his ope a o -based ep esen a ion we p o ed in ACL2 he main p op-
e ies o ⇒u. Tha is: a) he se o solu ions o a unifica ion p oblem is p ese ed
in each s ep, b) i he second sys em o a unifica ion p oblem is in sol ed o m,
hen he ans o med unifica ion p oblem has i s second sys em in sol ed o m,
and c) he ans o ma ion ela ion is e mina ing. These p ope ies a e mo e
na u ally p o ed wi h e ms ep esen ed in p efix o m, and his allows us o
euse pa o he heo y de eloped in [10] o he e ifica ion o he applica i e
unifica ion algo i hm.
Ha ing p o ed he main p ope ies o one-s ep ans o ma ions, we can easily
ex end hese p ope ies o fini e sequences o ans o ma ions. In pa icula we
p o e ha i { 1≈ 2};∅∗
⇒u∅;σ, henσis a mgu o 1and 2,andi { 1≈
2};∅∗
⇒u⊥, hen 1and 2a e no unifiable. No e ha in ou o maliza ion, a
sequence o ans o ma ion can be iden ified wi h a lis o (legal) ope a o s.
I is ema kable ha hese esul s do no deal wi h con ol o da a s uc u es
issues: o p o e he co ec ness o a conc e e unifica ion algo i hm, i suffices o
show ha he ac ions o he algo i hm can be simula ed by a fini e sequence o
ans o ma ions w. . . ⇒u. Tha is he main ad an age o ule-based specifica-
ions: hey allow o p o e he essen ial p ope ies o he p ocedu e wi hou he
bu den o echnical implemen a ion issues.
5.2 Dags and Well-Fo medness Condi ions
In o de o ansla e he main p ope ies o ⇒u o ou implemen ed algo i hm,
we ha e o ela e he in o ma ion s o ed in he e ms-dag s obj wi h he e ms
in p efix no a ion i may ep esen . In gene al, no e e y possible con en s o he
dag a ay ep esen fi s -o de e ms. The main eason is ha he g aph could
con ain cycles, and in ha case, no fi s -o de e m is ep esen ed by he cells
o he a ay.
This means ha we ha e o define p edica es o ecognize he p ope ies
needed o ensu e ha he a ay con en s ep esen a fi s -o de e m; he main
o hose p ope ies is acyclicness, ensu ing ha he g aph s o ed in he dag
a ay is ac ually a dag. Some o he well- o medness p ope ies a e also needed
( o ins ance he sha ing o a iables).
Ano he impo an eason why hese well- o medness condi ions a e needed
has o do wi h he es ic ions imposed by he ACL2 logic in i s p inciple o
defini ion: new unc ion defini ions a e admi ed as axioms in he logic only i
he e exis s a measu e in which he a gumen s o each ecu si e call dec ease
wi h espec o a well- ounded ela ion, ensu ing in his way ha he unc ion
e mina es on all inpu s (and consequen ly no inconsis encies a e in oduced by
new unc ion defini ions). Fo example, a unc ion implemen ing “occu -check”
(looking o he occu ence o a gi en a iable in a e m) may no e mina e i he
g aph s o ed in he a ay con ains cycles. The same happens wi h de e e encing
o e en wi h he unc ion ha i e a i ely applies dag- ans o m-mm-s .Thus,
hese unc ions equi e an explici check o e i y ha he s obj does indeed
ep esen an acyclic g aph, ensu ing hei e mina ion. We will commen mo e
abou his poin in sec ion 6.
Fo hese easons, we ha e de eloped a lib a y o esul s abou di ec ed
acyclic g aphs. Fo example, his lib a y con ains he defini ion o he unc ion
dag-p; his unc ion checks ha a gi en g aph (s o ed ollowing he con en ions
desc ibed in sec ion 3) does no con ain cycles. I is implemen ed as a s anda d
dep h-fi s sea ch algo i hm, looking o cycles in he g aph. The ollowing he-
o ems es ablish ha a g aph g e ifies he dag-p condi ion i and only i does
no con ain cycles:
(de hm dag-p-soundeness
(implies (no (dag-p g))
(cycle-p (one-cyclic-pa h g) g)))
(de hm dag-p-comple eness
(implies (cycle-p p g)
(no (dag-p g))))
Some o he gene al defini ions and esul s abou dags a e pa o his lib a y.
See [11] o de ails. Ha ing dag-p as i s main auxilia y unc ion, we can define a
unc ion checking he well- o medness condi ions o a unifica ion p oblem gi en
in dag o m: (well- o med-upl dag-upl) is ue i and only i dag-upl is a
h ee-elemen lis such ha i s fi s elemen is an indices sys em, he second
The in ui i e idea ha algo i hms employing mo e complex da a s uc u es
o mo e sophis ica ed con ol s uc u es equi e mo e effo in e ifica ion is
suppo ed by he able o subsec ion 5.5. These da a con as wi h he effo
needed in he e ifica ion o he same algo i hm using a p efix ep esen a ion
o e ms [10]. In ha wo k, we needed 19 defini ions and 129 heo ems, and in
his case we needed 177 defini ions and 703 heo ems. Anyway, his addi ional
e ifica ion effo has esul ed in he de elopmen o a numbe o ACL2 files ha
could be used in o he o maliza ions ( o example, he heo y abou di ec ed
acyclic g aphs).
As o ela ed wo ks, unifica ion algo i hms ha e been he cen e o se e al
o maliza ions. In pa icula , o mal p oo s o he co ec ness o a unifica ion
algo i hm ha e been gi en in LCF [8], Coq [9] and ALF [3]. Al hough hese
wo ks a e ela ed o ou s, he logic used is qui e diffe en and, mo e impo an ,
hei main conce n is no efficiency o he da a s uc u es used.
O he ela ed wo k is done by Meh a and Nipkow [7], who ha e ecen ly de-
eloped in Isabelle/HOL a gene al amewo k o easoning abou p og ams ha
use poin e s. As a non- i ial case s udy, hey p esen a p oo o he co ec ness
o he Scho –Wai e g aph ma king algo i hm. This wo k is mo e gene al han
ou s, since all he easoning abou poin e s ha we do is especifically de o ed
o he esul s needed by he algo i hm. Mo eo e , he logics used a e diffe en :
in [7], a Hoa e logic o poin e p og ams is embedded in Isabelle/HOL, whe eas
we a e using he ACL2 logic o easoning abou ACL2 unc ions ha can be
di ec ly execu ed in any complian Common Lisp. Ne e heless, some o he
echniques used in [7] a e simila o ou s: o example, wha hey call abs ac-
ion (mapping low le el s uc u es in he heap o highe le el concep s) is simila
o wha we do when we fi s eason abou he main p ope ies o he algo i hm
using he p efix ep esen a ion o e ms (a highe le el ep esen a ion) and hen
we ansla e hem o he algo i hm ha uses dags (a lowe le el ep esen a ion).
As o u he wo k, we al eady poin ed ou a he end o subsec ion 6 ha
we can in oduce some echnical imp o emen s in o de o make he e ified
algo i hm un in quad a ic ime. We also plan o e i y his imp o ed algo i hm.
Finally, no e ha al hough ou main conce n is an efficien and o mally e -
ified algo i hm, we do no p o e heo ems abou he efficiency o he algo i hm.
Al hough easoning abou complexi y o algo i hms in he ACL2 logic is (in
p inciple) possible, we hink ha i could be much mo e difficul han easoning
abou he co ec ness o he algo i hm, mainly due o he need o o malizing
he “big-O no a ion” (and i s asymp o ic cha ac e ) in he ACL2 logic.
Acknowledgmen s
Pa o his wo k was done du ing a isi o he fi s au ho o he Compu e
Science Depa men o he Uni e si y o Texas a Aus in. We would like o hank
he ACL2 g oup in Aus in, especially o J Moo e and Ma Kau mann, o hei
suppo , and o in oducing mbe in ACL2.

Re e ences
1. Baade , F. and Nipkow, T. Te m Rew i ing and All Tha . Camb idge Uni e si y
P ess, 1998.
2. Baade , F. and Snyde , W. Unifica ion heo y. Handbook o Au oma ed Rea-
soning, Else ie Science Publishe s, 2001.
3. Bo e, A. P og amming in Ma in-L Type Theo y: Unifica ion - A non- i ial Ex-
ample. Licen ia e Thesis, Depa men o Compu e Science, Chalme s Uni e si y
o Technology, 1999.
4. Boye R.S. and Moo e J S. Single- h eaded objec s in ACL2. In P ac ical As-
pec s o Decla a i e Languages, LNCS 2257, pages 9–27, Sp inge –Ve lag, 2002.
5. Kau mann, M., Manolios, P. and Moo e, J S. Compu e -Aided Reasoning:
An App oach. Kluwe Academic Publishe s, 2000.
6. Kau mann, M. and Moo e, J S. ACL2 Ve sion 2.7, 2002.
Homepage: h p://www.cs.u exas.edu/use s/moo e/acl2/
7. Meh a, F. and Nipkow, T. P o ing Poin e P og ams in Highe -O de Logic .
o be p esen ed a CADE-19, 2003.
8. Paulson, L. Ve i ying he unifica ion algo i hm in LCF. Science o Compu e
P og amming, 5, 1985.
9. Rouye , J. D eloppemen de l’algo i hme d’unifica ion dans le calcul des con-
s uc ions a ec ypes induc i s. Tech. Rep. 1795, INRIA Lo aine, 1992 (in ench).
10. Ruiz–Reina, J.L., Alonso, J.A., Hidalgo, M.J. and Ma ´
ın, F.J. A heo y
abou fi s –o de e ms in ACL2 In Thi d ACL2 Wo kshop, G enoble, 2002.
11. Ruiz–Reina, J.L., Alonso, J.A., Hidalgo, M.J. and Ma ´
ın, F.J. A e ified
dag unifica ion algo i hm in ACL2, 2002.
A ailable a h p://www.cs.us.es/~j uiz/uni icacion-dag