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” (Abel 2013). 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.
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. x`This 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.
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.
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
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 [ σ ∘ τ ]
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 of t, 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⁼⁼
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 ⟧
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
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 : T is difficult, and we will have to use a
logical relation to prove it in the following section
nf(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 imply
nf (nf t) = nf(t) by the algorithm’s completeness
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
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} σⓇδ | fundamental-lemma {t = s} σⓇδ
... | Γ⊨r | Γ⊨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} ⟩
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.
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 𝓊̂)↩︎