Formalization of a Normalization Theorem in Simplicial Topology
- Lambán, L. 1
- Martín-Mateos, F.-J. 2
- Rubio, J. 1
- Ruiz-Reina, J.-L. 2
-
1
Universidad de La Rioja
info
-
2
Universidad de Sevilla
info
ISSN: 1012-2443
Year of publication: 2012
Volume: 64
Issue: 1
Pages: 1-37
Type: Article
More publications in: Annals of Mathematics and Artificial Intelligence
Related Projects
2009/00207/001
2010/00182/001
Abstract
In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology stating that there exists a homotopy equivalence between the chain complex of a simplicial set, and a smaller chain complex for the same simplicial set, called the normalized chain complex. Even if the Normalization Theorem is usually stated as a higher-order result (with a Category Theory flavor) we manage to give a first-order proof of it. To this aim it is instrumental the introduction of an algebraic data structure called simplicial polynomial. As a demonstration of the validity of our techniques we developed a formal proof in the ACL2 theorem prover. © 2012 Springer Science+Business Media B.V.