Nonmodularity results for lambda calculus (Q2729668)

A \(\lambda\)-theory is a set of equations involving closed \(\lambda\)-terms which is consistent and closed under the postulates of the \(\lambda\)-calculus. \(\lambda\)-theories form a lattice which, as the author has shown previously, is the congruence lattice of the term algebra of the least \(\lambda\)-theory \(\lambda\beta \). This term algebra generates the variety LAA of all lambda abstraction algebras. (These are purely algebraic theories of untyped lambda calculus.) In this paper the author shows that the lattice of \(\lambda\)-theories is not modular and that the variety created by the term algebra of a semisensible \(\lambda\)-theory (one where no solvable and unsolvable term are equated) is not congruence modular. Also he shows that the Mal'tsev condition for congruence modularity is inconsistent with the lambda theory generated by equating all unsolvable \(\lambda\)-terms.