Boolean algebra and lambda calculus
by
Antonino Salibra
University of Venice

One of the milestones of modern algebra is the Stone representation theorem for Boolean algebras. In [1] Manzonetto and Salibra have shown that Comer's generalization of the Stone representation theorem holds also for combinatory algebras: any combinatory algebra is isomorphic to a weak Boolean product of directly indecomposable combinatory algebras. The proof of the representation theorem for combinatory algebras is based on the fact that every combinatory algebra has central elements, i.e., elements which define a direct decomposition of the algebra as the Cartesian product of two other combinatory algebras. Central elements in a combinatory algebra constitute a Boolean algebra, whose Boolean operations can be defined by suitable combinators. Then it is natural to investigate the semantics of lambda calculus given in terms of models, which are directly indecomposable as combinatory algebras (indecomposable semantics, for short).

The indecomposable semantics includes all known models of lambda calculus (i.e., the continuous, stable and strongly stable semantics), and the term models of all semisensible lambda theories (theories which do not equate solvable and unsolvable terms). The class of indecomposible combinatory algebras is a universal class, so that it is closed under subalgebras and ultraproducts. This implies that, if the term model of a lambda theory T is decomposible in a non-trivial way, then every model of T can be also decomposible in a non-trivial way. It follows that the indecomposable semantics is incomplete because there exist lambda theories whose term models admit non-trivial central elements.

We also study what is the influence of the logic underlying a model of lambda calculus over the equational theory of the model. Scott continuous models, which include graph models, Krivine models and filter models, can be classified according to the algebraic structure of their universe: a complete Boolean algebra for graph models, a complete Heyting algebra for Krivine models, and a complete lattice for filter models. We start the study of this problem by showing the following result: Let K be the class of all (isomorphs of) graph models in an algebraic signature including the Boolean operations. Then the class SP(K) is a variety and the class S(K) of all (isomorphs of) subalgebras of graph models is the universal class of simple algebras in SP(K). Is the variety SP(K) finitely axiomatizable?

[1] G. Manzonetto, A. Salibra. Boolean algebras for lambda calculus. 21th Annual IEEE Symposium on Logic in Computer Science (LICS 2006), IEEE Computer Society Press, 2006.

Date received: June 22, 2007