|
|
|
|
|
by chewxy
2405 days ago
|
|
Church-Turing concerns computations not algorithms. The difference is subtle. A "computation" is what we would call a function application today - given an input, compute the output based on some rules. An "algorithm" is a set of such rules, usually operational rules (do this, then do this). The class of computations that Church and Turing are equivalent are the functions from N to N (encoding required obvs), as proven by Turing. Everything else is conjecture. Turing gives "computable by Turing machine", and Church gives "effectively calculable by the lambda calculus". Kleene holds them both to be the same, culminating in Theorem XXX. This misses a subtle point that this only applies up to the class of functions from N->N. When the class of functions is S->S, where S is a string or tree of symbols, lambda calculus runs into some minor issues. For example, you cannot define equality of terms in lambda calculus nor can lambda calculus realize itself. Bob Harper's book is the only book I know of that was explicit about this fact, though he dismisses it as a minor issue. Barendregt surprisingly also missed this. |
|