Abstract

The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted to computing in Algebraic Topology. In this article we report on a complete formal proof of the underlying Eilenberg–Zilber theorem, using the ACL2 theorem prover. As our formalization is executable, we are able to compare the results of the certified programme with those of Kenzo on some universal examples. Since the results coincide, the reliability of Kenzo is reinforced. This is a new step in our long-term project towards certified programming for Algebraic Topology.

References

[1]
Andrés
M.
Lambán
L.
Rubio
J.
Ruiz-Reina
J. L.
Formalizing simplicial topology in ACL2
Proceedings ACL2 Workshop 2007
 , 
2007
University of Austin
(pg. 
34
-
39
)
[2]
Aransay
J.
Ballarin
C.
Rubio
J.
A mechanized proof of the basic perturbation lemma
Journal of Automated Reasoning
 , 
2008
, vol. 
40
 (pg. 
271
-
292
)
[3]
Aransay
J.
Ballarin
C.
Rubio
J.
Generating certified code from formal proofs: a case study in homological algebra
Formal Aspects of Computing
 , 
2010
, vol. 
22
 (pg. 
193
-
213
)
[4]
Domínguez
C.
Rubio
J.
Effective homology of bicomplexes, formalized in Coq
Theoretical Computer Science
 , 
2011
, vol. 
412
 (pg. 
962
-
970
)
[5]
Dousson
X.
Sergeraert
F.
Siret
Y.
The Kenzo program
 , 
1999
Grenoble
Institut Fourier
 
[6]
Edelsbrunner
H.
Harer
J.
Computational Topology: An Introduction
 , 
2010
American Mathematical Society
[7]
Heras
J.
Dénès
M.
Mata
G.
Mörtberg
A.
Poza
M.
Siles
V.
Towards a certified computation of homology groups for digital images
Proceedings CTIC 2012, Vol. 7309 of Lecture Notes in Computer Science
 , 
2012
(pg. 
49
-
57
)
[8]
Heras
J.
Poza
M.
Rubio
J.
Verifying an algorithm computing Discrete Vector Fields for digital imaging
Calculemus 2012, Vol. 7362 of Lecture Notes in Computer Science
 , 
2012
(pg. 
215
-
229
)
[9]
Hunt
W. A.
Kaufmann
M.
Krug
R. B.
Moore
J
Smith
E. W.
Meta reasoning in ACL2
Procedings TPHOLs 2005. Vol. 3603 of Lecture Notes in Computer Science
 (pg. 
163
-
178
)
[10]
Kaufmann
M.
Manolios
P.
Moore
J. S.
Computer-Aided Reasoning: An Approach
 , 
2010
Kluwer
[11]
Lambán
L.
Martín-Mateos
F. J.
Rubio
J.
Ruiz-Reina
J. L.
Applying ACL2 to the formalization of algebraic topology: simplicial polynomials
Proceedings ITP 2011. Vol. 6896 of Lecture Notes in Computer Science
 , 
2011
(pg. 
200
-
215
)
[12]
Lambán
L.
Martín-Mateos
F. J.
Rubio
J.
Ruiz-Reina
J. L.
Formalization of a normalization theorem in simplicial topology
Annals of Mathematics and Artificial Intelligence
 , 
2012
, vol. 
64
 (pg. 
1
-
37
)
[13]
Lambán
L.
Martín-Mateos
F. J.
Rubio
J.
Ruiz-Reina
J. L.
Formalization of the Eilenberg–Zilber Theorem (full code)
2012
 
[14]
Lambán
L.
Martín-Mateos
F. J.
Rubio
J.
Ruiz-Reina
J. L.
Certified symbolic manipulation: bivariate simplicial polynomials
Proceedings ISSAC 2013
 , 
2013
ACM Press
(pg. 
243
-
250
)
[15]
Martín-Mateos
F. J.
Alonso
J. A.
Hidalgo
M.
Ruiz-Reina
J. L.
A generic instantiation tool and a case study: a generic multiset theory
Proceedings of the third International ACL2 Workshop and its Applications
 , 
2002
(pg. 
188
-
201
Affiliated with ETAPS 2002
[16]
Martín-Mateos
F. J.
Rubio
J.
Ruiz-Reina
J. L.
ACL2 verification of simplicial degeneracy programs in the Kenzo system
Proceedings Calculemus 2009. Vol. 5625 of Lecture Notes in Artificial Intelligence
 , 
2009
(pg. 
106
-
121
)
[17]
May
J. P.
Simplicial Objects in Algebraic Topology
 , 
1967
Van Nostrand
[18]
Prouté
A.
Sur la Transformation d'Eilenberg–Mac Lane
Comptes Rendus Académie Sciences Paris, Série I
 , 
1983
, vol. 
297
 (pg. 
193
-
194
)
[19]
Prouté
A.
Sur la diagonale d'Alexander–Whitney
Comptes Rendus Académie Sciences Paris, Série I
 , 
1984
, vol. 
299
 (pg. 
391
-
392
)
[20]
Real
P.
Homological perturbation theory and associativity
Homology Homotopy and Applications
 , 
2000
, vol. 
2
 (pg. 
51
-
88
)
[21]
Romero
A.
Rubio
J.
Homotopy groups of suspended classifying spaces: an experimental approach
Mathematics of Computation
 , 
2013
, vol. 
82
 (pg. 
2237
-
2244
)
[22]
Rubio
J.
Homologie effective des espaces de lacets itérés : un logiciel
 , 
1991
Thèse, Institut Fourier
 
[23]
Rubio
J.
Sergeraert
F.
Siret
Y.
EAT: Symbolic Software for Effective Homology Computation
 , 
1997
Institut Fourier
 
[24]
Szczarba
R. H.
The homology of twisted cartesian products
Transactions of the American Mathematical Society
 , 
1961
, vol. 
100
 (pg. 
197
-
216
)