* This post has the content of a tutorial I wrote before creating this website.
Background
This site is both an overview of normalization by evaluation and a formalization in Agda of the algorithm for the simply typed lambda calculus, based largely on its presentation in Chapter 2 of Andreas Abel’s habilitation thesis, “Normalization by Evaluation: Dependent Types and Impredicativity”. It was compiled from a literate Agda file available here by following the helpful advice in this blog post by Jesper Cockx.
For clarity and readability, some parts of the source file are left out in this rendering, and this will be called out when possible.
Some familiarity with Agda (e.g. such as having worked through the first part of Programming Languages Foundations in Agda) is assumed along with some knowledge of programming language foundations, though the content is mostly self contained.
Introduction
Consider the following term in the lambda calculus:
λx. (λy. y) xThis term is not in its normal form, that is, it can still undergo some reductions. In this case, we can apply a beta reduction under the first binder and arrive at:
λx. xThis new term is now the normal form of λx. (λy. y) x. What we’ve just done,
believe it or not, is normalization by evaluation!
Normalization by evaluation is a technique for deriving the normal form of a term in an object language by evaluating the term in a meta language (a language we are using to describe the object language). In this case, our object language was the untyped lambda calculus, and our meta language was, well, just plain English.
In essence, you can reduce a term by evaluating the parts that can be evaluated while leaving the parts that can’t untouched. That is the intuition behind normalization by evaluation.
To actually formalize normalization by evaluation and prove its correctness in Agda, the algorithm may seem to become less intuitive, but it will still be based on this initial idea.
STLC
The object language that will be used here to define normalization by evaluation
will be the simply-typed lambda calculus with 𝟙 (“unit”) as a base type. It
has variables, functions, application, and a single value of type 𝟙: unit.
data Type : Set where -- unit 𝟙 : Type -- functions _⇒_ : ∀ (S T : Type) → Type
A typing context (for which the metavariable Γ will be used) is either the
empty context ∅ or an extension to a context Γ , x:S mapping an object
language variable to a type (here, Γ is extended with the variable x mapped
to the type S).
The Agda definition does not actually mention variable names at all, and is
really just a list of types. This is because a de Brujin representation will be
used for variables, so instead of a name, a variable will be an index into the
list of types making up the context (i.e. a de Brujin index). For example, the
variable x in the context Γ, x:S would be represented simply as the zeroth
index.
data Ctx : Set where ∅ : Ctx _,_ : Ctx → Type → Ctx
The de Brujin index representing a variable will not actually be a natural
number “index”, but rather a lookup judgements into a context. These lookup
judgements are very similar to natural numbers (and their contructors have been
named suggestively based on this similarity: 𝑍 for zero and 𝑆 for
successor). Defining them this way instead of simply using Agda’s natural
numbers will allow for an index into a context to always be well-defined (and
for variables to be intrinsically typed, as will be shown in a moment).
data _∋_ : Ctx → Type → Set where
𝑍 : ∀ {Γ : Ctx} {T : Type}
---------
→ Γ , T ∋ T
𝑆_ : ∀ {Γ : Ctx} {S T : Type}
→ Γ ∋ T
---------
→ Γ , S ∋ T
Using these, the context ∅, x:S, y:T can be represented along with the
variable names "x" and "y" as is done in the following example.
module Example (S T : Type) where ∅,x:S,y:T = ∅ , S , T x : ∅,x:S,y:T ∋ S x = 𝑆 𝑍 y : ∅,x:S,y:T ∋ T y = 𝑍
STLC terms will be embedded in Agda using an intrinsically typed representation. Types are defined first, and terms are only every considered with respect to their type.
Using this representation, terms that are not well-typed don’t even have to be
considered, as they are impossible to represent. An STLC term t embedded in
Agda as an expression of type Γ ⊢ T is, by definition, a well-typed STLC
term of type T in the context Γ (written as Γ ⊢ t : T).
For clarity, when talking about terms their representation in the STLC will be
used over their intrinsically typed representation using de Brujin indices, and
all terms will be assumed to be well-typed. (e.g. the variable # 𝑍 will be
referred to as Γ, x:T ⊢ x : T, or just x.)
data _⊢_ (Γ : Ctx) : Type → Set where
-- unit term
unit : Γ ⊢ 𝟙
-- variable
#_ : ∀ {S : Type}
→ Γ ∋ S
-----
→ Γ ⊢ S
-- abstraction
ƛ_ : ∀ {S T : Type}
→ Γ , S ⊢ T
---------
→ Γ ⊢ S ⇒ T
-- application
_·_ : ∀ {S T : Type}
→ Γ ⊢ S ⇒ T
→ Γ ⊢ S
---------
→ Γ ⊢ T
Here are some sample programs in STLC embedded here using these constructors:
module SamplePrograms where
-- Γ ⊢ λx. x : T → T
ex0 : ∀ {Γ : Ctx} {T : Type} → Γ ⊢ T ⇒ T
ex0 = ƛ # 𝑍
-- ∅ ⊢ (λx. x) unit : 𝟙
ex1 : ∅ ⊢ 𝟙
ex1 = ex0 · unit
With this embedding of the simply typed lambda calculus in Agda, an algorithm for normalization by evaluation can actually be written. However, to prove properties about the algorithm (e.g. that it is actually correct), a few more language constructs are still needed. They are: context extension, substitutions, and definitional equality. These will be defined before getting into the details of the algorithm itself.
Context extension
When defining the algorithm for normalization by evaluation, it will be
necessary to determine whether or not a context is an extension of another. A
context Γ′ extends another context Γ if every mapping in Γ is also in
Γ′.
Since contexts are really just lists in their Agda representation, Γ′ will be
an extension of Γ if Γ is a “sublist” of Γ′. The relation for context
extension is defined inductively based somewhat on this idea: a context extends
itself, and given that a context Γ′ extends another context Γ, an extension
of Γ′ is still an extension of Γ′.
data _≤_ : Ctx → Ctx → Set where
≤-id : ∀ {Γ : Ctx} → Γ ≤ Γ
≤-ext : ∀ {Γ Γ′ : Ctx} {T : Type}
→ Γ′ ≤ Γ
----------
→ Γ′ , T ≤ Γ
The relation is antisymmetric, meaning that if Γ′ ≤ Γ and Γ ≤ Γ′, then
Γ′ and Γ must be the same context. This proof is left out in the rendering,
though it is proven mutually with the fact that Γ is never an extension of
Γ, x:T.
≤-antisym : ∀ {Γ Γ′ : Ctx}
→ Γ ≤ Γ′
→ Γ′ ≤ Γ
------
→ Γ ≡ Γ′
Γ≰Γ,T : ∀ {Γ : Ctx} {T : Type} → ¬ (Γ ≤ Γ , T)
This relation is also transitive, a proof that follows by induction:
≤-trans : ∀ {Γ″ Γ′ Γ : Ctx}
→ Γ″ ≤ Γ′
→ Γ′ ≤ Γ
-------
→ Γ″ ≤ Γ
≤-trans ≤-id ≤-id = ≤-id
≤-trans ≤-id (≤-ext pf) = ≤-ext pf
≤-trans (≤-ext pf) ≤-id = ≤-ext pf
≤-trans (≤-ext pf₁) (≤-ext pf₂) = ≤-ext (≤-trans pf₁ (≤-ext pf₂))
Finally, this relation can be made decidable. Its decidability requires that equality between contexts (and by extension, type) also be decidable; these proofs are also left out in the rendering.
_≟Tp_ : ∀ (S T : Type) → Dec (S ≡ T)
_≟Ctx_ : (Γ Γ′ : Ctx) → Dec (Γ ≡ Γ′)
With these, the relation can be made decidable in Agda:
_≤?_ : ∀ (Γ′ Γ : Ctx) → Dec (Γ′ ≤ Γ)
∅ ≤? ∅ = yes ≤-id
∅ ≤? (_ , _) = no λ()
(_ , _) ≤? ∅ = yes Γ≤∅ where
Γ≤∅ : ∀ {Γ : Ctx} → Γ ≤ ∅
Γ≤∅ {∅} = ≤-id
Γ≤∅ {Γ , _} = ≤-ext Γ≤∅
(Γ′ , T) ≤? Γ@(_ , _)
with (Γ′ , T) ≟Ctx Γ
... | yes refl = yes ≤-id
... | no Γ′≢Γ
with Γ′ ≤? Γ
... | yes pf = yes (≤-ext pf)
... | no ¬pf = no λ where
≤-id → Γ′≢Γ refl
(≤-ext pf) → ¬pf pf
Substitution
A parallel substitution Γ ⊢ σ : Δ provides a term in Γ to substitute for
each variable in the context Δ. In other words, a substitution σ is a
function from variables in a context to terms in another context.
Sub : Ctx → Ctx → Set
Sub Γ Δ = ∀ {T : Type} → Δ ∋ T → Γ ⊢ T
To actually use a substitution, an operation is needed to apply the substitution to a term in the context being used by the substitution:
Δ ⊢ σ : Γ Δ ⊢ t : T
------------------------
Γ ⊢ t[σ] : TThis operation would allow for transforming a term t that is well-typed in the
context Δ using a substitution σ that maps every variable in Δ to a term
that is well-typed in Γ.
Defining this operation is actually a little tricky in Agda, because the
typical definition of the application of a substitution σ is not obviously
terminating. To solve this problem, it is necessary to separately define a
smaller subset of substitution: renaming.
A renaming is a specialized substitution where the only terms that can be
substituted for variables are other variables (i.e. a renaming Γ ⊢ ρ : Δ
provides a variable in Γ, not a term in Γ, to replace for every variable
in Δ).
Ren : Ctx → Ctx → Set
Ren Γ Δ = ∀ {T : Type} → Δ ∋ T → Γ ∋ T
Any renaming can be transformed to the more general definition for substitutions:
ren : ∀ {Γ Δ : Ctx} → Ren Γ Δ → Sub Γ Δ
ren ρ x = # ρ x
Two renamings that will be especially relevant are the identity renaming (which
substitutes variables for themselves) and the shifting renaming (which shifts
all variables by 1). To indicate that these are renamings specifically (as they
will also be defined for the more general definition of substitutions), the
superscript ʳ is used.
idʳ : ∀ {Γ : Ctx} → Ren Γ Γ
idʳ x = x
↥ʳ : ∀ {Γ : Ctx} {T : Type} → Ren (Γ , T) Γ
↥ʳ x = 𝑆 x
Any two renamings can also be composed. For a renaming substitution, this is
really just function compostition. Agda’s own symbol for function composition,
∘, is used for this reason (though again with the superscript ʳ).
_∘ʳ_ : ∀ {Γ Δ Σ : Ctx} → Ren Δ Γ → Ren Σ Δ → Ren Σ Γ
ρ ∘ʳ ω = λ x → ω (ρ x)
It is possible to define a renaming for a context Γ′ using a context Γ that
it extends by composing many shifting renamings, ending finally at the identity
renaming.
ρ-≤ : ∀ {Γ′ Γ : Ctx} → Γ′ ≤ Γ → Ren Γ′ Γ
ρ-≤ ≤-id = idʳ
ρ-≤ (≤-ext pf) = ρ-≤ pf ∘ʳ ↥ʳ
The application of a renaming substituion Γ ⊢ ρ : Δ to a term Δ ⊢ t : T
rebases the term to the context Γ. This is done by “distributing” the
renaming substitution across all subterms of the term, renaming all variables
used in the term with their corresponding variable in Γ. When going under a
binder, the renaming substitution has to be “extended” (ext) to now use the
newly bound variable 𝑍.
ext : ∀ {Γ Δ : Ctx} → Ren Γ Δ → ∀ {T : Type} → Ren (Γ , T) (Δ , T)
ext ρ 𝑍 = 𝑍
ext ρ (𝑆 x) = 𝑆 ρ x
_[_]ʳ : ∀ {Γ Δ : Ctx} {T : Type}
→ Δ ⊢ T
→ Ren Γ Δ
-------
→ Γ ⊢ T
unit [ _ ]ʳ = unit
# x [ ρ ]ʳ = # ρ x
(ƛ t) [ ρ ]ʳ = ƛ t [ ext ρ ]ʳ
(r · s) [ ρ ]ʳ = r [ ρ ]ʳ · s [ ρ ]ʳ
With the application of a renaming substitution, it is now possible to define
the application of any general substitution such that it is guaranteed to
terminate. Extending the terms in the substitution under a binder requires
applying a shifting substitution to every term in the binder. By defining
the application of renaming substitutions separately, extending a substitution
can be done such that the overall definition of the application Γ ⊢ t [ σ ]: T
of a substitution Γ ⊢ σ : Δ is guaranteed to be terminating. The definition is
very similar to the more specific application of a renaming substitution, except
variables are now being replcaed with entire terms.
exts : ∀ {Γ Δ : Ctx} → Sub Γ Δ → ∀ {T : Type} → Sub (Γ , T) (Δ , T)
exts σ 𝑍 = # 𝑍
exts σ (𝑆 x) = (σ x) [ ↥ʳ ]ʳ
_[_] : ∀ {Γ Δ : Ctx} {T : Type}
→ Δ ⊢ T
→ Sub Γ Δ
-------
→ Γ ⊢ T
unit [ _ ] = unit
# x [ σ ] = σ x
(ƛ t) [ σ ] = ƛ t [ exts σ ]
(r · s) [ σ ] = r [ σ ] · s [ σ ]
The more general identity and shifting substitutions are defined exactly as they
were for renamings, except now the variable term is used. Parallel substitutions
can also be composed, by applying a substitution Γ ⊢ τ : Δ to every term in a
substitution Δ ⊢ σ : Σ.
id : ∀ {Γ : Ctx} → Sub Γ Γ
id x = # x
↥ : ∀ {Γ : Ctx} {T : Type} → Sub (Γ , T) Γ
↥ x = # 𝑆 x
_∘_ : ∀ {Γ Δ Σ : Ctx} → Sub Δ Γ → Sub Σ Δ → Sub Σ Γ
(σ ∘ τ) x = (σ x) [ τ ]
Any substitution Γ ⊢ σ : Δ can be have a well-typed term Γ ⊢ s : S added to
it as well, which will be written as Γ ⊢ σ ∷ s : Δ, x:S (with ∷ used for
“cons”). This operation is similar to the extension exts of a substitution,
except that terms in the substitution do not need to be shifted (and in fact,
exts σ is equivalent to (σ ∘ ↥) ∷ # 𝑍).
_∷_ : ∀ {Γ Δ : Ctx} {S : Type} → Sub Γ Δ → Γ ⊢ S → Sub Γ (Δ , S)
(_ ∷ s) 𝑍 = s
(σ ∷ _) (𝑆 x) = σ x
Using the renaming substitution for context extension, any well-typed term in
Γ can be “weakened” to a well-typed term in a context Γ′. ≤⊢ will be used
as shorthand for the application of a weakening substitution (and in Agda, this
will look a lot like an extended judgement: Γ′≤Γ ≤⊢ t).
weaken : ∀ {Γ′ Γ : Ctx}
→ Γ′ ≤ Γ
--------
→ Sub Γ′ Γ
weaken pf x = # ρ-≤ pf x
_≤⊢_ : ∀ {Γ′ Γ : Ctx} {T : Type} → Γ′ ≤ Γ → Γ ⊢ T → Γ′ ⊢ T
pf ≤⊢ t = t [ weaken pf ]
It will similarly be useful to introduce shorthand for the application of a shifting substitution:
_↥⊢_ : ∀ {Γ : Ctx} {T : Type} → (S : Type) → Γ ⊢ T → Γ , S ⊢ T
_ ↥⊢ t = t [ ↥ ]
To actually prove results about terms, a number of substitution lemmas will be
necessary. Their proofs are omitted, though they are directly inspired from the
Substitution chapter of PLFA. The
most import ones are sub-sub (substitutions can be composed) and
[id]-identity (the application of the identity substitution is an identity).
[id]-identity : ∀ {Γ : Ctx} {T : Type} {t : Γ ⊢ T}
→ t [ id ] ≡ t
sub-sub : ∀ {Γ Δ Σ : Ctx} {T : Type} {τ : Sub Γ Δ} {σ : Sub Δ Σ}
{t : Σ ⊢ T}
→ t [ σ ] [ τ ] ≡ t [ σ ∘ τ ]
Definitional Equality
There is still one language construct left to define ─ equality. To explain why an embedding of equality in Agda is needed, we can begin discussing normalization by evaluation in more detail.
Normalization by evaluation is an algorithm for normalization, the process of
transforming a term into its normal form. The normal form of a term is unique,
being the term with all possible reductions (i.e. “computations”) applied to it.
For any normalization algorithm nf such that nf(t) is the normal form of a
term Γ ⊢ t : T, we would expect the following properties to hold.
Γ ⊢ nf(t) : T(well-typedness of normal form)A normalization algorithm should still produce a term that is well-typed under the context
Γ(and with the same type)⟦ nf(t) ⟧ = ⟦ t ⟧(preservation of meaning)The
⟦ t ⟧notation here indicates the denotation oft, which is equivalent to its meaning (in some meta-language).We want an algorithm for normalization by evaluation to ensure that the normal form of a term that is obtained is semantically equal to the original term. Put simply, this means that the two terms must have the same meaning.
nf(nf(t)) = nf(t)(idempotency)This property refers to the “normalization” part of the algorithm ─ it should actually produce a term that has been fully normalized, i.e. it cannot undergo any more normalization.
Equality of functions is undecidable, so the last property is especially tricky
to prove for any algorithm in general. Instead, we will want to use
βη-equivalence, or definitional equality. In STLC, we have that two terms are
definitionally equal if and only if they have the same meaning. By proving that
Γ ⊢ nf(t) = t : T, that the normal form of a term is definitionally equal to
the original term, we will be proving that the normal form of a term preserves
the meaning of the original term.
To actually define βη-equivalence, we need to first define operations for β-reductions and η-expansions.
A β-reduction will be the application of a substitution t[s/x] that
substitutes the term s for the variable x in the term t. In Agda, this
substitution will be the identity substitution with the term s added as the
first term in the substitution. For convenience, we will use t [ s ]₀ (as we
are replacing the zeroth term in the identity substitution).
_[_]₀ : ∀ {Γ : Ctx} {S T : Type}
→ Γ , S ⊢ T
→ Γ ⊢ S
---------
→ Γ ⊢ T
_[_]₀ {Γ} {S} t s = t [ id ∷ s ]
η-expansion for a functional term Γ ⊢ t : S → T will be an abstraction
Γ ⊢ λx . t x : S → T containing the application of a variable Γ, x:S ⊢ x : S to the term t. The term t needs to have a shifting substitution applied
to it as we are using an intrinsically-typed representation (in changing the
context from Γ to Γ, x:S, the expression t itself also changes).
η-expand : ∀ {Γ : Ctx} {S T : Type}
→ Γ ⊢ S ⇒ T
→ Γ ⊢ S ⇒ T
η-expand {S = S} t = ƛ (S ↥⊢ t) · # 𝑍
With these defined, we can actually introduce definitional equality in Agda.
We use t == t′ in Agda instead of Γ ⊢ t = t′ : T, though we will refer to
two terms that are definitionally equal with the latter.
data _==_ : ∀ {Γ : Ctx} {T : Type} → Γ ⊢ T → Γ ⊢ T → Set where
-- computation rule: beta reduction
β : ∀ {Γ : Ctx} {S T : Type}
{t : Γ , S ⊢ T}
{s : Γ ⊢ S}
----------------------
→ (ƛ t) · s == t [ s ]₀
-- η-expansion / function extensionality
-- i.e. Γ ⊢ t = Γ ⊢ λx. t x : S ⇒ T
η : ∀ {Γ : Ctx} {S T : Type}
{t : Γ ⊢ S ⇒ T}
----------------------
→ t == η-expand t
-- compatibility rules
abs-compatible : ∀ {Γ : Ctx} {S T : Type} {t t′ : Γ , S ⊢ T}
→ t == t′
-----------
→ ƛ t == ƛ t′
app-compatible : ∀ {Γ : Ctx} {S T : Type}
{r r′ : Γ ⊢ S ⇒ T} {s s′ : Γ ⊢ S}
→ r == r′
→ s == s′
----------------
→ r · s == r′ · s′
-- equivalence rules
refl⁼⁼ : ∀ {Γ : Ctx} {T : Type} {t : Γ ⊢ T}
------
→ t == t
sym⁼⁼ : ∀ {Γ : Ctx} {T : Type} {t t′ : Γ ⊢ T}
→ t == t′
-------
→ t′ == t
trans⁼⁼ : ∀ {Γ : Ctx} {T : Type} {t₁ t₂ t₃ : Γ ⊢ T}
→ t₁ == t₂
→ t₂ == t₃
--------
→ t₁ == t₃
For the readability of some of the proofs that will follow, it will be helpful to have equational reasoning defined with respect to definitional equality. Its definition is almost identical to Agda’s own equational reasoning for propositional equality, so it is left out in the rendering.
open ==-Reasoning public
Propositional equality implies definitional equality, a fact that will be helpful to include here for later use.
≡→== : ∀ {Γ : Ctx} {T : Type} {t t′ : Γ ⊢ T}
→ t ≡ t′
-------
→ t == t′
≡→== pf rewrite pf = refl⁼⁼
Evaluation
The evaluation, or interpretation, ⟦ t ⟧ of a well-typed term Γ ⊢ t : T
assigns a meaning to t by equating it to a semantic object in our meta
language, using an interpretation of the context Γ (an environment) under
which the term t is well-typed.
For types, we can interpret 𝟙 as Agda’s own unit type, ⊤, and functions as
Agda functions, with their meaning defined inductively.
⟦ 𝟙 ⟧ = ⊤
⟦ S ⇒ T ⟧ = ⟦ S ⟧ → ⟦ T ⟧An empty context is interpreted as the unit type (an “empty” environment), and an extension to a context is defined inductively, with the extension itself being the interpretation of the type the context is extended with.
⟦ ∅ ⟧ = ⊤
⟦ Γ , S ⟧ = ⟦ Γ ⟧ × ⟦ S ⟧We will use the lowercase Greek letter of a context to refer to its environment
(e.g. γ is an environment for Γ).
The interpretation of a variable expects an environment, and is essentially a lookup into the environment for the variable’s value:
⟦ Γ ∋ x:T ⟧ (γ ∈ ⟦ Γ ⟧) ∈ ⟦ T ⟧
⟦ Γ , T ∋ x:T ⟧ (γ , a) = a
⟦ Γ , y:S ∋ x:T ⟧ (γ , _) = ⟦ Γ ∋ x:T ⟧ γThe interpretation of a typed term expects an environment as well, evaluating the term by using the environment for the variables that the term is using.
⟦ Γ ⊢ t : T ⟧ (γ ∈ ⟦Γ⟧) ∈ ⟦ T ⟧
⟦ Γ ⊢ unit : 𝟙 ⟧ γ = tt
⟦ Γ ⊢ x : T ⟧ γ = ⟦ Γ ∋ x:T ⟧ γ
⟦ Γ ⊢ λx . t : S ⇒ T ⟧ γ = λ a → ⟦ Γ , x:S ⊢ t : T ⟧ (γ , a)
⟦ Γ ⊢ r s : T ⟧ γ = (⟦ Γ ⊢ r : S ⇒ T ⟧ γ) (⟦ Γ ⊢ s : S ⟧ γ)Before moving forward, we introduce the record we will use to represent interpretations of types and contexts. For now, we will only include the interpretation of a context as an environment, as our interpretation of types will change subtly to better fit our algorithm for normalization by evaluation ─ this is also why we have only discussed evaluation at a high level.
record Interpretation (D : Set) : Set₁ where
field
⟦_⟧ : D → Set
open Interpretation ⦃...⦄ public
instance
⟦Γ⟧ : ⦃ _ : Interpretation Type ⦄ → Interpretation Ctx
Interpretation.⟦ ⟦Γ⟧ ⟧ ∅ = ⊤
Interpretation.⟦ ⟦Γ⟧ ⟧ (Γ , T) = ⟦ Γ ⟧ × ⟦ T ⟧
Normalization by Evaluation
The key idea behind normalization by evaluation is that we have inherently
performed some normalization of the term t in its evaluation – if t was an
application r s, we are actually performing that application and reducing the
term. Normalization by evaluation as an algorithm takes advantage of this fact.
An issue with this view is that evaluation is not actually giving us the normal form of a term, but rather its meaning as a semantic object in our meta language. An algorithm for normalization by evaluation would need a way to to convert a semantic object in our meta language back into a term in the object language.
One way to achieve this is to evaluate (i.e. normalize) the parts of the expression that actually can be evaluated (such as function application), while leaving the parts that cannot intact. Under this view, normalization by evaluation becomes the evaluation of an expression with unknowns (i.e. variables) to another, possibly simplified, expression with unknowns.
To get this behavior, we make a subtle change to the “meaning” of a term in the meta language – instead of terms of type 𝟙 mapping to Agda’s unit type, they
will now evaluate to terms in their normal form.
This is a subtle distinction with a significant impact on the algorithm we will
define. We can now easily convert back to the object language, because
technically we never left it to begin with: functions in Agda can be
translated simply abstractions in the STLC, and for terms of type 𝟙, we
already have the term!
In Agda, we do not yet have a concept of normal form. We can define terms in their normal form (normal terms) mutually with terms that are blocked on evaluation because they are unknown (neutral terms).
data Nf : (T : Type) → (Γ : Ctx) → Γ ⊢ T → Set -- Normal terms data Ne (T : Type) (Γ : Ctx) : Γ ⊢ T → Set -- Neutral terms
The rules for these will follow shortly ─ but with this definition we can change
the interpretation of a term of type 𝟙 to what we would want it to be to
define a suitable algorithm for normalization by evaluation:
⟦ 𝟙 ⟧ = Nf 𝟙Note that our data type for normal terms is indexed both by a type and a
context, yet here the interpretation of a type is only indexed by the type
itself. We will get to this later, but it is for this reason that we have again
not written an implementation out in Agda yet. For now, we can give an initial
sketch of the algorithm, using a reflection function ↑ᵀ that maps neutral
terms of type T to semantic objects in ⟦ T ⟧, and a reification function
↓ᵀ for mapping a semantic object in ⟦ T ⟧ to normal forms of type T:
Putting all of these pieces together, we can present (in pseudocode) what an algorithm for normalization by evaluation would do.
⟦ 𝟙 ⟧ = Nf 𝟙
⟦ S → T ⟧ = ⟦ S ⟧ → ⟦ T ⟧
↑ᵀ ∈ Ne T → ⟦ T ⟧
↑ᵘⁿⁱᵗ 𝓊 = 𝓊
↑ˢ ⃕ ᵗ 𝓊 (a ∈ ⟦ S ⟧) = ↑ᵀ (𝓊 𝓋) , 𝓋 = ↓ˢ a
↓ᵀ ∈ ⟦ T ⟧ → Nf T
↓ᵘⁿⁱᵗ 𝓋 = 𝓋
↓ˢ ⃕ ᵗ f = λx. ↓ᵀ (f(a)) , where a = ↑ᵀ x and x is "fresh"
↑ᶜᵗˣ ∈ ⟦ Γ ⟧
↑∅ = tt
↑Γ,x:S = ↑Γ , ↑ᵀ x
nf(t) = ↓ᵀ (⟦ t ⟧ ↑Γ)In summary, the algorithm proceeds as follows:
reflect the variables of the context
Γ(↑Γ)interpret the value of the term using the environment of reflected variables (
⟦ t ⟧ ↑Γ)“reify” the interpreted value of the term (
↓ᵀ (⟦ t ⟧ ↑Γ)), returning it to a term in normal form
The “freshness” condition in this sketch is a key part of why we have not
started defining a more concrete version of the algorithm, but with this sketch
we can see how our new interpretation of the type 𝟙 has benefitted us: we are
able to evaluate a term while leaving its unknowns “untouched”: reflection of an
unknown term of type 𝟙 yields the unknown itself, while we always η-expand at
reification to continue evaluation. Once we have finished evaluating the term,
we are easily able to convert it back into our object language.
As an initial step in formally defining this algorithm, we can now introduce the
rules for normal and neutral terms in Agda. Going forward, we will be using 𝓊
(for “unknown”) to refer to neutral terms and 𝓋 (for “value”) to refer to
normal terms.
Neutral terms are normal terms in their blocked form. Variables are the “base case” for blocked terms, with application of an unknown function to a normal term also being blocked.
data Ne T Γ where
ne-var : (x : Γ ∋ T)
------------
→ Ne T Γ (# x)
ne-app : ∀ {S : Type} {𝓊 : Γ ⊢ S ⇒ T} {𝓋 : Γ ⊢ S}
→ Ne (S ⇒ T) Γ 𝓊
→ Nf S Γ 𝓋
--------------
→ Ne T Γ (𝓊 · 𝓋)
Normal terms are terms in their normal form. unit is a normal term, as is an
abstraction whose body is itself normalized. Any neutral term is also a normal
term.
data Nf where
nf-unit : ∀ {Γ : Ctx} → Nf 𝟙 Γ unit
nf-abs : ∀ {S T : Type} {Γ : Ctx} {𝓋 : Γ , S ⊢ T}
→ Nf T (Γ , S) 𝓋
------------------
→ Nf (S ⇒ T) Γ (ƛ 𝓋)
nf-neutral : ∀ {T : Type} {Γ : Ctx} {𝓊 : Γ ⊢ T}
→ Ne T Γ 𝓊
--------
→ Nf T Γ 𝓊
Now, we can discuss the issue of the freshness condition used when reifying at
function type. We are using a de Brujin index representation, so “freshness” is
given to us freely by extending the context. However, there is no context
anywhere in our definition of reification, so what context do we extend with the
fresh variable? This is actually an intentional decision for reification,
because of a problem that is more subtle: after we reflect the variable, it may
later be reified in a different context than it was created. Consider the
reification of a semantic object f with type (S → T) → U:
↓⁽ˢ ⃕ ᵗ⁾ ⃕ ᵘ f = λx. ↓ˢ ⃕ ᵗ (f(a)) , where a = ↑ᵘ xThe inner reification evaluates further:
↓ˢ ⃕ ᵗ (f(a)) = λy. ↓ᵗ (f(a)(b)) , where b = ↑ˢ yThis example showcases the problem: when we reflected x into our meta
language, we had to (presumably) use some context Γ to produce the Agda
expression a with the type Nf T Γ. But later, when we reify f(a)(b), we
will produce a term that is possibly using the variable x, but the term is
now in a different context: Γ, y:S.
This suggests that we need to generalize our reflection of terms in the object language over all contexts, so that at reification we can use a different context than the one that was used at reflection.
We introduce liftable normal and neutral terms to address this. These are normal/neutral terms that are generalized over contexts.
While they will be generalized over contexts, this means that a liftable neutral or normal term may not be well-typed when lifted to some contexts. It will be the case that the liftable terms we will use in our algirhtm will only be able to be lifted at reification to a context that is an extension of the context used when the liftable term was reflected (and with the example above, the reason is clear: our algorithm would otherwise never produce a term that is well-typed).
Because we cannot apply any context to a liftable normal/neutral term, we will need a placeholder value for some contexts.
-- Liftable neutral term Ne^ : Type → Set Ne^ T = ∀ (Γ : Ctx) → ∃[ t ] Ne T Γ t ⊎ ⊤ -- Liftable normal term Nf^ : Type → Set Nf^ T = ∀ (Γ : Ctx) → ∃[ t ] Nf T Γ t
For convenience, we only use this placeholder for liftable neutral terms.
This is possible because of how the algorithm for normalization by evaluation
is designed ─ reification always η-expands at function type, so there will only
ever be a need to use a placeholder value at our base type 𝟙. In the case of
liftable normals, we can fallback to using unit (which is a valid normal term)
instead of using our placeholder value.
We allow ourselves this convenience because in proving the soundness of
normalization by evaluation, we will be proving that neither the placeholder
value nor the fallback of unit will actually be used.
Going forward, we will use 𝓋̂ and 𝓊̂ as the metavariables for liftable normal
terms and neutral terms respectively, and will append the symbol ^ for the
“liftable” counterpart of a language construct. For example, we define the
overloaded application (𝓊̂ 𝓋̂)(Γ) = 𝓊̂(Γ) 𝓋̂(Γ) of liftable terms as ·^.
_·^_ : ∀ {S T : Type} → Ne^ (S ⇒ T) → Nf^ S → Ne^ T
(𝓊̂ ·^ 𝓋̂) Γ with 𝓊̂ Γ
... | inj₁ ⟨ 𝓊 , pf-𝓊 ⟩ =
let ⟨ 𝓋 , pf-𝓋 ⟩ = 𝓋̂ Γ in
inj₁ ⟨ 𝓊 · 𝓋 , ne-app pf-𝓊 pf-𝓋 ⟩
... | inj₂ tt = inj₂ tt
The actual interpretation of the base type 𝟙 will be an extension to Agda’s
unit type that embeds liftable neutrals: ⊤̂ (pronounced “top hat”). With it
defined, we can also define the interpretation of types, along with the
evaluation of terms. These are exactly as was shown earlier in pseudocode.
data ⊤̂ : Set where
unit : ⊤̂
ne : Ne^ 𝟙 → ⊤̂
instance
⟦Type⟧ : Interpretation Type
Interpretation.⟦ ⟦Type⟧ ⟧ 𝟙 = ⊤̂
Interpretation.⟦ ⟦Type⟧ ⟧ (S ⇒ T) = ⟦ S ⟧ → ⟦ T ⟧
env-lookup : ∀ {Γ : Ctx} {T : Type} → Γ ∋ T → ⟦ Γ ⟧ → ⟦ T ⟧
env-lookup {Γ , T} 𝑍 ⟨ _ , a ⟩ = a
env-lookup {Γ , T} (𝑆 x) ⟨ γ , _ ⟩ = env-lookup x γ
⟦⊢_⟧ : ∀ {Γ : Ctx} {T : Type} → Γ ⊢ T → ⟦ Γ ⟧ → ⟦ T ⟧
⟦⊢ unit ⟧ _ = unit
⟦⊢ # x ⟧ γ = env-lookup x γ
⟦⊢ ƛ t ⟧ γ a = ⟦⊢ t ⟧ ⟨ γ , a ⟩
⟦⊢ r · s ⟧ γ = ⟦⊢ r ⟧ γ (⟦⊢ s ⟧ γ)
To reify an Agda expressions of type ⊤̂, we will define a function ↓⊤̂. It is
here that the fallback to unit happens, when the context that the embedded
liftable neutral is being lifted to results in it being undefined. This case
will be irrelevant and we will prove that it will never actually be used in the
algorithm for normalization by evaluation by proving that the algorithm
preserves the meaning of the original term (such a fallback actually being used
would make this impossible to prove).
↓⊤̂ : ⟦ 𝟙 ⟧ → Nf^ 𝟙 ↓⊤̂ unit = unit^ where unit^ = (λ _ → ⟨ unit , nf-unit ⟩) ↓⊤̂ (ne 𝓊̂) Γ with 𝓊̂ Γ ... | inj₁ ⟨ 𝓊 , pf ⟩ = ⟨ 𝓊 , nf-neutral pf ⟩ ... | inj₂ tt = ⟨ unit , nf-unit ⟩
We are now ready to actually define reflection and reification in Agda. These
are mutually recursive, and will each be defined by induction on the type T.
Their definition is almost the same as the sketch shown in pseudocode, except
that the implicit changing of contexts is now being handled by using liftable
terms instead.
mutual
↑ᵀ : {T : Type} → Ne^ T → ⟦ T ⟧
↑ᵀ {𝟙} 𝓊̂ = ne 𝓊̂
↑ᵀ {S ⇒ T} 𝓊̂ a = ↑ᵀ (𝓊̂ ·^ 𝓋̂) where 𝓋̂ = ↓ᵀ a
↓ᵀ : {T : Type} → ⟦ T ⟧ → Nf^ T
↓ᵀ {𝟙} = ↓⊤̂
↓ᵀ {S ⇒ T} f Γ =
let ⟨ 𝓋 , pf ⟩ = ↓ᵀ (f a) (Γ , S) in
⟨ ƛ 𝓋 , nf-abs pf ⟩
where a = ↑ᵀ (𝓍̂ S Γ)
Freshness is given to us almost for free as we are using a de Brujin
representation, so a fresh variable would just be the de Brujin index 𝑍. This
variable will be used in a different context from the one in which it was
created, so it will need to be renamed.
For this purpose we use 𝓍̂ S Γ, a liftable variable of type S that can only
be lifted to extensions of the context Γ, x:S. When lifted to an extension
Γ′ of Γ, x:S we apply the extension renaming to the de Brujin index 𝑍 to
obtain its corresponding index in the extended context.
𝓍̂ : (S : Type) → Ctx → Ne^ S
𝓍̂ S Γ Γ′
with Γ′ ≤? (Γ , S)
... | no _ = inj₂ tt
... | yes pf = inj₁ ⟨ # x , ne-var x ⟩ where x = ρ-≤ pf 𝑍
We can also define the reflection of a context Γ into an environment, which
will be the reflected environment over which a typed term in the context Γ
will be evaluated.
↑ᶜᵗˣ : ∀ (Γ : Ctx) → ⟦ Γ ⟧ ↑ᶜᵗˣ ∅ = tt ↑ᶜᵗˣ (Γ , T) = ⟨ ↑ᶜᵗˣ Γ , ↑ᵀ (𝓍̂ T Γ) ⟩
Finally, the algorithm for normalization by evaluation can be written in Agda.
Its definition is again almost exactly the same as the sketch in pseudocode,
except that we now lift the reified normal term to the original context Γ.
nbe : ∀ {Γ : Ctx} {T : Type} → Γ ⊢ T → ∃[ t ] Nf T Γ t
nbe {Γ} t = ↓ᵀ (⟦⊢ t ⟧ (↑ᶜᵗˣ Γ)) Γ
nf : ∀ {Γ : Ctx} {T : Type} → Γ ⊢ T → Γ ⊢ T
nf t = let ⟨ t′ , _ ⟩ = nbe t in t′
And here is an example of the algorithm in action:
module AlgorithmExample where -- (λx. (λy. y) x) unit ex : ∅ ⊢ 𝟙 ex = (ƛ (ƛ # 𝑍) · # 𝑍) · unit -- normal form is unit nf-ex : nf ex ≡ unit nf-ex with ex ... | _ = refl
Correctness
We wish for our algorithm for normalization by evaluation to be both complete and sound. First, we need to prove the property that if two terms are definitionally equal, then they must have the same interpretation. This proof is omitted in the rendering as well ─ it is an adaptation of the proof of soundness of reduction with respect to denotational semantics in PLFA seen in this chapter.
==→⟦≡⟧ : ∀ {Γ : Ctx} {T : Type} {t t′ : Γ ⊢ T} {γ : ⟦ Γ ⟧}
→ t == t′
→ ⟦⊢ t ⟧ γ ≡ ⟦⊢ t′ ⟧ γ
We consider our algorithm for normalization by evaluation complete if two terms that are definitionally equal (and thus have the same meaning) have the same normal form:
Γ ⊢ t = t′ : T implies nf(t) = nf(t′)Expanding out nf here gives us the following theorem:
Γ ⊢ t = t′ : T ⇒ ↓ᵀ (⟦ t ⟧ ↑Γ) Γ = ↓ᵀ (⟦ t′ ⟧ ↑Γ) ΓThis follows directly from Γ ⊢ t = t′ : T implying that ⟦ t ⟧ = ⟦ t′ ⟧.
completeness : ∀ {Γ : Ctx} {T : Type} {t t′ : Γ ⊢ T}
→ t == t′
→ nf t ≡ nf t′
completeness {Γ} t==t′ rewrite ==→⟦≡⟧ {γ = ↑ᶜᵗˣ Γ} t==t′ = refl
As for the soundness properties that we wanted from the algorithm:
Γ ⊢ nf(t) : T(well-typedness of normal form)We are using an intrinsically typed representation of terms, so this property is given to us automatically
⟦ nf(t) ⟧ = ⟦ t ⟧(preservation of meaning)As discussed, equality of functional terms in Agda is undecidable, for which we have introduced definitional equality. Even proving that
Γ ⊢ nf(t) = t : Tis difficult, and we will have to use a logical relation to prove it in the following sectionnf(nf(t)) = nf(t)(idempotency)This follows directly from the preservation of meaning and completeness properties of the algorithm:
By the soundness property of preservation of meaning, we will have
Γ ⊢ nf t = t : T, which will in turn implynf (nf t) = nf(t)by the algorithm’s completeness
Soundness
To prove that the algorithm for normalization by evaluation implemented preserves the meaning of a program, we will prove that a term is definitionally equal to its normal form:
Γ ⊢ t = nf(t) : T
In proving that a term is definitionally equal to its normal form, we will have
that ⟦ nf (t) ⟧ = ⟦ t ⟧, as definitional equality implies semantic equality.
This new property we wish to prove expands to:
Γ ⊢ t = ↓ᵀ a Γ, where a = ⟦ t ⟧ ↑ΓTo prove this, we will establish a logical relation Γ ⊢ t : T Ⓡ a between a
well-typed term Γ ⊢ t : T and a semantic object in our meta language
a ∈ ⟦ T ⟧ such that it implies Γ ⊢ t = ↓ᵀ a Γ : T. Later, we will prove that
Γ ⊢ t : T Ⓡ ⟦ t ⟧ ↑Γ (which will then finish our proof), but we will focus on
the logical relation itself for now.
For defining the relation in Agda, we will need to first define another relation
that “lifts” definitional equality to include liftable neutrals. If the liftable
neutral can be lifted to the context Γ, this is just definitional equality.
Otherwise, the relation can never hold, as there is no lifted term in the
context to compare to.
_==^_ : {Γ : Ctx} {T : Type} → Γ ⊢ T → Ne^ T → Set
_==^_ {Γ} t 𝓊̂ with 𝓊̂ Γ
... | inj₁ ⟨ 𝓊 , _ ⟩ = t == 𝓊
... | inj₂ _ = ⊥
Formally, this relation represents the condition Γ ⊢ 𝓊 = 𝓊̂(Γ) : T, meaning
that a term 𝓊 is definitionally equal to the liftable neutral 𝓊̂ lifted to
the context Γ.
We also need to define a relation lifting definitional equality to the unit type with embedded liftable neutrals. If the expression is unit, then this is just regular definitional equality, and otherwise we reuse definitional equality for liftable neutrals.
_==⊤̂_ : ∀ {Γ : Ctx} → Γ ⊢ 𝟙 → ⟦ 𝟙 ⟧ → Set
_==⊤̂_ {Γ} t unit = t == unit
_==⊤̂_ {Γ} t (ne 𝓊̂) = t ==^ 𝓊̂
This will represent the condition Γ ⊢ t = 𝓋̂(Γ) : 𝟙 that we will now see, as we
are ready to begin defining the logical relation Γ ⊢ t : T Ⓡ a inductively on
types. At type 𝟙, the relation is defined as:
Γ ⊢ t : 𝟙 Ⓡ 𝓋̂ ⇔ ∀ Γ′ ≤ Γ. Γ′ ⊢ t = 𝓋̂(Γ′) : 𝟙In other words, t is logically related to a semantic object 𝓋̂ ∈ ⊤̂ if and
only if the term is definitionally equal to 𝓋̂ when lifted to any context Γ′
that is an extension of Γ.
For function types, the relation is defined as:
Γ ⊢ r : S → T Ⓡ f ⇔ ∀ Γ′ ≤ Γ. Γ′ ⊢ s : S Ⓡ a ⇒ Γ′ ⊢ r s : T Ⓡ f(a)The relation is written so that it sort of expands functions, reducing our proof
that a functional term in STLC is logically related to a function in Agda to
only having to prove that given related arguments, the functional term and the
function in Agda both produce related results. Again, this is generalized over
all extensions of the context Γ. While our final results will only be
concerned with the context Γ, to prove these results we will need the relation
to be strengthened in this way.
_Ⓡ_ : ∀ {Γ : Ctx} {T : Type} → Γ ⊢ T → ⟦ T ⟧ → Set
_Ⓡ_ {Γ} {𝟙} t 𝓋̂ = ∀ {Γ′ : Ctx} → (Γ′≤Γ : Γ′ ≤ Γ) → Γ′≤Γ ≤⊢ t ==⊤̂ 𝓋̂
_Ⓡ_ {Γ} {S ⇒ T} r f =
∀ {Γ′ : Ctx}
→ (Γ′≤Γ : Γ′ ≤ Γ)
→ ∀ {s : Γ′ ⊢ S} {a : ⟦ S ⟧}
→ s Ⓡ a
-------------------------
→ (Γ′≤Γ ≤⊢ r) · s Ⓡ f a
As the logical relation between terms and semantic objects is defined using
definitional equality, it is transitive with respect to definitional equality.
This is the first lemma we will prove using equational reasoning for
definitional equality. As for most proofs related to the logical relation Ⓡ
between terms and semantic objects, we prove it by induction on types, and do a
case analysis at type 𝟙 on the semantic object a ∈ ⊤̂. The proof makes use of
a lemma whose proof has been omitted, cong⁼⁼-sub: if two terms are
definitionally equal , the terms with the same substitution applied are still
definitionally equal.
cong⁼⁼-sub : ∀ {Γ Δ : Ctx} {T : Type} {t t′ : Γ ⊢ T} {σ : Sub Δ Γ}
→ t == t′
→ t [ σ ] == t′ [ σ ]
==-Ⓡ-trans : ∀ {Γ : Ctx} {T : Type} {t t′ : Γ ⊢ T} {a : ⟦ T ⟧}
→ t == t′
→ t Ⓡ a
-------
→ t′ Ⓡ a
==-Ⓡ-trans {T = 𝟙} {t} {t′} {unit} t==t′ pf Γ′≤Γ =
begin==
Γ′≤Γ ≤⊢ t′
==⟨ sym⁼⁼ (cong⁼⁼-sub t==t′) ⟩
Γ′≤Γ ≤⊢ t
==⟨ pf Γ′≤Γ ⟩
unit
==∎
==-Ⓡ-trans {T = 𝟙} {t} {t′} {ne 𝓊̂} t==t′ pf {Γ′} Γ′≤Γ
with 𝓊̂ Γ′ | pf Γ′≤Γ
... | inj₁ ⟨ 𝓊 , _ ⟩ | t==𝓊 =
begin==
Γ′≤Γ ≤⊢ t′
==⟨ sym⁼⁼ (cong⁼⁼-sub t==t′) ⟩
Γ′≤Γ ≤⊢ t
==⟨ t==𝓊 ⟩
𝓊
==∎
==-Ⓡ-trans {T = S ⇒ T} {r} {r′} r==r′ pf Γ′≤Γ sⓇa =
==-Ⓡ-trans r·s==r′·s r·sⓇfa
where
r·s==r′·s = app-compatible (cong⁼⁼-sub r==r′) refl⁼⁼
r·sⓇfa = pf Γ′≤Γ sⓇa
Additionally, because we have defined the relation so that its implication holds
for all extensions of a context, we can “weaken” the logical relation
Γ ⊢ t : T Ⓡ a for all Γ′ ≤ Γ, having that Γ′ ⊢ t : T Ⓡ a holds as well.
For this proof, we use another lemma whose proof has also been omitted,
compose-weaken: weakening a term t twice is equivalent to weakening it once
with a composed weakening substitution.
compose-weaken : ∀ {Γ″ Γ′ Γ : Ctx} {T : Type}
→ (Γ″≤Γ′ : Γ″ ≤ Γ′)
→ (Γ′≤Γ : Γ′ ≤ Γ)
→ (t : Γ ⊢ T)
→ Γ″≤Γ′ ≤⊢ Γ′≤Γ ≤⊢ t ≡ (≤-trans Γ″≤Γ′ Γ′≤Γ) ≤⊢ t
Ⓡ-weaken : ∀ {Γ′ Γ : Ctx} {T : Type} {Γ′≤Γ : Γ′ ≤ Γ} {t : Γ ⊢ T}
{a : ⟦ T ⟧}
→ t Ⓡ a
→ Γ′≤Γ ≤⊢ t Ⓡ a
Ⓡ-weaken {T = 𝟙} {Γ′≤Γ} {t} pf Γ″≤Γ′
rewrite compose-weaken Γ″≤Γ′ Γ′≤Γ t = pf (≤-trans Γ″≤Γ′ Γ′≤Γ)
Ⓡ-weaken {T = S ⇒ T} {Γ′≤Γ} {t} pf Γ″≤Γ′ sⓇa
rewrite compose-weaken Γ″≤Γ′ Γ′≤Γ t = pf (≤-trans Γ″≤Γ′ Γ′≤Γ) sⓇa
The logical relation between terms and semantic objects is “sandwiched” between reflection and reification – to arrive at a logical relation between a term and a semantic object, the semantic object must be a reflection of a liftable neutral that is definitionally equal to the term. Likewise, if a logical relation holds between a term and a semantic object, then the term must be definitionally equal to the reification of that semantic object.
This is intentional, as these results will be exactly what we will need to prove the soundness of normalization by evaluation. We formalize them with the following lemmas, which we will prove mutually (as reflection and reification are themselves defined mutually) by induction on types.
The first lemma is that if the liftable variable 𝓊̂ is definitionally equal
to a term 𝓊 for all contexts Γ′ ≤ Γ, then 𝓊 is logically related to the
reflection of 𝓊̂:
(∀ Γ′ ≤ Γ. Γ′ ⊢ 𝓊 = 𝓊̂(Γ′) : T) ⇒ Γ ⊢ 𝓊 : T Ⓡ ↑ᵀ 𝓊̂==^→Ⓡ↑ : ∀ {Γ : Ctx} {T : Type} {𝓊 : Γ ⊢ T} {𝓊̂ : Ne^ T}
→ (∀ {Γ′ : Ctx}
→ (Γ′≤Γ : Γ′ ≤ Γ)
→ Γ′≤Γ ≤⊢ 𝓊 ==^ 𝓊̂)
-------------------
→ 𝓊 Ⓡ (↑ᵀ 𝓊̂)
An immediate consequence of this lemma is that Γ , x:T ⊢ x Ⓡ ↑ᵀ 𝓍̂ Γ, which we
can define in Agda now as it will be necessary for proving the next lemma we
will introduce.
xⓇ↑ᵀ𝓍̂ : ∀ {Γ : Ctx} {T : Type}
-------------------------
→ # 𝑍 {Γ} {T} Ⓡ ↑ᵀ (𝓍̂ T Γ)
The second lemma is that if Γ ⊢ t : T and a ∈ ⟦ T ⟧ are logically related,
then t is definitionally equal to the reification of a for all contexts
Γ′ ≤ Γ:
Γ ⊢ t : T Ⓡ a ⇒ ∀ Γ′ ≤ Γ. Γ′ ⊢ t = ↓ᵀ a Γ′ : TⓇ→==↓ : ∀ {Γ′ Γ : Ctx} {T : Type} {t : Γ ⊢ T} {a : ⟦ T ⟧}
→ t Ⓡ a
----------------------------
→ (Γ′≤Γ : Γ′ ≤ Γ)
→ Γ′≤Γ ≤⊢ t == proj₁ (↓ᵀ a Γ′)
This lemma is in fact what we wanted in the first place: that if a term is logically related to a semantic object, then it is definitionally equal to the reification of said object. It is stronger than we need it to be, but again this is necessary to actually prove the implication.
We will start by proving the first lemma, focusing on each case of the proof separately, before moving on to proving the second lemma. Again, the first lemma is:
(∀ Γ′ ≤ Γ. Γ′ ⊢ 𝓊 = 𝓊̂(Γ) : T) ⇒ Γ ⊢ 𝓊 : T Ⓡ ↑ᵀ 𝓊̂We prove this by induction on the type T. At type 𝟙, our proof is
immediate, as Γ ⊢ u : 𝟙 Ⓡ ↑ᵘⁿⁱᵗ 𝓊̂ is defined as:
∀ Γ′ ≤ Γ. Γ′ ⊢ 𝓊 = 𝓊̂(Γ) : 𝟙Which is exactly our given proof.
==^→Ⓡ↑ {T = 𝟙} pf Γ′≤Γ = pf Γ′≤Γ
At type S → T, the proof is more complicated. We want to prove that:
(∀ Γ′ ≤ Γ. Γ′ ⊢ 𝓊 = 𝓊̂(Γ) : S → T) ⇒ Γ ⊢ 𝓊 : S → T Ⓡ ↑ˢ ⃕ ᵗ 𝓊̂By definition of Ⓡ, this expands to:
(∀ Γ′ ≤ Γ. Γ′ ⊢ 𝓊 = 𝓊̂(Γ) : S → T) ⇒
∀ Γ′ ≤ Γ. Γ′ ⊢ s Ⓡ a ⇒
Γ′ ⊢ 𝓊 s Ⓡ (↑ˢ ⃕ ᵗ 𝓊̂) aThis simplifies further by the definition of reflection:
(∀ Γ′ ≤ Γ. Γ′ ⊢ 𝓊 = 𝓊̂(Γ) : S → T) ⇒
∀ Γ′ ≤ Γ. Γ′ ⊢ s Ⓡ a ⇒
Γ′ ⊢ 𝓊 s Ⓡ ↑ᵀ (𝓊̂ · ↓ˢ a)Our induction hypothesis gives us that at type T, the following holds:
(∀ Γ″ ≤ Γ′. Γ″ ⊢ 𝓊 s = (𝓊̂ · ↓ˢ a) Γ″) ⇒
Γ′ ⊢ 𝓊 s Ⓡ ↑ᵀ (𝓊̂ · ↓ˢ a)With our induction hypothesis, our new goal is to prove only that:
∀ Γ″ ≤ Γ′. Γ″ ⊢ 𝓊 s = (𝓊̂ · (↓ˢ a)) Γ″ : TNote that (𝓊̂ · (↓ˢ a)) Γ″ is equivalent to 𝓊̂(Γ″) · (↓ˢ a)(Γ″) (application
of liftable neutrals is overloaded), so the final form of the property we have
to prove is:
Γ″ ⊢ 𝓊 s = 𝓊̂(Γ″) · ↓ˢ a Γ″ : TUsing the definitional equality rule of compatibility for application, we need only prove that:
Γ″ ⊢ 𝓊 = 𝓊̂(Γ″) : S → T
Γ″ ⊢ s = ↓ˢ a Γ″ : SThe first property is our given evidence. We can use our other given proof (that
Γ′ ⊢ s : S Ⓡ a) with the the second lemma we will be proving to prove the
second property:
Γ′ ⊢ s : T Ⓡ a ⇒ ∀ Γ″ ≤ Γ′. Γ″ ⊢ s = ↓ᵀ a Γ″ : T==^→Ⓡ↑ {T = _ ⇒ _} {𝓊} {𝓊̂} pf {Γ′} Γ′≤Γ {s} {a} sⓇa =
==^→Ⓡ↑ 𝓊·s==𝓊̂·↓ˢa
where
𝓊·s==𝓊̂·↓ˢa : ∀ {Γ″ : Ctx}
→ (Γ″≤Γ′ : Γ″ ≤ Γ′)
→ Γ″≤Γ′ ≤⊢ (Γ′≤Γ ≤⊢ 𝓊) · s ==^ 𝓊̂ ·^ (↓ᵀ a)
𝓊·s==𝓊̂·↓ˢa {Γ″} Γ″≤Γ′
with 𝓊̂ Γ″ | pf (≤-trans Γ″≤Γ′ Γ′≤Γ)
... | inj₁ ⟨ 𝓊″ , _ ⟩ | 𝓊==𝓊″ =
begin==
Γ″≤Γ′ ≤⊢ (Γ′≤Γ ≤⊢ 𝓊) · s
==⟨ app-compatible (≡→== compose-weaken-𝓊) refl⁼⁼ ⟩
(Γ″≤Γ ≤⊢ 𝓊) · (Γ″≤Γ′ ≤⊢ s)
==⟨ app-compatible 𝓊==𝓊″ refl⁼⁼ ⟩
𝓊″ · (Γ″≤Γ′ ≤⊢ s)
==⟨ app-compatible refl⁼⁼ s==↓ᵀaΓ″ ⟩
𝓊″ · proj₁ (↓ᵀ a Γ″)
==∎
where
compose-weaken-𝓊 = compose-weaken Γ″≤Γ′ Γ′≤Γ 𝓊
s==↓ᵀaΓ″ = Ⓡ→==↓ sⓇa Γ″≤Γ′
Γ″≤Γ = ≤-trans Γ″≤Γ′ Γ′≤Γ
This brings us to our second lemma:
Γ ⊢ t : T Ⓡ a ⇒ ∀ Γ′ ≤ Γ. Γ′ ⊢ t = ↓ᵀ a Γ′ : TIt will similarly be proven by induction on the type T. First, let us prove
the lemma for the type 𝟙. At type 𝟙, our lemma simplifies (by definition
of Ⓡ) to:
(∀ Γ′ ≤ Γ. Γ′ ⊢ t : T = a (Γ′)) ⇒ ∀ Γ′ ≤ Γ. Γ′ ⊢ t = ↓ᵘⁿⁱᵗ a Γ′ : TWe can break this down further into a case analysis on a, which can be either
unit or an embedded liftable neutral 𝓊̂. In both cases, we can use our given
proof.
Ⓡ→==↓ {T = 𝟙} {a = unit} pf with ↓ᵀ {𝟙} unit
... | _ = pf
Ⓡ→==↓ {Γ′} {T = 𝟙} {a = ne 𝓊̂} pf Γ′≤Γ
with 𝓊̂ Γ′ | pf Γ′≤Γ
... | inj₁ ⟨ 𝓊 , _ ⟩ | t==𝓊 = t==𝓊
For the case where we are at a function type S → T, our lemma now simplifies
to:
(∀ Γ′ ≤ Γ. Γ′ ⊢ x : S Ⓡ a ⇒ Γ′ ⊢ t x : T Ⓡ f a) ⇒
∀ Γ′ ≤ Γ. Γ′ ⊢ t = ↓ˢ ⃕ ᵗ f Γ′ : S → TWe can once again expand out the definition of reification at type S → T,
simplifying the lemma to:
(∀ Γ′ ≤ Γ. Γ′ ⊢ x : S Ⓡ a ⇒ Γ′ ⊢ t x : T Ⓡ f a) ⇒
Γ′ ⊢ t = λx. ↓ᵀ f a (Γ′, x:S) : T , where a = ↑ˢ (𝓍̂ S Γ′)We prove this by η-expanding t to λx. t x and then using the compatibility
rule for abstractions to simplify our goal to proving:
Γ′, x:S ⊢ t x = λx. ↓ᵀ f a (Γ′, x:S) : TOur inductive hypothesis gives us that:
∀ Γ″ ≤ Γ′. Γ″ ⊢ t x = ↓ᵀ f a : TWith it, all we need to prove is:
Γ′ , x : S ⊢ t x : T Ⓡ f aOur given proof further simplifies this goal to simply proving that
∀ Γ″ ≤ Γ′, x:S. Γ″ ⊢ x : S Ⓡ a. We have been using a for simplicity,
but again, a = ↑ˢ (𝓍̂ S Γ′). Earlier, we established a lemma xⓇ↑ᵀ𝓍̂ giving us
exactly this goal, so we use it here to finish our proof.
Ⓡ→==↓ {Γ′} {T = S ⇒ _} {t} {f} pf Γ′≤Γ =
begin==
Γ′≤Γ ≤⊢ t
==⟨ η ⟩
ƛ (S ↥⊢ Γ′≤Γ ≤⊢ t) · # 𝑍
==⟨
abs-compatible (
begin==
(S ↥⊢ Γ′≤Γ ≤⊢ t) · # 𝑍
==⟨ app-compatible subst-lemma refl⁼⁼ ⟩
(≤-ext Γ′≤Γ ≤⊢ t) [ id ] · # 𝑍
==⟨ Ⓡ→==↓ (pf (≤-ext Γ′≤Γ) xⓇa) ≤-id ⟩
proj₁ (↓ᵀ (f a) (Γ′ , S))
==∎
)⟩
proj₁ (↓ᵀ f Γ′)
==∎
where
a = ↑ᵀ {S} (𝓍̂ S Γ′)
xⓇa = xⓇ↑ᵀ𝓍̂ {Γ′} {S}
subst-lemma =
≡→== (trans
(sub-sub {τ = ↥} {weaken Γ′≤Γ} {t})
(sym [id]-identity))
Lastly, we can quickly derive the lemma Γ, x:T ⊢ x : T Ⓡ ↑ᵀ 𝓍̂ Γ as a special
case of (∀ Γ′ ≤ Γ. Γ′ ⊢ 𝓊 = 𝓊̂(Γ′) : T) ⇒ Γ ⊢ 𝓊 Ⓡ ↑ᵀ 𝓊̂. The proof requires an
additional lemma with its proof ommitted, ≤-pf-irrelevance: any proof of
context extension is equivalent.
≤-pf-irrelevance : ∀ {Γ′ Γ : Ctx}
→ (pf₁ : Γ′ ≤ Γ)
→ (pf₂ : Γ′ ≤ Γ)
→ pf₁ ≡ pf₂
xⓇ↑ᵀ𝓍̂ {_} {T} = ==^→Ⓡ↑ x==𝓍̂ where
x==𝓍̂ : ∀ {Γ Γ′ : Ctx}
→ (Γ′≤Γ,T : Γ′ ≤ Γ , T)
→ Γ′≤Γ,T ≤⊢ # 𝑍 ==^ 𝓍̂ T Γ
x==𝓍̂ {Γ} {Γ′} pf
with Γ′ ≤? (Γ , T)
... | no ¬pf = ¬pf pf
... | yes pf′
with 𝓍̂ T Γ | ≤-pf-irrelevance pf pf′
... | _ | refl
with ρ-≤ pf′ 𝑍
...| _ = refl⁼⁼
Let’s focus on one of the lemmas we have proven:
Γ ⊢ t : T Ⓡ a ⇒ ∀ Γ′ ≤ Γ. Γ′ ⊢ t = ↓ᵀ a Γ : TWe have defined our logical relation with the goal of having the following case of this property:
Γ ⊢ t : T Ⓡ a ⇒ Γ ⊢ t = ↓ᵀ a Γ : TWe now need to show that:
Γ ⊢ t : T Ⓡ ⟦t⟧ ↑ΓWith this, we can arrive at the definitional equality of a term and its normal form as obtained from our algorithm for normalization by evaluation:
Γ ⊢ t = ↓ᵀ (⟦t⟧ ↑Γ) Γ : TTo prove Γ ⊢ t : T Ⓡ ⟦t⟧ ↑Γ, we will need to extend our logical relation to
include substitutions and environments.
A parallel substitution Γ ⊢ σ : Δ will be logically related to an environment
δ ∈ ⟦ Δ ⟧ if every term that the substitution σ is substituting for the
context Δ is logically related to the corresponding semantic object in the
environment δ. In Agda, we will use Ⓡˢ as Ⓡ is already reserved for terms
and semantic objects, though we will refer to the relation as Γ ⊢ σ : Δ Ⓡ δ.
_Ⓡˢ_ : ∀ {Γ Δ : Ctx} → Sub Γ Δ → ⟦ Δ ⟧ → Set
_Ⓡˢ_ {Δ = Δ} σ δ =
∀ {T : Type} → (x : Δ ∋ T) → σ x Ⓡ env-lookup x δ
Similarly as for the logical relation between terms and semantic objects, if a
logical relation holds between a substitution and an environment, it holds for
any weakening of the substitution. The proof is immediate using Ⓡ-weaken.
Ⓡˢ-weaken : ∀ {Γ′ Γ Δ : Ctx} {Γ′≤Γ : Γ′ ≤ Γ} {σ : Sub Γ Δ}
{δ : ⟦ Δ ⟧}
→ σ Ⓡˢ δ
→ σ ∘ (weaken Γ′≤Γ) Ⓡˢ δ
Ⓡˢ-weaken {Γ′≤Γ = Γ′≤Γ} σⓇδ x = Ⓡ-weaken {Γ′≤Γ = Γ′≤Γ} (σⓇδ x)
With the logical relation extended to substitutions and environments, we can
introduce the semantic typing judgement Δ ⊨ t : T: for any substitution
Γ ⊢ σ : Δ that is logically related to an environment δ ∈ ⟦ Δ ⟧,
Γ ⊢ t[σ] : T must be logically related to ⟦ t ⟧ δ. Using the semantic typing
judgement, we will be able to derive that Γ ⊢ t Ⓡ ⟦ t ⟧ ↑Γ.
_⊨_ : ∀ {T : Type} → (Δ : Ctx) → Δ ⊢ T → Set
_⊨_ {T} Δ t =
∀ {Γ : Ctx} {σ : Sub Γ Δ} {δ : ⟦ Δ ⟧}
→ σ Ⓡˢ δ
-------
→ t [ σ ] Ⓡ ⟦⊢ t ⟧ δ
We can prove the semantic typing judgement Δ ⊨ t : T by induction on the
typing judgement Δ ⊢ t : T; this is called the fundamental lemma of logical
relations.
For unit, the proof follows immediately from how we have defined the logical
relation between terms and semantic objects at type 𝟙. In the case of
variables, the given proof is exactly what we need. Application follows from our
inductive hypotheses, leaving us at the abstraction case, which is the most
complicated to prove. Here are the first three cases:
fundamental-lemma : ∀ {Δ : Ctx} {T : Type} {t : Δ ⊢ T}
→ Δ ⊨ t
fundamental-lemma {t = unit} σⓇδ _ = refl⁼⁼
fundamental-lemma {t = # x} σⓇδ = σⓇδ x
fundamental-lemma {t = r · s} {σ = σ} σⓇδ
with fundamental-lemma {t = r} σⓇδ
... | Γ⊨r
with fundamental-lemma {t = s} σⓇδ
... | Γ⊨s
with Γ⊨r ≤-id Γ⊨s
... | pf
rewrite [id]-identity {t = r [ σ ]} = pf
In the case of an abstraction Γ ⊢ λx. t : S → T, we want to prove:
Γ ⊢ σ : Δ Ⓡ δ ⇒
Γ ⊢ (λx. t)[σ] : S → T Ⓡ ⟦ Γ ⊢ λx. t : S → T ⟧ δBy the definition of the application of a substitution to an abstraction, as well as the definition of evaluation of an abstraction, this simplifies to:
Γ ⊢ σ : Δ Ⓡ δ ⇒
Γ ⊢ λx. t[exts σ] : S → T Ⓡ f
where f = λ a → ⟦ Γ, x:S ⊢ t : T ⟧ (δ , a)We can also expand this using the definition of Ⓡ for functions (and
immediately reducing the application of f to a):
Γ ⊢ σ : Δ Ⓡ δ ⇒
∀ Γ′ ≤ Γ. Γ′ ⊢ s : S Ⓡ a ⇒
Γ′ ⊢ (λx. t[exts σ]) · s : T Ⓡ ⟦ Γ, x:S ⊢ t : T ⟧ (δ , a)Already, this is a tricky property to parse. To start, we can use our lemma
that Ⓡ is transitive with respect to definitional equality, and use the β
rule to reduce (λx. t[exts σ]) · s to t[exts σ][s/x]. Now, we need only
prove:
Γ′ ⊢ t[exts σ][s/x] : T Ⓡ ⟦ Γ, x:S ⊢ t : T ⟧ (δ , a)Here, we can use a few substitution lemma to compose these two substitutions and
reduce them into just σ ∷ s, giving us:
Γ′ ⊢ t [σ ∷ s] : T Ⓡ ⟦ Γ, x:S ⊢ t : T ⟧ (δ , a)The property we want to show now looks like our induction hypothesis! Using the induction hypothesis, we only need to show that:
Γ′ ⊢ σ ∷ s : (Δ, x:S) Ⓡ (δ , a)In other words, we need to prove that for any variable x in the context
Δ, x:S that σ is substituting a term for, the term being substituted for
that variable must be logically related to its corresponding semantic object in
the environment (δ , a). We can do a case analysis on x to break this down
further. The first case is what the relation simplifies to in the case that the
variable being substituted for is 𝑍 ─ all that needs to be proven is that the
term being substituted for the first variable in Δ, x:S (which is s) is
logically related to the first semantic object in (δ , a). In other words,
for this case, what needs to be proven is:
Γ′ ⊢ s : S Ⓡ aThis is already our given proof, so this case follows immediately. The second
case is what the relation simplifies to in the case that the variable being
substituted for is in Δ, meaning x is 𝑆 x:
Γ′ ⊢ (σ ∷ s) (𝑆 x) : U Ⓡ env-lookup x δHere, we need to use a few substitution lemmas (which have been omitted as their proofs are unrelated to the logical relation itself) to rewrite this to:
Γ′ ⊢ σ x : U Ⓡ env-lookup x δThis is again already given to us from our given proof that Γ ⊢ σ : Δ Ⓡ δ.
There is one small problem: we are now considering the context Γ′ while our
given proof is over the context Γ. There was, in fact, an implict weakening
of σ in the changing of contexts (and it would be more correct to have been
writing σ ∘ weaken Γ′≤Γ throughout, though the explanation used σ for
simplicity). Here, we can use the earlier lemma that if a substitution is
logically related to an environment, then so is a weakening of the substitution.
With that, the abstraction case is proven.
In Agda, we require some substitution lemmas (both for the conversion of
t[exts σ][s/x] to t[σ ∷ s] and to handle the implcit weakening) which have
been omitted (and for convenience, we use the variables t[exts-σ] and σ∷s,
whose definitions are also omitted).
fundamental-lemma {Δ} {S ⇒ T} {ƛ t} {σ = σ} {δ} σⓇδ {Γ′} Γ′≤Γ {s}
{a} sⓇa =
==-Ⓡ-trans (sym⁼⁼ β) t[exts-σ][s/x]Ⓡ⟦t⟧⟨δ,a⟩
where
t[exts-σ] : Γ′ , S ⊢ T
σ∷s : Sub Γ′ (Δ , S)
σ∷sⓇ⟨δ,a⟩ : σ∷s Ⓡˢ ⟨ δ , a ⟩
σ∷sⓇ⟨δ,a⟩ 𝑍 = sⓇa
σ∷sⓇ⟨δ,a⟩ (𝑆_ {T = U} x) rewrite subst-lemma₁ {x = x} =
Ⓡˢ-weaken {Γ′≤Γ = Γ′≤Γ} σⓇδ x
t[exts-σ][s/x]Ⓡ⟦t⟧⟨δ,a⟩ : t[exts-σ] [ s ]₀ Ⓡ ⟦⊢ t ⟧ ⟨ δ , a ⟩
t[exts-σ][s/x]Ⓡ⟦t⟧⟨δ,a⟩ rewrite subst-lemma₂ | subst-lemma₃ =
fundamental-lemma {t = t} σ∷sⓇ⟨δ,a⟩
Separately, we have that the identity substitution is logically related to
our environment of reflected variables, Γ ⊢ id : Γ Ⓡ ↑Γ. We prove this by
induction on the variable being substituted for, using the lemma that
Γ, x:T ⊢ x : T Ⓡ ↑ᵀ 𝓍̂ Γ for the base case. For the inductive step, there is a
need to weaken the inductive hypothesis (which gives us that
Γ ⊢ y : T Ⓡ ↑ᵀ 𝓍̂ Γ) to the context Γ, x:S.
idⓇ↑Γ : ∀ {Γ : Ctx}
→ id Ⓡˢ (↑ᶜᵗˣ Γ)
idⓇ↑Γ 𝑍 = xⓇ↑ᵀ𝓍̂
idⓇ↑Γ {Γ , T} (𝑆 x) =
Ⓡ-weaken {Γ′≤Γ = ≤-ext ≤-id} {t = # x} (idⓇ↑Γ {Γ} x)
Now, we can arrive at the soundness of our algorithm for normalization by
evaluation. We have Γ ⊢ id : Γ Ⓡ ↑Γ, so we can use the fundamental lemma
here:
Γ ⊢ t [ id ] Ⓡ ⟦ t ⟧ ↑ΓNote also that t [ id ] ≡ t. Using the lemma that a logical relation between a
term and a semantic object implies the definitional equality of the term to the
reification of the semantic object, we have:
Γ ⊢ t = ↓ᵀ (⟦ t ⟧ ↑Γ) Γ : TThus, our algorithm for normalization by evaluation preserves the meaning of a term that it normalizes. By extension, the algorithm is also idempotent (as we have already shown it is complete), so the algorithm as a whole satisifies the soundness properties we wanted (as a reminder, the well-typedness of the algorithm is given automatically with our intrinsically typed representation).
nf-== : ∀ {Γ : Ctx} {T : Type} {t : Γ ⊢ T}
→ t == nf t
nf-== {Γ} {T} {t}
with fundamental-lemma {t = t} (idⓇ↑Γ {Γ})
... | tⓇ⟦t⟧↑Γ
with Ⓡ→==↓ tⓇ⟦t⟧↑Γ ≤-id
... | t==↓ᵀ⟦t⟧↑Γ
rewrite [id]-identity {t = t [ id ]}
| [id]-identity {t = t} = t==↓ᵀ⟦t⟧↑Γ
nf-preserves-meaning : ∀ {Γ : Ctx} {T : Type} {t : Γ ⊢ T} {γ : ⟦ Γ ⟧}
→ ⟦⊢ t ⟧ γ ≡ ⟦⊢ nf t ⟧ γ
nf-preserves-meaning {t = t} = ==→⟦≡⟧ (nf-== {t = t})
nf-idempotent : ∀ {Γ : Ctx} {T : Type} {t : Γ ⊢ T}
→ nf t ≡ nf (nf t)
nf-idempotent {t = t} = completeness (nf-== {t = t})
soundness : ∀ {Γ : Ctx} {T : Type} {t : Γ ⊢ T} {γ : ⟦ Γ ⟧ }
→ (⟦⊢ t ⟧ γ ≡ ⟦⊢ nf t ⟧ γ) × (nf t ≡ nf (nf t))
soundness {t = t} =
⟨ nf-preserves-meaning {t = t} , nf-idempotent {t = t} ⟩
Conclusion
In the end, we have formalized an algorithm in Agda for normalization by evaluation that is based on the intuition of leaving the parts of a term that cannot be evaluated (i.e. “unknowns”) unchanged while still evaluating the parts of the term that we do know how to reduce. The algorithm is both complete and sound with respect to definitional equality, as we have proven. Completeness followed quickly from the definition of the algorithm, while soundness required a more in-depth proof involving the use of logical relations and their fundamental lemma.
In his habilitation thesis, Andreas Abel goes on to introduce the algorithm for the untyped lambda calculus after introducing normalization by evaluation for System T (an extension of the simply typed lambda calculus with primitive recursion). He continues to build upon these concepts, arriving at an algorithm for a language with dependent types and a language with impredicativity. This introduction to normalization to evaluation should hopefully be a good starting point to explore these and other extensions of the algorithm, such as simply trying out these proofs for yourself with a different extension of the simply typed lambda calculus, or implementing the algorithm in a language other than Agda.
Unicode
This site uses the following unicode in its Agda source code1:
λ U+03BB GREEK SMALL LETTER LAMBDA (\Gl)
⊥ U+22A5 UP TACK (\bot)
⊤ U+22A4 DOWN TACK (\top)
⊎ U+228E MULTISET UNION (\u+)
₁ U+2081 SUBSCRIPT ONE (\_1)
₂ U+2082 SUBSCRIPT TWO (\_2)
× U+00D7 MULTIPLICATION SIGN (\x)
∃ U+2203 THERE EXISTS (\ex)
⟨ U+27E8 MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩ U+27E9 MATHEMATICAL RIGHT ANGLE BRACKET (\>)
¬ U+00AC NOT SIGN (\neg)
≡ U+2261 IDENTICAL TO (\==)
⇒ U+21D2 RIGHTWARDS DOUBLE ARROW (\=>)
∀ U+2200 FOR ALL (\all)
→ U+2192 RIGHTWARDS ARROW
≟ U+225F QUESTIONED EQUAL TO (\?=)
∅ U+2205 EMPTY SET (\0)
∋ U+220B CONTAINS AS MEMBER (\ni)
𝑍 U+1D44D MATHEMATICAL ITALIC CAPITAL Z (\MiZ)
Γ U+0393 GREEK CAPITAL LETTER GAMMA (\GG)
𝑆 U+1D446 MATHEMATICAL ITALIC CAPITAL S (\MiS)
≤ U+2264 LESS-THAN OR EQUAL TO (\le)
′ U+2032 PRIME (\'1)
≢ U+2262 NOT IDENTICAL TO (\==n)
⊢ U+22A2 RIGHT TACK (\|-)
ƛ U+019B LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-)
· U+00B7 MIDDLE DOT (\cdot)
σ U+03C3 GREEK SMALL LETTER SIGMA (\Gs)
Δ U+0394 GREEK CAPITAL LETTER DELTA (\GD)
ʳ U+02B3 MODIFIER LETTER SMALL R (\^r4)
↥ U+21A5 UPWARDS ARROW FROM BAR (\u-|)
Σ U+03A3 GREE CAPITAL LETTER SIGMA (\GS)
∘ U+2218 RING OPERATOR (\o)
ω U+03C9 GREEK SMALL LETTER OMEGA (\Go)
∷ U+2237 PROPORTION (\::)
θ U+03B8 GREEK SMALL LETTER THETA (\Gth)
Φ U+03A6 GREEK CAPITAL LETTER PHI (\Gf)
⟦ U+27E6 MATHEMATICAL LEFT WHITE SQUARE BRACKET (\[[)
⟦ U+27E7 MATHEMATICAL RIGHT WHITE SQUARE BRACKET (\]])
β U+03B2 GREEK SMALL LETTER BETA (\Gb)
η U+03B7 GREEK SMALL LETTER ETA (\Gh)
∎ U+220E END OF PROOF (\qed)
⦃ U+2983 LEFT WHITE CURLY BRACKET (\{{)
⦄ U+2984 RIGHT WHITE CURLY BRACKET (\}})
𝓊 U+1D4CA MATHEMATICAL SCRIPT SMALL U (\Mcu)
𝓋 U+1D4CB MATHEMATICAL SCRIPT SMALL V (\Mcv)
γ U+03B3 GREEK SMALL LETTER GAMMA (\Gg)
↑ U+2191 UPWARDS ARROW (\u)
ᵀ U+1D40 MODIFIER LETTER CAPITAL T (\^T)
↓ U+2193 DOWNWARDS ARROW (\d)
ᶜ U+1D9C MODIFIER LETTER SMALL C (\^c)
ᵗ U+1D57 MODIFIER LETTER SMALL T (\^t)
ˣ U+02E3 MODIFIER LETTER SMALL X (\^x)
̂ U+0302 COMBINING CIRCUMFLEX ACCENT (\^)
𝓍 U+1D4CD MATHEMATICAL SCRIPT SMALL X (\Mcx)
≰ U+2270 NEITHER LESS THAN NOR EQUAL TO (\len)
₃ U+2083 SUBSCRIPT 3 (\_3)
Ⓡ U+24C7 CIRCLED LATIN CAPITAL LETTER R (\(r)2)
″ U+2033 DOUBLE PRIME (\'2)
δ U+03B4 GREEK SMALL LETTER DELTA (\Gd)̂ (
\^) may be displayed on top of another character when written after it (e.g.\Mcu\^produces 𝓊̂)↩︎