Lambda calculus

Often called the c. elegans of programming languages: an extremely well-studied “model organism” in biology. Important for its minimal, but still extensive properties.

Created by Alonzo Church in the 1930s. A minimal programming language. It only has variables, functions, and function application. Even while untyped, it is still Turing complete. In OCaml syntax:

type exp =
 | Var of var          (* variables *)
 | Fun of var * exp    (* functions: fun x -> exp *)
 | App of exp * exp    (* function application *)

Free and bound variables, scoping

In the expression $\text{fun }y\to x+y$, the variable $x$ is considered free while $y$ is closed.

• Free variables are defined in an outer scope. We don’t know what $x$ will be yet.
• Bound variables are defined in the function. Here, $\text{fun }y$ binds $y$, and it is considered in scope in the body $x+y$.

Terms that have only have bound variables are considered closed, and terms that have free variables are called open.

Expressions that are just a variable like $x$ are considered singletons. Not free nor closed.

Alpha equivalence

$\text{fun }x\to y+x$ and $\text{fun }z\to y+z$ are equivalent and only differ in variable naming. Here, both functions use the name consistently and therefore have the same meaning.

They are considered alpha equivalent because if we consistently replaced every instance of $x$ with $z$ in the first function, they would be the exact same.

Students who cheat by renaming variables are exploiting alpha equivalence…

However, the naming of free variables does matter. Above, naming $y$ is intentional. The intuition is that an outside scope may define a variable named $y$, so naming it something else changes the way the function works.

Values and substitution

The only values in lambda calculus are closed functions.

We can substitute a closed value $v$ for some variable $x$ in an expression $e$. This is how function application works: replace all free occurrences of $x$ in $e$ with $v$. Mathematical notation for this is $e\{v/x\}$. Some properties:

• $x\{v/x\}=v$. We’re replacing $x$ with $v$.
• $y\{v/x\}=y$, assuming that $y\ne x$. Nothing changes because the expression doesn’t have $x$ in the first place.
• $(\text{fun }x\to \exp )\{v/x\}=(\text{fun }x\to \exp )$. $v$ does not replace $x$ because it’s already bound in the function definition.
• $(\text{fun }y\to \exp )\{v/x\}=(\text{fun }y\to \exp \{v/x\})$. We pass the substitution into the expression given by the function definition. This assumes that $y\ne x$.
• $(e_1{e}_2)\{v/x\}=(e_1\{v/x\}{e}_2\{v/x\})$. We pass the substitution on to the two expressions.

Capture-avoiding substitution

Consider $e_1\{e_2/x\}$. $e_2$ might mention a variable that is already bound in $e_1$. This behavior is usually not intentional (some languages implement this as a feature, e.g. Emacs Lisp), so we can rename conflicting variables by picking an alpha equivalent version. We respect scope:

$$(\text{fun }x\to x+y)\{\text{fun }z\to x/y\}=(\text{fun }{x}^{\prime }\to x^{\prime }+y)\{\text{fun }z\to x/y\}$$

Here, we consistently rename all $x$‘s to $x^{\prime }$ so that when we replace $y$ with $\text{fun }z\to x$, the $x$ in this function cannot possibly conflict with $x^{\prime }$.

Implementing first-class functions

Applying lambda calculus, many programming languages (e.g. OCaml, Haskell, Scheme, Python, C#, Java, Swift) allow functions to be passed as arguments, returned as values, and nested within each other. There are many ways to implement this in a compiler.

Environment-based interpreter, closures

When evaluating, we also interact with an environment, which simply maps variables to their values. Extend and remove bindings from the environment as we execute function calls.

A closure is a pair of an environment and a code pointer.

• The environment can be implemented as a map of variables to values.
• A code pointer is the first-class function, modified to take an additional argument for the environment. If we have a function A -> B, in OCaml syntax we can have a function pointer type of (Env * A -> B)

To apply a closure, we simply invoke the environment associated with it and then call the function with the environment and its other, “real” arguments.

Since the first-class function now has all the context it needs to operate (contained within the environment data structure), we’re able to hoist it out and lift it to the top level.