Formalization of a normalization theorem in simplicial topology

Formalization of a normalization theorem in simplicial topology Laureano Lambán · Francisco-Jesús Martín–Mateos · Julio Rubio · José-Luis Ruiz–Reina 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. Keywords Automated reasoning · Formalization of mathematics · ACL2 · Algebraic topology · Normalization theorem This work is dedicated to our colleague and friend Mirian Andrés. She started this research but passed away at the age of only 29 due to a car accident. Mirian, the best friend for your friends, we do not forget you. Partially supported by Ministerio de Ciencia e Innovación, project MTM2009-13842, and by European Commission FP7, STREP project ForMath, n. 243847. L. Lambán ·J. Rubio (B) Department of Mathematics and Computation, University of La Rioja, Edificio Vives, Luis de Ulloa s/n. 26004, Logroño, Spain e-mail: [email protected] L. Lambán e-mail: [email protected] F.-J. Martín–Mateos ·J.-L. Ruiz–Reina Computational Logic Group, Department of Computer Science and Artificial Intelligence, University of Seville, Avda. Reina Mercedes, s/n. 41012, Sevilla, Spain F.-J. Martín–Mateos e-mail: [email protected] J.-L. Ruiz–Reina e-mail: [email protected] Introduction The Normalization Theorem is an important result in Algebraic Simplicial Topology explaining that, in order to obtain the homology groups of a space, one can work with a chain complex (called normalized) smaller than the standard chain complex constructed from all the simplexes of the space. In this paper we present a complete formal proof of the Normalization Theorem. As a demonstration of the soundness of our approach we have written a complete development of the formal proof in the ACL2 theorem prover. The interest of this work stems from three sources. First, it constitutes a good example of using efficiently first-order logic in a context where a higher-order approach could seem more natural, due to the character of the mathematics formalized. Second, our proof validates some formulas found experimentally, giving an explicit version of the Normalization Theorem, unknown in the literature (up to our knowledge). And third, the Normalization Theorem is the basis for some design decisions in the Kenzo computer algebra system, a program for computing in Algebraic Topology. This last point is further explained in the next paragraphs. The origin of this work comes from a Computer Algebra system called Kenzo [8], a Common Lisp program created by F. Sergeraert around 1990 and devoted to computing homology groups of topological spaces. In other words, Kenzo is a system devoted to Algebraic Topology, the branch of mathematics dealing with algebraic structures (groups, rings,...) associated to topological spaces. Usually, the topological spaces are presented under a combinatorial form as simplicial complexes or simplicial sets. The objective of Algebraic Topology is to classify or to distinguish topological spaces by observing the algebraic structures associated to them, which are, in principle, amenable to a systematic treatment (algebra would be considered, in this sense, easier than topology). One feature of Algebraic Topology is that, in order to get information from spaces of finite dimension, it is required to pass through some infinite dimensional spaces (as loop spaces for instance; see [19] for details). This explains why Sergeraert chose Common Lisp as implementation language for Kenzo: he used functional programming to encode infinite sets needed in Algebraic Topology constructions. Although Kenzo is a very reliable system which has been intensively tested, and is in production several years ago, it turns out that Kenzo was able to compute new results (“new” in the sense that no known theoretical result can be used to confirm it; see [24]). Then, some concrete outputs of the program cannot be tested, that is, compared with any expected value. This is the reason why a project to apply formal methods to the study of Kenzo as a software system was launched some years ago [6, 12]. Eventually, this research line arrived to the formalization of some parts of Algebraic Topology and Homological Algebra by using proof assistants as Isabelle/HOL [2, 3]orCoq [7]. A different approach to using Coq to implement in constructive type theory some features of Kenzo can be found in [4]. When talking about mechanized theorem proving and Kenzo, it is easy to think about ACL2 [11]. ACL2 is, at the same time, a programming language, a logic for specifying and proving properties of the programs defined in the language and a theorem prover supporting mechanized reasoning in the logic. The ACL2 programming language is an extension of an applicative subset of Common Lisp, and the logic is first-order, in which formulas do not have quantifiers and all the variables in them are implicitly universally quantified. It includes axioms for propositional logic, equality and for a number of predefined Common Lisp functions and data types. Rules of inference of the logic include those for propositional calculus, equality, instantiation and induction. The previous discussion on Kenzo however shows the limitations of an ACL2 approach to verify Kenzo properties, since Kenzo uses higher order functional programming, while ACL2 is, essentially, a first order tool. This constraint has not been an obstacle for us to effectively use ACL2 to study first order fragments of Kenzo [10,18]. The ACL2 proof of the Normalization Theorem described in this paper (a preliminary version of this work was presented in [13]) differs from previous ACL2 formalizations in two aspects. The first peculiarity of this paper is that the formalized algorithm is not directly used in Kenzo. It is rather a precondition for Kenzo, because only normalized chain complexes are dealt with in that system. Thus, our ACL2 proof certifies that the encoding strategy applied in Kenzo is reliable. In addition, if in some future development the non-normalized chain complex is needed, then our ACL2 proof will provide a certified transfer to the Kenzo coding style (for a different but related problem, where algorithms involving non-normalized objects are needed, see [22], pp. 102–104). The second differential feature of the problem tackled in this paper is that, in principle, it is a higher order result, because it quantifies over every simplicial set (which, in general, would be characterized by predicates). The key point of this paper is that, for this concrete result, first order is enough. It is not due to a simulation of higher order logic in ACL2 by means of encapsulates [11] (although this technique will be also used in our development, in order to present our statements in a standard mathematical terminology). A symbolic setting is introduced in which the theorem can be proved by using only simplification and induction on lists, the kind of proofs ACL2 was designed for. We think that this approach could be useful in other related results, because it is based on some features of the simplicial category. Thus, this work could be considered a first milestone to formalize simplicial topology in a first order frame. The organization of the paper is as follows. In Section 2we introduce both the problem (including the minimal mathematical machinery needed to state and understand the main theorem) and the strategy of the solution we are proposing for it. The symbolic framework based on simplicial polynomials is then described in Section 3. It is applied to give a proof of the Normalization Theorem in Section 4. The statement of the Normalization Theorem in Section 4is expressed in terms of the first order concepts introduced in Section 3; then, in Section 5we reformulate it by using ACL2 encapsulates, providing a statement more readable from the point of view of standard mathematical textbooks. Section 6is devoted to put the proof in context, illustrating that our approach is not so-original: higher order logic is avoided due to working with a concrete category of pre-sheaves. The last section in the paper deals with conclusions and further work. In addition, we include two appendices. In Appendix Awe give a short recipe allowing an interested reader to check on his own computer the formalized proof, even if he is not an ACL2 user. Appendix Bcontains a sample ACL2 session showing the literal output for an automatic proof of one formalized theorem. 2 Presentation of the problem and the solution In this section we introduce the mathematical preliminaries required to understand the problem, and we give some clues about the nature of the formalization developed. More concretely, the most important simplicial concepts needed to state the main theorem are presented in Sections 2.1–2.5. (More details on simplicial topology can be found, for instance, in [19].) Sections 2.6 and 2.7 explain the big lines of the proof and some formalization issues, respectively. Finally, in Section 2.8, an example of a (simple) proof is described, in order to illustrate our methods. 2.1 Simplicial sets Definition 1 Asimplicial set K is a graded set {Kn}n∈Ntogether with functions: ∂n i:Kn→Kn−1,n>0,i=0,...,n, ηn i:Kn→Kn+1,n≥0,i=0,...,n, subject to the following equations: ∂n−1 i∂n j=∂n−1 j∂n i+1if i≥j,(1) ηn+1 iηn j=ηn+1 j+1ηn iif i≤j,(2) ∂n+1 iηn j=ηn−1 j−1∂n iif i<j,(3) ∂n+1 iηn j=ηn−1 j∂n i−1if i>j+1,(4) ∂n+1 iηn i=∂n+1 i+1ηn i=idn(5) The functions ∂n iand ηn iare called face and degeneracy maps, respectively. The function idndenotes the identity function on Kn. The elements of Knare called n-simplexes (or simplexes of dimension n).Ansimplex xis degenerate if x=ηn−1 iyfor some simplex y, and for some degeneracy map ηn−1 i;otherwisexis non degenerate. Although we have not enough room here to illustrate the notion of simplicial set, let us try to explain where the identities come from. If we think that n-simplexes are non-decreasing integer lists of length n+1, and we interpret a face operator ∂n i as erasing the element at position iin a list (the first element is that at index 0), and a degeneracy operator ηn ias repeating the element at position i, the equalities obtained are exactly those of Definition 1. With this interpretation, non-degenerate simplexes are those lists strictly increasing, while the degenerate simplexes have some repetition. This kind of simplicial set (whose simplexes are lists) is called simplicial complex [5]. It can be considered that a simplicial set is an abstraction of a simplicial complex, where simplexes are no more lists, but whatever elements. If no confusion can arise, usually we remove the superindex in the face and degeneracy operators, writing simply ∂iand ηi, respectively. 2.2 Chain complexes and homology groups A simplicial set is a combinatorial model of a topological space. Algebraic Topology associates algebraic objects to topological spaces. This is the reason of the following definitions. Let Kbe a simplicial set. For each n∈N, let us consider Z[Kn], the free Abelian group generated by the n-simplexes Kn, denoted by Cn(K). Then, the elements of such a group are formal linear combinations r j=1λjxj,whereλj∈Zand xj∈ Kn,∀j=1,...,r. These linear combinations are called chains of simplexes or, in short, chains. Now, if n>0, we introduce a homomorphism dn:Cn(K)→Cn−1(K), first defining it over each generator, and then extending it by linearity. Given x∈Kn, define dn(x)=n i=0(−1)i∂i(x). It can be proved that (1) in the definition of simplicial set implies that dn◦dn+1=0,∀n∈N. That is to say, the family {dn}n∈Ndefines a differential (or boundary) homomorphism on the graded group {Cn(K)}n∈N. Or, still in other words, the family of pairs {(Cn(K), dn)}n∈Nis the chain complex associated to the simplicial set K, denoted by C(K). Let C={(Cn,dn)}n∈Nbe a general chain complex (that is, each Cnis an Abelian group, and each dnis a homomorphism such that the boundary condition holds). The boundary property dn◦dn+1=0implies Im(dn+1)⊆Ker(dn), and since we are working with Abelian groups, it is possible to consider the quotient group Ker(dn)/Im(dn+1). It is called the n-th homology group of the chain complex C, denoted by Hn(C). In the particular case where C=C(K)(Kbeing a simplicial set) we call it the (simplicial) n-th homology group of K, denoted by Hn(K). Much effort is devoted in Algebraic Topology to study and determine such homology groups. And it is also the main object to be computed by means of Kenzo. 2.3 Normalized chain complexes There is an alternative way to associate a chain complex to a simplicial set K. Given n∈N, let us denote by KD nand KND nthe sets of degenerate and non-degenerate nsimplexes of K, respectively (note that this gives a disjoint partition of the whole set Kn). We now consider the following Abelian free groups: Dn(K)=Z[KD n],thatis to say the Abelian group freely generated by degenerate simplexes. Conditions (3)– (5) in Definition 1 imply that the differential dnis well defined on D(K)(that is, if we take a combination c=m j=1λjxjwhere every xjis degenerated, then dn(c)∈ Dn−1(K)). Thus, the chain complex D(K)is a subcomplex of C(K), and we can obtain the quotient chain complex C(K)/D(K), which is denoted by CN(K)and is called the normalized chain complex of the simplicial set K. There exists an alternative isomorphic description of the normalized chain complex CN(K). It consists of defining as CN n(K)the free Abelian group Z[KND n] generated by non-degenerate simplexes. Then, to get an actual chain complex, it is necessary to redefine the differential map dnby erasing, in the image, the generators which are degenerate. With this description the group CN n(K)is no more a quotient, but a subgroup of Cn(K). Observe however that CN(K)is not in general a chain subcomplex of C(K)(because some faces of a non-degenerate simplex can be degenerate simplexes). 2.4 The normalization theorem With any of the two descriptions of the normalized chain complex CN(K), there exists a canonical epimorphism f:C(K)→CN(K).IfCN(K)is considered a quotient, the map fis nothing but the canonical projection. If CN(K)is described as a free graded group, then f(r j=1λjxj)consists simply of erasing in the combination the terms λjxjwhere xjis a degenerate simplex. Note that the map frespects in both cases the differentials; that is to say, fn−1◦ dn=dN n◦fn,∀n>0,wheredNdenotes the differential of CN(K). Or still in other words, fis a chain morphism. This canonical chain morphism fpreserves the homological information, and this is established by the normalization theorem. Theorem 1 (Normalization theorem) For all simplicial set K, the canonical homomorphism f :C(K)→CN(K)induces group isomorphisms Hn(C(K)) ∼ = Hn(CN(K)), ∀n∈N. The theorem explains that, from the computational point of view, it is the same to work with C(K)or with CN(K). This justifies Sergeraert’s decision of working in Kenzo only with the smaller chain complex CN(K)to compute homology groups of a simplicial set K. One proof of the Normalization Theorem can be found in [14], pp. 236–237. It consists of filtering the big group Cn(K)by considering sequentially n-simplexes of the form ηn−1x, then of the form ηn−2xor ηn−1x, and so on. In each step, the homological information is preserved. And finally fis described as the composition of all these homology-preserving maps. 2.5 Statement of the theorem to formalize It is not difficult to give a more precise proof (and statement) of the normalization theorem using the notion of reduction. (In [22], pp. 102–104, a proof similar to Mac Lane’s one is converted into an algorithm constructing a reduction, in a slightly different context.) Definition 2 Areduction is a 5-tuple (C,C,f,g,h) C f ++ h55C g kk where C=(M,d)and C=(M,d)are chain complexes, f:C→Cand g:C→C are chain morphisms, h=(hi:Mi→Mi+1)i∈Nis a family of homomorphisms (called homotopy operator), which satisfy the following properties for all i∈N: (a)fi◦gi=idM i, (b)di+2◦hi+1+hi◦di+1+gi+1◦fi+1=idMi+1, (c)fi+1◦hi=0, (d)hi◦gi=0, (e)hi+1◦hi=0 This concept precisely describes a situation where the homological information is preserved. More concretely, if (C,C,f,g,h)is a reduction, then fninduces an isomorphism of groups (with gndefining the corresponding inverse) between Hn(C) and Hn(C), ∀n>0. Therefore the following statement describes a stronger version of the normalization theorem. Theorem 2 (Normalization reduction) For all simplicial sets K, there exists a reduction (C(K), CN(K), f,g,h)where f is the canonical chain epimorphism. 2.6 Plan for the formalized proof Instead of trying a proof based on Mac Lane’s ideas, we formalized a different proof, with the additional goal of applying it to study an experimental result presented in [23]. There, after running several examples, it was conjectured that some possible formulas for the Normalization Theorem could be: •gm=(−1)p i=1ai+biηap...η a1∂b1...∂ bp where the indexes range over 0≤a1<b1<...<ap<bp≤m,with0≤p≤ (m+1)/2. •hm=(−1)ap+1+p i=1ai+biηap+1ηap...η a1∂b1...∂ bp where the indexes range over 0≤a1<b1<...<ap<ap+1≤bp≤m,with0≤ p≤(m+1)/2. We will prove in ACL2 that, with some recursive versions of these formulas, the equalities (a), (b) and (c) in Definition 2 hold. This result is the most difficult one in all our formalization. To stress the complexity of this task, let us observe that the sum for gmhas 2mterms, while that for hmhas 2m+1−1terms. Let us call prereduction to a 5-tuple (C,C,f,g,h)as in the definition of reduction, but where equalities (d) and (e) are possibly not satisfied.1Then, the following result can be used to construct, from our previous explicit formulas, a reduction linking C(K)and CN(K). 1One of the anonymous referees observed that, to be a prereduction, it is enough for the tuple (C,C,f,g,h)to satisfy the properties (a) and (b), because the formula h1:= (1−gf)h(1−gf)gives the properties (c) and (d) for h1. In our concrete situation, the definitions of fand hsatisfy already Property (c), fh=0, and thus our weaker result is enough in our case. Theorem 3 Let (C,C,f,g,h0)be a prereduction. Then, an algorithm produces a reduction (C,C,f,g,h). Let us explain the proof of this last theorem, because it will serve us later to illustrate how ACL2 can be effectively used in this kind of higher-order reasoning (observe that Cand Ccan be supported by infinite sets, defined by predicates, and that the construction of hfrom (f,g,h0)would require higher order functional programming). First, we define: h1:= h0−h0gf. This new homomorphism of degree +1satisfies conditions (a)-(b)-(c) in the definition of reduction. For instance: dh1+h1d= d(h0−h0gf)+(h0−h0gf)d=dh0−dh0gf +h0d−h0gfd=dh0−dh0gf +h0d− h0dgf =dh0+h0d−(dh0+h0d)gf=id −gf −(id −gf)gf=id −gf −gf+gfgf= id −gf −gf +gf =id −gf, and so condition (b) is satisfied for the new homotopy h1. In addition: h1g=(h0−h0gf)g=h0g−h0gfg=h0g−h0g=0. Now, with this kind of simple rewritings, it is easy to verify that all the properties of a reduction are obtained with the following homotopy operator: h:= h1dh1. 2.7 Formalization issues Summarizing the previous subsection, our problem is to prove in ACL2 the Normalization Theorem (in its strong version providing a reduction, as in Theorem 2). In addition, our proof should be based on the explicit formulas experimentally found in [23]. As already mentioned, the statement in Theorem 2 is clearly of second-order. It quantifies over all simplicial sets. But a simplicial set is given by a collection of predicates (defining, ∀n∈N,thesetofn-simplexes, that can be an infinite set) and of functions ∂n i,ηn i. To deal with these structures as first-class citizens (to pass them as arguments to functions, and to produce them as outputs of functions) Kenzo uses higher-order functional programming. Higher order can be simulated in ACL2 by means of encapsulates,amechanism to introduce abstract functions with constraints. For instance, a generic definition of a reduction can be encoded in an encapsulate. Then, properties obtained from that encapsulate can be applied to any reduction. In Section 5we will use this technique to produce in ACL2 a presentation of the Normalization Theorem close to the one usually found in textbooks. Furthermore, we prove there Theorem 3, by guiding the theorem prover. However, to give a proof of Theorem 2, a greater degree of automation would be desirable, because the mathematical proof is much more complicated than that of Theorem 3. To this aim, we have devised an ACL2 proof free of encapsulates. That is to say, a purely first order proof. The idea is as follows. Let us define a simplicial operator as any sequence of face and degeneracy maps. For instance, ∂5η3∂1∂2η4is such a simplicial operator. Observe that, as dimensions are dropped (there are no superindexes), this expression denotes a functional object in each valid dimension (at least dimension 5in the example), and for every simplicial set on which it is applied. Now, if equalities in Definition 1 are considered as rewriting rules (reading them from left to right) then there exists a canonical form for each simplicial operator (see [1] for a complete development of this idea, formalized in ACL2). Let us show this conversion to canonical form step by step in our running 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 operator can be encoded, in a unique way, as a pair of lists of natural numbers: the first list being a strictly decreasing list of natural numbers, and the second one strictly increasing. In our example: ((3 2) (1 2 5)).Letuscall such pairs simplicial terms, using a terminology borrowed from algebraic polynomial theory (see, for instance, the formalization in [20]). Note that although a simplicial term is a simplicial operator, we call it in a special way to emphasize the fact that it is in canonical form. Simplicial terms can be composed (by using again the simplicial identities of Definition 1) and so they are endowed with a monoid structure (the unity being the pair with two empty lists). Now, let us observe that the formulas for gmand hmin the previous subsection can be interpreted as linear combinations of simplicial terms. Thus it is sensible to try the proof in the ring freely generated by simplicial terms. We will call the elements of this ring simplicial polynomials. The ACL2 formalization of simplicial polynomials presented here is similar to the formalization of polynomials over the rational field developed in [20]. Simplicial polynomials can be interpreted functionally only over a single chain complex C(K). This implies, for instance, that the canonical projection fcannot be represented inside this framework (since it links two different chain complexes, namely C(K)and CN(K)). In Section 4, we manage to reformulate the properties of a reduction in the simplicial polynomials setting. Then, in Section 5,weusethe encapsulation principle to recover the standard statement of the results (in terms of functional objects). 2.8 An example at work The intuitive idea underlying our approach is that if we prove a result by only using the simplicial equalities of Definition 1, then the scope of the proof is the whole category of Simplicial Sets. Let us see it in action with the following example. (In Appendix Bwe give an ACL2 session corresponding to this same theorem.) Theorem 4 dn◦dn+1=0,∀n∈N. Let us start from the definition: 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 forbidden operation: remove the superindexes in the last expression. This allows us a recursive definition of the differential: 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 the formal properties of the simplicial ring, we obtain: 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 then, using the induction hypothesis dn◦dn+1= −∂n∂n+1+(−1)n∂ndn+(−1)n+1dn−1∂n+1. It is not difficult to prove, also by induction, the following auxiliary result. Lemma 1 ∂ndn=(−1)n∂n∂n+1+dn−1∂n+1. clear that another restriction we must impose on a simplicial polynomial, in order to being able to interpret it as a function on chains, is that all its terms must have the same degree (what we will call a uniform polynomial). We have formalized in ACL2 those restrictions by means of three functions valid-sp,uniform-sp and degree-sp, whose definitions we omit here: valid-sp(p,m) checks whether all the simplicial terms in pare valid for dimension m,uniform-sp(p) checks if all the terms in phave the same degree and degree-sp(p) is the common degree of the terms of a uniform polynomial (or 0 if it is the zero polynomial). We will say that a polynomial is well-formed for dimension mwhen it is valid for mand uniform. It is important to note that well-formedness is not needed to prove the ring properties of simplicial polynomials, which are true for every polynomial, wellformed or not. But it will be needed in Section 5, where we will interpret simplicial polynomials as functions on chains. 4 Formal proofs in the polynomial framework As sketched in Section 2, our main goal is to prove the Normalization Theorem (in its strong version), by explicitly giving a reduction (C(K), CN(K), f,g,h). Unfortunately, we cannot directly state this theorem in the simplicial polynomial framework. There are several reasons for this. For example, fis defined to be the canonical chain epimorphism, from C(K)to CN(K). This function can be described as the operation of erasing all the degenerate simplexes of a chain (recall from Section 2.1: a linear combination of simplexes with integer coefficients). Since a simplicial polynomial does not have an explicit mentioning of the arguments on which the function that it represents is supposed to be applied, this epimorphism cannot be described as a simplicial polynomial. Also, we should not forget that in our polynomial setting we dropped any explicit mentioning of the dimensions of the face and degeneracy maps involved, and these dimensions are explicit in the definition of simplicial set (Definition 1). But fortunately, we can do most of the work (or at least, the hard part) using simplicial polynomials in a convenient way, as we will describe. The idea is to define polynomial versions for the differential dand for gand h, and prove, in the simplicial polynomial ring, their main properties. 4.1 The polynomials dm,gmand hm First, let us recall the definitions (parameterized by m∈N) for the differential dm and for the conjectured definitions of gmand hm, given in Section 2: •dm=m i=0(−1)i∂i •gm=(−1)p i=1ai+biηap...η a1∂b1...∂ bp, where the indexes range over the aiand bisuch that 0≤a1<b1<...<ap<bp≤m,with0≤p≤(m+1)/2. •hm=(−1)ap+1+p i=1ai+biηap+1ηap...η a1∂b1...∂ bp, where the indexes range over 0≤a1<b1<...<ap<ap+1≤bp≤m,with0≤p≤(m+1)/2. Note that, viewed as symbolic expressions, the above define three families of simplicial polynomials. In order to translate them to ACL2, we found an essential hindrance: ACL2 does not admit iterative definitions, and therefore it is mandatory to work with an equivalent recursive definition. At the end of the way, it will give to our proof a recursive flavor, and so differences with the above mentioned Mac Lane’s proof [14] could be unnoticed. However, our proof was directly inspired by these summations, and carried out following combinatorial clues given by them. (In fact, after our formalization was completed, we found the paper [9], where David Epstein gave formulas very close to our recursive versions of the summations.) We first introduce the recursive polynomials (that is, the polynomial for mwill be defined in terms of the polynomial for m−1) and then explain with some detail the translation from the summations to the recursive polynomials. The case of the function diff-pol, defining the differential dm, is easy and does not deserve a thoughtful explanation: Definition: [dm] diff-pol(m):= if m∈ N+then ∂0 else (−1)m·∂m+diff-pol(m−1) For the definition of gm,letpi,jdenote the polynomial ηi∂j,wheni<j. Consider the following recursive definition: Definition: [gm] G-pol(m):= if m∈ N+then id else G-pol(m−1)·(id −pm−1,m) Some explanation is needed to show why this definition can be considered as a recursive version implementing the explicit formula conjectured in [23], that we repeat here to ease the reading: gm=(−1)p i=1ai+biηap...η a1∂b1...∂ bp,wherethe indexes range over the aiand bisuch that 0≤a1<b1<...<ap<bp≤m,with 0≤p≤(m+1)/2. Let us first observe that, by applying the simplicial identities: ηap...η a1∂b1...∂ bp=ηa1∂b1...η ap∂bp=pa1,b1...pap,bp Therefore, gmis the simplicial polynomial whose monomials are (up to sign, +1 or −1) all the simplicial terms which are a product of disjoint terms pi,j(we called two terms pi1,j1and pi2,j2disjoint terms if i1<j1<i2<j2) with subindexes less or equal than m. This is the idea allowing us to define our recursive version of gm,as explained below. The composite terms pa1,b1...pap,bpcan be grouped into two disjoint families, expressing gmas a sum of two polynomials: – Products where bp<m, whose addition gives rise to gm−1(including p=0), and – Products where its last factor is pα,m,withα∈{0,...,m−1}. Then we claim that the corresponding polynomial obtained by adding all the factors in this family is equal to −gm−1pm−1,m.Thatis,ifα=m−1the product has the adequate shape, and the sign changes because 2m−1is an odd number; if α<m−1we can write pα,m=pα,m−1pm−1,m, and the sign changes because the second subindex has been decreased by one. Thus, gm=gm−1−gm−1pm−1,m=gm−1(Id−pm−1,m)which is the implemented recursive definition. For example, this is the result obtained when we compute g3using the above definition: idT−η0∂1+η0∂2−η0∂3−η1∂2+η1∂3−η2∂3+η2η0∂1∂3. For the recursive definition of hm, we first define a new family of parameterized polynomials, denoted qm,inthefollowingway: Definition: [qm] Q-pol(m):= if m∈ N+then 0 else −Q-pol(m−1)·pm−1,m+(−1)m−1·ηm·gm−1·pm−1,m Now we define hmin the following recursive way: Definition: [hm] H-pol(m):= if m∈ N+then η0 else H-pol(m−1)+(−1)m·ηm+qm Let us prove here that this recursive definition is equivalent to hm= (−1)ap+1+p i=1ai+biηap+1ηap...η a1∂b1...∂ bp, where the indexes range over 0≤a1< b1<...<ap<ap+1≤bp≤m,with0≤p≤(m+1)/2(the formula conjectured in [23]). Asinthecaseofgm, we can describe hmas the polynomial having monomials extracted (up to sign) from the expressions: ηap+1pa1,b1...pap,bp,where0≤a1< b1<...<ap<ap+1≤bp≤m. Again, we have two disjoint families of monomials: – Products where bp<m, whose addition corresponds to hm−1+(−1)mηm(including p=0), and – Products where its last factor is pα,m. Let us add all the polynomials in the second family producing a polynomial called ˆ qm. The polynomial ˆ qmcan be, in turn, decomposed into two families: monomials starting from ηm(according to the discussion on gm, they correspond to ηm(gm− gm−1)=−ηmgm−1pm−1,m) and monomials starting from ηkwith k<m, which can be expressed as −ˆ qm−1pm−1,m(since ηk...pα,m=ηk...pα,m−1pm−1,m, provided that ηk...pα,m−1appears in ˆ qm−1; observe that the sign changes due to the decreasing of the subindex). This discussion proves that ˆ qmis equal to the polynomial qmdefined above, and shows the validity of the expression hm=hm−1+(−1)mηm+qm. As an example, the following is the computation of h3using the above definition: η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 theorems Having defined the functions, the following are the ACL2 theorems establishing the main properties (regarding the Normalization Theorem) of those polynomials: Theorem: cmp-diff-pol-diff-pol=0 m∈N→dm·dm+1=0 Theorem: G-pol-on-degenerate=0 (m∈N∧i∈N∧i<m)→gm·ηi=0 Theorem: G-pol-and-diff-pol-commute m∈N→dm·gm=gm−1·dm Theorem: H-pol-property-b m∈N+→dm+1·hm+hm−1·dm=id −gm We emphasize the fact that in these formulas, +and ·respectively denote addition and composition of simplicial polynomials. That is, we prove that the above equalities hold in the ring of simplicial polynomials. These properties are polynomial versions of some of the results we need to prove Theorem 2. In particular, cmp-diff-pol-diff-pol=0 is the polynomial version of the result establishing that dmis a differential homomorphism; theorem G-pol-on-degenerate=0 gives the behavior of gmon degenerate simplexes; G-pol-and-diff-pol-commute is the polynomial version of the result that states that gmis a chain morphism; and H-pol-property-b will be essential to prove property (b) required in the definition of reduction. These four theorems, although with substantial differences in its difficulty, have been proved in a similar way: we apply induction on the natural numbers and use the properties of the simplicial polynomial ring and the simplicial identities, to prove the inductive case. To illustrate this, we describe in the following subsection a sketch of the proof of the theorem G-pol-and-diff-pol-commute.2We hope this description will give the reader a flavor of how we prove properties in the ring of simplicial polynomials. The proof of the theorem H-pol-property-b is by far the most difficult, and we omit its description here due to the lack of space. We urge the interested reader to consult the source files. 4.3 A sketch of a proof of dm·gm=gm−1·dm Let us first give some lemmas that will be used in the proof. First, the following lemma establishes that gmand ∂kcommute when m<k: Lemma: G-pol-and-faces-commute (m∈N∧k∈N∧m<k)→∂k·gm=gm·∂k This property is easily proved by induction on m, and expanding the definition of gm. Now we prove a lemma that establishes how we can commute dmand pi,jwhen m<i<j. Again, this property is easily proved by induction on m, and expanding the definition of dm: Lemma: pij-pol-and-diff-pol-commute (n∈N∧i∈N∧j∈N∧m<i∧i<j)→pi−1,j−1·dm=dm·pi,j 2A sketch of the proof of the theorem cmp-diff-pol-diff-pol=0 was also given in Section 2 and its concrete ACL2 realization is presented in Appendix B. Let us now describe the proof of G-pol-and-diff-pol-commute,whichis proved by induction on m: •Base case: m=0.Thisistrivial,sinced0·id =id ·d0. •Inductive case: suppose m>0and dm−1·gm−1=gm−2·dm−1. We will see how we can rewrite dm·gmto gm−1·dm. First, we expand the definitions of gmand dm, and apply ring properties: 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-faces-commute above and the induction hypothesis, rewriting the last expression: gm−2·dm−1·(id −pm−1,m)+(−1)m·gm−1·∂m·(id −pm−1,m) Note that using the simplicial identity (5), it is easy to prove ∂m·(id −pm−1,m)= 0; using this identity and then applying distributivity, we obtain: gm−2·dm−1·(id −pm−1,m)=gm−2·(dm−1−dm−1·pm−1,m) Expanding the second occurrence of dm−1and applying distributivity, we have: gm−2·(dm−1−(−1)m−1·∂m−1·pm−1,m−dm−2·pm−1,m) Now, by the lemma pij-pol-and-diff-pol-commute, we have that dm−2· pm−1,mis equal to pm−2,m−1·dm−2; and applying the simplicial identity (5)we prove ∂m−1·pm−1,m=∂m. So we can simplify the last expression (contracting also the definition of dm) to the following: gm−2·(dm−pm−2,m−1·dm−2) Finally, it is not difficult to prove (using the simplicial identities) that pm−2,m−1· dm−2is equal to pm−2,m−1·dm; applying this to the last expression and factoring out dmwe obtain: gm−2·(id −pm−2,m−1)·dm=gm−1·dm The mechanical proof of G-pol-and-diff-pol-commute is carried out in ACL2 in a very similar way to the hand proof described above, guiding the prover with the appropriate lemmas and applying the same rewriting steps (although not necessarily in the same direction). As pointed out in Section 3, the polynomial ring properties, used as rewriting rules, are an essential component in this proof. 5 Reformulating the statement As we have seen, simplicial polynomials give us a convenient framework for reasoning about the simplicial maps and how they combine according to the simplicial identities. In this framework we have proved non-trivial properties about those combinations, needed for the proof of the Normalization Theorem. Nevertheless, being symbolic expressions, what we have proved is not a complete and faithful formalization of the standard formulation of this theorem in Simplicial Topology. For example, we have not defined notions like simplicial sets, chain complexes or degenerate simplexes. In this section we show a formalization of the Normalization Theorem in ACL2, as close as possible to the standard mathematical formulation presented in Section 2. We will also show how the theorems proved in the polynomial framework can be translated and used in this formalization. 5.1 Simplicial sets and chain complexes It is clear that the first step in our formalization has to be the definition of the notion of simplicial set, as presented in Definition 1. Since the theorem we want to prove is a result on any simplicial set, we introduce a generic simplicial set using the ACL2 encapsulation principle. A simplicial set can be defined by means of three functions K,dand n.The function Kis a predicate with two arguments, with the idea that K(m,x) holds if and only if x∈Km. The functions dand nhave both three arguments and they represent the face and degeneracy maps, respectively. The intended meanings for d(m,i,x)and n(m,i,x) are respectively ∂m i(x)and ηm i(x). To be generic, the only assumed properties about K,dand nare those stating well-defineness and the simplicial identities. They are introduced via encapsulate: Assumption: d-well-defined (x∈Km∧m∈N+∧i∈N∧i≤m)→∂m i(x)∈Km−1 Assumption: n-well-defined (x∈Km∧m∈N∧i∈N∧i≤m)→ηm i(x)∈Km+1 Assumption: 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)) Assumption: 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)) Assumption: 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)) Assumption: 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)) Assumption: simplicial-id5 (x∈Km∧m∈N∧i∈N∧j∈N∧i≤j≤i+1∧i≤m) →∂m+1 j(ηm i(x)) =x These assumptions are a formalization of the standard definition of simplicial set, as given in any textbook, and constitute the basis where we will state the Normalization Theorem. To differentiate from the polynomial framework, we will call this the “standard framework”. The next step is to define chain complexes in this standard framework. Since chains are linear combinations of simplexes of a given dimension, it is natural to represent them as lists whose elements are (dotted) pairs formed by an integer and a simplex. As with simplicial polynomials, we will consider only chains in canonical form: their elements must have non-null coefficients and have to be increasingly ordered with respect to a strict ordering. The following function sc-p defines chains in a given dimension m. It uses the function ss-p recognizing the dotted pairs formed by a non-null integer and a m-simplex, and the function ss-< implementing a strict ordering between such pairs (note that these functions take the dimension mas an argument): Definition: ss-p(m,s):=(consp(s)∧car(s)∈Z−{0}∧cdr(s)∈Km) Definition: sc-p(m,c):= if endp(c)then c=nil elseif endp(cdr(c)) then ss-p(m,first(c)) ∧rest(c)=nil else ss-p(m,first(c)) ∧ss-<(m,first(c),second(c)) ∧ sc-p(m,rest(c)) As with polynomials, the main advantage of considering chains in canonical form is that we can check its equality using equal. The main operations on chains are addition and scalar product by an integer, for each dimension m. The ACL2 functions for these operations are add-sc-sc(m,c1,c2)andscl-prd-sc(m,k,c). We omit their definitions here, because they are very similar to the corresponding operations on polynomials. In this paper we will use c1+c2and k·c, respectively, for those operations on chains. Note that, for the sake of readability, we omit the dimension and that we abuse of the notation using the same notation as with polynomials. Anyway, the precise meaning of every use of these symbols will be clear from the context. We have proved that the set of chains of a given dimension is an Abelian group with respect to addition, where the identity in this group is the zero chain (represented as nil and denoted here as 0). It is worth mentioning that, as we did in the case of polynomials, these definitions and theorems about chains were automatically generated as a particular instance of a more generic theory about the free Abelian group generated by a generic basis. Simplicial maps can be linearly extended on chains. For example, this is the definition of c-d, the face map extended to chains: Definition: [∂m i(c)] c-d(m,i,c):= if endp(c)then c else cons(car(first(c)),∂m i(cdr(first(c)))) +c-d(m,i,rest(c))) Note that this function is not a simple “mapcar” on the simplexes of a chain, since the result is returned in canonical form. In a similar way, we define c-n, the extension of the degeneracy map to chains. We will use the same notation (∂m i(c)and ηm i(c))to denote these maps both on simplexes and on chains. 5.2 Evaluation of simplicial polynomials As we have said before, our intention is to translate the theorems described in Section 3from the polynomial framework to the standard framework. The key point here is to interpret a simplicial polynomial as a function on chains of a given dimension. Recall from Section 3.3 that this will be only possible when the polynomial is well-formed for that dimension. To define the functional behaviour of a simplicial polynomial, we simply apply the operations indicated in the symbolic expression. For example, the following function eval-ld is the evaluation of a list of faces ld on a chain cof dimension m(where ld is expected to be valid for dimension m): Definition: eval-ld(ld,m,c):= if endp(ld)then c else c-d(m-len(rest(ld)),first(ld), eval-ld(rest(ld),m,c))) In a similar way, we can define the evaluation of a list of degeneracies of a given dimension. Extending these, we define the evaluation of simplicial terms (eval-st) and the evaluation of monomials (eval-sm). Finally, we define eval-sp,the evaluation of a polynomial on a chain in a given dimension: Definition: eval-sp(p,m,c):= if endp(p)then 0 else eval-sm(first(p),m,c)+eval-sp(rest(p),m,c)) The key properties of the evaluation function we have just defined is that for a given dimension, it behaves consistently with respect to the operations of the ring of simplicial polynomials, whenever the input polynomials are well-formed for that dimension: Theorem: eval-sp-add-sp-sp (p1∈P∧p2∈P∧m∈N∧c∈Cm(K)∧uniform-sp(p1)∧ uniform-sp(p2)∧valid-sp(p1,m)∧valid-sp(p2,m)∧ (endp(p1)∨endp(p2)∨degree-sp(p1)=degree-sp(p2))) →eval-sp(p1+p2,m,c)=eval-sp(p1,m,c)+eval-sp(p2,m,c)) Theorem: eval-sp-scl-prd-sp (p∈P∧m∈N∧c∈Cm(K)∧uniform-sp(p)∧ valid-sp(p,m)∧k∈Z) →eval-sp(k·p,m,c)=k·eval-sp(p,m,c) Theorem: eval-sp-cmp-sp-sp (p1∈P∧p2∈P∧m∈N∧c∈Cm(K)∧uniform-sp(p1)∧ uniform-sp(p2)∧valid-sp(p1,m+degree-sp(p2)) ∧valid-sp(p2,m)) →eval-sp(p1·p2,m,c)= eval-sp(p1,m+degree-sp(p2),eval-sp(p2,m,c)) These properties allow us to translate in a convenient way the properties proved in the polynomial framework to the corresponding properties in the standard framework. We can illustrate this by showing how we prove the differential property. Recall that the precise definition (without removing the superindexes) of the differential homomorphism is dm(c)=m i=0(−1)i∂m i(c). The following is the corresponding ACL2 definition in the standard framework. Note that we need an auxiliary function diff-aux to deal properly with the superindex: Definition: diff-aux(m,i,c):= if i∈ N+then ∂m 0(c) else (−1)i·∂m i(c)+diff-aux(m,i−1,c)) Definition: [dm(c)] diff(m,c):=diff-aux(m,m,c) The following theorem establishes the connection between the differential polynomial and the differential function, via eval-sp: Theorem: eval-sp-diff-pol (m∈N+∧c∈Cm(K)) →eval-sp(dm,m,c)=dm(c) Now, from the theorem cmp-diff-pol-diff-pol=0 in Section 3,usingthe theorem eval-sp-cmp-sp-sp and previously proving that dmis a polynomial wellformed for dimension mand with degree −1, we can easily prove the differential property for the function dm: Theorem: diff-diff=0 (m∈N+∧c∈Cm+1(K)) →dm(dm+1(c)) =0 5.3 The normalized chain complex We now describe the formalization of the normalized chain complex CN(K). First of all we define degenerate simplexes, those that can be obtained applying a degeneracy map to another simplex: Definition: [x∈KD m] Kd(m,x):=∃y,i(i∈N∧i<m∧y∈Km−1∧ηm−1 i(y)=x) The existential quantifier in this definition is introduced using defun-sk,which is the way ACL2 provides support for first-order quantification. This macro allows (by means of a choice axiom) to define functions whose body has an outermost quantifier. Having defined degenerate simplexes, we define non-degenerate simplexes simply as the negation of that property: Definition: [x∈KND m] Kn(m,x):=x∈Km∧x∈ KD m Since normalized chains are linear combinations of non-degenerate simplexes of a given dimension, we represent them in the same way as we represent general chains, but in this case requiring non-degenerate generators. As with general chains, the theory of normalized chains is obtained as an instance of the generic theory of freely generated groups. That is, this instantiated theory contains the definitions and properties showing that normalized chains together with addition is an Abelian group. We also proved that it is a subgroup of Cm(K)so it makes sense to denote c1+c2the addition of two normalized chains c1and c2;andk·cthe scalar product of an integer kand a normalized chain c. Since in our representation an element x of CN m(K)is also an element of Cm(K)(that is to say, there is a canonical implicit inclusion from CN m(K)to Cm(K), as sets), then any function defined on Cm(K)can also be considered defined on CN m(K); analogously, any function ranging over CN m(K) will be interpreted, implicitly, as ranging over Cm(K), too. We define the canonical epimorphism f:C(K)→CN(K)as the function that, given an element of Cm(K), returns the normalized chain obtained eliminating its degenerate addends. In our formalization, the following function F-norm defines f (here SSn-P checks the property of being a non-degenerate addend, and it uses the function Kn above): Definition: [fm(c)] F-norm(m,c):= if endp(c)then 0 elseif SSn-P(m,first(c)) then first(c)+F-norm(m,rest(c))) else F-norm(m,rest(c)) A key property relating the canonical chain epimorphism fand the differential on C(K)is the following: fm−1(dm(fm(c))) =fm−1(dm(c)). Intuitively, this means that if we apply normalization on the result of the differential of a chain, we obtain the same result as if we apply the same operation previously normalizing the chain. A sketch of the proof of this result is the following: given a chain c∈Cm(K),wecan write it as the result of summing its normalization and a linear combination of degenerate simplexes: c=fm(c)+kλk·ηm−1 ik(y). Thus, dm(c)=dm(fm(c)) +kλk· dm(ηm−1 ik(y)). From the definition of dmand applying the simplicial identities, it can be proved that dm(ηm−1 j(y)) is still a linear combination of degenerate simplexes (this is the essential property proving that the degenerate chain complex D(K), introduced in Section 2.1, is a chain subcomplex of C(K)). Thus, kλk·dm(ηm−1 ik(y)) is a linear combination of degenerate simplexes and therefore fm−1(dm(c)) =fm−1(dm(fm(c))). The following theorem establishes this result: Theorem: diff-n-F-norm (m∈N+∧c∈Cm(K)) →fm−1(dm(fm(c))) =fm−1(dm(c)) Let us now define the differential operation of the normalized chain complex CN(K), denoted as dN m(c). We will define it as the result of applying the differential dm, and after that, normalizing with fm−1. Definition: [dN m(c)] diff-n(m,c):= fm−1(dm(c)) The differential property for din C(K)(theorem diff-diff=0 in the last subsection), together with the property diff-n-F-norm, allows us to prove the differential property for dNin CN(K), since for all c∈CN m(K),dN m(dN m+1(c)) = fm−1(dm(fm(dm+1(c)))) =fm−1(dm(dm+1(c))) =fm−1(0)=0. The following theorem establishes it: Theorem: diff-n-diff-n=0 (m∈N+∧c∈CN m+1(K)) →dN m(dN m+1(c)) =0 6.2 The normalized chain complex In our approach to the problem, in order to build for each simplicial set Ka reduction (f,g,h):C(K)→CN(K), we have defined, by means of explicit formulas, two families of simplicial polynomials gmand hm(see Section 4.1).Forthesakeof simplicity, let us denote by Gin this subsection the function defined on C(K)by gm. Observe that the expression for G(as in the case of the homotopy operator h)is independent from the simplicial set K(and from the evaluation of simplicial operators over simplexes), while f(the canonical projection) requires for its definition a test function, determining whether a given simplex is degenerate or not. This implies that fdepends on K, and, as a consequence, it cannot be represented as a simplicial polynomial. This is the reason why in the formal proof the morphism fdoes not appear until Section 5. However, the very definition of CN(K)as a quotient in the category of chain complexes (recall: CN(K)=C(K)/D(K)) establishes that to define a chain morphism from CN(K)to another chain complex Camounts to defining a chain morphism form C(K)to Cwhich is null on D(K). In particular, the morphism G:C(K)→C(K)is null on degenerated simplexes (it has been proved in ACL2 by using the G-pol-on-degenerate=0 property) and it allows us to define g: CN(K)→C(K)as the unique chain morphism such that g◦f=G, identifying f with the canonical quotient map. Let us note that, in Section 5, a version slightly different has been used, considering CN(K)as a retract of C(K)in the category of graded Abelian groups. In other words, we take as definition CN n(K)=Z[KND n]. In this case, we have the diagram C(K) f --CN(K), i llwith an explicit definition of f, introducing dN:= f◦d◦iand checking that G=G◦i◦f, we obtain a chain morphism g:= G◦i. With this presentation the required prereduction properties follow easily from others proved in the simplicial framework. 6.3 Simplicial terms and dimension The equivalence between natural transformations and simplicial polynomials described in Section 6.1 allowed us to reduce the initial problem to deal with simplicial polynomials plus one dimension. Our ACL2 proof, described in Section 4,was however carried out over simplicial polynomials without any dimension information. The reason for this third, and last, simplification is now explained. Let us interpret i(which skips the element i∈N)andδj(which cover j∈Ntwice) as orderpreserving maps from Nto N. We denote by Nthe monoid of maps generated (by composition) from {i,δj;∀i,j∈N}. The elements of Nare exactly the orderpreserving maps from Nto Ncontaining a finite amount of information: they stabilize from a given number (that is, a function γ:N→Nsuch that there exists r0∈N satisfying γ(r+1)=γ(r)+1,∀r>r0). The elements in Ncan be represented in canonical form as explained for morphisms of the category . This proves that, as monoids, there is a canonical isomorphism between Nand our monoid of simplicial terms (the isomorphism being simply induced by contravariance). In Section 4we have worked with simplicial terms without dimension, that is to say with maps in Nand not in . We can now think in Nas a (monoidal) category with only one object, and morphisms the elements of the monoid. We can consider the functor (−)#:→Nwhich completes each morphism α:[n]→[m]of ,by stabilizing it in the following way: α#(k)=α(k)if k≤nand α#(k)=m+(k−n)if k>n. This is actually a functor; in particular, (α ◦β)#=α#◦β#. Moreover (−)#is faithful, that is to say: given two morphisms α, β :[n]→[m]such that α#=β#then α=β. In others words, equational reasoning about simplicial operators can be safely simulated over simplicial terms, without any reference to the dimensions where the simplicial operators apply. The same argument can be used in the ring of simplicial polynomials (defined as the free Abelian group on the monoid of simplicial terms), showing that any chain of equalities deduced from combinations over morphisms of the monoidal category Nalso holds in the valid dimensions. Thus, the complete proof of the Normalization Theorem can be developed in a first order setting by using equational reasoning on simplicial polynomials without explicit dimensions, as it has been done in ACL2 in Section 4, and it can be expressed as in Section 5by simply adding the validity condition among terms and dimensions. 7 Conclusions and further work In this paper we have formalized the Normalization Theorem, an important result in simplicial topology establishing a link between the two chain complexes that can be naturally associated to a simplicial set. An outstanding feature of our formalization is that it has been carried out in a first-order logic, even though in principle a higherorder setting could be considered more natural to state it. As a demonstration of this characteristic we have implemented the whole proof in the ACL2 theorem prover (we hope the techniques introduced have been explained in this paper with enough detail to be re-produced in other inductive reasoning environments, too). Another interesting benefit obtained from our proof is that it was inspired by some explicit formulas experimentally found in [23], showing the validity of the formulas, which kept up to now unproven. To quantify the proof effort, the complete formalization contains 100 definitions and 532 lemmas and theorems (with 89 non trivial proof hints explicitly given), which gives an idea of the degree of automation of the proof. As for the formalization development, we followed a standard interaction with the theorem prover. That is, we first had an original hand proof of the result that suggested the main definitions and lemmas. Some of these lemmas were not proved in a first attempt and new lemmas are then suggested from the inspection of the failed attempts. It is also worth pointing out that the whole development has benefited from the use of our instantiation tool for generic theories described in [17]. That allowed us to obtain in an automated way, the definitions and theorems proving the ring of simplicial polynomials and the Abelian group of chains and normalized chains, as instances of generic theories (we have not included these automatically generated definitions and lemmas in the statistics above). The planned future work is trying to extend the techniques introduced here (based on simplicial polynomials) to other problems in simplicial topology. Our next objective is the Eilenberg–Zilber Theorem [9,19]. It is a very important result giving a reduction between the chain complex of a Cartesian product of simplicial sets, CN(A×B), and the tensor product of the corresponding chain complexes of the factors, CN(A)⊗CN(B). The associated algorithm (in its most explicit version, arrows f,g,hare described by explicit formulas; see the Appendix in [21]) is very important in Kenzo, being responsible for a great part of the (exponential) complexity of many Kenzo programs. Thus the task of formalizing it can be considered a good next step for our project. The results in Section 6show that there are categorical reasons to think that the Eilenberg–Zilber Theorem could be tackled in a first order setting. From the ACL2 point of view, the challenge is that in the Eilenberg–Zilber Theorem there are two simplicial sets involved, and then the scope of our techniques should be significantly extended to be applied in that case. Acknowledgements We thank the anonymous referees for their careful revision and useful feedback. Appendix A: Checking the formalized proof To check our formalized proof in ACL2, the system has to be properly installed and the books that come with the distribution certified. Details about the installation of ACL2 can be obtained in section Obtaining and Installing at the web page http://www.cs.utexas.edu/users/moore/acl2/. The complete source files with the ACL2 formalization of the Normalization Theorem are accessible at: http://www.glc.us.es/fmartin/acl2/fantist in a file named fantist.tgz. This file should be expanded with the command: ...> tar -xzvf fantist.tgz This command builds the directory fantist with the whole formalization. To certify the formalization, the following command should be executed in the fantist directory: ...> cd fantist .../fantist> make -s all This command certifies all the books. It generates files .o,.cert and .date for every book in the distribution. A file .log is also created containing the ACL2 certification output corresponding to every book. Appendix B: ACL2 proof of 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))))) [Note: A hint was supplied for our processing of the goal above. Thanks!] By the simple: definition NATP and the :executable-counterpart of ADD-SP-SP-ID we reduce the conjecture to Goal’ (IMPLIES (AND (INTEGERP N) (<= 0 N)) (EQUAL (CMP-SP-SP (DIFF-POL N) (DIFF-POL (+ 1 N))) NIL)). This simplifies, using the :compound-recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER, the:definition DIFF-POL, primitive type reasoning, the :rewrite rules |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 the :type-prescription rule EXP-1, to 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 the formula above *1. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (DIFF-POL N). This suggestion was produced using the :induction rule DIFF-POL. If we let (:P N) denote *1 above then the induction scheme we’ll use is AND (IMPLIES (AND (NOT (ZP N)) (:P (+ -1 N))) (:P N)) (IMPLIES (ZP N) (:P N))). This induction is justified by the same argument used to admit DIFF-POL. When applied to the goal at hand the above induction scheme produces four nontautological 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))))))). But simplification reduces this to T, using the :compound-recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER, the :definitions ADD-SP-SP, DIFF-POL and SCL-PRD-SP, the :executable-counterparts of ADD-SP-SP-ID, CONSP, SP-P and ZIP, linear arithmetic, primitive type reasoning, the :rewrite rules |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 the :type-prescription rule 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))))))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. 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))))))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. 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))))))). But simplif\/ication reduces this to T, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of <, ADD-SP-SP, BINARY-+, CMP-SP-SP, DI, DIFF-POL, EXP-1, INTEGERP, NOT, SCL-PRD-SP and ZP and linear arithmetic. That completes the proof of *1. Q.E.D. ... Time: 0.56 seconds (prove: 0.51, print: 0.03, other: 0.02) CMP-DIFF-POL-DIFF-POL$=$0 References 1. Andrés, M., Lambán, L., Rubio, J., Ruiz-Reina, J.L.: Formalizing simplicial topology in ACL2. In: Proceedings ACL2 Workshop 2007, pp. 34–39. University of Austin (2007) 2. Aransay, C., Ballarin, C., Rubio, J.: A mechanized proof of the basic perturbation lemma. J. Autom. Reason. 40(4), 271–292 (2008) 3. Aransay, C., Ballarin, C., Rubio, J.: Generating certified code from formal proofs: a case study in homological algebra. Form. Asp. Comput. 22(2), 193–213 (2010) 4. Coquand, T., Spiwack, A.: Towards constructive homological algebra in type theory. In: Calculemus 2007, Lecture Notes in Artificial Intelligence, vol. 4573, pp. 40–54. Springer (2007) 5. De Loera, J.A., Rambau, J., Santos, F.: Triangulations. Structures for Algorithms and Applications. Springer (2010) 6. Domínguez, C., Lambán, L., Rubio, J.: Object-oriented institutions to specify symbolic computation systems. Rairo-Theor. Inform. Appl. 41, 191–214 (2007) 7. Domínguez, C., Rubio, J.: Computing in coq with infinite algebraic data structures. In: Calculemus 2010, Lecture Notes in Artificial Intelligence, vol. 6167, pp. 204–218. Springer (2010) 8. Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo Program. Institut Fourier, Grenoble (1999) http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/ 9. Epstein, D.B.A.: Semisimplicial objects and the Eilenberg–Zilber theorem. Invent. Math. 1, 209– 220 (1966) 10. Heras, J., Pascual, V., Rubio, J.: Proving with ACL2 the correctness of simplicial sets in the Kenzo system. In: LOPSTR 2010, Lecture Notes in Computer Science, vol. 6564, pp. 37–51. Springer (2010) 11. Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer (2000) 12. Lambán, L., Pascual, V., Rubio, J.: An object-oriented interpretation of the EAT System. Appl. Algebra Eng. Commun. Comput. 14(3), 187–215 (2003) 13. Lambán, L., Martín–Mateos, F.J., Rubio, J., Ruiz–Reina, J.L.: Applying ACL2 to the formalization of algebraic topology: simplicial polynomials. In: Interactive Theorem Proving 2011, Lecture Notes in Computer Science, vol. 6898, pp. 200–215. Springer (2011) 14. Mac Lane, S.: Homology. Springer (1963) 15. Mac Lane, S.: Categories for the Working Mathematician. Springer (1971) 16. Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. Springer (1992) 17. Martín–Mateos, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz–Reina, J.L.: A generic instantiation tool and a case study: a generic multiset theory. In: Proceedings of the Third International ACL2 Workshop and its Applications, pp. 188–201 (2002) 18. Martín–Mateos, F.J., Rubio, J., Ruiz–Reina, J.L.: ACL2 verification of simplicial degeneracy programs in the Kenzo system. In: Calculemus 2009, Lecture Notes in Artificial Intelligence, vol. 5625, pp. 106–121. Springer (2009) 19. May, J.P.: Simplicial Objects in Algebraic Topology. Van Nostrand (1967) 20. Medina–Bulo, I., Palomo–Lozano, F., Ruiz–Reina, J.L.: A verified common lisp implementation of Buchberger’s algorithm in ACL2. J. Symb. Comput. 45(1), 96–123 (2010) 21. Real, P.: Homological perturbation theory and associativity. Homol. Homotopy Appl. 2(5), 51–88 (2000) 22. Romero, A.: Effective homology and spectral sequences. PhD Thesis. Universidad de La Rioja (2007). Available at: http://www.unirioja.es/cu/anromero/tesis.pdf 23. Rubio, J., Sergeraert, F.: Supports acycliques and algorithmique. Astérisque 192, 35–55 (1990) 24. Rubio, J., Sergeraert, F.: Constructive algebraic topology. Bull. Sci. Math. 126, 389–412 (2002)