Enter the vast world of programming languages by following the tutorials provided here to learn about functional programming in Haskell.
Now that we have a nice grasp on Haskell and functional programming, we will begin to switch gears to the more theory side of things. To this end, we will be studying lambda calculus.
Formally speaking, lambda calculus is a formal mathematical system for expressing computation. It is Turing complete, and it is based around the idea of binded variables and substitution.
Specifically, a lambda expression can be defined as follows:
| E := x | λx. E1 | E1 E2 |
What this means is that a lambda expression can either be a:
For example, ((((λx.(λy. x y)) p) q)) is an expression that is an application between a variables p and q and an abstraction (λx.(λy. x y)). We can drop the parentheses if there is no ambiguity in the expression. Thus, we can write the previous lambda expression as (λx.λy. x y) p q without any abiguity.
When working with lambda expressions, there are two computation rules that we follow:
In our previous example, we had the lambda expression (λx.(λy. x y)). In this abstraction, we say that x and y are bounded variables. Thus, we can change the names for boundeed variables without modifying the logic of the expression. Formally, we say
λx. E[x] → λy. E[y]
That is, we are replacing every apperence of x in E with y. We say that λx. E[x] and λy. E[y] are alpha-equivalent since there underlying logic remains the same. Using our previous example,
(λx.(λy. x y)) → (λw.(λv. w v))
We use alpha-conversion to avoid name conflicts. (i.e. when bounded variables and free variables share a name). For example,
(λx. x) x
In this example, x is both used for the bounded term in the abstraction and the free term in the argument. To fix this, we use alpha-conversion to produce the following
(λx. x) x → (λy. y) x
This fixes our previous name conflict. If we use De Bruijn indices, then alpha-conversion is no longer needed. We will talk about De Bruijn indices in a future blog post.
Another computation rule that we follow is called beta-reduction. The rule states that we will replace every occurence of a bound variable in an abstraction with its respective argument. Formally we say,
(λx. E1) E2 → E1[x := E2]
From our previous example,
(λx.λy. x y) p q → (λy. p y) q → p q
Before we continue, it is important to recognize some things about lambda calculus. Now we said that lambda calculus is Turing complete, but it isn’t terminating. For example, let’s take a look at the lambda expression
(λx. x x) (λx. x x)
Now if we use our beta-reduction rule from before we get
(λx. x x) (λx. x x) → (λx. x x) (λx. x x)
As we can see, this expression doesn’t terminate.
This discussion of non-termination brings us to our next discussion: call-by-name and call-by-value. Now you might be familar with these terms already from previous programming experience. CBN is a method of expression evaluation that waits until a expression is needed before it is evaluated; on the other hand, CBV immediately evaluates an expression, whether or not it will be used. This might not seem like a big difference, but deciding on which method to use can have major consequences on the topic of termination. For example, consider the following lambda expression:
(λx.λy. x) z ((λx. x x) (λx. x x))
If we use CBN, then this expression reduces to:
(λx.λy. x) z ((λx. x x) (λx. x x)) → z
However, if we evaluate it using CBV, then the program will not terminate, as it will continously be evaluating the argument, ((λx. x x) (λx. x x)), which doesn’t terminate as we showed before.
Now that we hopefully have a solid understanding of the language and rules of lambda calculus, how can we actually apply this knowledge. Well, one interesting thing (out of many things) we can do in lambda calculus is implement conditionals.