[bcoates]

That's just the lambda abstraction, not the lambda calculus.

The idea is that a lambda abstraction, in a math sense, is much less general than a single argument function. 'sin θ' is a single argument function that's defined by some business about the ratio of sides of a right triangle with angle θ, but it's not a lambda abstraction because all they're allowed to do is substitute a variable into some expression. 'f(x) = x² - x' can be directly expressed as a lambda abstraction (f = λ x. x² - x)

Once you guarantee that the function takes the specific form, you can manipulate it in ways you can't manipulate the general-case function, and it turns out those manipulations give you enough power to define almost anything else you'd want to do.

As it turns out, (IIRC) Python makes lambdas essentially opaque objects, and doesn't let you peek into them any more than you can a general-case function. This means you can't do any lambda-calculus on them, even simple stuff like determining if they are exactly the same expression.

[kd0amg]

Once you guarantee that the function takes the specific form, you can manipulate it in ways you can't manipulate the general-case function, and it turns out those manipulations give you enough power to define almost anything else you'd want to do.

In λ calculus, the only way one term can inspect another is by applying it. You don't get an intensional view of a λ abstraction. The other language features that get built on top of this (conditionals, tuples, etc.) only rely on functions' extensional features.