# 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?

-

## migrated from cstheory.stackexchange.comNov 20 '12 at 20:02

This question came from our site for theoretical computer scientists and researchers in related fields.

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? –  AzaraT 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)? –  AzaraT 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. –  AzaraT 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. –  AzaraT 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.