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

Question

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

or even Haskell's notation

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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.

Answer 5

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)

Answer 6

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.

Answer 7

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