Applying Universal Algebra to Lambda Calculus

The aim of this paper is double. From one side we survey the knowledge we have acquired these last ten years about the lattice of all λ-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 can be generalized to combinatory algebras and λ-abstraction algebras. In every combinatory and λ-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 ...

• Type: Journal
• Year: 2010
• Where: LOGCOM
• Authors: Giulio Manzonetto, Antonino Salibra
• Keywords: Algebras, Lambda Calculus, LOGCOM 2010, λ-abstraction Algebra