This is an Agda library for abstract binding trees as in Chapter 1 of Robert Harper's book Practical Foundations for Programming Languages. An abstract binding tree (ABT) is an abstract syntax tree that also knows about binders and variables. Thus, this library also defines substitution on ABTs and provides theorems about substitution. The library represents variables using de Bruijn indices.
An abstract binding tree ABT
consists of two kinds of nodes:
-
Variables: A variable node is a leaf (no children) and stores the de Bruijn index.
-
Operators: An operator node is tagged with the kind of operator and it has zero or more children, depending on the kind of operator.
The ABT
data type is defined in the
AbstractBindingTree
module, which is parameterized by the kinds of operators and their
signatures, which specifies things like the number of child nodes for
each kind of operator.
To specify the operators, create a data type definition with one constructor for each kind. Using the lambda calculus as an example, one would define two kinds: one for lambda abstraction and another for application.
data Op : Set where
op-lam : Op
op-app : Op
To specify the signatures, write a function that maps your operators
to a list of the Sig
data type. The length of the list says the number
of children nodes and the Sig
in the list controls changes
in variable scoping that child. The Sig
data type is defined
recursively as follows:
data Sig : Set where
■ : Sig
ν : Sig → Sig
∁ : Sig → Sig
The ν
brings one variable into scope. The ∁
clears the scope of
the child, so that the child does not have access to the surrounding
lexical scope. The ■
terminates the changes in scope.
For the lambda calculus, the signature function would be as follows.
sig : Op → List Sig
sig op-lam = (ν ■) ∷ []
sig op-app = ■ ∷ ■ ∷ []
A lambda abstraction has one child expression, its body, and one
variable binding comes into scope for the parameter, indicated by
the ν
followed by a terminating ■
. Application has two child expressions,
the function and the argument. Application does not bind any variables,
indicated by the ■
. Suppose we also wanted the language
to include let
expressions. We could add another constructor to Op
, perhaps
named op-let
, and add the following line to the sig
function.
sig op-let = ■ ∷ (ν ■) ∷ []
This says that a let
has two child, the right-hand side and the
body. The let
does not bring any variable bindings into scope for
the right-hand side, but it does for the body expression. With Op
and sig
complete, we can instantiate and import the Syntax
module
and its inner module OpSig
.
open import Syntax
open Syntax.OpSig Op sig
The Syntax.OpSig
module defines an ABT
data type, which we now
look at in more detail. The constructor for variables, the grave
accent, takes one parameter, the natural number that is the de Bruijn
index for the variable. The constructor for operator nodes, written
op ⦅ args ⦆
takes the operator and the arguments, which we explain
below.
Var : Set
Var = ℕ
data Arg : Sig → Set
data Args : List Sig → Set
data ABT : Set where
`_ : Var → ABT
_⦅_⦆ : (op : Op) → Args (sig op) → ABT
The Args
data type is just a list representation, with constructors
nil
and cons
. However, it is parameterized by the list of numbers
that controls its length and binding structure. For each number in the
list, there is one element in the Args
.
data Args where
nil : Args []
cons : ∀{b ls} → Arg b → Args ls → Args (b ∷ ls)
Each element of Args
is an argument, defined by the Arg
data type.
It is parameterized by a Sig
that controls the variable scoping. The
bind
constructor represents a variable binding and corresponds to
the ν
signature. The clear
constructor corresponds to ∁
and
empties the environment for the child. The ast
constructor
corresponds to the terminating ■
and contains the abstract binding
tree for the child.
data Arg where
ast : ABT → Arg ■
bind : ∀{b} → Arg b → Arg (ν b)
clear : ∀{b} → Arg b → Arg (∁ b)
This use of Args
and Arg
makes for rather verbose notation for
abstract binding trees. Therefore we recommend that you use Agda's
pattern synonyms to introduce more concise syntax. For example, to use
ƛ N
as the notation for lambda abstractions, you would define the
following pattern.
pattern ƛ N = op-lam ⦅ cons (bind (ast N)) nil ⦆
To use the syntax L · M
for the application of function L
to
argument M
, you would write:
infixl 7 _·_
pattern _·_ L M = op-app ⦅ cons (ast L) (cons (ast M) nil) ⦆
The complete Agda code for this lambda calculus example is
in the file Lambda.agda
.
The library defines a type Subst
, for substitution, to represent
mappings from de Bruijn indices to ABTs. The identity substitution is
id
, it maps each variable to itself. Given some substitution σ
,
the substitution M • σ
maps 0
to the ABT M
and each number n
greater than zero to σ (n - 1)
.
For example:
(M • L • id) 0 ≡ M
(M • L • id) 1 ≡ L
(M • L • id) 2 ≡ ` 0
(M • L • id) 3 ≡ ` 1
In general, substitution replaces a variable i
with
the ith ABT in the substitution:
(M₀ • … • Mᵢ • … • Mⱼ • id) i ≡ Mᵢ
unless i > j
where Mⱼ is the last ABT before the terminating id
,
in which case the result is i - (j + 1)
(M₀ • … • Mᵢ • … • Mⱼ • id) i ≡ ` (i - (j + 1))
The reason that the substitution subtracts j + 1
from variables
greater than j
is that we typically perform substition when removing
bindings from around a term, and so the remaining variables in the
term become closer to their bindings.
The library defines the notation ⟪ σ ⟫ M
for applying a substitution
σ
to an ABT M
. When M
is a variable, we have
⟪ σ ⟫ x ≡ ` (σ x)
For example:
⟪ M • L • id ⟫ (` 0) ≡ ` ((M • L • id) 0) ≡ M
Next suppose M
is an application with variables in the operator and
argument positions.
⟪ M • L • id ⟫ (` 1 · ` 0) ≡ L · M
In general, substitution acts on application according to the following equation.
⟪ σ ⟫ (L · M) ≡ (⟪ σ ⟫ L) · (⟪ σ ⟫ M)
The action of substitution on lambda abstractions is more interesting because the lambda brings a variable into scope. Consider the following substitution.
σ ≡ M₀ • M₁ • M₂ • …
To transport this substitution across a lambda abstraction, we need to
do two things. First, inside the lambda, the de Bruijn index 0 is
bound to the lambda's parameter, and should not be changed by the
substitution. So the new substitution should map 0 to 0 and map the
rest of the natural numbers to M₀, M₁, M₂ and so on. Second, as the
substitution σ moves over the lambda, each of the Mᵢ
in the substitution
moves further away from the bindings of their free variables. Thus, to make
sure the free variables in each Mᵢ
still point to the appropriate bindings,
they all need to be incremented by one. The library defines a shift
operator, written ↑ k
, that adds k
to every free variable in an
ABT. The operator ⟰ σ
applies shift by 1 to every term in the
substitution.
⟰ σ ≡ ⟪ ↑ 1 ⟫ M₀ • ⟪ ↑ 1 ⟫ M₁ • …
Putting these two actions together, the library defines a
function named ext
that transports a substitution σ across one
lambda abstraction.
ext σ ≡ ` 0 • ⟰ σ
So we have the following two equations about exts
:
(exts-0) (ext σ) 0 ≡ 0
(exts-suc)† (ext σ) (suc x) ≡ (σ ⨟ ↑ 1) x
where the operation σ₁ ⨟ σ₂
composes two substitutions by applying
σ₁
and then σ₂
.
In general, substitution acts on lambda abstractions according to the following equation.
⟪ σ ⟫ (ƛ N) ≡ ƛ (⟪ ext σ ⟫ N)
Even more generally, and recalling the way in which we defined lambda
abstraction in terms of an ABT operator node, each occurrence of the
bind
argument constructor causes substitution to introduce one
exts
around the substitution.
Last but not least, the library introduces the notation N [ M ]
for the common case of substituting M
for de Bruijn index 0
inside N
.
N [ M ] ≡ ⟪ M • id ⟫ N
For example, β reduction would be expressed as
(ƛ N) M -→ N [ M ]
The following is an example of β reduction.
The inner ƛ is applied to M
.
(ƛ ((ƛ (` 0 · ` 1)) · M)) · L —→ (ƛ (M · ` 0)) · L
An important property of (single) substitution is that two substitutions commute with one another if the variables are different, a property known as the Substitution Lemma in Barendregt's The Lambda Calculus.
M[ x := N ][ y := L ] ≡ M[ y := L ][ x := N[ y := L] ]
The Substitution Lemma is used, for example, in the proof of confluence of the untyped lambda calculus.
Converting the Substitution Lemma to our notation and to Bruijn
indices (let x
be index 0 and y
be index 1), we obtain
M[ N ][ L ] ≡ (⟪ ext (L • id) ⟫ M) [ N [ L ] ]
Generalizing the substitution by L
to any simultaneous substitution
σ
, we have the following theorem which is provided by the library.
(commute-subst)† ⟪ σ ⟫ (N [ M ]) ≡ (⟪ ext σ ⟫ N) [ ⟪ σ ⟫ M ]
Setting up the infrastructure necessary to prove this theorem is a fair bit of work, so it is nice to reuse this theorem instead of having to prove it yourself.
The need for a slightly different property, shown below, arises in proofs based on logical relations. A simultaneous substitution followed by a single substitution can be combined into one simultaneous substitution as follows.
(exts-sub-cons)† (⟪ ext σ ⟫ N) [ M ] ≡ ⟪ M • σ ⟫ N
The proof of this property is also provided in the library, using the
same infrastructure needed to prove commute-subst
.
We refer to the special case of a substitution that maps variables to
variables as a renaming. In some situations, it helps to prove
lemmas about renaming on the way to proving the corresponding lemmas
about substitutions. For example, in
Lambda.agda
we define a simple type
system for the lambda calculus and prove type safety via the standard
progress and preservation lemmas. For the preservation lemma, one must
prove that substitution preserves typing. That proof goes through more
smoothly if we first prove that renaming preserves typing.
We use much of the same syntax for renamings: id
is the identity
renaming, x • ρ
maps 0
to x
and each number n
greater than
zero to ρ (n - 1)
. To apply a renaming ρ
to a variable x
, the
library defines the notation ⦉ ρ ⦊ x
. Similar to the exts
function
for substitutions, the library defines an ext
function that
transports a renaming across one binder, providing the following
equations.
(ext-0) (ext ρ) 0 ≡ 0
(ext-suc) (ext ρ) (suc x) ≡ suc (⟅ ρ ⟆ x)
To apply a renaming ρ
to a term M
, the library defines the
rename
function. This function is quite similar to the ⟪_⟫
function for substitutions, except that when it goes under a binder,
it uses ext
instead of exts
. For example, here is the equation
for renaming applied to a lambda abstraction.
rename ρ (ƛ N) ≡ ƛ (rename (ext ρ) N)
The library provides a function for converting a renaming to a
substitution, named rename→subst
, and the following equation that
relates the application of a renaming to the application of the
corresponding substitution.
(rename-subst)† rename ρ M ≡ ⟪ rename→subst ρ ⟫ M
For example, from this equation we have
rename (↑ 1) M ≡ ⟪ ↑ 1 ⟫ M
Combining this with the (exts-suc)
equation, we can express exts
in terms of rename
.
(exts-suc-rename)† (ext σ) (suc x) ≡ rename (↑ 1) (⟪ σ ⟫ (` x))
Analogous to the commute-subst
theorem mentioned above,
renaming also commutes with single substitution.
(rename-subst-commute)†
(rename (ext ρ) N) [ rename ρ M ] ≡ rename ρ (N [ M ])
You may very well have need of other equations involving substitutions. If those equations only involve the following substitution operators, then there is a decidable algorithm for proving or disproving the equations.
id
↑ k
M • σ
σ₁ ⨟ σ₂
These four operators form the σ algebra of Abadi, Cardelli, Curien,
and Levy (1991). The exts
function is not part of the σ algebra but
it is equivalent to the following σ algebra expression.
(exts-cons-shift)† ext σ ≡ ` 0 • (σ ⨟ ↑ 1)
The equations of the σ algebra, adapted to ABTs, are as follows.
(sub-head) (M • σ) 0 ≡ M
(sub-tail)† ↑ 1 ⨟ (M • σ) ≡ σ
(Z-shift)† (` 0 • ↑ 1) x ≡ ` x
(sub-η)† ((⟪ σ ⟫ (` 0)) • (↑ ⨟ σ)) x ≡ σ x
(sub-op) ⟪ σ ⟫ (op ⦅ args ⦆) ≡ op ⦅ ⟪ σ ⟫₊ args ⦆
(sub-nil) ⟪ σ ⟫₊ nil ≡ nil
(sub-cons) ⟪ σ ⟫₊ (cons arg args) ≡ cons (⟪ σ ⟫ₐ arg) (⟪ σ ⟫₊ args)
(sub-ast) ⟪ σ ⟫ₐ (ast M) ≡ ast (⟪ σ ⟫ M)
(sub-bind) ⟪ σ ⟫ₐ (bind arg) ≡ bind (⟪ ext σ ⟫ₐ arg)
(sub-sub)† ⟪ τ ⟫ ⟪ σ ⟫ M ≡ ⟪ σ ⨟ τ ⟫ M
(sub-idL)† id ⨟ σ ≡ σ
(sub-idR)† σ ⨟ id ≡ σ
(sub-assoc)† (σ ⨟ τ) ⨟ θ ≡ σ ⨟ (τ ⨟ θ)
(sub-dist)† (M • σ) ⨟ τ ≡ (⟪ τ ⟫ M) • (σ ⨟ τ)
When the equations are applied from left to right, they form a rewrite
system that decides whether any two substitutions are equal. Many of
the equations of the σ algebra are definitional equalities, so they
are automatically taken into account when you use refl
to prove an
equality in Agda.
† The σ algebra equations that are not definitional equalities are marked with a †. We would have liked to add them to Agda's automatic rewrites, but we have found that the rewriting extension triggers internal errors in Agda. Thus, you will need to manually apply the equations marked with †.