Lambda calculus outside functional programming?

Question

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?

Answer 1

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.

Answer 2

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

Answer 3

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.

Answer 4

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.

Answer 5

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

http://www.sfu.ca/~jeffpell/Ling406/LambdaAbstractionOH.pdf, https://files.nyu.edu/cb125/public/Lambda/