Re:Whiteboard problems in pure Lambda Calculus
by vilhelm_s on Monday March 20, 2017 @01:56PM
(#13916222)
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".
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/c... [1] https://projecteuclid.org/download/pdf_1/euclid.dmj/10774894... [2] https://en.wikipedia.org/wiki/%CE%9C-recursive_function