# Lambda calculus didn't seem abstract. And I can't see the point of it

The underlying question:

What does lambda calculus do for us that we can't do with the basic function properties and notation generally learned in middle school algebra?

First of all, what does abstract mean in the context of lambda calculus? My understanding of the word abstract is something that is divorced from the machinery, the conceptual summary of a concept.

However, lambda functions, by doing away with function names, prevents a certain level of abstraction. For example:

f(x) = x + 2
h(x, y) = x + 5 y


But even without defining the machinery of these functions, we can easily talk about their composition. For example:

1. h(x, y) . f(x) . f(x) . h(x, y) or
2. h . f . f . h


We can include the arguments if we want, or we can abstract away completely to give an overview of what's happening. And we can quickly reduce them to a single function. Let's look at composition 2. I can have student layers of detail I can write with depending on my emphasis:

g = h . f . f . h
g(x, y) = h(x, y) . f(x) . f(x) . h(x, y)
g(x, y) = h . f . f . h = x + 10 y + 4


Let's perform the above with lambda calculus, or at least define the functions. I'm not sure this is right, but I believe the first and second expressions increment by 2.

(λuv.u(u(uv)))(λwyx.y(wyx))x


And to multiply by 5y.

(λz.y(5z))


Rather than be abstract, this seems to get into the very machinery of what it means to add, multiply, etc. Abstraction, in my mind, means higher level rather than lower level.

Furthermore, I am struggling to see why lambda calculus is even a thing. What is the advantage of

(λuv.u(u(uv)))(λwyx.y(wyx))x


over

h(x) = x + 5 y


or a combined notation

Hxy.x+5y


h x y = x + 5 * y


Again, what does lambda calculus do for us that we can't do with the f(x)-style function properties and notation many are familiar with.

• It's funny that you give an example from Haskell, since Haskell is based on the lambda calculus. Lambda calculus is not about any particular notation. It's a computational model, equivalent to Turing machines, in which "everything is a function". – Yuval Filmus Dec 3 '16 at 8:36
• Yes, I’m told it’s based on lambda calculus. The question that I have yet to see answered in a way that makes sense to me is why haskell is based on lambda calculus as opposed to just . . . the basic attributes of functions I learned in grade school. That’s really the gist of this entire question. – JDG Dec 3 '16 at 10:11
• Isn't "no purpose immediately comes to mind" almost the definition of "abstract"? :-) – David Richerby Dec 3 '16 at 14:51
• I wouldn’t say it’s derogatory. That treatment of functions is serviceable through calculus. But I can see how being labeled as middle school could be thus interpreted. I’ll adjust it. – JDG Dec 3 '16 at 16:31
• I doubt you actually have a formal definition of "middle school algebra function notation". If you have any definition for such functions it's probably the set theoretic one which has no computational meaning. Part of the point of the lambda calculus is to understand such notation on it's own terms and, dare I say it, abstracted from particular applications like polynomial functions or calculus. – Derek Elkins left SE Dec 3 '16 at 17:30

There are many reasons why the lambda calculus is so important.

A very important reason is the lambda calculus allows us to have a model of computation in which computable functions are first-class citizens.

One cannot express higher-order functions in the language of middle school algebra.

Take as example the lambda expression

$$\lambda f. \lambda g. \lambda x. f(g(x))$$

This simple expression shows us that, within the lambda calculus, function composition is itself a function. In middle school algebra, this is not easily expressed.

In the lambda calculus, it is very easy to express that a function will return a function as its result.

Here is a small example. The expression (where I here assume an applied lambda calculus with addition and integer constants)

$$(\lambda f. \lambda g. \lambda x. f((g(x)))(\lambda x. x+2)$$

will reduce to

$$\lambda g. \lambda x. g(x)+2$$

Notice also that within the lambda calculus, functions are expressions and not definitions of the form $f(x) = e$. This frees us from the need to name functions and to distinguish between a syntactic category of expressions and a syntactic category of definitions.

Also, when it becomes impossible (or just notationally cumbersome) to express higher-order functions, one will also have problems with assigning types to expressions.

Function composition has the polymorphic type

$$\forall \alpha.\forall \beta. \forall \gamma. (\beta \rightarrow \gamma) \rightarrow ((\alpha \rightarrow \beta) \rightarrow \gamma)$$

in the Hindley-Milner type system.

A very strong selling point for the lambda calculus is precise the notion of typed lambda calculus. The various type systems for functional programming languages such as Haskell and the ML family are based on type systems for lambda calculi, and these type systems provide strong guarantees in the form of mathematical theorems:

If a program $e$ is well-typed and $e$ reduces to the residual $e'$, then $e'$ will also be well-typed.

And if $e$ is well-typed, then $e$ will not exhibit certain errors.

The proofs as programs correspondence is particularly noteworthy. The Curry-Howard isomorphism (see e.g. https://www.rocq.inria.fr/semdoc/Presentations/20150217_PierreMariePedrot.pdf) shows that there is a very precise correspondence between the simply typed lambda calculus and intuitionistic propositional logic: To every type $T$ corresponds a logical formula $\phi_T$. A proof of $\phi_T$ corresponds to a lambda term with type $T$, and a beta-reduction of this term corresponds to performing a cut elimination in the proof.

I urge those who feel that middle school algebra is a good alternative to the lambda calculus to develop an account of higher-order, polymorphically typed middle school algebra together with an appropriate notion of Curry-Howard isomorphism. If you can even work out an interactive proof assistant based on middle school algebra that would allow us to prove the many theorems that have been formalized using lambda calculus-based proof assistants such as Coq and Isabelle, that would be even better. I would then start using middle school algebra, and so, I am sure, would many others with me.

• This is great explanation. It’s helpful to hear that higher-order functions (like composition) and typing are better represented in lambda calculus is encouraging, even moreso that this facilitates proofs and provable code. I don’t see the ramifications of much of what you mentioned and why the traditional notation is inadequate (eg, about not needing a separate definition syntax f(x) = e), however it is helpful that you named some of these reasons and it gives a sense of what areas are improved by lambda calculus. – JDG Dec 3 '16 at 17:03
• One can of course introduce local definitions of the form $\texttt{let}\; x = e' \; \text{in}\; e$ but these can already be expressed in the syntax of the lambda calculus as $(\lambda x.e)e'$. The lambda calculus allows us to express functions without having to name them, just as one can (in middle school algebra!) speak of the number $4$ without having to name them by some variable. – Hans Hüttel Dec 4 '16 at 13:26

When functions are first described to youngsters, they are essentially identified with graphs (plots), or perhaps with formulas; this is the way functions were understood historically before the advent of formalist trends in mathematics. Nowadays functions, as taught in first year calculus, are real functions, that is, functions from $\mathbb{R}$ to $\mathbb{R}$.

The functions in lambda calculus are much more general. The exact definition depends on whether your lambda calculus is typed or untyped. In pure untyped lambda calculus everything is a function. This is much more general than the real functions of calculus.

Even procedural languages sometimes use ideas from lambda calculus. The sorting function in C accepts as a parameter a comparison function, which it uses to compare elements. Lambda calculus goes much further – functions not only accept functions as inputs, but can also output them.

Lambda calculus is a model of computation equivalent in power to Turing machines. It is a system complete unto itself. Pure lambda calculus doesn't have "5" or "+" as primitive terms – they can be defined inside the calculus, just like "5" and "+" are not primitives of set theory. (Practical programming languages implement natural numbers natively for reasons of efficiency.)

I suspect that one of the reasons that you are not impressed with lambda calculus is that its ideas have pervaded the programming discourse so much that it no longer looks innovative.

• "I suspect that one of the reasons that you are not impressed with lambda calculus" Therin lies the question I’m asking: What does lambda calculus do for us? In other words, when we don’t use lambda calculus, what happens. When we do use lambda calculus, what do we gain? If lambda calculus was the first time that people thought, what if functions could themselves create functions, then is that impressive? Among my initial python programs made text containing functions that I later evaluated, much like delegating the task of decision making to anther person. Seems obvious? – JDG Dec 3 '16 at 10:50
• this was before I knew much of anything. I just thought code was annoying to type over and over and that programming should help me auto generate functionality, including functions themselves. – JDG Dec 3 '16 at 10:51
• Python supports functional programming. The first programming languages didn't. If you had programmed in FORTRAN, you would not have created programs with text containing functions that you later evaluated. Without even noticing it, you made use of the capabilities provided by ideas from the lambda calculus. – Yuval Filmus Dec 3 '16 at 11:13
• Eval originated in LISP, which was strongly influenced by the lambda calculus. Something like this isn't possible in FORTRAN, C, COBOL, and many other programming languages. – Yuval Filmus Dec 3 '16 at 12:04
• Yes, python supports functional progamming---but I'm not sure it's eval() ability was inspired by λCalc---you don't λCalc to think: I want to auto-generate code that I can eval later. That's like saying λCalc is required to think, "I'll tell Miranda to use her best judgement on how to run her department"---in other words getting a function to generate its own functions. You don't need λCalc to think about delegating high-level tasks. If you want to talk about drawing inspiration from λCalc, it's more appropriate point to lambda functions, comprehensions, etc. – JDG Dec 3 '16 at 12:06

One of the basic ambiguities of common mathematical notation is that sometimes $x^2$ is used to denote a number (the square of the number $x$), and sometimes $x^2$ is used to denote a function (the function that returns the square of its argument).

Lambda calculus removes this ambiguity; you can write $\lambda x.x^2$ to refer to the function, making it unambiguous that $x^2$ refers to a number, like it should.

Yes, you could break the flow of an argument or calculation to say "now define $f$ by $f(x) = x^2$" and then use $f$, but that gets cumbersome fast. Lambda abstraction lets you do that inline without making an interruption.

The use of lambda expressions in programming languages has a similar advantage; you can write what the function does right there where it's needed rather than having to define a whole new function elsewhere in your program.

You can even see lambda abstraction implicit in mathematics; e.g. students of calculus are only taught about derivatives of functions, so to reconcile Leibniz notation $\frac{d}{dx} x^2$ with derivatives of functions, you can interpret $\frac{d}{dx}$ as implicitly performing a lambda abstraction on $x^2$ to interpret it as a function. You're more or less forced to do so, if you don't want to have the ambiguity described in the opening paragraph.

Also, people are often uncomfortable with function-valued functions in traditional notation; e.g. the usual map $\theta : V \to V^{**}$ that identifies a finite-dimensional vector space with its double dual is defined by

$$\theta(v)(f) = f(v)$$

Many people find this double-evaluation notation confusing and/or unsettling, as well as this recursive use of pointwise definition of a function. The lambda abstraction version

$$\theta = \lambda v . \lambda f . f(v)$$

doesn't have that problem.

Finally, there's a theorem of abstract nonsense that "simply typed lambda calculus" is basically the same thing as "cartesian closed category" — so if you ever find yourself wanting to do calculation in a cartesian closed category, it's probably a good idea to use simply typed lambda calculus to do so.

• I'm coming back to this question and am finding this answer great. Thank you. The answers here in general are really interesting. – JDG Nov 17 '17 at 21:34

I'll say up front I'm not an expert on this topic, but I did just spend a bit of time studying it and one of the most fascinating things to me in any topic is the history behind it. So to me understanding a bit of the history behind lambda calculus helps explain why it is useful.

The short summary is that in the early 1900s after set theory started to take off and math was re-envisioned based on sets, some mathematicians noticed that while a set theory definition allows you to claim that a certain structure exists they do not tell you how to construct it and calculate it. So set-theoretic definitions are nonconstructive. Mathematicians began wondering if there was a way to develop constructive definitions that would go beyond proving that something is and instead prove how it is.

From Wikipedia:

In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existence proof or pure existence theorem) which proves the existence of a particular kind of object without providing an example.

Turing developed the Turing Machine automata to answer the question, and Church developed the lambda calculus also to answer the question. Kleene also developed a method involving the Kleene Star $*$ which were adopted into regular expressions, and there was someone else (can't recall offhand) who developed yet another method. All of these were developed in an attempt to build a system of math on a basis that would allow constructive definitions from the beginning.

It was then shown that lambda calculus and the Turing machine could both represent any computable function and are thus equivalent.

In theory any mathematical function or concept can be encoded in lambda calculus form and computed. This means that lambda calculus can be a completely separate basis for mathematics, though obviously an extremely tedious one.

Lambda calculus isn't "useful" in the sense that you aren't going to write code using it, but it does form the basis for denotational semantics which is used to describe programs and their dynamic effects. This is used in discussions of program correctness and semantic meaning. It also obviously heavily influenced the development of functional programming languages, which draw their entire concept of execution from lambda calculus.

Hope that helps.

Edit to add: I was just pointed to this paper showing the relationship between topology, lambda calculus, and physics. Skimming over it briefly I ran across this fantastic statement:

While a Turing machine can be seen as an idealized, simplified model of computer hardware, the lambda calculus is more like a simple model of software. ... Poetically speaking, the lambda calculus describes a universe where everything is a program and everything is data: programs are data.

The point is that the lambda calculus is an idealized model of software computation, and as such isn't tied to a particular implementation in any programming language. It models pure computation.

• More on history: Brief history of λ-calculus at the Stanford Encyclopedia of Philosophy. They have more entries than one can process in a lifetime. – David Tonhofer Jan 20 '17 at 11:16

As Yuval pointed out in the comments Haskell is based on the $\lambda$-calculus. Another reason why lambda calculus is so important is the Church-Rosser Theorem, which justifies the existence of lazy evaluation. (Which is one of Haskell's many cool features)

Lambda calculus wasn't designed to be a programming language. Indeed, it was created in the 1930s, decades before we even had programmable computers. Rather, it was created as a formal model for studying computation, itself. If you're disappointed in how easily it expresses code, or mathematical functions, that's because that's not what it's for.

• "decades before we even had programmable computers" -- wrong. Programmable computer existed before (if maybe not universal ones) and the first universal computers were built during the 1930s. – Raphael Dec 4 '16 at 12:30

Lambda calculus exists so that anonymous (aka lambda) functions can be created. If you don't do away with function names, then the namespace can get cluttered and one can run out of available function names. This is especially important when dealing with so-called "higher order functions" that return functions (or function pointers) for obvious reasons.

Essentially, lambda functions are equivalent to locally scoped variables. Functional programming without lambda functions is analogous to procedural programming without any local variables, ie, a terrible idea.

"why lambda calculus is even a thing" mathematicians love redundancy. lambda calculus is rarely used in math because as you've discovered the notation isn't very useful.

"If you can even work out an interactive proof assistant based on middle school algebra that would allow us to prove the many theorems that have been formalized using lambda calculus-based proof assistants such as Coq and Isabelle, that would be even better. I would then start using middle school algebra, and so, I am sure, would many others with me." Have you heard of metamath? No lambda calculus involved there, can prove many of the coq/isabelle theorems

• Aside from some opinions, what does this answer offer? – Raphael Dec 4 '16 at 12:31
• @Raphael Misinformation. Most of this answer doesn't even make sense. There is no shortage of names. "Lambda functions" are not equivalent to locally scoped variables; this doesn't even make sense. I assume this is meant to refer to let, but while let can be encoded with anonymous functions, you clearly can't go the other way. Functional programming does not require "lambda functions", e.g. Backus' FP or Sisal. – Derek Elkins left SE Dec 4 '16 at 23:09
• mostly i wanted to post a comment to hans's answer but didn't have enough karma. so i decided to turn the comment into a full-fledged answer – s n Dec 5 '16 at 5:05