# Lambda calculus outside functional programming?

I'm a university student, and we're currently studying Lambda Calculus. However, I still have a hard time understanding exactly why this is useful for me. I realize if you do loads of functional programming it might be useful, however I reckon that it's not really needed for learning functional programming, what do you think?

Secondly, is there any use for Lambda Calculus within the realm of Computer Science but outside of functional programming languages?

The lambda calculus is fundamental in logic, category theory, type theory, formal verification, ... Basically, anything to do with programming language semantics and formal logic. It is such a fundamental formalism that people working in these fields do not even question the benefit of it.

I think that it is extremely useful for understanding functional programming because it gives you the essence of functional programming. Functions, application, substitution. Based on this you can build your skills in reasoning about functional programs and transformations of them. Higher-order functions are a breeze.

Sure you could learn functional programming without the lambda calculus, but you would never truly understand functional programming without it.

• Thank you very much for your response Dave. I think formal verification is the best reason yet, as to why lambda calculus is useful for me to learn, and funnily enough, I'll do a course on formal verification next semester. Would you also use lambda calculus to do a formal verification of a piece of software written in any language, e.g an imperative or object orientated one? – Jacob Nov 21 '12 at 9:16
• You may not use the lambda calculus directly when doing formal verification, but it will appear in the foundations of formal verification. Writing specifications often involves writing in a functional language, even for imperative/OO code. – Dave Clarke Nov 21 '12 at 9:48
• Okay that's interesting thanks a bunch, now I have a bit more reason to study this. Do you know if lambda calculus is used to design any non-functional languages (at lower levels)? – Jacob Nov 21 '12 at 10:40
• ALGOL. Scala. Ultimately, your question is difficult to answer. The lambda-calculus has become a part of the common knowledge for (most) language designers and it therefore influences language design, even if it is not explicitly used. Consider blocks in Smalltalk or Ruby, anonymous classes in Java. These are closures, which are closely linked with higher-order functions in the lambda calculus. – Dave Clarke Nov 21 '12 at 10:43
• Okay, thanks a lot Dave, that's highly appreciated. – Jacob Nov 21 '12 at 10:44

You are asking for an application outside of computer science and logic. That is easily found, for example in algebraic topology it is convenient to have a cartesian closed category of spaces, see convenient category of topological spaces on nLab. The formal language corresponding to cartesian closed categories is precisely the $\lambda$-calculus. Let me illustrate with a very simple example how this comes in handy.

First, as a warmup exercise, suppose someone asks you whether the function $f : \mathbb{R} \to \mathbb{R}$ defined by $f(x) = x^2 e^x + \log (1 + x^2)$ is differentiable. You do not actually have to prove that it is, you just observe that it is a composition of differentiable functions, therefore differentiable. In other words, you made an easy conclusion based on the form of definition.

Now for the real example. Suppose someone asks you whether the function $f : \mathbb{R} \to \mathbb{R}$ defined by $$f(x) = \left(\lambda f : \mathcal{C}(\mathbb{R}) . \int_{-x}^{x} f(1 + t^2) dt\right)(\lambda y : \mathbb{R} . \max(x, \sin(y + 3))$$ is continuous. Again, we can immediately answer "yes" because the function is defined using the $\lambda$-calculus and starting from continuous maps $\max$, $\int$, $\sin$, etc.

Various extensions of the $\lambda$-calculus make it possible to do the same sort of thing in other areas. For example, because a smooth topos is a cartesian closed category, any map which is defined using the $\lambda$-calculus, starting from derivatives and the ring structure of the reals (and you can throw in the exponential function if you wish) is automatically smooth. (Actually, the main thrust of the smooth topos is the existence of nilpotent infinitesimals which allow you to meaningfully say things like "we disect a disc into infinitely thin isosceles triangles".)

• Thank you for you elaborate response. Actually I was trying to find a use for lambda calculus within computer science but outside of functional programming, apologies if this was not clear. I've changed the question to more clearly state this. – Jacob Nov 21 '12 at 9:14
• Ah, too bad, I would have written an elaborate response about that. – Andrej Bauer Nov 21 '12 at 13:04
• I think Dave's question is fine, I have nothing to add. If you want to see what exciting things you can do with the $\lambda$-calculus, perhaps you can have a look at the impossible functionals. But as a general answer, Dave's is very good. – Andrej Bauer Nov 22 '12 at 16:52

One way of looking at $\lambda$-calculus is as a simple and terse model of parametersing programs. You parameterise code in almost any programming language that has functions, procedures or methods, and in any language that has modules or that enables you to parameterise types. Parameterisation is a form of reuse. Because $\lambda$-calculus is so simple, the commonalities between many programming languages that enable you to parameterise code, come to the fore especially clearly.

It's certainly possible to be a very good programmer without knowing about $\lambda$-calculus, but you are missing out on something beautiful that is also highly useful.

Microsoft LINQ (Language INtegrated Query) grafts functional programming capabilities into procedural languages. It makes extensive and quite direct use of $\lambda$-calculus to untangle dependencies and segregate portions of the expression tree that can be delegated to the database server. This is an extremely practical application with high commercial value.

I have written a small commercial application using a functional language and I can assure you that while well worthwhile to academics and researchers they are less useful commercially than their procedural cousins. Really it's a question of horses for courses, and most practical of all is a language that can be procedural or functional as required. As a consequence, functional capabilities that were introduced (to C#) in support of LINQ, such as $\lambda$-expressions, get quite a lot of use outside of the context of database queries.

So when you finally find yourself compelled to do icky things because you'd like to be paid, you may find $\lambda$-calculus more useful than you expected even though you almost certainly won't be using a functional language.

Without knowing more about it, I hear that linguists are using lambda calculus.

• Can you summarize what's behind the links? They have a tendency to break. It will also make your answer more self-contained. – Juho Nov 20 '12 at 22:22