The Turing Machine vs. Lambda Calculus

[0xBADFEED]

The Turing Machine vs. Lambda Calculus, which is the superior formal model of computing? Yes, I know they are equivalent in power but which is superior in style and general amzingness.

I have to go with The Turing Machine.

It's very intuitive and you can explain it to a layman in less than 5 minutes. Further, it's amazing to me that such a simple concept is so deep. The idea of formalizing an abstract machine for the purpose of studying computation is just really cool and was fairly revolutionary at the time. Also, it forms the theoretical basis for operations at the actual hardware level.

It's just one of those really cool thought-experiments that bore some amazing fruits.

[Xanthir]

Turing Machines blow. Doing *anything* with them is stupid.

Lambda calculus is better, but not by much. Depending on how pure you're being, it can be just as stupid.

BRAINF*CK is the best trivial model of computation.

[stephentyrone]

BRAINF*CK is the best trivial model of computation.

+1 for brainfuck as a model of computation.

[TNorthover]

Lambda calculus for me. In fact I'm just working on a Haskell program to translate stuff into lambda for the giggles.

Turing machines are nice and revolutionary for their time, but pretty much the same as any computer that any of us could use; no really novel concepts for anyone who's done any programming.

[Briareos]

The lambda calculus, because it's (structurally) simpler. And more abstract.

[Berengal]

Lambda calculus, for actually being useful instead of just another turing tarpit.

You all probably know, but for thoroughness, here's the definition:

• Variables: I'll write these with lowercase letters
• Abstraction: \lambda and .
• Grouping: Parenthesis
• Expressions: Defined by the set \Lambda
  • x is a variable \rightarrow x \in \Lambda
    
  • x is a variable \wedge M \in \Lambda \rightarrow (\lambda x.M) \in \Lambda
    
  • M, N \in \Lambda \rightarrow (M N) \in \Lambda

I'll be using usual shorthand when writing expressions.
In addition, I'm going give names to some expressions. These are purely shorthand, meaning the expression can be substituted for the name anywhere in another expression, alpha-converting variables in case of any clashes. Substitution can always be performed and will always terminate, meaning a name will never appear on the right-hand-side of its definition, no matter how often you substitute any other names appearing there.

The definition of the lambda calculus is only seven lines long, but is it useful? Indeed it is. In fact, it's a fully fledged programming language despite being completely abstract and without any relation to any real-world machine, or even mathematics outside of its definition.

So what can we program?

Well, let's start with some simple definitions and see where they take us.


Here's part of a nice abstraction. I like to call it boolean algebra.
TRUE = \lambda x y. x
FALSE = \lambda x y. y

Some syntactic sugar:
IF = \lambda p t f. p t f

- IF TRUE TRUE FALSE -> TRUE TRUE FALSE -> (\lambda x y. x) TRUE FALSE -> TRUE

AND = \lambda x y. IF x y FALSE
OR = \lambda x y. IF x TRUE y
NOT = \lambda x. IF x FALSE TRUE
BOOLEQ = \lambda x y. IF x y (NOT y)

- AND TRUE FALSE -> IF TRUE FALSE FALSE -> TRUE FALSE FALSE -> FALSE
- OR TRUE FALSE -> IF TRUE TRUE FALSE -> TRUE TRUE FALSE -> TRUE
- NOT TRUE -> IF TRUE FALSE TRUE -> TRUE FALSE TRUE -> FALSE
- BOOLEQ FALSE TRUE -> IF FALSE TRUE (NOT TRUE) -> NOT TRUE -> FALSE

How about datastructures? We carry on and define linked lists:

CONS = \lambda x y f. f x y
FIRST = \lambda p. p (\lambda x y. x)
SECOND = \lambda p. p (\lambda x y. y)
NIL = \lambda x. TRUE
NIL? = \lambda p. p (\lambda x y. FALSE)

- FIRST (CONS TRUE FALSE) -> CONS TRUE FALSE (\lambda x y. x) -> (\lambda x y. x) TRUE FALSE -> TRUE

Lists of bools are a little boring. Let's define numbers
ZERO = \lambda f x. x
ONE = \lambda f x. f x
PLUS = \lambda m n f x. m f (n f x)
SUCC = \lambda n -> PLUS n ONE
MULT = \lambda m n f x. m (n f) x
SHIFTINC = \lambda p. CONS (SECOND p) (SUCC (SECOND p))
- (P = (CONS ZERO ONE) in:) SHIFTINC P -> CONS (SECOND P) (SUCC (SECOND P)) -> CONS ONE (SUCC ONE)
PRED = \lambda n. FIRST (n SHIFTINC (PAIR 0 0))
SUB = \lambda m n. (n PRED) m
ZERO? = \lambda n. n (CONST FALSE) TRUE
NUMEQ = \lambda m n. AND (ZERO? (SUB m n)) (ZERO? (SUB n m))

Most of you should still be relatively unconfused, I think. Let's define a few more list function. Unfortunately, they're mostly recursive, since lists are a recursive datastructure. We need recursion! Fortunately, lambda calculus has recursion. Of course it does, or it wouldn't be turing-complete!

Y = (\lambda f. (\lambda x. f (x x)) (\lambda x. f (x x)))

Now then, the list functions we all know and love

MAP = Y (\lambda map f l.
IF (NIL? l)
NIL
(CONS (f (FIRST l))
(map f (SECOND l))))

FILTER = Y (\lambda filter p l.
IF (NIL? l)
NIL
(IF (p (FIRST l))
(CONS (FIRST l) (filter p (SECOND l)))
(filter p (SECOND l))))

FOLDL = Y (\lambda foldl f x l.
IF (NIL? l)
x
(foldl f (f x (FIRST l)) (SECOND l)))

I don't know about you, but to me this is starting to look very much like lisp...
Now, to compare what we've got to a few real languages, let's implement sum-of-a-list in a couple of them and lambda calculus.

- Haskell first:

Code: Select all

sum list = foldl (+) 0 list

- How about Java?

Code: Select all

int sum(int[] nums){
        int total = 0;
        for(int i = 0; i < nums.length; i++){
            total += nums[i];
        }
        return total;
    }

- And lambda calculus?
SUM = \lambda list. FOLDL PLUS ZERO list

[TNorthover]

To be fair, a similar analysis could be applied to Turing machines, depending on the symbol set. The rules for combining two programs would be a little more complicated but really once you've got substitution useful programs arrive quickly.

[EduardoLeon]

The Turing Machine is nicer, because it's a lot like actual computers, while Lambda Calculus is "out of this world". I doubt you can implement a machine that evaluates lambda expressions natively.

Some things are nice in lambda calculus, though:

1. You can do this kind of elimination:

( λ abc...xyz . (expression that doesn't involve x y z) x y z ) = ( λ abc... . (expression) )

Examples:

MULT = ( λ mnfx . m (n f) x ) = ( λ mnf . m (n f) )
EXP = ( λ mnfx . (n m) f x ) = ( λ mn . n m )

2. The Church numeral 1 is nothing but an empty lambda; when it's evaluated, it just disappears without affecting the rest of the expression:

1 = ( λ fx . fx ) = ( λ f . f )
1 = ( λ . ) ???

3. The Church numeral 0, when evaluated, has the only effect of disappearing the next symbol:

0 = ( λ fx . x )
0 = ( λ f . ) ???

[Briareos]

As usual, Berengal is at least twelve times as eloquent as I am when making a point in the C.S. fora.

As to implementing a machine that "natively" deals with the lambda calculus: who cares? The Church-Turing thesis says the two models are equal in power, as the OP already mentioned. The lambda calculus is the better abstraction of computation. I think it makes it easier and nicer to think about computation. Implementation isn't relevant.

[rabuf]

The Turing Machine is nicer, because it's a lot like actual computers, while Lambda Calculus is "out of this world". I doubt you can implement a machine that evaluates lambda expressions natively.

If you consider lisp (specifically scheme) sufficiently close to the \lambda-calculus, then this paper describes just such a machine:
http://dspace.mit.edu/handle/1721.1/5731

[EduardoLeon]

If you consider lisp (specifically scheme) sufficiently close to the -calculus, then this paper describes just such a machine:
http://dspace.mit.edu/handle/1721.1/5731

At some lower level, perhaps at hardware level, computation must be dealt with in an imperative way. Or else, you should build a piece of electronics that can represent natively either a lambda expression or the symbols lambda expressions are made of.

[stephentyrone]

At some lower level, perhaps at hardware level, computation must be dealt with in an imperative way.

Seriously? Did you even read the paper?

Also: even in a normal commercial hardware, at the lowest levels, there is rather little "imperative" structure. Big swaths of chip area are dedicated to functionality that allows a processor to behave as though it had cohesive state and acted in a strictly imperative fashion.

[qbg]

Skip the lambda calculus and go straight to lisp.

[phillipsjk]

Nitpick: True Turing Machines have unlimited memory and execution time. (Halting problem loophole!)

[littlebuddy]

lambda calculus

[0xBADFEED]

Lots of people seem to be talking about the relative usefulness of Lambda Calculus compared to the Turing Machine. In a matter such as this I think usefulness is highly overrated.

[Berengal]

There's lots of research still going on in Lambda Calculus. Especially when it comes to types, LC is pretty much the go-to petri dish.

Also, the term language of statically typed functional languages (Haskell and friends) pretty much is LC with sugar on top.

It's not what I'd call useless.

Turing machines on the other hand...

[0xBADFEED]

There's lots of research still going on in Lambda Calculus. Especially when it comes to types, LC is pretty much the go-to petri dish.
...
It's not what I'd call useless.
Turing machines on the other hand...

Oh I'm not debating whether LC is more useful (in most ways) than the Turing Machine, it is. I was just saying I don't consider 'usefulness' to be one of the major criteria I use as to which one I think is cooler. Largely I like the TM for the historical aspects and ease of explanation. I would never 'use' it for anything (except maybe in the context of a proof).

One question I was thinking of is what would have happened if Turing had never created any of his works or any of his research and we were only left with LC at that time. How far back would that have set the arrival of actually usable computers, if at all? The TM is fairly obviously mappable to an actual machine, LC not so much.

[stephentyrone]

One question I was thinking of is what would have happened if Turing had never created any of his works or any of his research and we were only left with LC at that time. How far back would that have set the arrival of actually usable computers, if at all? The TM is fairly obviously mappable to an actual machine, LC not so much.

My money is on "not at all". Shannon and Von Neumann (and others) were much more directly responsible for the modern approach to mapping computation onto actual hardware. Complexity Theory would likely look entirely different as a field, though I suspect that many of the same results would have been derived, just with entirely different approaches.

[Berengal]

One question I was thinking of is what would have happened if Turing had never created any of his works or any of his research and we were only left with LC at that time. How far back would that have set the arrival of actually usable computers, if at all? The TM is fairly obviously mappable to an actual machine, LC not so much.

My money is on "not at all". Shannon and Von Neumann (and others) were much more directly responsible for the modern approach to mapping computation onto actual hardware. Complexity Theory would likely look entirely different as a field, though I suspect that many of the same results would have been derived, just with entirely different approaches.

Agreed. The Turing Machine seems more like an accidental byproduct than an arche. Computers existed before the Turing Machine, and were well into their infancy before the Turing Machine was well known. So while the machine provides a succinct and easy to understand mapping between the physical devices and a mathematical concept, it wasn't the inspiration for either, and both existed before the machine did.

At least this is how I've interpreted the history. I don't have much hard evidence to back it up.

[LakatosIstvan]

I am pretty shocked a little that so little teaching resources concerning Lambda Calculus can be found on the Internet. Considering how mind-bogglingly useful it is it really amazes me...

[bieber]

I am pretty shocked a little that so little teaching resources concerning Lambda Calculus can be found on the Internet. Considering how mind-bogglingly useful it is it really amazes me...

Speaking of which, does anyone have a preferred resource they'd care to point me towards for learning more about the lambda calculus? I'm mid-way through my CS bachelors now, and I'm not entirely sure if we'll ever be covering it (we're doing the assorted categories of automota in Discrete Structures now, starting wih FSAs and working up towards the Turing machine), so a good read I can find online would be much appreciated.

[hotaru]

Speaking of which, does anyone have a preferred resource they'd care to point me towards for learning more about the lambda calculus?

Sushi's Universal Logic Catalogue – The Ultimate Lambda Pow(d)ers

[LakatosIstvan]

Speaking of which, does anyone have a preferred resource they'd care to point me towards for learning more about the lambda calculus?

Sushi's Universal Logic Catalogue – The Ultimate Lambda Pow(d)ers

From what I understood, this is more about A++, you know, the implementation of the generalization of lambda calculus.

But thanks for the hint. A++ now became my favorite programming language

[MadRocketSci2]

Please compose your next post on a machine designed around Lambda Calculus. Thank you.

[Meteorswarm]

Please compose your next post on a machine designed around Lambda Calculus. Thank you.

Historical precedent is not proof of superiority. Just because the designers of circuits made processors act more similarly to Turing machines doesn't imply that Turing machines are somehow better. There's no reason we can't build a lambda calculator, it's just not what we've geared ourselves to do, and since there are lovely compilers for functional languages that work on Turing machine-like computers, I don't think we ever will.

[qbg]

Turing machines are too boring; combinator calculus is much more interesting.

[afarnen]

My vote is with the Lambda Calculus.

First of all, I just find this to be pretty:

(\lambda mnfx.mf(nfx))(\lambda fx.f(f(fx)))\lambda fx.(f(f(f(f(fx)))))

Second, the entire state of, and everything you need to know about the computer is recorded within a single algebraic expression--that's elegance that a Turing Machine can never possess.

Thirdly, the Lambda Calculus is useful, simple (and dare I say fun) as Berengal pointed out so well.

[ochuckles]

Aren't LC and TM equivalent in power in precisely the same way that Lisp and Brainfuck are?

[Robert'); DROP TABLE *;]

Aren't LC and TM equivalent in power in precisely the same way that Lisp and Brainfuck are?

Well, we're in for a shock if they aren't, since that's the Church Turing hypothesis.

(\lambda mnfx.mf(nfx))(\lambda fx.f(f(fx)))\lambda fx.(f(f(f(f(fx)))))

Can someone well-versed in the lambda calculus explain what they does? It just looks like a mess to me.

[scarecrovv]

(\lambda mnfx.mf(nfx))(\lambda fx.f(f(fx)))\lambda fx.(f(f(f(f(fx)))))

Can someone well-versed in the lambda calculus explain what they does? It just looks like a mess to me.

I would hardly consider myself well-versed, but it looks like the above expression is equivalent to

\lambda fx.(f(f(f(f(f(f(f(fx))))))))

which is the function that takes a function and a second argument, and applies the function to the second argument 8 times. Don't ask me why this is useful, though I'm sure it serves some purpose. Attaching some variable names would be nice.

And Lambda Calculus is better.

[Ptolom]

Has anybody read To Mock a Mockingbird by Raymond Smullian? It's an introduction to lambda calculus in the form of puzzles about birds. I've been enjoying working through it.

[phlip]

which is the function that takes a function and a second argument, and applies the function to the second argument 8 times. Don't ask me why this is useful, though I'm sure it serves some purpose.

It's the Church numeral for 8. It's just a way of embedding arithmetic in lambda calculus (like how the finite ordinals are a way of embedding arithmetic in set theory).

Specifically, afarnen's lambda thing is representing 3+5 - \lambda m n f x. m f (n f x) is addition, in that if you apply it to two Church numerals, it'll evaluate to the Church numeral representing their sum.