Church's Thesis

From ProofWiki
Jump to: navigation, search

Thesis

The notion of an algorithmically computable function coincides with that of a recursive function.


Discussion

We have precise definitions of URM computable functions and recursive functions, and proved that a URM Computable Function is Recursive and vice versa.

Church's Thesis attempts to identify the precise mathematical idea of a recursive function with the more intuitively understood algorithmically computable function.

We can not have proof of the equivalence of these.

However, there are cogent arguments in favour, as follows.


Turing's Analysis

When Alonzo Church presented this thesis, Alan Turing's work had not been published.

However, from a philosophical standpoint, it gives considerable support to Church's Thesis.

In fact, Gödel himself did not accept Church's Thesis until he had seen Turing's work.

What Turing did was analyse very carefully what went on in an algorithmic computation, and design a theoretical machine, now called a Turing machine.

The functions that can be calculated by a Turing machine are precisely the recursive functions.

The unlimited register machine, documented in some detail on this website, is a descendant of the original Turing machine. The two machines are computationally completely equivalent.


Different Formulations of Computable Functions

On this website there is a body of work demonstrating that a URM Computable Function is Recursive and vice versa.

URMs were not devised until long after Church had stated his thesis.[1{{Stub}} However, in the 1930's, several different approaches were taken with a view to determining the character of algorithmically computable functions, and the interesting thing is that all of them turned out to be equivalent.


Gödel-Herbrand-Kleene

The concept of a primitive recursive function had been raised by Kurt Gödel in his famous paper of 1931{{Proofread}}2], although at the time he called them just "recursive functions". He also noted that they were computable (although did not use that term in his paper), but this was incidental - he raised the concept because they played a particular technical purpose in his paper.

The concept of a recursive function (which Gödel called a "general recursive function") had been obtained from the idea of minimization as raised by Jacques Herbrand.

Then it was Stephen Kleene who published his Normal Form Theorem, which introduced the notion of considering recursive functions as generated by operations on functions. It is possible (but not trivial) to prove that this approach leads to the same class of functions as does the earlier approach of treating them as functions whose values can be derived by an equation calculus.


Church's Lambda Calculus

Alonzo Church developed the lambda calculus as a general system for deriving theorems about numbers. This system was shown to be inconsistent, but he rescued the bit which dealt with definitions of functions.

The idea is that in usual mathematics, it is difficult to tell the difference between a function of $f \left({x}\right)$ and its value for an unknown $x$.

Nowadays we have various notations, like $x \mapsto x^2$, and so on. Church's notation was different, but equivalent.

He used $\lambda x \left[{x^2}\right]$. Expressions of that type are called lambda terms, and he introduced rules for turning one term into another.

But the point was that lambda terms are to be thought of as strings of symbols, not numbers and functions. Numbers are represented by particular lambda terms, and a function is said to be lambda-definable if there is a lambda term which can map between the lambda terms and the function itself.

Church was able to prove, with Kleene's help, that the class of lambda-definable functions coincides with the class of recursive functions.


Post Systems

Emil Post derived, independently of Alan Turing, an approach to computation machines very similar to Turing's.

While Turing machines manipulate symbols on tape, Post's system consists of manipulating strings of symbols according to a set of specific rules called production rules.



Strict Formalism

Church's Thesis is nowadays generally accepted, but it can be argued that it does not even "make sense", on the grounds that mathematics can not be allowed to deal with informal concepts of any kind.

That is, mathematics is the study of formal systems.

This is the view of strict formalism.

In contrast exists the view that ideally we "should" present mathematics as a formal system, but underlying this is the idea that by learning what we can about them, we may be able to gain greater insight into less regimented streams of thought.


Source of Name

This entry was named for Alonzo Church.

He made this proposal in a paper published in 1936: An unsolvable problem in elementary number theory, published in the American Journal of Mathematics Issue 58.

That paper was based on a talk he had delivered a year earlier.

Because of the influence of Alan Turing, this thesis is sometimes called the Church-Turing Thesis.


References

  1. The URM was introduced in the paper Computability of Recursive Functions J. ACM 10(2): 217-255 (1963) by John C. Shepherdson and Howard E. Sturgis.
  2. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme ("On formally undecidable propositions of Principia Mathematica and related systems") Monatshefte für Mathematik und Physik 38: 173-98.