I have three related subquestions, which are highlighted by bullet points below (no, they could not be split, if you are wondering). Andrej Bauer wrote, here, that some functions are realizable through a Turing machine, but not through lambda-calculus. A key step of his reasoning is:
However, if we use the lambda calculus, then [the program] c is supposed to compute a numeral representing a Turing machine out of a lambda term representing a function f. This cannot be done (I can explain why, if you ask it as a separate question).
- I would like to see an explanation/informal proof proof.
I don't see how to apply Rice's theorem here; it would apply to the problem "are this turing machine T and this lambda-term L equivalent?", because applying this predicate to equivalent terms gives the same result. However, the required function might compute different, but equivalent, TMs for different, but equivalent, lambda-terms.
- Moreover, if the problem is with introspection of a lambda-term, I think that passing a Gödel encoding of a lambda-term would be also acceptable, wouldn't it?
On the one hand, given that his example involves computing, in the lambda calculus, the number of steps needed by a Turing Machine to complete a given task, I'm not very surprised.
- But since here lambda-calculus can't solve a Turing-machine-related problem, I wonder whether one can define a similar problem for lambda-calculus and prove it unsolvable for Turing machines, or there is actually a difference in power in favor of Turing Machines (which would surprise me).