### 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:

• It provided the conceptual substrate for denotational semantics (perhaps the most promising, comprehensive and rigorous technique for describing what programming languages "mean").
• It inspired the field of pure-functional programming, probably the currently the promising line of research in programming language design. ("Haskell" appears likely to be to functional programming what Smalltalk was to object-oriented programming: The proof-of-concept implementation that moves the idea from the lab into mainstream consciousness.)
• It influenced the creation of Lisp, as witness the "lambda" syntax used to this day in Lisp -- although John McCarthy, inventor of Lisp, strenuously denies that Lisp was ever intended to be an implementation of the lambda calculus.

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.