What is the contribution of lambda calculus to the theory of computation?

> Seeing proofs as programs really helped me come to terms (heh) with mathematical logic.

I suppose this underscores how some people think algebraically while others think analytically. I am an algebraic thiner. I like to break apart algorithms into a mathematical calculus to understand them.

Humorous: http://bentilly.blogspot.com/2010/08/analysis-vs-algebra-pre...

Two brief comments:

(1) The λ-calculus is better thought of as the MVP of SEQUENTIAL programming languages. It is not a good formalism for concurrency. Thee π-calculus is more suitable for concurrency, and, in a real sense, subsumes λ-calculus (see R. Milner's "Functions as Processes" and its subsequent elaborations for details).

(2) Proofs = λ-terms works best for CONSTRUCTIVE logic. With classical logic where not-not-A = A, it kind of works, but not really well.

> implement it almost for free

What does this phrase mean?

The term calculus generally refers to a system of calculation. I don't get why you're expecting lambda calculations to solve anything.

The lambda calculus is an intellectual framework for the description of computation and logic, just like Newton's calculus forms the basis for a description of physical processes.

Lambda calculus, like Turing Machines, was created as part of an investigation into the fundamentals of mathematics and in particular what is meant by "computation" - so it was never really intended as a practical tool for solving real world problems - which was arguably very much the motivation for Newton's creation of what is generally called "calculus".

Edit: I don't think javajosh's question is unreasonable - not sure why it is getting downvoted.

Interesting point, since personally in my experience, lambda calculus is overly held up as useful to learn. While simple models are very useful, it has a geek culture/hierarchy aspect too. (http://en.wikipedia.org/wiki/Knights_of_the_Lambda_Calculus)

In explaining things, I find it very important to deflate intimidating-sounding jargon; and discover for oneself if something really is important, or whether it has more of a dysfunctional social purpose like mystery-of-the-priesthood for initiates.

How would you write a program which compute the speed of the ball in your example, and how would you ensure or prove that your program is correct? That's what lambda calculus and all its derived works give you. Others have described it more elegantly here, so please refer to their posts, but if you want references, check out the Curry-Howard isomorphism, Hindley-Milner type system, System F, or what Coq, Agda and similar languages bring on the table.

You could also look at the answers given in the linked stackexchange page, of course.

A century ago, mathematicians were busy proving theorems (for instance, about calculus), and some of them were trying to figure out if we could start with a mathematical/logical statement and just calculate the answer, "this is true" or "this is false". They were not thinking about electronic computers, and they weren't concerned about how long it would take, they just wanted to know if you could calculate the answer at all, using an algorithm and pen an paper, and eventually finishing with an answer. For example, if you have just something like "10^23423 is bigger than 23454^10", there's no question about it, you can calculate the answer by using the definitions of integer numbers, product and exponentiation . But what about any mathematical or logical statement? That was the big question.

A re-statement of your example is that differential calculus gives you the definitions of limit and derivative, and it helps you with real world problems that are well modeled by differentiable functions. It also tells you that some functions are not differentiable.

Lambda calculus starts with a definition of what is calculating, and then it tells us that the answer to big question is "no", some functions cannot be calculated. But it also tells us that whatever can be calculated, can be done with a very, very simple programming language.

A concrete example: say we use your own.

Say we do have a function f(t) that tells us the location of the ball with respect to time. Something like (I'll use JavaScript as my implementation language, as it is capable and accessible):

    function location_x(t){ return 2 * t; }
    function location_y(t){ return 3 * t; }

In calculus, we say that the derivative of f(t) with respect to t can be approximated by calculating the limit as dt approaches 0 in the equation "(f(t + dt) - f(t)) / dt". Since you imply you know linear calculus, I'll not explain the jargon there.

Well, f(t) could be anything in that description, it doesn't necessarily have to be a function describing the position of a ball. So why don't we make f a variable? Why don't we write a general-purpose derivation function that can compute the derivative of any function given to it?

To do this, we need the ability to treat functions as "first-class citizens", as things we can manipulate just as much as we do primitive integers and decimal numbers.

That includes being able to refer to a function without evaluating it (i.e. storing it as a variable, able to pass it around, with no special knowledge of its purpose, just as we can pass integers to a function and it doesn't matter that the integer is 10 or 173 or -83491, we pass it to our function in the same way every time). We also need to be able to create functions on the fly (just as we might create integers other than the ones we typed in literally through arithmetic operations). We finally need the ability to capture the the values of any variable defined outside of our functions at the time the function was defined. This is called lexical scope, because it follows how we read the code, and functions that do this are called closures, because they "close over" the referenced values. Imagine the function hugging out further and further to accept everyone in. It's important that the values get captured and not the references, which we'll see why later.

Because of these three things, I could have also written my location functions as:

    var location_x = function (t){ return 2 * t; }
    var location_y = function (t){ return 3 * t; } 

How do you write the literal value of an integer? "2". How do you write the literal value of a function? In JavaScript it's "function(args){statements}". A named function--as you are used to them in procedural languages--is really just a function value stored in a variable that has a name. Just like a named integer is just a literal integer stored in a variable that has a name. We could even have an array of functions!

    var location = [function (t){ return 2 * t; },
                    function (t){ return 3 * t; }];

Okay, so what does our derive function look like:

    function derive(f){ // f is an argument that accepts a function as a parameter
        return function(t, dt){ // we will return a new function
            return (f(t + dt) - f(t)) / dt; // the bare definition of a derivative! Nothing fancy!
        };
    }

This is where "closing over" gets important. I want the function(t, dt)... to have access to the value of f when it was created. A simpler example, say I wanted to make an array of functions:

    var arr = [];
    for(var i = 0; i < 100; ++i)
        arr.push(function(t){ return i * t; });

What do you expect arr[50](3) to return? If you said "150", you've been paying attention. Closing over the value of "i" allows us to do natural things with our code.

Unfortunately, it's incorrect. JavaScript does unexpected things with scope, so it can break our natural understanding of it. Every one of these 100 functions will return 100 * t, because 100 was the final value of i that caused the for loop to break, and the i variable is still in scope after the for loop finishes. It's one of the ways in which JavaScript is fundamentally broken. In JavaScript, this example has to be fudged to work right:

    var arr = [];
    for(var i = 0; i < 100; ++i)
        arr.push((function(_i){ // an anonymous function...
            return function(t){ return _i * t; }
        })(i)); // ...that we call right away

We are used to the for loop introducing new scope, but in JavaScript it does not. We have to explicitly introduce the scope. It's bad, but thankfully the ability to treat functions as first-class values allows us to fix it!

Moving on, let's apply our derive function:

    var velocity_x = derive(location_x);
    var velocity_y = derive(location_y);
    // evaluate a few values
    var x = location_x(10);  // x == 20
    var dx = velocity_x(10, 0.0000001); // 1.999999987845058 which, for an approximation, is very close to the correct value of 2

"Oh, but 2 times t is easy to derive." You might say. Well, what if our location function described the ball moving in an ellipse?

    location_x = function (t){ return 2 * Math.cos(t); }
    location_y = function (t){ return 3 * Math.sin(t); }

Then the derivative is exactly the same:

    velocity_x = derive(location_x);
    velocity_y = derive(location_y);

And we will get reasonably good approximations for increasingly small values of dt.

Now, try doing that in C. We live in blessed times where most of the popular languages have the basic building blocks of functional programming enough to support the lambda calculus. This didn't used to be the case.

FWIW I think it's an insightful question.

Other replies to this thread do a pretty good job at pointing out the applications of lambda calculus. I want to contribute this excerpt from one of the original papers on the topic:

"In this paper we present a set of postulates for the foundation of formal logic, in which we avoid use of the free, or real, variable... Our reason for avoiding use of the free variable is that we require that every combination of symbols belonging to our system, if it represents a proposition at all, shall represent a particular proposition, unambiguously, and without the addition of verbal explanations."

The motivation was a setting for doing "precise and unambiguous" mathematics. Mathematical results are used pervasively today, so the overall vision is obviously important.

Whereas The Calculus was developed in response to the difficulty of calculating physical quantities, such as those about celestial bodies, the lambda calculus had a more foundational motivation.

None-the-less, lambda calculus is tremendously useful for solving "real world" problems. Most of these problems arise where doing "precise mathematics" is important but tedious, difficult and/or time-consuming; or the related task of defining computations correctly.

Lambda calculus is a rigorous mathematical way to define what "computation" even means. You need something -like- Lambda calculus to even begin reasoning about computation mathematically.

I'm not sure what you mean by "equivalent", but historically, the "computer science problem" that lambda calculus has been used to address is understanding the meaning of expressions in programming languages. The first paper to introduce lambda calculus in relation to computers was Peter Landin's "The mechanical evaluation of expressions" (1964). Its specific goal was to use the lambda calculus to model the facilities of other programming languages in use at the time. Landin continued this investigation with two more papers in the series: "A Correspondence Between ALGOL 60 and Church's Lambda-Notation" (1965) and "The Next 700 Programming Languages" (1966). Because of the LC's basis in mathematics and logic, it provided a useful way to define the semantics of programming languages. It continued in this role over the next few decades. One of many high points in this evolution was the use of the LC as the basis of Scheme, "An Interpreter for Extended Lambda Calculus". Among many other contributions, the "Lambda Papers" investigated other models of computation (e.g., actors).

So the lambda calculus has been used as a consistent and primitive basis for understanding computation itself and how it is expressed in programming languages. I suppose it is more "equivalent" to Newton's 2nd Law than any particular way to solve a problem. It's perhaps worth remembering that Principia used geometry, not what we know of as calculus, to clarify mechanics.

The reason why he did not there was no rigorous proof is probably in parts that the result is not controversial at all.

Viewed that way, that lambda calculus expresses a particular (kind of tiny) feature in a PL, it's pretty boring. What you want to do is take note that lambda calculus, this single, tiny feature in a PL, is powerful enough to simulate every other feature in the PL.

The other nice thing is that if you do base your whole language on LC then you get really excellent variable scoping without further questions. That's something that a lot of languages still struggle with (js).

The Python usage isn't very instructive:

http://python-history.blogspot.com/2009/04/origins-of-python...

That's the Python language designer saying he wasn't a huge fan of the name when it was introduced, because it didn't quite live up to the expectations it set.

The usage of 'lambda' to construct anonymous functions is just a reference to Lambda calculus, the actual thing is a formal system of operating on those functions.

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.

Yes, you miss something important: that this can be written down in one line is a great breakthrough. You also miss that languages like Scheme and Python are the way they are because they copy the lambda-calculus. They are (in parts) implementations of the lambda-calculus. If you look at the history of programming languages this is very clear.

Perhaps you refer to lambdas in Python.

Those are not the same thing as Lambda calculus -- it's just a bad naming decision for a Python language feature (short anonymous function construct).