From \(\lambda \)-calculus to universal algebra and back. (English) Zbl 1173.03302

Manzonetto, Giulio; Salibra, Antonino

Ochmański, Edward (ed.) et al., Mathematical foundations of computer science 2008. 33rd international symposium, MFCS 2008, Toruń Poland, August 25–29, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85237-7/pbk). Lecture Notes in Computer Science 5162, 479-490 (2008).

Summary: We generalize to universal algebra concepts originating from \(\lambda \)-calculus and programming to prove a new result on the lattice \(\lambda T\) of \(\lambda \)-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 \(\lambda \)-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 \(\lambda \)-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 \(\lambda \)-theories: for every recursively enumerable \(\lambda \)-theory \(\varphi \) and each \(n\), there is a \(\lambda \)-theory \(\varphi _{n } \supseteq \varphi \) such that \(\{\psi : \psi \supseteq \varphi _{n }\}\) “is” the Boolean lattice with \(2^{n }\) elements.
For the entire collection see [Zbl 1154.68021].

MSC:

03B40	Combinatory logic and lambda calculus
08A70	Applications of universal algebra in computer science

Keywords:

lambda calculus; universal algebra; Church algebras; Stone representation theorem; lambda theories