I find "To Dissect A Mockingbird" a more intuitive and simpler explanation of Lambda Calculus. I think the visuals help a lot.

http://dkeenan.com/Lambda/

There is also Bret Victor's Alligator Eggs game: http://worrydream.com/AlligatorEggs/

I know about these because I'm currently trying to learn λ-calculus by deriving and implementing functions in CoffeeScript: https://github.com/rbonvall/lambda-coffee/blob/master/lambda...

[1] - http://codon.com/programming-with-nothing

Audio: "This is the basics of lambda calculus right here. You’ve got the little lambda function, a lambda character and that’s indicates the beginning of a function definition. you say this function takes a varia..uh argument called x. The period denotes the beginning of the body of the function, and then whatever comes after the period is what is returned by the function. So this is an identify function here. Anything you give it, it returns back the same value. You have arguments, well ok you have variables, and you have functions. That's all you have in lambda calculus. There is nothing else, but variables and functions. "

Visual: There is a title to the slide, "λ-calculus". There is an image on the center of the slide with λx.x, and there are these words with arrows going to λx.x :

"punctuation", with two arrows coming out of it, going λ and . "argument (variable)" with an arrow to the first x "body (λ-expression)" with an arrow to the second x.

This person would fail the first definition-proof based math exam at Harvard. Let's say, the question is "What is a function?"

You can't say, well, uh, you have your f there, so basically, that's the function, and you have these arrows, and the x between the arrows, that's uh, your variable. f takes that, and uh, returns whatever's after the equal. So that's basically a function.

And I'd draw an image of f(x) = y, and have arrows to ()= saying punctuation, to f, "function", and x,y "variables".

Sloppy thinking like this is what resulted in inconsistencies in calculus, until people got rigorous and started giving good definitions of what exactly they're talking about. Here's a standard definition:

http://en.wikipedia.org/wiki/Function_(mathematics)#Definiti...

Common Intuition is not always a good guide for mathematics or computer science. The world is not as it seems. You have things like the Banach Tarski paradox, or Brouwer's fixed-point theorem which may be counterintuitive but once things clearly defined, makes more sense.

A more rigorous or 'correct' treatment of lambda calculus would not have improved his talk, it would have distracted from it..

And that's incredibly frustrating for both sides of the student/teacher relationship.

This article, and your comment, reminded me of 'Math Class (Imagined by Kids)' http://www.youtube.com/watch?v=KdxEAt91D7k (2 minutes long)

  def teach(something):
      lesson = None
      // Aye, there's the rub...
      if knowsHowToTeach():
          lesson = createLessonForSomething(something)
      else:
          lesson = teach(something)
      return lesson

2 x 3 = MULTIPLY 2 3 :⇔ (λ abc.a(bc)) (λ sz.s(s(z))) (λ xy.x(x(x(y)))) = λ c.(λ sz.s(s(z)))((λ xy.x(x(x(y))))c) = λ cz.((λ xy.x(x(x(y))))c)(((λ xy.x(x(x(y))))c)(z)) = λ cz.(λ y.c(c(c(y)))) (c(c(c(z)))) = λ cz.c(c(c(c(c(c(z)))))) = 6

This makes Brainf*ck look elegant!

By combining simple constructs according to simple rules, you can be certain that more complex constructs are themselves correct. This also often highlights simplicity and elegance in the underlying structure of otherwise complex constructs.

[1] http://en.wikipedia.org/wiki/Compass-and-straightedge_constr...

It's elegant, but elitist, because it's unnecessarily difficult and hostile.

[1]: http://mathoverflow.net/questions/152352/is-euclid-dead

Do you really think that Alonzo Church made his own work more difficult just to make others feel excluded? That's ludicrous.

I am just saying that lambda calculus is not the best approach in an engineering context, because it's too abstract, just like in practical terms, I see little use of Euclidean geometry in proving new theorems.

There isn't, in the similar sense that there is no inherent value in spending two hours assembling a bicycle then traveling with it one mile instead of simply taking 20 minutes to walk one mile.

Lambda calculus was not created as a better way of multiplying two numbers, just like you do not construct a bicycle to travel one mile. They have grander, or more ambitious, purposes. Multiplying two numbers or travelling one mile in over two hours simply serve as demonstrations of some of the capabilities of what was constructed.

Lambda calculus was created to help study computability; to explore mathematics with mathematics.

2 * 3 = (1 + 1) + (1 + 1) + (1 + 1) = 1 + 1 + 1 + 1 + 1 + 1 = 6?

Generally it's kind of pointless, but consider:

1 + 1 + 1 + 1 + 1 + 1 = (1 + 1 + 1) + (1 + 1 + 1) = 3 * 2

Interesting (imho), I just swapped the operands without assuming multiplication is commutative.

    a + S(b) = S(a) + b
    a + 0 = a

    a + S(b) = S(a) + b
    a + 1 = S(a)