danielogue

Jun 24
Permalink

Turing’s paper is very clear

http://lambda-the-ultimate.org/node/3304#comment-48516

You should read Turing’s original paper, then. It’s a model of clarity! At the time he wrote his paper on TMs, mathematicians and logicians had spent almost fifty years trying to figure out how what an “effective procedure” or “finite computation” meant. His paper was the first entirely satisfying account of what that was.

In the early part of nineteenth century, when mathematicians used the word “function”, they meant some algebraic expression built out of things like +, -, × ÷, sine, cosine, exponentiation, and so on, perhaps defined piecewise over intervals. Basically, the idea was that you could interpret functions as rules telling you how to compute one number from another.

However, people kept generalizing the notion of function, and between the twin demands of analysis and set-theoretic formalization, eventually the concept of function had to be generalized to its modern form, which is to interpret a function from a set A to a set B, as a relation pairing each element of A with a single element of B. However, this allows obviously non-rule-like functions, especially since the post-Cantorian world allows the definition of enormously infinite sets.

But obviously, something has been lost in this generalization — namely, we’ve given up the idea that a function must supply an effective method for producing Bs from As. Since this is obviously a valuable idea, mathematicians then spent a lot of time effort trying to formalize what an effective method might be. This was especially vital given the importance of finitist methods to both Hilbert’s program and Brouwer’s constructivism.

They came up with a lot of contenders! Skolem suggested using primitive recursive arithmetic definitions to formalize Hilbert’s notion of finite method. Church advocated the lambda calculus. Goedel suggested the use of systems of guarded recursive equations. And those are just the systems of the most famous logicians; there were many more.

The reason that none of them took over is because while it was possible to see that many definitions could be expressed in each one, it wasn’t clear that any intuitively effective method could be so expressed. What Turing did was to analyze the operations that human mathematicians performed while doing a calculation, and then give a formal model in which each thing that we do corresponds to exactly one of the operations of his machine.

This made the intuitive argument that he had gotten things right much more compelling, and that’s why Goedel and Church and all those guys hailed TMs as such a triumph — Turing had made it extremely clear exactly what was going in in the transition from informal to formal. This meant that you could now take any model of computation you like, chosen for whatever good mathematical properties it had, and then show its universality simply by showing its equivalence with TMs.

For example, I love lambda calculus because of its tight connections to intuitionistic mathematics, and I know I haven’t lost anything because it’s easy to prove that the lambda calculus is equivalent in power to TMs.

By neelk