Church's Thesis

== 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 presented this thesis, 's work had not been published.
However, from a philosophical standpoint, it gives considerable support to Church's Thesis.
In fact, himself did not accept Church's Thesis until he had seen '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.The URM was introduced in the $1963$ paper by and . 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 in his famous paper of $1931$, 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 called a "general recursive function") had been obtained from the idea of minimization as raised by .
Then it was 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 ====
 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 $\map f x$ 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 \sqbrk {x^2}$. 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 help, that the class of lambda-definable functions coincides with the class of recursive functions.
==== Post Systems ====
 derived, independently of , 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 cannot 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.
== Also known as ==
== Historical Note ==
== References ==
== Sources ==
* 
* 
* 
* 
* 
* 
Category:Church's Thesis
Category:Mathematical Logic
Category:Philosophical Questions