Algebra and Topology in Lambda Calculus The

untyped lambda calculus was introduced around 1930 by Church [11] as part of an investigation in the formal foundations of mathematics and logic. Although lambda calculus is a very basic language, it is sufficient to express all the computable functions. The process of application and evaluation reflects the computational behavior of many modern functional programming languages, which explains the interest in the lambda calculus among computer scientists. The lambda calculus, although its axioms are all in the form of equations, is not a true equational theory since the variable-binding properties of lambda abstraction prevent variables in lambda calculus from operating as real algebraic variables. Consequently the general methods that have been developed in universal algebra, for defining the semantics of an arbitrary algebraic theory for instance, are not directly applicable. There have been several attempts to reformulate the lambda calculus as a purely algebraic theory. The earliest, and best known, algebraic models are the combinatory algebras of Curry and Schönfinkel (see [12]). Combinatory algebras have a simple purely equational characterization and were used to provide an intrinsic first-order, but not equational, characterization of the models of lambda calculus, as a special class of combinatory algebras called λ-models [1, Def. 5.2.7]. Lambda theories are equational extensions of the untyped lambda calculus closed under derivation. They arise by syntactical or semantic considerations. Indeed, a λtheory may correspond to a possible operational semantics of lambda calculus, as well as it may be induced by a model of lambda calculus through the kernel congruence relation of the interpretation function. The set of lambda theories is naturally equipped with a structure of complete lattice (see [1, Chapter 4]), where the meet of a family of lambda theories is their intersection, and the join is the least lambda theory containing their union. The bottom element of this lattice is the minimal lambda theory λβ, while the top element is the inconsistent lambda theory, hereafter denoted by ∇. Although researchers have mainly focused their in