Normalization by Evaluation for Martin-Löf Type Theory with One Universe

From PER Model to Subset Model

Andreas Abel^{1}

Institut für Informatik, Ludwig-Maximilians-Universität Oettingenstr. 67, D-80538 München

Abstract We show how to replace the PER model of the original MFPS 2007 publication by a simpler subset model without losing any results. This observation follows from the general insight that PER semantics is strongly preferable when one models judgemental (aka typed) equality, yet for untyped equality is has no advantage over subset semantics.

The paper under discussion[1] constructs a model of type theory over an untyped λ-model D, by constructing a partial equivalence relation (PER) Type ⊆ D×D which identifies the type values in D, plus for each a ∈ Type an associated PER [a] ⊆ D×D which identifies the values of type a in D. Equal types a = a′ ∈ Type have equal extensions [a] = [a′]. The purpose of a PER semantics is to model extensional equality on values, and it defines f = f′ ∈ [Pi a g] iff f · d = f′ · d′ ∈ [g(d)] for all d = d′ ∈ [a]. However, we have already treated η-equality in the term model D; in Lemma 3.4 we show that t ⟶_{βη} t′ implies [[t]]_{ρ} ⊑ [[t′]]_{ρ} (in particular [[λfλx. f x]] ⊑ [[λf. f]]). Also, since we are constructing an open model where Nat is inhabited by the neutrals in addition to the numerals, extensionality does not mean more than η-equality.

We can therefore replace the PER model by a simpler subset model. By induction-recursion we define a subset Type ⊆ D and for each a ∈ Type a subset [a] ⊆ D. Type and types are upward closed, and improving the definedness of a type does not change its extension. Thus, if a ∈ Type then a ⊑ a′ implies a′ ∈ Type and [a] = [a′], and d ∈ [a] and d ⊑ d′ imply d′ ∈ [a]. Improvement does not change the normal form, so ⇓ a ≡ ⇓ a′ and ↓^{a} d ≡ ↓^{a′} d′.

1 Email: abel@tcs.ifi.lmu.de

Abel

The resulting subset model fulfills Alexandre Miguel’s specification [2, p. 122] of an abstract model of the implicit calculus restricted to two universes and stripped of implicit quantification ∀.

To replace the PER model by a subset model, implement the following changes in sections 4 and 5.

PER model.

Replace Per by P(D) in the whole paper. Define Π ∈ (A ∈ P(D)) → (A → P(D)) → P(D) by

Π A G = {e ∈ D | e · d ∈ G(d) for all d ∈ A}

Let Ne = {Ne ŝ | ŝ ∈ TM }.

Semantical natural numbers.

Define Nat ⊆ D inductively by

\overline{Zero ∈ Nat}  \frac{d ∈ Nat}{Succ d ∈ Nat}  \overline{Ne t̂∈ Nat} .

Lemma 4.1 now speaks of subsets instead of PERs, otherwise is remains unchanged. The definition of Set simplifies to

\frac{a ∈ Set  g(d) ∈ Set for all d ∈ [a]}{Pi a g ∈ Set}  \overline{Nat ∈ Set}  \overline{Ne t̂∈ Set}

In fact a ∈ Set can now be defined just as (a, A) ∈ T for some A. Lemma 4.2 shrinks to the statement that a ∈ Set implies that [a] is defined, but this is trivial since [a] = A.

Lemma 4.3 (Semantical sets are upward-closed)

(i) If c ∈ Set and c ⊑ c′ then c′ ∈ Set and [c] = [c′]. (ii) If c ∈ Set, e ∈ [c], and e ⊑ e′, then e′ ∈ [c].

The new Lemma 4.3 is proven like the old one, replace instances of the proposition c = c′ ∈ Set by “c′ ∈ Set and [c] = [c′]”, and d = d′ ∈ [a] by “d, d′ ∈ [a] and d ⊑ d′.”

Semantical types.

Analogous changes. We introduce the new notation d ⊑ d′ ∈ A for d, d′ ∈ A and d ⊑ d′. This is for any subset A of D, including Set and Type. The notation d = d′ ∈ A means now just the literal “d = d′ and d′ ∈ A”.

Lemma 4.5 (Up and down)

(i) If c ⊑ c′ ∈ Type then ↑^{c} t̂= ↑^{c′} t̂∈ [c]. (ii) If c ⊑ c′ ∈ Set then ⇓ c ≡ ⇓ c′ ∈ TM . (iii) If c ⊑ c′ ∈ Type then ⇓ c ≡ ⇓ c′ ∈ TM . (iv) If c ⊑ c′ ∈ Type and e ⊑ e′ ∈ [c] then ↓^{c} e ≡ ↓^{c′} e′ ∈ TM .

Lemma 4.6 (Soundness of recursion)

It now suffices to show rec a d_{z} d_{s} e ∈ [a · e] under the appropriate assumptions.

Semantical contexts.

Let

ρ ∈ [Γ] :⟺ ρ(i) ∈ [[[Γ(i)]]_{ρ}] for 0 ≤ i < |Γ|

We define valid contexts Γ ⊧ inductively by the following rules:

\overline{⋄ ⊧}  \frac{Γ ⊧  [[A]]_{ρ} ∈ Type for all ρ ∈ [Γ]}{Γ, A ⊧}

Validity.

The definition Γ ⊧ t = t′ : A never served any purpose, so it could have been dropped already from the original paper, together with Lemma 4.8 (ii). We only have to model type equality (in contrast to systems with judgemental equality).

Γ ⊧ A  :⟺ Γ ⊧ and ∀ρ ∈ [Γ]. [[A]]_{ρ} ∈ Type
Γ ⊧ A = A′ :⟺ Γ ⊧ A and Γ ⊧ A′ and ∀ρ ∈ [Γ]. [[[A]]_{ρ}] = [[[A′]]_{ρ}]
Γ ⊧ t : A :⟺ Γ ⊧ A and ∀ρ ∈ [Γ]. [[t]]_{ρ} ∈ [[[A]]_{ρ}]

Lemma 4.8 (Convertible terms are semantically related)

If Γ ⊧ A, A′ and A =_{βη} A′ then Γ ⊧ A = A′.

Proof. Fix some ρ ∈ [Γ]. By assumption, a := [[A]]_{ρ} ∈ Type and a′ := [[A′]]_{ρ} ∈ Type. Further, A ⟶^{∗} B^{∗}⟵ A′, which implies a ⊑ [[B]]_{ρ} =: b and a′ ⊑ b. By Lemma 4.4 (modified analogously to Lemma 4.3), [a] = [b] = [a′]. □

The proof of Theorem 4.9 (Validity) becomes simpler, type conversion goes through unchanged (omitting the intermediate inference [[A]]_{ρ} = [[A′]]_{ρ} ∈ Type).

In Section 5 we need to change

Lemma 5.4 (Equality)

If c ⊑ c′ ∈ Type then R_{k}^{c} = R_{k}^{c′}. Moral: use subset models for untyped equality and PER models for judgmental equality.

References

[1] Abel, A., K. Aehlig and P. Dybjer, Normalization by evaluation for Martin-Löf type theory with one universe, in: M. Fiore, editor, Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII), New Orleans, LA, USA, 11-14 April 2007, Electronic Notes in Theoretical Computer Science 173 (2007), pp. 17–39.

[2] Miquel, A., “Le Calcul des Constructions implicite: syntaxe et sÃ\begin{matrix}c \\ ◯ \end{matrix}mantique.” Ph.D. thesis, Université Paris 7 (2001), thèse de doctorat.