Go to the first, previous, next, last section, table of contents.


Turing Machines and Lambda Calculus

One of the surprising results from mathematical analysis of computation (generally credited independently to Alan Turing and Alonzo Church) is that a very simple machine of the von Neuman variety (or of any one of many similar designs, including for example Conway's ingenious Game of Life, a cellular automaton popular nowadays as a computer screen saver) is capable of computing anything which we know any way at all of computing.

For example, it is quite possible to build a machine of this sort with only one or two instructions (which perhaps respectively read two bits and store back the negated OR of them, and conditionally select one of two possible next instructions depending on the value of a given bit) which is quite capable of performing any computation we might want. Almost all the instructions contained in modern computers are logically unneccessary: They are included only to speed up specific common operations, such as addition.

Turing's proof that a given machine is a Universal Turing Machine, capable of computing anything which can be computed at all, is quite simple in concept, reducing to showing that such a machine can be programmed to emulate perfectly any other machine which you can describe precisely, and hence can compute whatever the described machine could compute.

Alonzo Church worked in a more mathematical setting, developing a simple abstract lambda calculus, and then similarly showing that any other computational scheme could be described in terms of it.

Turing's proof has an intuitively pleasing nuts-and-bolts quality to it that made it more immediately appealing and popular: To this day we speak of "Universal Turing Machines" rather than (say) "Lambda Calculus Isomorphism". (Turing's name also produces better puns about Universal Touring Machines...)

Church's lambda calculus has however perhaps had a deeper and more significant impact:

Since Muq MUF is in turn based heavily on Lisp, it can be reasonably argued that anyone programming in Muq MUF owes a considerable intellectual debt to both Alan Turing's proof, with his abstract "Turing Machines" which led to the underlying computer architecture, and to Church's proof, which led to the underlying software architecture.

Both proofs were of course at the time considered to be exercises in "pure mathematics", devoid of any practical application grin.


Go to the first, previous, next, last section, table of contents.