Normalization by Evaluation (NbE) Techniques and Abstract Values

Andreas Abel^{1}, Thierry Coquand^{2}, Ulf Norell^{2}

1Ludwig-Maximilians-University Munich 2Chalmers University of Technology

Curry-Howard Implementation Techniques 2006 December 19, 2006

Introduction

Normalization by Evaluation

Evaluate term t, obtain value v = [[t]]_{ρ} ∈ Val. Val contains the variables and neutral terms. Reify v to a normal form. Semantical type-checking is NbE, without reification.

Introduction

The Language

Set Tm of raw terms:

r, s, t, A, B, C ::= x | λxt | r s | Πx :A.B | Type

Judgements

Γ ⊢  Γ is a well-formed context
Γ ⊢ A  A is a well-formed type
Γ ⊢ t : A  t has type A

Wellformed types

\frac{Γ ⊢}{Γ ⊢ Type}  \frac{Γ ⊢ A : Type}{Γ ⊢ A}  \frac{Γ ⊢ A  Γ, x :A ⊢ B}{Γ ⊢ Πx :A. B}

Abel Coquand Norell (LMU Chalmers)  NbE and Abstract Values  CHIT’06  3 / 13

Introduction

Typing Rules

Lambda-calculus

\frac{Γ ⊢}{Γ ⊢ x : Γ(x)}  \frac{Γ, x :A ⊢ t : B}{Γ ⊢ λxt : Πx :A. B}

\frac{Γ ⊢ r : Πx :A. B Γ ⊢ s : A}{Γ ⊢ r s : B[s/x]}

Π in Type, conversion:

\frac{Γ ⊢ A : Type  Γ, x :A ⊢ B : Type}{Γ ⊢ Πx :A. B : Type}  \frac{Γ ⊢ t : A  Γ ⊢ A′}{Γ ⊢ t : A′} A =_{βη} A′

Abel Coquand Norell (LMU Chalmers)  NbE and Abstract Values  CHIT’06  4 / 13

Introduction

Evaluation, Abstractly

λ-model: D with application · and evaluation [[t]]_{ρ} Computation law for application

[[λxt]]_{ρ} · v = [[t]]_{ρ[x↦v]}

Computation laws for evaluation

\begin{aligned}[[x]]_{ρ} & = & ρ(x) \\ [[r s]]_{ρ} & = & [[r]]_{ρ} · [[s]]_{ρ} \end{aligned}

Substitution law: [[t[s/x]]]_{ρ} = [[t]]_{ρ[x↦[[s]]_{ρ}]} (Ir)relevance law: [[t]]_{ρ} = [[t]]_{ρ′} if ρ(x) = ρ′(x) for all x ∈ FV(t).

Abel Coquand Norell (LMU Chalmers)  NbE and Abstract Values  CHIT’06  5 / 13

Introduction

Values as Scott Domain

Variables and neutral objects

\frac{v_{1}, …, v_{k} ∈ Val}{x v_{1} … v_{k} ∈ Val}

Canonical objects, using functions of the Metalanguage

\frac{f ∈ Val → Val}{Lam f ∈ Val}  \frac{v ∈ Val  f ∈ Val → Val}{Pi v f ∈ Val}  \overline{Type ∈ Val}

Abel Coquand Norell (LMU Chalmers)  NbE and Abstract Values  CHIT’06  6 / 13

Introduction

Evaluation, Concretely

Application

(Lam f ) · v = f (v)
x v⃗ · v = x (v⃗, v)

Evaluation

[[x]]_{ρ} = ρ(x)
[[r s]]_{ρ} = [[r]]_{ρ} · [[s]]_{ρ}
[[λxt]]_{ρ} = Lam f  where f (d) = [[t]]_{ρ[x↦d]}
[[Πx :A. B]]_{ρ} = Pi [[A]]_{ρ} g where g(d) = [[B]]_{ρ[x↦d]}
[[Type]]_{ρ} = Type

[[t]] := [[t]]_{ρ_{0}} with ρ_{0}(x) = x.

Abel Coquand Norell (LMU Chalmers)  NbE and Abstract Values  CHIT’06  7 / 13

Semantical Type-Checking

Bidirectional. Use evaluation instead of rewriting. Subject (context Δ, type V ) is evaluated. Object (term) is raw. Each object is checked before evaluation. Only evaluation creates values. All other operations just take values apart.

Introduction

Type Checking Rules

Inference: Δ ⊢ t ↓ V (V is output).

\overline{Δ ⊢ x ↓ Δ(x)} \frac{Δ ⊢ r ↓ Pi V F Δ ⊢ s ↑ V}{Δ ⊢ r s ↓ F · [[s]]}

Checking: Δ ⊢ t ↑ V (only inputs).

\frac{Δ ⊢ t ↓ V Δ ⊢ V = V′ ↑ Type}{Δ ⊢ t ↑ V′} \frac{Δ, x :V ⊢ t ↑ F · x}{Δ ⊢ λxt ↑ Pi V F}

\frac{Δ ⊢ A ↑ Type Δ, x :[[A]] ⊢ B ↑ Type}{Δ ⊢ Πx :A. B ↑ Type} Δ ⊢ Type ↑ Type

Abel Coquand Norell (LMU Chalmers)  NbE and Abstract Values  CHIT’06  9 / 13

Introduction

Bidirectional η-Equality on Semantics

Structural: Δ ⊢ v = v′ ↓ V (V is output).

\overline{Δ ⊢ x = x ↓ Δ(x)} \frac{Δ ⊢ v = v′ ↓ Pi V F Δ ⊢ w = w′ ↑ V}{Δ ⊢ v w = v′ w′ ↓ F · v}

Type-directed: Δ ⊢ v = v′ ↑ V (only inputs).

\frac{Δ ⊢ v = v′ ↓ V Δ ⊢ V = V′ ↑ Type}{Δ ⊢ v = v′ ↑ V′}

\frac{Δ, x :V ⊢ v · x = v′ · x ↑ F · x}{Δ ⊢ v = v′ ↑ Pi V F}

Δ ⊢ Type = Type ↑ Type

\frac{Δ ⊢ V = V′ ↑ Type Δ, x :V ⊢ F · x = F′ · x ↑ Type}{Δ ⊢ Pi V F = Pi V′ F′ ↑ Type}

Abel Coquand Norell (LMU Chalmers)  NbE and Abstract Values  CHIT’06  10 / 13

On Higher-Order Values

Values with embedded functions Val → Val give elegant type-checking. But scale badly to local definitions, metavariables... Survived in Agdalight for just one year.

Abstract Values

Benjamin Gregoire: compiling terms in Coq. Keep values abstract! View: u ::= x v⃗ | Lam f | Pi V F | Type. Saves clear type-checking design. Values could be implemented as closures (Coquand 1996):

v ::= x v⃗ | tρ (t ::= λxt | Πx :A. B | Type)

view (λxt)ρ  = Lam (v ↦ [[t]]_{ρ[x↦v]})
view (Πx :A. B)ρ = Pi [[A]]_{ρ} (v ↦ [[B]]_{ρ[x↦v]})
view (Type)ρ  = Type

Conclusions

Values-as-functions allow clear type-checking design. But should only be a view on the values. Closures are more flexible (initial model?).