Functional programming languages are based on the lambda-calculus. As explained in the previous article, the lambda-calculus grew out of an attempt by Alonzo Church to formalize the notion of computability. As with mathematical expressions, the principle is that the value of an expression depends only on the values of its subexpressions. The lambda-calculus is a simple language with expressive semantics as it can express any computable function.
First rules of lambda calculus
Let’s start with an example and let’s consider the following function: $$ f: x \rightarrow x^2 + 5x - 2. $$
In the lambda-calculus, the notation $λx.M$ is used to denote a function with parameter $x$ and expression $M$. That is, $x$ is mapped to $M$. We rewrite our function in this format $$ \lambda x.(x^2+ 5x - 2) $$ Besides, the lambda-calculus uses prefix form and so we rewrite the body in prefix form,
$$ \lambda x. (- (+ (* x x) (* 3 x)) 5) $$
As we mentionned in the last post, lambda-calculus curries its functions of more than one variable i.e. $(+ x y)$ is written as $((+ x) y)$, the function $(+ x)$ is the function which adds something to x. Rewriting our example in this form we get: $$ \lambda x.((- ((+ ((* x) x)) ((* 3) x))) 5) $$
To denote the application of a function $f$ to an argument $a$ we write $fa$.
Grammar of Lambda Calculus
The lambda calculus consists of a language of lambda terms, that are defined by a certain formal syntax, and a set of transformation rules for manipulating the lambda terms. As described in the previous example, we don’t have to name the expressions and all functions in the lambda calculus are anonymous functions. In python, we can use lambda expressions for anonymous functions as follow:
(lambda x: x**2)
Any lambda calculus expressions is called a lambda term, and any lambda term follows three rules:
- a variable x is a valid term
- if $t$ is a lambda term, and if $x$ is a variable, then $(\lambda x.t)$ is a lambda term (called an abstraction). It represents the definition of an anonymous function as described in the previous example. The right term is called the body of the function.
- if $t$ and $u$ are lambda terms, then $(t u)$ is also a lambda term (called an application). It represents the application of a function $t$ to an input $u$.
As described in the previous article, functions may be used as the inputs, or be returned as outputs from other functions.
Bound and free variables
In $\lambda x . ∗ 3 x$, x is a bound variable, which is the formal parameter of the function. But the body can include any valid lambda expression, including another unnamed function, with an unbound variable:
$$\lambda y . ∗ (+ x y) 4$$ In this case, $x$ is a free variable, and the expression is valid. We can bound the total expression with: $$ \lambda x . \lambda y . ∗ (+ x y) 4$$
The funny thing here is that the first abstraction is returning another function, which is returning the sum of $x$ and $y$ multiplied by 4
Currying
The previous example is a good example of currying, mentionned in the previous article. If you look closer to the expression $ \lambda x . \lambda y . ∗ (+ x y) 4$, you will see that this is equivalent to a function with two arguments. So, any multiple arguments functions can be built with this trick called “currying”.
Calling Lambda Functions
To apply a Lambda function, we place it in parentheses before its argument when we need to avoid ambiguities. Thus, calling $\lambda x . ∗ 3 x$ with $a$ is written: $$ (\lambda x . ∗ 3 x) a$$
Reduction
There are three kinds of reduction:
- $\alpha$-conversion: changing bound variables;
- $\beta$-reduction: applying functions to their arguments;
- $\eta$-reduction: which captures a notion of extensionality.
Alpha conversion
$\alpha$-conversion allows bound variable names to be changed. For example, $(\lambda x . ∗ 3 x)$ is said to be $\alpha$-equivalent to $(\lambda y . ∗ 3 y)$.
Beta-reduction
Computation in the lambda calculus takes the form of beta reduction: the $\beta$-reduction of $(\lambda x.M) s$ is $M[x := s]$. In the point of view of functional programming, $\beta$-reduction corresponds to the computational steps, which can be repeated until there is nothing to reduce. In untyped $\lambda$ calculus, this computation may not terminate.
Eta-reduction
$\eta$-reduction converts between $\lambda$x.f x and f whenever x does not appear free in f.
The Church-Rosser Theorems
In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions. It means that, any way you choose to evaluate a lambda expression can produce the same result, i.e., it is confluent. Besides, if the program terminates, the result is deterministic and produce its normal form, which means that the expression cannot be reduced further. This result gives fundations to functional programming computations. Note that in $\lambda$-calculus, the final form is not necessarely a value, but could be any irreducible expression.
Arithmetic in lambda calculus
In pure lambda calculus, nothing is defined except the rules described at the beginning of this article, so natural numbers are not predefined, nor the sum operation. Let’s try to define this function from scratch. There are many way to define the Natural Numbers, but the most common is known as Church numerals. The Church numerals are defined as:
$$0 := \lambda f.\lambda x.x $$ $$1 := \lambda f.\lambda x.f x $$ $$2 := \lambda f.\lambda x.f (f x) $$ $$3 := \lambda f.\lambda x.f (f (f x)) $$ etc…
Here, natural numbers are defined as functions that take a function as input, and apply this function $n$ times to define the $n^{th}$ natural number. So, for instance, 0 is defined as a function which for any function $f$ is returning the identity function, and 1 is defined as a function which for any function $f$ is returning a function applying $f$ one time etc…
Let’s now try to define the sum function: $$SUM: (\lambda m.\lambda n. \lambda f. \lambda x.m f (n f x)$$
Observe $SUM$ applies the input function $n+m$ times. Hence, the function is returning $n+m$
This example is to show you that we can actually redefined any arythmetic computations only with the three rules defined by lambda calculus.
Typed lambda calculus
Another aspect of the untyped lambda calculus is that it does not distinguish between different kinds of data. For instance, it may be desirable to write a function that only operates on numbers. However, in the untyped lambda calculus, there is no way to prevent a function from being applied to truth values, strings, or other non-number objects. For example, we could write $7 + (λx. x)$, which is syntactically well-formed but cannot step and is not a value. This is what we could call a type error.
A type system is a tractable syntactic method for proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute. (B. Pierce, Types and Programming Languages)
Thus, those are the properties we are looking for:
- type safe (well-typed programs “do not go wrong”)
- not too conservative (most useful programs should be typeable)
The simply typed lambda calculus is a typed interpretation of the lambda calculus with only one type constructor.
Adding types to the semantic
In simply typed lambda theory, a term is:
- a variable $x$
- an application $(u t)$ where u and t are lambda terms
- an abstraction $\lambda x:T .t$ where the bounded variable $x$ is of type T.
- a boolean constant True or False
- a conditional expression (if t then u else v)
This is similar, but now, abstraction are typed, and we added a base type (Boolean), by adding two constant values. Types in general are defined as:
$$T ::= (T \rightarrow T | Bool)$$
It means that a type is either the base type (also called the atomic type), or it is a function type (example: $T_1 \rightarrow T_2$). $\rightarrow$ is a type constructor, because it creates a new type based on two other types. $t : T$ means $t$ is of type $T$.
From lambda calculus to functional programming
We can try to extend simply typed lambda calculus to add recursive functions and some new primitive types.
Recursion
When we evaluate typed lambda calculus terms by simplification, all evaluations terminate in finite amount of time. That is because there is no mechanism for iteration. To allow recursive programs, we add a (generic) operation:
$$ Fix_T : (T \rightarrow T) \rightarrow T $$
so that $Fix_T F$ represents the infinite expansion $F(F(F(. . .)))$ Such an infinite expansion is a “fixed point” of F:
$$Fix_T F = F(Fix_T F)$$
$Fix_T$ is a new lambda-term and extends simply typed lambda calculus with recursive functions.
Unit
Simply typed lambda calculus can be extended further by introducing another primitive type called Unit. There is as single constant value of type Unit called unit. We define those as following:
- $t ::= . . . | unit$ (terms)
- $v ::= . . . | unit$ (values)
- $T ::= . . . | Unit$ (types)
Conclusion
I hope you enjoyed this brief introduction to the lambda calculus, and that it gave you a clearer idea of its nature. The lambda calculus is the foundation of functional programming, and understanding its philosophy makes it easier to write code in this paradigm. Simple and powerful, the lambda calculus and its extensions are fascinating to study! For more information on the lambda calculus, I recommend the following book. In my next post, we’ll take it a step further by discussing category theory and how it relates to functional programming with examples in haskell.