Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Alonzo Church was an American mathematician and logician who made important contributions to mathematical logic and to theoretical computer science. He developed the lambda calculus in the 1930s as a tool to study computability,Footnote 1 and he showed that anything that is computable is computable by the lambda calculus. He proved that the first-order logic is undecidable (i.e. there is no algorithm to determine whether an arbitrary mathematical proposition is true or false). He founded the Journal of Symbolic Logic in 1936 (Fig. 15.1).

Fig. 15.1
figure 00151

Alonzo Church

Full size image

He was born in Washington, D.C., in 1903 and attended Princeton University. He obtained a bachelor’s degree in mathematics in 1924 and earned his Ph.D. in mathematics from the university in 1927. He received a 2-year National Research Fellowship in 1927 and spent a year at Harvard University and a year at the University of Göttingen and the University of Amsterdam. He taught at Princeton from 1929 until his retirement in 1967. He then taught at the University of California from 1967 until his second retirement in 1990. He died in 1995.

15.1 Lambda Calculus

Lambda calculus (λ-calculus) was developed by Alonzo Church in the 1930s to study computability. It is a formal system that may be used to study function definition, function application, parameter passing and recursion. It may be employed to define what a computable function is, and any computable function may be expressed and evaluated using the calculus. Church used lambda calculus in 1936 to give a negative answer to Hilbert’s Entscheidungsproblem.

It is equivalent to the Turing machine formalism developed by Alan Turing. However, the emphasis in the lambda calculus is on transformation rules, whereas Turing machines are concerned with computing on primitive mathematical machines. Lambda calculus consists of a small set of rules:

Every expression in the λ-calculus stands for a function with a single argument. The argument of the function is itself a function with a single argument, and so on. The definition of a function is anonymous in the calculus. For example, the normal definition of a function that adds one to its argument is f(x) = x + 1. However, in λ-calculus this successor function is defined as

$$ \lambda\;x\cdot x+1 $$

The name of the formal argument x is irrelevant, and an equivalent definition of the function is λ z · z + 1. The evaluation of a function f with respect to an argument (e.g. 3) is usually expressed by f(3). In λ-calculus this would be written as (λ x · x + 1) 3, and this evaluates to 3 + 1 = 4. Function application is left associative: i.e. f x y = (f x) y. A function of two variables is expressed in lambda calculus as a function of one argument which returns a function of one argument. This is known as currying, and it was developed by the Russian logician Schönfinkel and made popular by the American logician Haskell Curry. For example, the functionf(x, y) = x + y is written as λ x · λ y · x + y. This is often abbreviated to λ x y · x + y.

λ-calculus is a simple mathematical system, and its syntax is defined as follows:

$$ \begin{array}{lll} <\!\!\exp\!\!>\!\!&:: = <\!\!\mathrm{identifier}\!\!>\quad \quad \quad \quad | \\ & \boldsymbol{\lambda}\!\!<\!\!\mathrm{identifier}\!\!>\!\!.\!\!<\!\!\exp\!\!> \quad \; \; |-\mathrm{abstraction} \\ & <\!\!\exp\!\!> <\!\!\exp\!\!> \quad \quad \quad \qquad\!\!|-\mathrm{application} \\ & \left( {<\!\!\exp\!\!>} \right) \\ \end{array} $$

λ-Calculus’s four lines of syntax plus conversion rules are sufficient to define Booleans, integers, data structures and computations on them. It inspired Lisp and modern functional programming languages.

15.2 Decidability

Formalism was proposed by Hilbert as a foundation for mathematics in the early twentieth century. A formal system consists of a formal language, a set of axioms and rules of inference. Hilbert’s program was concerned with the formalization of mathematics (i.e. the axiomatization of mathematics) together with a proof that the axiomatization is consistent. The specific objectives were to:

  • Develop a formal system where the truth or falsity of any mathematical statement may be determined.

  • Provide a proof that the system is consistent (i.e. that no contradictions may be derived).

A proof in a formal system consists of a sequence of formulae, where each formula is either an axiom or derived from one or more preceding formulae in the sequence by an application of one of the rules of inference. Hilbert believed that every mathematical problem could be solved, and he therefore expected that the formal system of mathematics would be complete (i.e. all truths could be proved within the system) and decidable: i.e. that the truth or falsity of any mathematical proposition could be determined by an algorithm.

He believed that the truth or falsity of any mathematical proposition could be determined in a finite number of steps, and that the formalism would allow a mechanical procedure (or algorithm) to determine whether a particular statement was true or false. The problem of the decidability of mathematics is known as the decision problem (Entscheidungsproblem).

Definition 15.1 (Decidability)

Mathematics is decidable if the truth or falsity of any mathematical proposition may be determined by an algorithm.

Church and Turing independently showed this to be impossible in 1936. Turing showed that decidability was related to the halting problem for Turing machines, and that if first-order logic were decidable, then the halting problem for Turing machines could be solved. However, he had already proved that there was no general algorithm to determine whether a given Turing machine halts or not. Therefore, first-order logic is undecidable.

The question as to whether a given Turing machine halts or not can be formulated as a first-order statement. If a general decision procedure exists for first-order logic, then the statement of whether a given Turing machine halts or not is within the scope of the decision algorithm. However, Turing had already proved that it is not possible algorithmically to decide whether or not an arbitrary Turing machine will halt or not. Therefore, since there is no general algorithm that can decide whether any given Turing machine halts, there is no general decision procedure for first-order logic. The only way to determine whether a statement is true or false is to try to solve it. However, if one tries but does not succeed this does not prove that an answer does not exist.

There are first-order theories that are decidable. However, first-order logic that includes Peano’s axioms of arithmetic (or any formal system that includes addition and multiplication) cannot be decided by an algorithm. Propositional logic is decidable as there is a procedure (e.g. using a truth table) to determine if an arbitrary formula is valid in the calculus.

15.3 Computability

Church developed the lambda calculus in the mid-1930s, as part of his work into the foundations of mathematics. Turing published a key paper on computability in 1936, which introduced the theoretical machine known as the Turing machine. This machine is computationally equivalent to the lambda calculus and is capable of performing any conceivable mathematical problem that has an algorithm. Church defined the concept of an algorithm formally in 1936 and defined computability in terms of the lambda calculus. Turing defined computability in terms of the theoretical Turing machine.

Definition 15.2 (Algorithm)

An algorithm (or effective procedure) is a finite set of unambiguous instructions to perform a specific task.

A function is computable if there is an effective procedure or algorithm to compute f for each value of its domain. The algorithm is finite in length and sufficiently detailed so that a person can execute the instructions in the algorithm. The execution of the algorithm will halt in a finite number of steps to produce the value of f(x) for a given x in the domain of f. However, if x is not in the domain of f, then the algorithm may produce an answer saying so, or it may get stuck, or it may run forever and never halt.

The Church-Turing thesis states that any computable function may be computed by a Turing machine. There is overwhelming evidence in support of this thesis, including the fact that alternative formalizations of computability in terms of lambda calculus, recursive function theory and Post systems have all been shown to be equivalent to Turing machines.