Turing’s contributions to lambda calculus

1. Fixed point combinators in untyped lambda calculus The untyped lambda calculus was introduced in 1932 by Church as part of an investigation in the formal foundations of mathematics and logic. The two primitive notions of the lambda calculus are application and λ-abstraction. Application, writtenMN, is the operation of applying the termM considered as an algorithm to the term N considered as an input. Lambda abstraction, written λx.M, is the process of forming a function from the expression M (possibly) depending on x. We refer to Barendregt et al. (2012) (this volume) for an intuitive account of the system. An important feature of lambda calculus is that it has fixed point com-binators, namely programs Y satisfying YM = M(YM) for all M ’s. These constitute the main ingredient for writing recursive programs in functional style. Turing contributed to this subject by providing a fixed point combi-nator Θ having the additional property that the equality between ΘM and M(ΘM) results simply by reducing the former to the latter (which is not the case, in general). Finally we report how Böhm and van der Mey gave a general receipt to generate many new fixed point combinators starting from a fixed one. Turing’s fixed point operator can be obtained in this way. Lambda terms, reduction and conversion Formally, the set Λ of λ-terms is defined inductively as follows. every variable x is in Λ; if M,N ∈ Λ, then MN ∈ Λ; if M ∈ Λ, then λx.M ∈ Λ, for every variable x