Editing Lambda calculus (section)

== Computability ==
There is no algorithm that takes as input any two lambda expressions and outputs {{Mono|TRUE}} or {{Mono|FALSE}} depending on whether one expression reduces to the other.<ref name="Church1936" /> More precisely, no [[computable function]] can [[decision problem|decide]] the question. This was historically the first problem for which undecidability could be proven. As usual for such a proof, ''computable'' means computable by any [[model of computation]] that is [[Turing complete]]. In fact computability can itself be defined via the lambda calculus: a function ''F'': '''N''' → '''N''' of natural numbers is a computable function if and only if there exists a lambda expression ''f'' such that for every pair of ''x'', ''y'' in '''N''', ''F''(''x'')=''y'' if and only if ''f'' {{Mono|''x''}}&nbsp;=<sub>β</sub>&nbsp;{{Mono|''y''}}, where {{Mono|''x''}} and {{Mono|''y''}} are the [[Church numeral]]s corresponding to ''x'' and ''y'', respectively and =<sub>β</sub> meaning equivalence with β-reduction. See the [[Church–Turing thesis]] for other approaches to defining computability and their equivalence.

Church's proof of uncomputability first reduces the problem to determining whether a given lambda expression has a [[beta normal form|normal form]]. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a [[Gödel numbering]] for lambda expressions, he constructs a lambda expression {{Mono|''e''}} that closely follows the proof of [[Gödel's incompleteness theorems|Gödel's first incompleteness theorem]]. If {{Mono|''e''}} is applied to its own Gödel number, a contradiction results.