Nonmodularity Results for Lambda Calculus

Abstract

The variety (equational class) of lambda abstraction algebras was introduced 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 variety generated by the term algebra of a semi-sensible lambda theory is not congruence modular. Another result of the paper is that the Mal'cev condition for congruence modularity is inconsistent with the lambda theory generated by equating all the unsolvable λ-terms.