Applying Universal Algebra to Lambda Calculus

摘要

The aim of this article is double. From one side we survey the knowledge we have acquired these last ten years about the lattice of all A-theories (equational extensions of untyped λ-calculus) and the models of lambda calculus via universal algebra. This includes positive or negative answers to several questions raised in these years as well as several independent results, the state of the art about the long-standing open questions concerning the representability of λ-theories as theories of models, and 26 open problems. On the other side, against the common belief, we show that lambda calculus and combinatory logic satisfy interesting algebraic properties. In fact the Stone representation theorem for Boolean algebras can be generalized to combinatory algebras and A-abstraction algebras. In every combinatory and A-abstraction algebra, there is a Boolean algebra of central elements (playing the role of idempotent elements in rings). Central elements are used to represent any combinatory and A-abstraction algebra as a weak Boolean product of directly indecomposable algebras (i.e. algebras that cannot be decomposed as the Cartesian product of two other non-trivial algebras). Central elements are also used to provide applications of the representation theorem to lambda calculus. We show that the indecomposable semantics (i.e. the semantics of lambda calculus given in terms of models of lambda calculus, which are directly indecomposable as combinatory algebras) includes the continuous, stable and strongly stable semantics, and the term models of all semisensible A-theories. In one of the main results of the article we show that the indecomposable semantics is equationally incomplete, and this incompleteness is as wide as possible.