Normalization by Evaluation for Martin-Löf Type Theory

Andreas Abel^{1}, Klaus Aehlig^{2}, Peter Dybjer^{3}

1Ludwig-Maximilians-University Munich

2University of Wales Swansea 3Chalmers University of Technology

Arbeitstreffen Bern-München 2006 December 7, 2006

Introduction

Normalization by Evaluation

Slogan: implement computation in the object language (syntax) by mapping it to computation in the meta language (semantics) For the λ-calculus: interpret object-level abstraction and application by meta-level abstraction and application Berger Schwichtenberg (LICS91): objects of the meta-language can be brought “down” to the object-language

Related Work

Martin-Löf 1975: NbE for Type Theory (weak conversion) Martin-Löf 2004: Talk on NbE (philosophical justification) Danvy et al: Type-directed partial evaluation Altenkirch Hofmann Streicher 1996: NbE for λ-free System F Berger Eberl Schwichtenberg 2003: Term rewriting for NbE Aehlig Joachimski 2004: Untyped NbE, operationally Filinski Rohde 2004: Untyped NbE, denotationally Danielsson 2006: strongly typed NbE for LF

Our Approach

Interpretation of Martin-Löf Type Theory (MLTT) in Scott Domain [D → D] ⊆ D. Each type A is mapped to a set of total elements in D Total elements can be brought down to syntax in long βη-normal form

Martin Löf Type Theory

The Language

Set Tm of raw terms:

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

Plus natural numbers and primitive recursion like in Gödel’s T Non-dependent function space A → B := Π :A. B βη-reduction: Congruence closure of

(λxt) s ⟶ t[s/x]
λx. (t x) ⟶ t  if x ∉ FV(t)

Plus computation rules for primitive recursion

Andreas Abel, Klaus Aehlig, Peter Dybjer (LMU Munich) NbE for Type Theory  ABM’06  5 / 18

Martin Löf Type Theory

Example: Functions with Variable Arity

A dependent type

T  : Nat → Set
T 0  = Nat
T (n + 1) = Nat → T n
T 3  = Nat → Nat → Nat → Nat

Summation of n + 1 natural numbers

sum′  : Πn:Nat. Nat → T n
sum′ 0 a = a : T 0
sum′ (n + 1) a x = sum′ n (a + x)  : T n
sum′ 3 0 6 7 8  = 21
Andreas Abel, Klaus Aehlig, Peter Dybjer (LMU Munich) NbE for Type Theory  ABM’06  6 / 18

Martin Löf Type Theory

Inference Rules

Judgements

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

Wellformed types

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

Andreas Abel, Klaus Aehlig, Peter Dybjer (LMU Munich) NbE for Type Theory  ABM’06  7 / 18

Martin Löf Type Theory

Inference Rules II

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 Set, conversion: \frac{Γ ⊢ A : Set Γ, x :A ⊢ B : Set}{Γ ⊢ Πx :A. B : Set} \frac{Γ ⊢ t : A Γ ⊢ A′}{Γ ⊢ t : A′} A =_{βη} A′ Plus rules for natural numbers

Andreas Abel, Klaus Aehlig, Peter Dybjer (LMU Munich) NbE for Type Theory  ABM’06  8 / 18

NbE Algorithm

Interpretation Domain

Scott domain

D = Lam [D → D] + Pi D [D → D] + Set + Ne Tm

Application

·  : [D → [D → D]]
(Lam f ) · d = f (d)
e · d = ⊥ if e is not a Lam

“Bad guy” in D is, e. g., Lam f where

f (Ne x) = Ne y
f (d)  = ⊥
Andreas Abel, Klaus Aehlig, Peter Dybjer (LMU Munich) NbE for Type Theory  ABM’06  9 / 18

NbE Algorithm

Evaluation

Let ρ ∈ Var → D an environment.

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

(D, · , [[ ]] ) is a weakly extensional λ-model t =_{β} t′ implies [[t]]_{ρ} = [[t′]]_{ρ}

NbE Algorithm

Reification and Reflection

Bringing semantic objects down to βη-long forms ↓ : [D × D → Tm]

↓^{Set} Pi a g = Πx :↓^{Set} a. ↓^{Set} g(d) where d = ↑^{a} x and x “fresh”
↓^{Set} a  = ↓^{Set} a
↓^{Pi a g} e = λx. ↓^{g(d)}(e · d) where d = ↑^{a} x and x “fresh”
↓^{c}(Ne t) = t  if c not a Pi

Embedding neutral terms x t_{1} … t_{n} into D ↑ : [D × Tm → D]

↑^{Pi a g} t = Lam f  where f (d) = ↑^{g(d)}(t (↓^{a} d))
↑^{c} t  = Ne t  if c not a Pi
Andreas Abel, Klaus Aehlig, Peter Dybjer (LMU Munich) NbE for Type Theory  ABM’06  11 / 18

NbE Algorithm

NbE Algorithm

Environment ↑Γ satisfies (↑Γ)(x) = ↑^{a} x where a = [[Γ(x)]]_{↑Γ}. A term Γ ⊢ t : A is normalized by

nbe_{Γ}^{A}t = ↓^{[[A]]_{↑Γ}}[[t]]_{↑Γ}

Completeness of NbE

Soundness and Completeness

Goal: show that nbe_{Γ}^{A}t produces a canonical form for Γ ⊢ t : A. Consequence: NbE decides βη-equality. Completeness: If Γ ⊢ t, t′ : A then

t =_{βη} t′ implies nbe_{Γ}^{A}t ≡ nbe_{Γ}^{A}t′.

Soundness: If Γ ⊢ t : A then

t =_{βη} nbe_{Γ}^{A}t

Completeness

Partial equivalence relation (PER) c = c′ ∈ Type identifies codes for semantical types c, c′ ∈ D. For c = c ∈ Type, define PER e = e′ ∈ [c]. Definition mutually: use Dybjer’s induction-recursion.

\frac{a = a′ ∈ Type g(d) = g(d′) ∈ Type for all d = d′ ∈ [a]}{Pi a g = Pi a′ g′ ∈ Type}

[Pi a g] = {(e, e′) | e · d = e′ · d′ ∈ [g(d)] for all d = d′ ∈ [a]}

PERs single out total elements. PERs are extensional (handle η).

Completeness of NbE

Completeness Proof (Sketch)

Let t, t′ : A.

t =_{βη} t′
⇓
[[t]] = [[t′]] ∈ [[[A]]]
⇓
↓^{[[A]]}[[t]] ≡ ↓^{[[A]]}[[t′]]

Generalizes to open terms.

Soundness of NbE

Soundness via Term Model

For σ ∈ Var → Tm let ⦇t⦈_{σ} denote parallel substitution. T = Tm/=_{βη}. (T, _{,}⦇ ⦈ ) is an extensional λ-model. Logical Relation R^{a} ⊆ T × [a] for a ∈ Type.

r R^{Pi a g} e ⟺ r s R^{g(d)} e · d for all s R^{a} d
r R^{c} e  ⟺ r =_{βη} ↓^{c} e

Relating models: If t : A then ⦇t⦈ R^{[[A]]} [[t]]. Consequence t =_{βη} ↓^{[[A]]}⦇t⦈.

Conclusion

NbE is sound and complete for MLTT. Draft paper available (email me). Freshness formally treated with de Bruijn indices. Kripke logical relation needed instead.

Future Work

Reification not necessary to decide A =_{βη} A′ in conversion rule. Instead of Tm ⊆ D, use a D with atoms v_{k}. Neutral v_{k} d_{1} … d_{n} in D. Justification seems harder: Kripke-PER model? Other direction: work with judgmental equality Γ ⊢ t = t′ : A.