What Is Lambda Calculus?

July 4, 2017

Forget the name calculus and maybe even lambda. A lambda calculus is the smallest Turing complete language using only one operation: evaluationAlso known as -reduction. , and one object: functions.

The way the lambda and the calculus comes up is the following: we typically name the functions starting with a (lambda) symbol, and we say it’s ‘‘calculus’’ in the sense of a particular method or system of calculation or reasoningSource: Google. .

So how do we write functions, and what is this way of reasoning?

Writing and evaluating functions

The function writing is fairly simple. We write the identity function as .

For example, if we have the function foo (which is secretly some function of course), then

For functions, it is well known is the same as because we only care about the transformation on the input, not what the input looks like. Analogously, is the same as . This property is known as -equivalence.

We can curry functions (nest one function after the other) using for example which is some way of saying (unfortunately, there is no easy way to reduce this further). We write as for shorthand.

Since functions are the only objects in lambda calculus, we evaluate the function on another function to see what it does.

Let foo and bar be -functions. Then

Implicit in this calculation is the assumption that function evaluation is done using left associativity. So far our calculations haven’t demanded us to pay particular attention to this, but as we will see in the next example, it’s pretty important to remember this one rule.

A more elaborate example

Let’s consider the expression to reduce.

Remarks

Not every expression converges to a normal form (or irreducible form). For example, the expression ( regenerates itself under susbsitution of the first . We say that this expression diverges. Expressions that diverges are expression which do not halt upon evaluation.

But yeah! Lambda calculus is essentially applying this one evaluation rule left-associatively on functions until we can’t further reduce (unless the expression diverges, in which case we don’t terminate).

In the next post, we will see how we can generate a Turing complete language using functions, evaluation, and left-associativity!

Source

Haskell Programming from First Principles super friendly bookIf I had a choice, I would only read those. by Christopher Allen and Julie Moronuki.

This post was written from the perspective of a mathy beginner.

Special thanks to Iain McCoy and Rudi Chen for the feedback.

What Is Lambda Calculus? - July 4, 2017 - Hang Lu Su