Nonmodularity results for lambda calculus
                            Antonino Salibra
               Universit`a Ca’Foscari di Venezia, Dipartimento di Informatica,
                      Via Torino 155, 30172 Venezia, Italy,
                          salibra@dsi.unive.it
                              Abstract
              The variety (equational class) of lambda abstraction algebras was intro-
            duced to algebraize the untyped lambda calculus in the same way cylindric
            and polyadic algebras algebraize the first-order predicate logic. In this paper
            we prove that the lattice of lambda theories is not modular and that the va-
            riety generated by the term algebra of a semi-sensible lambda theory is not
            congruencemodular. AnotherresultofthepaperisthattheMal’cev condition
            for congruence modularity is inconsistent with the lambda theory generated
            by equating all the unsolvable λ-terms.
            Key words and phrases. Lambda calculus, lambda abstraction algebras, combi-
            natory algebras, lattice of lambda theories, modularity, commutator.
         1 Introduction
         The untyped lambda calculus was introduced by Church [3, 4] as a foundation for
         logic. Although the appearance of paradoxes caused the program to fail, a consistent
         part of the theory turned out to be successful as a theory of “functions as rules”
         (formalized as terms of the lambda calculus) that stresses the computational process
         of going from the argument to value. Every object is at the same time a function
         and an argument; in particular a function can be applied to itself. There have been
         several attempts to reformulate the lambda calculus as a purely algebraic theory.
         However the general methods that have been developed in universal algebra and
         category theory, for defining the semantics of an arbitrary algebraic theory, are not
         directly applicable, since the untyped lambda calculus is not an equational theory
         in the normal sense. In fact, the equations, unlike the associative and commutative
         laws for example, are not always preserved when arbitrary terms are substituted for
         variables (e.g., λx:yx = λz:yz does not imply λx:xx = λz:xz). In [21, 25] Pigozzi
         and Salibra have introduced lambda abstraction algebras (LAA’s) which constitute
         a purely algebraic theory of the untyped lambda calculus. The equational theory
         of lambda abstraction algebras is intended as an alternative to combinatory logic
         (see Curry-Feys [5]) since it is a first-order algebraic description of lambda calculus,
         which allows to keep the lambda notation and hence all the functional intuitions.
         Combinatory algebras (CA’s) and lambda abstraction algebras are both defined by
          2
          universally quantified equations and thus form varieties in the universal algebraic
          sense. There are important differences however that result in theories of very differ-
          ent character. Functional application is taken as a fundamental operation in both
          CA’s and LAA’s. Lambda (i.e., functional) abstraction is also fundamental in LAA’s
          but in CA’s is defined in terms of the combinators k and s. A more important
          difference is connected with the role variables play in the lambda calculus as place
          holders. In a LAA this is also abstracted. It takes the form of a system of basic
          elements (nullary operations) of the algebra. This is a crucial feature of LAA’s that
          is borrowed from cylindric and polyadic algebras (see Henkin-Monk-Tarski [13] and
          Halmos [12]) and has no direct analogue in CA’s.
           The most natural LAA’s are algebras of functions, called functional LAA’s, which
          arise as “expansions” of suitable combinatory algebras by the variables of lambda
          calculus in a natural way. The situation in algebraic logic is analogous, and it is the
          algebraic-logic model that mainly motivated our study. In analogy to the case for
          LAA’s, the most natural cylindric (and polyadic) algebras are algebras of functions
          that are obtained by coordinatizing models of classical first-order logic. The smallest
          variety that includes all the functional algebras that are most closely connected with
          models of first-order logic constitutes the class of representable cylindric algebras. It
          is a proper subvariety of the class of all cylindric algebras, hence non-representable
          cylindric algebras exist. Questions related to the functional representation of various
          subclasses of lambda abstraction algebras were investigated by Pigozzi and Salibra
          in a series of papers [21, 23, 24, 25, 27]. In a recent paper Salibra and Goldblatt
          [31] have solved the problem of representability for LAA’s, by showing that every
          LAA is isomorphic to a functional LAA and that the class of isomorphic images of
          functional lambda abstraction algebras constitutes a variety of algebras axiomatized
          by the finite schema of identities characterizing LAA’s.
           The theory of lambda abstraction algebras can be regarded as axiomatizing the
          equations that hold between contexts of the lambda calculus, as opposed to lambda
          terms with free variables. We recall from Barendregt [1, Def. 14.4.1] that a context
          is a λ-term with some ‘holes’ in it. The essential feature of a context is that a free
          variable in a λ-term may become bound when we substitute it for a ‘hole’ within the
          context. Barendregt’s ‘holes’ play the role of algebraic variables, and the contexts
          are the algebraic terms in the similarity type of lambda abstraction algebras. In
          [30] Salibra has shown that, for every variety of LAA’s, there exists exactly one
          lambda theory whose term algebra generates the variety. For example, the variety
          generated by the term algebra of the least lambda theory λβ is the variety LAA of all
          lambda abstraction algebras. Hence the explicit finite equational axiomatization for
          the variety of lambda abstraction algebras provides also an explicit axiomatization
          of the identities between contexts satisfied by the term algebra of the least lambda
          theory λβ. These results prove useful in the lambda calculus as a way for applying
          the methods of universal algebra: we can study the properties of a lambda theory
          by means of the variety of LAA’s generated by its term algebra.
           It is well known that the structure of an algebra is affected by the shape of its
          congruence lattice. For example, it is easy to show that if a group G has three nor-
          malsubgroups (recall that normal subgroups of a group correspond to congruences),
          any two of which intersect in the trivial subgroup and generate the whole G, then
          Nonmodularity results for lambda calculus            3
          Gmust be Abelian. Put in another way, if the finite lattice M3 is a 0-1-sublattice
          of the lattice of congruences of G, then G is Abelian. Alternatively, the concept of
          Abelian group (and other important concepts such as the center of a group, the cen-
          tralizer of a normal subgroup, solvable group, and nilpotent group) can be defined
                                             −1 −1
          in terms of the commutator operation [M;N] = Sg({a b ab : a ∈ M;b ∈ N}) on
          normal subgroups: G is Abelian if, and only if, [G;G] is the trivial subgroup. The
          extension of the commutator to algebras other than groups is due to the pioneer-
          ing papers of Smith [33] and Hagemann-Hermann [11]. General commutator theory
          has to do with a binary operation, the commutator, that can be defined on the set
          of congruences of any algebra. The operation is very well-behaved in congruence
          modular varieties (see Freese-McKenzie [6] and Gumm [10]). Lipparini [17, 18] and
          Kearnes-Szendrei [15] have recently shown that under very weak hypotheses the
          commutator proves also useful in studying algebras without congruence modularity.
          Their deep results essentially connect: (a) identities or quasi-identities in the lan-
          guage of lattices satisfied by congruence lattices; (b) properties of the commutator;
          and (c) Mal’cev conditions, that characterize properties in varieties by the existence
          of certain terms involved in certain identities.
           The lattice of lambda theories of lambda calculus (see [1, Chapter 4]) is the
          congruence lattice of the term algebra of the least lambda theory λβ, and this term
          algebra generates the variety LAA of all lambda abstraction algebras (see Salibra
          [30]). We propose to study the properties of the lattice of lambda theories by the
          corresponding properties of the commutator in the variety LAA. In the present
          paper, we show that every variety of LAA’s generated by the term algebra of a
          semi-sensible lambda theory is not congruence modular, as a consequence it is not
          possible to apply to it the theory of commutator developed for congruence modular
          varieties. We also prove that two interesting lattices are not modular: the lattice of
          the lambda theories of lambda calculus and the lattice of the subvarieties of LAA. In
          spite of these negative results, we believe that the recent theory of the commutator
          for algebras without congruence modularity [17, 18, 15] can be fruitfully applied to
          the lambda calculus and we intend to investigate it in a future paper.
           Unless otherwise stated we shall use the terminology of Barendregt [1] for lambda
          calculus and that of Salibra and Goldblatt [31] for lambda abstraction algebras.
          For the general theory of lambda calculus the reader may consult Barendregt [1]
          and Krivine [16]. For lambda abstraction algebras and variable-binding calculi the
          reader may consult Goldblatt [7, 8], Pigozzi and Salibra [22, 27, 25, 26], Salibra and
          Goldblatt [31], and Salibra [29, 30]. For the general theory of universal algebras
          the reader may consult Burris and Sankappanavar [2], Gratzer [9], and McKenzie,
          McNulty and Taylor [19]. For commutator theory the reader may consult Freese
          and McKenzie [6], and Gumm [10]. The main references for cylindric algebras are
          [13] and [14]; for polyadic algebras it is [12]. We also mention here N´emeti [20]. It
          contains an extensive survey of the various algebraic versions of quantifier logics.
             4
             2 Basic Definitions
             Alattice order is a partial order on a nonempty set L with respect to which every
             subset of L with exactly two elements has both a least upper bound (join) and a
             greatest lower bound (meet). The join and meet of a and b are denoted respectively
             bya+bandab. AlatticeLismodularifitsatisfies themodularlaw: a(b+c) = ab+c
             for all a;b;c ∈ L such that c ≤ a.
               Acongruence on an algebra is just a compatible equivalence relation, that is, the
             kernel of some homomorphism. ConA, the set of all congruences of the algebra A,
             is naturally equipped with a lattice structure, with meet defined as set theoretical
             intersection. As a matter of notation, the least and largest congruences of an algebra
             are denoted by 0 and 1. A variety V of algebras is congruence modular if for all
             A∈V,thelattice ConA is modular.
             2.1   The lambda calculus
             The two primitive notions of the lambda calculus are application, the operation
             of applying a function to an argument (expressed as juxtaposition of terms), and
             lambda (functional) abstraction, the process of forming a function from the “rule”
             that defines it. The set F of λ-terms of lambda calculus over an infinite set I of
                                   I
             variables is constructed as usual: every variable x ∈ I is a λ-term; if t and s are
             λ-terms, then so are (st) and λx:t for each variable x ∈ I.
               An occurrence of a variable x in a λ-term is bound if it lies within the scope of
             a lambda abstraction λx; otherwise it is free. A λ-term without free variables is
             said to be closed. t[x := s] is the result of substituting s for all free occurrences of
             x in t subject to the usual provisos about renaming bound variables in t to avoid
             capture of free variables in s. The axioms of the λβ-calculus are as follows: t and s
             are arbitrary λ-terms and x;y variables.
              (α) λx:t = λy:t[x := y], for any variable y that does not occur free in t;
              (β) (λx:t)s = t[x := s];
                • t = t;
                • t = s implies s = t;
                • t = s, s = r imply t = r;
                • t = s, u = r imply tu = sr;
                • t = s implies λx:t = λx:s.
               (β)-conversion expresses the way of calculating a function (λx:t) on an argument
             s, while (α)-conversion says that bound variables can be replaced in a term under
             the obvious condition. A lambda theory T is any set of equations between λ-terms
             that is closed under (α) and (β) conversion and the five equality rules. We will write
             either T ⊢ t = s or t =T s for t = s ∈ T. λβ denotes the least lambda theory. The