Church's Thesis

From ProofWiki
Jump to navigation Jump to search


This page has been identified as a candidate for refactoring of advanced complexity.
In particular: Bring this into line with house standards.
Until this has been finished, please leave {{Refactor}} in the code.

New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.

Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Refactor}} from the code.


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 Mathison Turing's work had not been published.

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

In fact, Kurt Friedrich 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] 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 Friedrich Gödel in his famous paper of $1931$[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 Cole 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 $\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 Kleene's help, that the class of lambda-definable functions coincides with the class of recursive functions.


Post Systems

Emil Leon 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.



This needs considerable tedious hard slog to complete it.
In particular: More work to do yet.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Finish}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.



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.


Source of Name

This entry was named for Alonzo Church.


Historical Note

Alonzo Church made this proposal in a paper published in Volume $58$ of the American Journal of Mathematics in $1936$: An unsolvable problem in elementary number theory

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 $1963$ paper Computability of Recursive Functions (J. ACM Vol. 10, no. 2: pp. 217 – 255) by John C. Shepherdson and Howard E. Sturgis.
  2. ↑ 1931: Kurt Gödel: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme ("On formally undecidable propositions of Principia Mathematica and related systems") (Monatshefte f. Math. und Phys. Vol. 38: pp. 173 – 198)


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Church%27s_Thesis&oldid=628401"