The Lambda Calculus for Absolute Dummies (2012)(palmstroem.blogspot.com)
palmstroem.blogspot.com
The Lambda Calculus for Absolute Dummies (2012)
http://palmstroem.blogspot.com/2012/05/lambda-calculus-for-absolute-dummies.html
10 comments
Lambda calculus is the computational equivalent of compass and straightedge geometrical construction[1]. It's about starting with fundamental and simple components and building higher-level abstractions upon these firm foundations. Euclid's Elements, which heavily relied on this approach and made it famous, was arguably the most influential mathematical text ever written.
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...
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...
... and just as Euclidean geometry, nobody actually uses it, and it is a controversial matter whether it is a good teaching tool [1].
It's elegant, but elitist, because it's unnecessarily difficult and hostile.
[1]: http://mathoverflow.net/questions/152352/is-euclid-dead
It's elegant, but elitist, because it's unnecessarily difficult and hostile.
[1]: http://mathoverflow.net/questions/152352/is-euclid-dead
Oh give me a break. Lambda calculus was created to study computation. To study computation in a rigorous manner, a mathematical model of computation was necessary. The more complex the model of computation, the more axioms you need. Complex models with many axioms are more difficult to reason about but are not actually more powerful (since they are all equivalent...) With a simple model of computation you can quickly build yourself more user-friendly systems (such as demonstrating how Church Encoding works, then proceeding to use it instead of writing it all out every time). It wasn't created out of some sense of elitism, it was created out of pragmatism.
Do you really think that Alonzo Church made his own work more difficult just to make others feel excluded? That's ludicrous.
Do you really think that Alonzo Church made his own work more difficult just to make others feel excluded? That's ludicrous.
... just like Euclidean geometry, it was created by a geometer for "internal usage". I am not contesting the usefulness of lambda calculus in academic contexts!
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.
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.
> I see no inherent value in writing [...]
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.
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.
Would you suppose there's any value in writing it as:
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.
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.
Although you did assume addition is associative (I wonder if there is some duality involved here)
Yeah I'm not sure. Actually, I wouldn't be surprised if I made a hidden commutativity assumption that would surface if I tried to justify treating multiplication as repeated addition like that.
Lambda calculus is model for abstract computation. Any computation. The fact that it can express and operationally reduce arithmetic is just a proof of usefulness, but it's not supposed to be limited to that.
I don't actually find this explanation easier to understand...
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/
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/
These diagrams are interesting too: http://homepages.cwi.nl/~tromp/cl/diagrams.html
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...
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...
I like this talk http://www.confreaks.com/videos/1287-rubyconf2012-y-not-adve...
Jim Weirich was an excellent speaker, and this was one of his best presentations. I thought his method of building up to the purpose of combinators (not just the Y) was much better than just an explanation. He references [1] (note url change) which does something similar and is also a good read/view.
[1] - http://codon.com/programming-with-nothing
[1] - http://codon.com/programming-with-nothing
I loved that talk. I found this lecture also instructive (not as entertaining as Jim's though): https://www.youtube.com/watch?v=FWkiO-F6X5E
This article is actually really confusing...
I thought it was clear. I would start with 1, not 0 for the first example of the derivation of Natural numbers via succession or the related Peano axiom. I know some texts start with 1 and others 0, but given counting most likely started with objects, it is more fundamental to begin with 1. The concept of nothing or zero just seems an abstract step away. Nice treatment of the lambda calculus.
[deleted]
It makes for a more elegant (imho) recursive definition of the sum. Instead of:
a + S(b) = S(a) + b
a + 0 = a
a + S(b) = S(a) + b
a + 1 = S(a)
You really want zero.
What's so funny about watching/reading all these explanations (videos, images, tutorials etc.) is the utter lack of mastery displayed by all the computer scientists / programmers in presenting a simple, rigorous, complete mathematical definition. Due to leaving out these essential details, and unable to actually define what 'the lambda calculus' is, they end up confusing people. Jim Weirich never actually articulates a clear definition and ends up uttering a jumble of words.. although I'm sure he understands it intuitively, he's not able to convey it.
[deleted]
Umm, Jim Weirich's explanation in this video makes pretty much perfect sense:
http://vimeo.com/45140590
Not if you don't already know what it is. It's not a definition. This is exactly what he says and shows starting at 6:30
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.
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.
He wasn't given a lecture about lambda calculus, he was giving a lecture about Y Combinators. While he gave a quick overview of lambda calculus (an overview which I would describe as effective and _sufficient for the rest of the lecture_), that should not be confused with an attempt to give a lecture about lambda calculus.
A more rigorous or 'correct' treatment of lambda calculus would not have improved his talk, it would have distracted from it..
A more rigorous or 'correct' treatment of lambda calculus would not have improved his talk, it would have distracted from it..
I wish I was an absolute dummy to get all of that...
yeah, TL;DR
My ADD brain just ain't up for that particular challenge tonight.
My ADD brain just ain't up for that particular challenge tonight.
People hate math formalism because it only makes sense if you already understand it.
It's more: you can only see how simple it really is once you understand it and it seems incredibly complicated until you do.
And that's incredibly frustrating for both sides of the student/teacher relationship.
And that's incredibly frustrating for both sides of the student/teacher relationship.
>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)
This article, and your comment, reminded me of 'Math Class (Imagined by Kids)' http://www.youtube.com/watch?v=KdxEAt91D7k (2 minutes long)
Heh, hadn't seen that before. I mostly remember wondering why the teacher was always talking about pizza.
And we already have man pages for that, thank you very much.
how to teach recursion
def teach(something):
lesson = None
// Aye, there's the rub...
if knowsHowToTeach():
lesson = createLessonForSomething(something)
else:
lesson = teach(something)
return lesson[deleted]
I lost interest at the 'minimalist gossip newspaper' analogy. In my opinion the power of the analogy is exaggerated. The text was easy to undestand until that part.
Lambda Calculus is actually extremely simple, and in my opinion, boring. When I took a unit on it in college, I guess the prof didn't do a good job motivating it. It's just substitution, and sometimes renaming variables. Nothing really useful, innovative, or interesting, except as representing computable functions.
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!