[tikhonj]

The λ-calculus is basically the MVP of programming languages. It allows somebody designing a language feature or part of a type system to experiment with that feature in isolation. Fast iteration for programming language designers.

It's also great as the core of a programming language. If you can express a feature just in terms of the λ-calculus, you can implement it almost for free. It's just desugaring. Most of Haskell is like this: while the surface language has become rather complex, the majority of the features boil away rather transparently into typed lambda terms. Haskell uses a variant of System F which it actually calls "Core" to underscore how core this concept is :).

Of course, as the accepted answer points out, the λ-calculus is also very useful for logic. In some sense, it is a sort of "proof essence": the basic building block of what a proof is. I really like this notion because it gives me a concrete, first-class object to represent a proof. Seeing proofs as programs really helped me come to terms (heh) with mathematical logic.

One surprising use for the λ-calculus outside of CS is in linguistics. In particular, linguists use typed λ-calculi to construct formal semantics for sentences. It's a way to build up the meaning of, well, meaning. Or at least the things we say ;). I'm not super familiar with semantics in linguistics, but I've always thought it was very cool that they also use some of the same tools as programming language theory! Wikipedia has more about this: http://en.wikipedia.org/wiki/Formal_semantics_%28linguistics...

[mafribe]

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.

[DanWaterworth]

(1) I don't think that's fair to say. The lambda calculus is a way of expressing computations with little regard for how they are actually executed.

(2) True, it works better if you add continuations.

[chrismonsanto]

re 1) one of the primary limitations of the lambda calculus wrt concurrency is that it does not model time--there is no way to determine how long a computation takes. An example of a function the lambda calculus cannot define is f(x, y) where the fastest computation of x and y wins. You'll see that function pop up in a number of places in the Haskell world, where it is called "amb". This function is obviously important from a pragmatic POV but it turns out it is also important when doing formal work as well: see the parallel-or/full abstraction problem for PCF[0].

My personal favorite concurrency formalism is the Chemical Abstract Machine[1]. The y-calculus is a neat extension that preserves the spirit of the lambda calculus, but also permits (purely non-deterministic) concurrency.

[0]: http://en.wikipedia.org/wiki/Fully_abstract#Abstraction

[1]: http://www.lix.polytechnique.fr/~fvalenci/papers/cham.pdf

[mafribe]

Most process calculi (including the CHAM) don't model time. I think it's perfectly possible to consider computation without timing.

Adding timing is straightforward for any model of computation with operational semantics. This addition generally changes the semantics dramatically (eg. equalities that hold). There are many timed versions of process calculus, e.g. timed CCS, timed CSP, timed pi-calculus.

[mafribe]

As to (1) I disagree, it's difficult to express general concurrent/parallel computation in lambda-calculus. You need to resort to encodings. That's why process calculi were invented.

Regarding (2), I'm afraid I also disagree. While continuations can express classical logic in some way, it's generally only possible to express certain cut elimination strategies (e.g. call-by-value, as in the Stewart-Ong lambda-mu-calculus). I don't think we know how to do all of classical logic yet. Moreover, adding jumps (which is what continuations are) to lambda-calculus results in an extremely complicated and hard to understand system (e.g. the reduction semantics of the lambda-mu-calculus is usually only handwaved). If you write the very same semantics in pi-calculus, it's trivial and extremely transparent (see "Control in the Pi-Calculus" by Honda et al). Finally, I think it's conceptually deeply confused to 'add' continuations to lambda-calculus. A much cleaner picture emerges when one understands that the call-return jumping discipline engendered by the function-calls of lambda-calculus is a special case of the general jumping that continuations can do. So really one should start with a continuation calculus, and can then see lambda-calculus as a strict sub-calculus of especially disciplined jumps (call-return with affine usage of the return jump).

[DanWaterworth]

w.r.t (1), it's interesting that you and the other replier thought that I meant LC was good for expressing concurrent processes. What I actually meant was that it was also bad at expressing sequential processes, because it doesn't have a single agreed upon operational semantics and it's too high level.

[JumpCrisscross]

> 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...

[ryanklee]

> implement it almost for free

What does this phrase mean?

[nmrm]

I suspect what the parent author meant is that the lambda calculus is a very simple language. If a new language feature can be defined as a small extension to the lambda calculus, then creating a toy implementation is should be easy because the new language is so small.

More importantly, since your new language is small, you can eyeball the implementation and be fairly confident that the implementation "matches" your formal definition (about which you might prove theorems such as type safety).

Contrast this with defining a new feature as an extension of C++, Haskell or Java. You'll invest a lot of time, and in the end might not even be very confident that your implementation matches your theory. So you might write a few hundred line program in your new programming language, get a wonky result, and not be sure if the formal definition is flawed or if the implementation is buggy.

The "implement almost for free" phrase takes on a different meaning if you decide to implement computer-checkable proofs about your language.

[ryanklee]

Excellent! Thank you for your explanation.

My initial suspicion was that the phrase somehow related to logarithmic efficiency -- which made no sense at all to me!