Church thesis

A principle according to which the class of functions computable by means of algorithms in the broad intuitive sense (cf. Algorithm), coincides with the class of partial recursive functions. Church' thesis is this fact of nature, which is confirmed by the experience accumulated in mathematics throughout its history. All known examples of algorithms in mathematics satisfy it. The thesis was first formulated by A. Church (1936). Each different precise definition of the intuitive notion of algorithm corresponds to its own version of Church' thesis. Turing's thesis is the assertion that every function that is computable in the intuitive sense is computable by some Turing machine, and Markov's normalization principle says that any function that is computable in the intuitive sense is computable by some normal algorithm. From the equivalence of the known definitions of the notions of algorithm, it follows that the various forms of Church' thesis are equivalent. This fact is yet another confirmation of Church' thesis. The thesis of Church cannot be strictly proved, since its formulation involves the inexact notion of "algorithm in the intuitive sense" . There were attempts to refute Church' thesis, but they have not led to success (1984). The acceptance of Church' thesis is useful in the theory of algorithms and its applications. First, in proving the existence of an algorithm of one kind or another — Turing machines, recursive functions, normal algorithms, and others — one may, by virtue of Church' thesis, restrict oneself to intuitively obvious constructions, and need not write out the corresponding formal scheme.

Moreover, Church' thesis is the basis for deducing the unsolvability of given algorithmic problems (cf. Algorithmic problem), according to which one can give a strict proof that some problem cannot be solved in the framework of this or that precision of the notion of algorithm.

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2]	H. Rogers jr., "Theory of recursive functions and effective computability" , McGraw-Hill (1967) pp. 164–165

Comments

Among the "different precise definitions of the intuitive notion of algorithm" Church and S.C. Kleene promoted especially the computation of functions via $\lambda$-definability (see Church $\lambda$-abstraction; $\lambda$-calculus). The importance of this approach is that it anticipated some essential features of high-level programming languages (cf. Programming language).

References

[a1]	H.P. Barendrecht, "The lambda-calculus, its syntax and semantics" , North-Holland (1978)