3 ms·

Turing discovered the Universal machine. Church tried convincing Godel that lambda-calculus is universal, but Godel wasn't ready to accept it. When Turing defi

by sn41 10y ago

Turing discovered the Universal machine. Church tried convincing Godel that lambda-calculus is universal, but Godel wasn't ready to accept it. When Turing defined his machine model as a model for mechanical computation, Godel was convinced. In an appendix to that paper, Turing also showed that his model was computationally equivalent to the lambda calculus. This involved writing a "universal" lambda expression, i.e. a combinator. (Y combinator is the most famous one, I think that was discovered by Haskell B. Curry.) It was when Turing proved this equivalence that Godel accepted lambda calculus as a model of intuitive computation. In between, I have heard that Church's student, Kleene, did formulate fixed-point combinators when proving addition was computable in the lambda-calculus. Kleene was then convinced that this was a universal model of computation. I do not know why Church did not follow this up. So Turing does have some primacy over Church. *edit: Most of Turing's work on this was done as an undergraduate at Cambridge, /before/ he became Church's doctoral student. So the work was not done under Church's supervision. If you want to read further, you can read Soare's work on this tangled history: http://www.people.cs.uchicago.edu/~soare/History/compute.pdf http://www.people.cs.uchicago.edu/~soare/History/compute.pdf https://en.wikipedia.org/wiki/History_of_the_Church%E2%80%93Turing_thesis#Soare https://en.wikipedia.org/wiki/History_of_the_Church%E2%80%93...

vilhelm_s 10y ago
Surely Church must also have discovered the universal machine? Church's major result was the undecidability of the halting problem, and to set up the diagonalization proof you need a notion of interpreting a program. Looking at his paper[0], he has THEOREM XII. It is possible to associate simultaneously with every well-formed formula an enumeration of the formulas obtainable from it by conversion, in such a way that the function of two variables, whose value, when taken of a well-formed formula A and a positive integer n, is the n-th formula in the enumeration of the formulas obtainable from A by conversion, is recursive. THEOREM XVI. Every recursive function of positive integers is λ-definable. So approximately, Theorem XII gives an algorithm for evaluating a program A n steps, and theorem XVI says that this algorithm can be compiled in the a λ-calculus program. Church cites a paper by Kleene for this construction[1]. It's true that the Kleene doesn't prove this using a general recursion combinator like the Y combinator; instead he first shows how to λ-encode primitive recursive functions, and gives a combinator for the μ operator [2]. When you talk about Church "not following up" the notion of universality, I'm not sure what more you would want him to do. Of course he did not prove that λ-calculus was equivalent to Turing machines, because those had not been invented yet. But he and Kleene did prove that the λ-definable functions coincide with the μ-recursive functions, which was the best known model of universal computation. And he argues ([0] section 7) that this captures the intuitive notions of "a function for which there exists an algorithm" and "a function which can be proven to have a given value". [0] https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/church.pdf https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/c... [1] https://projecteuclid.org/download/pdf_1/euclid.dmj/1077489488 https://projecteuclid.org/download/pdf_1/euclid.dmj/10774894... [2] https://en.wikipedia.org/wiki/%CE%9C-recursive_function https://en.wikipedia.org/wiki/%CE%9C-recursive_function

by sn41 10y ago

vilhelm_s 10y ago

Surely Church must also have discovered the universal machine? Church's major result was the undecidability of the halting problem, and to set up the diagonalization proof you need a notion of interpreting a program. Looking at his paper[0], he has THEOREM XII. It is possible to associate simultaneously with every well-formed formula an enumeration of the formulas obtainable from it by conversion, in such a way that the function of two variables, whose value, when taken of a well-formed formula A and a positive integer n, is the n-th formula in the enumeration of the formulas obtainable from A by conversion, is recursive. THEOREM XVI. Every recursive function of positive integers is λ-definable. So approximately, Theorem XII gives an algorithm for evaluating a program A n steps, and theorem XVI says that this algorithm can be compiled in the a λ-calculus program. Church cites a paper by Kleene for this construction[1]. It's true that the Kleene doesn't prove this using a general recursion combinator like the Y combinator; instead he first shows how to λ-encode primitive recursive functions, and gives a combinator for the μ operator [2]. When you talk about Church "not following up" the notion of universality, I'm not sure what more you would want him to do. Of course he did not prove that λ-calculus was equivalent to Turing machines, because those had not been invented yet. But he and Kleene did prove that the λ-definable functions coincide with the μ-recursive functions, which was the best known model of universal computation. And he argues ([0] section 7) that this captures the intuitive notions of "a function for which there exists an algorithm" and "a function which can be proven to have a given value". [0] https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/church.pdf https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/c... [1] https://projecteuclid.org/download/pdf_1/euclid.dmj/1077489488 https://projecteuclid.org/download/pdf_1/euclid.dmj/10774894... [2] https://en.wikipedia.org/wiki/%CE%9C-recursive_function https://en.wikipedia.org/wiki/%CE%9C-recursive_function