Variables and Abstraction
Learning Objectives
- You understand the untyped lambda calculus syntax and semantics.
- You know the difference between free and bound variables.
- You understand substitution and its pitfalls.
- You can implement the
Termtype,free_vars, andsubstitutefunctions in Rust.
From Calculator to Calculus
In the previous part, we built a calculator that could evaluate and type check terms like + 1 2 and if 1 < 2 then 1 else 2.
This is great, but we want to build programming languages, not calculators!
We begin from scratch by learning about the untyped lambda calculus — no arithmetic, no conditionals, no type checking.
Untyped Lambda Calculus
In brief, untyped lambda calculus is a formal system for expressing symbolic computation based on function abstractions and applications.
The untyped lambda calculus, at its core, contains the following three kinds of terms:
- Variables are for giving names to things.
- Abstractions are the star of the show — they let us define unnamed functions, also called lambda abstractions.
- Applications are terms which apply a term to another term.
These are expressed by the following enum in Rust:
/// A term of the untyped lambda calculus
pub enum Term {
Var(String),
Abs { var: String, body: Box<Term> },
App(Box<Term>, Box<Term>),
}We start using the word “term” instead of “AST” as the latter is a representation of code whereas the former is something we manipulate during evaluation. This distinction will become more clear in the following chapters.
To make talking about the language easier, we define the following mathematical notation for the Terms.
Let’s look at some examples next.
Evaluation in Lambda Calculus
In part 1: Calculation and Proof we saw the following definition of function application in functional programming
This is also how we define evaluation in lambda calculus. For example, applying (the identity function) to reduces to :
We will formally define substitution in this (and the following) chapter and then study evaluation and -reduction.
Free, Bound and Binding Variables
Before we define what exactly free and bound variables are in lambda calculus, let’s look at an example in Rust.
fn foo(y: i32) {
x + y
}
fn main() {
let x = 5;
let y = foo(x);
println!("{y}");
}The concept of free and bound variables is closely tied to the concept of scope.
Scope tracks which name are “usable” in different parts of the code.
For example, variables x and y are usable in main after they have been declared, but x is not usable in foo.
Also, as function names are tracked by scope, we say that foo and main are usable everywhere in the code, although they are not variables.
Looking at just the foo function, we say that the variable y is bound but x is free.
We identify occurrences of variables using the following three categories:
- Binding: a variable is binding, if it occurs in the parameter list of a function (like y in
(y: i32)) or in an assignment pattern (like x inlet x = 5). - Bound: a bound variable is one that is correctly scoped. We also consider binding variables as bound.
- Free: a free variable is one that is not correctly scoped like an undefined variable.
Let’s look at how this concept translates to lambda calculus to give a more precise definition of free and bound variables.
In the following term
we use a blue underline to denote the “scope” of the variable — the abstraction binds within its scope. As the in the body is within the scope of the abstraction binding , it is bound by the abstraction.
Next, let’s look at an example with two abstractions.
Notice that occurs in the body of the first abstraction, which is outside the scope of the bound in the second. Likewise in the second abstraction is outside the scope of the first.
Therefore we say that and occur as free variables in the term.
In the following term with nested abstractions, we observe that all occurrences of and are bound, so there are no free variables.
Note: we also count the variable immediately after the as an occurrence even though it’s not a
Var-term.
Next, let’s define exactly what bound variables are.
Here are more examples of lambda terms and their sets of free and bound variables.
| Term | Free variables | Bound variables |
|---|---|---|
Notice that in for instance, occurs as a free variable once and as a bound variable twice.
Other Variable-Binding Operators from Math
In the following examples, every variable is bound by some operator/construction.
The first equation shows how a new function is defined as it takes an argument and returns the term . The sum () binds the variable and evaluates the term ten times. The limit binds a variable and uses the defined earlier. The quantifies, i.e. binds, the variable to express a logical proposition which may or may not be true1.
In the following examples, the variables and are bound just like earlier, but the variables occur free.
Computing Free Variables
Next, we give an inductive definition (i.e. a recursive algorithm) for computing the set of free variables in a term. Afterwards your get to translate the algorithm to Rust.
Before diving in to the exercises, let’s implement a simple formatter/pretty-printer for lambda terms.
We would like to use the following ASCII-style notation to express terms of lambda calculus:
- Variables:
x,y - Applications:
x y,f (x y) - Abstractions:
x => x,x => y => x,(x => x) y
Let’s implement the Display trait by recursively walking over the term.
This should make it easier to debug what the lambda terms actually look like.
If you are interested in how to make a macro for creating terms with less hassle, expand the following info box.
Parser Macro for Terms
The following declarative macro makes it possible to also conveniently write terms using the syntax we just described.
For example, we can now write t!(x => y) to create the lambda term .
Closed Terms
A closed term is simply one with no free variables.
As we already have an algorithmic definition of , we can define is_closed : Term -> bool trivially in Rust.
However, there’s another way to check if a term is closed which involves a recurring concept called context.
For now, it suffices to think of contexts as sets of variable names.
Before we can define is_closed inductively, we define a helper function which keeps track of a context.
The idea is, when recursively traversing a term and encountering an abstraction, to push the name of the bound variable to the context and pass the new context down recursively.
We will use this idea in the next definition of a term closed under a context .
We can now define that is closed if and only if is closed under the empty context .
Closure of a Term
A context can be converted to a prefix of abstractions. For example, if , and is a term, then the following is the term formed by abstracting over using the variables in :
This idea can be turned into a function: .
Now, as function acting on a term is defined inductively over contexts that are finite in size:
Usually contexts are used to keep track of bound variables, however nothing says we can’t define a context with free variables instead. If we take we calle the closure of . The closure is clearly closed, as all free variables in are now bound in .
Substitution
Next, we define the notion of substituting a variable by a term inside a term.
Substitution only substitutes free occurrences. We denote substitution with , where is a variable name and are terms where is the term where want to perform the substitution.
To get an intuition of substitution, let’s look at some examples before giving a precise definition.
Notice that in , substitutions are performed from right to left, so the first (i.e. the rightmost) substitution results .
If we want to simultaneously substitute multiple variables, we would write . However we will only study substituting a single variable for now.
Substitution in Abstractions
Next, let’s think about how substituting into an abstraction should work. To make this concrete, let’s again look at some Rust code for perspective.
We define a function foo which returns a closure |y| { x + y }.
fn foo(x: i32) -> impl Fn(i32) -> i32 {
move |y| { x + y }
}
fn main() {
let add1 = foo(1);
}Inside main, the function application foo(10) can be thought of as taking the body of foo and replacing substituting foo’s parameters with the provided arguments.
This results in the following idea:
So foo(1) becomes the function |y| { 1 + y }.
In Rust, closures are very similar to anonymous functions from lambda calculus, but due to the ownership system, the borrows checker has to be quite strict with what they can do.
In this case we can transparently think of |y| { 1 + y } as an “arithmetic lambda term” .
Now, let’s look at some lambda calculus examples. As substitution should only substitute free variables, it should behave as follows.
It’s crucial to notice that substitution goes into an abstraction only if the substitution variable differs from the abstraction’s bound variable. For example, in , nothing is substituted because all occurrences of are bound.
Here is the formal definition of substitution.
When is Substitution Legal
Substitution, as we have just defined, is a brittle process. If the “value” that is substituted for the variable is not a closed term, we may end up in trouble. For example, consider the following substitution
Notice how the free variable got bound by an abstraction. This is called variable capturing, and must not happen during substitution. The key rule of substitution is: it must not cause any free variables in the substitute to become bound.
To avoid this, we define the notion of when a substitution is legal. The process conceptually takes two steps:
- Find the free variables in , i.e. compute .
- Next, find all free occurrences of in while keeping track of the context . When a free occurrence is found, check if and contain shared variables. If they have a shared variable at any free occurrence of , then the substitution is not legal.
Take a moment to walk through the process described above. Here it is in detail.
Step 1, we first notice that . Step 2. we then look for free occurrences of , while keeping track of the context.
The context starts initially as the empty set. When we traverse into the body of we insert into the context (). When we reach the inside , we notice that . Because the intersection is nonempty, the substitution is not legal.