From λ-calculus to universal algebra and back

Abstract

We generalize to universal algebra concepts originating from λ-calculus and programming to prove a new result on the lattice λT of λ-theories, and a general theorem of pure universal algebra which can be seen as a meta version of the Stone Representation Theorem. In this paper we introduce the class of Church algebras (which includes all Boolean algebras, combinatory algebras, rings with unit and the term algebras of all λ-theories) to model the "if-then-else" instruction of programming. The interest of Church algebras is that each has a Boolean algebra of central elements, which play the role of the idempotent elements in rings. Central elements are the key tool to represent any Church algebra as a weak Boolean product of indecomposable Church algebras and to prove the meta representation theorem mentioned above. We generalize the notion of easy λ-term of lambda calculus to prove that any Church algebra with an "easy set" of cardinality n admits (at the top) a lattice interval of congruences isomorphic to the free Boolean algebra with n generators. This theorem has the following consequence for the lattice of λ-theories: for every recursively enumerable λ-theory φ and each n, there is a λ-theory φ n ⊆ φ such that {ψ: ψ⊆ φn } "is" the Boolean lattice with 2 n elements. © 2008 Springer-Verlag Berlin Heidelberg.