Weak βη-Normalization and Normalization by Evaluation for System F

Andreas Abel

Department of Computer Science Ludwig-Maximilians-University Munich

Abstract. A general version of the fundamental theorem for System F is presented which can be instantiated to obtain proofs of weak β- and βη-normalization and normalization by evaluation.

1 Introduction and Related Work

Dependently typed lambda-calculi have been successfully used as proof languages in proof assistants like Agda [Nor07], Coq [INR07], LEGO [Pol94], and NuPrl [Ct86]. Since types may depend on values in these type theories, checking equality of types, which is crucial for type and, thus, proof checking, is non-trivial for these languages, and undecidable in the general case. In extensional type theories, such as the one underlying NuPrl, extensional, hence undecidable, type equality has been kept with the consequence that type checking is undecidable and requires user interaction. In intensional type theories, which are the basis of Agda, Coq, and LEGO, type equality has been restricted to a decidable fragment, called definitional equality, hence, type checking is decidable. However, the choice of this fragment strongly influences the comfort in using these systems: the more equal types are recognized as equal automatically, the fewer equality proofs the user has to construct manually.

Definitional equality encompasses at least computational equality, i. e., β, expanding of definitions, and recursion, and exactly like that it is currently implemented in Coq. However, there are suggestions to strengthen definitional equality by rewriting rules [Bla05,CWC07] and decision procedures [BJS07]. On another line, it is strongly desirable to include η, which does not fit well under the rewriting paradigm. For incorporating η, normalization-by-evaluation has proven to be successful. Besides being explored for simple types [BS91,Dan99,ADHS01] it has been extended to polymorphic types [AHS96] and predicative dependent type theories [ACD07]. Still open is its application to impredicative type theories such as the Calculus of Constructions (CoC), probably due to the difficult meta theory of CoC. Our long term goal is to formulate a verified normalization-by-evaluation (NbE) algorithm for impredicative type theories. This work is an important step towards this goal: we construct a generic model for System F whose instances are soundness and completeness proofs for NbE.

Altenkirch, Hofmann, and Streicher [AHS96] already developed an NbE algorithm for System F and proved it correct. However, their work concerns only a combinatory (λ-free) version of System F. Moreover, they construct an internal model of System F in category theory; their work is only accessible to experts in categories, and the structure of the algorithm is a bit lost among the category-related technical details. They provide an SML-implementation of the algorithm in the appendix, but it is not formally related to the mathematical algorithm in the main text. In an unpublished article [AHS97] they later extend their result to full System F (with λ-abstraction). Deep knowledge of category theory is a preliminary also for this paper, in the words of the authors, a “certain acquaintance with categories of presheaves” is assumed.

In this article, we try to give a more conventional presentation of NbE for System F, presuming only basic knowledge of λ-calculus and System F, domain theory, and inductive definitions in set theory. This way, we hope to make NbE for System F accessible to a wider audience, and to pave the way for an adaption of NbE to impredicative dependent type theories.

Overview. In Sec. 2, we introduce syntax and typing and computation rules for System F. A generic type interpretation is given in Sec. 3, and a generic formulation of the fundamental theorem for System F in Sec. 4. It is then instantiated to yield weak normalization proofs for β (Sec. 5) and βη (Sec. 6). As main results we obtain soundness and completeness of an NbE algorithm for System F in Sec. 7.

2 Church-style System F

In this section, we briefly recapitulate the syntax and static and dynamic semantics of System F. A more gentle introduction to System F can be found in Pierce’s book [Pie02, Ch. 23].

Syntax. Type variables X and term variables x are drawn from two distinct, countable supplies TyVar and Var.

Ty ∋ A, B, C ::= X | A → B | ∀XA  types
Tm ∋ r, s, t ::= x | λx:A. t | r s | ΛXt | r A  terms
Cxt ∋ Γ, Δ ::= ⋄ | Γ, x:A  typing contexts

We say context Γ′ extends Γ, written Γ′ ≤ Γ, if Γ′(x) = Γ (x) for all x ∈ dom(Γ). For instance, assuming y ∉ dom(Γ), we have (Γ, y:A) ≤ Γ, but not the other way round. Extending a context extends the set of terms typeable in that context; this theorem is called weakening. Remark 1. The direction of ≤ is chosen to be compatible with subtyping. There, we let Γ′ ≤ Γ if Γ′(x) ≤ Γ (x) for all x ∈ dom(Γ). Then Γ ⊢ t : A, Γ′ ≤ Γ, and A ≤ A′ imply Γ′ ⊢ t : A′ (contravariance!).

A substitution σ is a map from type variables to type expressions and from term variables to term expressions. We write Aσ, tσ for the simultaneous execution of substitution σ in A, t. As usual, FV(t) denotes the set of free type and term variables of t, and FV(A) the set of free type variables of A. Let FV(Γ) = ⋃{FV(A) | (x:A) ∈ Γ }.

Typing (static semantics) Γ ⊢ t : A.

\overline{Γ ⊢ x : Γ (x)}  \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λx:A. t : A → B}  \frac{Γ ⊢ r : A → B  Γ ⊢ s : A}{Γ ⊢ r s : B}

\frac{Γ ⊢ t : A}{Γ ⊢ ΛXt : ∀XA} X ∉ FV(Γ) \frac{Γ ⊢ t : ∀XA}{Γ ⊢ t B : A[B/X]}

Operational (dynamic) semantics. One step βη-reduction is the closure of the following axioms under all term constructors:

(λx:A. t) s ⟶_{βη} t[s/x]  λx:A. t x ⟶_{βη} t if x ∉ FV(t)
(ΛXt) A ⟶_{βη} t[A/X]  ΛX. t X ⟶_{βη} t if X ∉ FV(t)

We denote its reflexive-transitive closure by ⟶_{βη}^{∗} and its reflexive-transitive-symmetric closure by =_{βη}.

In the following metatheory of System F, we denote the dependent settheoretic function space by (x ∈ S) → T (x) which is an abbreviation for {f ∈ S → ⋃_{x∈S} T (x) | f(x) ∈ T (x) for all x ∈ S}.

3 Type Interpretation by Kripke Relations

We seek an interpretation of System F’s types which is general enough to account for different normalization results. In particular, we are interested in normalization by evaluation, which exists in different flavors. To name a few, Berger and Schwichtenberg [BS91] interpret simple types as set-theoretical function spaces over the base type of term families, Filinski [Fil99] uses continuous function spaces instead, and Altenkirch, Hofmann, and Streicher [AHS96] construct a glueing model of System F types. We choose Abel, Coquand, and Dybjer’s approach of contextual reification [ACD08], where types are modelled as applicative structures with variables, and reification, i. e., converting semantic objects back to syntax, is context- and type-sensitive. This means that we need to interpret types as Kripke relations, i.e., relations indexed by contexts.

Kripke relations. Given a poset (S, ⊆), we say F is Kripke if F ∈ Cxt → S and antitone, i.e., Γ′ ≤ Γ implies F (Γ) ⊆ F (Γ′). We usually write F_{Γ} for F (Γ).

We say D is an applicative System F structure, if D^{A} is Kripke for each A ∈ Ty and for all A, B ∈ Ty, X ∈ TyVar and Γ ∈ Cxt there exist operations

app_{Γ}^{A,B} ∈ D_{Γ}^{A→B} → D_{Γ}^{A} → D_{Γ}^{B},
App_{Γ}^{X.A} ∈ D_{Γ}^{∀XA} → (B ∈ Ty) → D_{Γ}^{A[B/X]}.

These operations need to be independent of type and context indices, i. e., app_{Γ}^{A,B}(f, d) = app_{Γ′}^{A′,B′}(f, d) if f ∈ D_{Γ}^{A→B} ∩D_{Γ′}^{A′→B′} and d ∈ D_{Γ}^{A} ∩D_{Γ′}^{A′}, and similar for App. Thus, we can introduce an overloaded notation · for application by f · d := app(f, d) and d · B := App(d, B).

Examples for applicative System F structures are Tm_{Γ}^{A} := {t | Γ ⊢ t : A}, as well as Tm_{Γ}^{A}/=_{βη}.

Let D, D̂ be applicative System F structures. We define the set of Kripke relations of type A by

A ∈ 𝕂^{A} ⟺ A_{Γ} ⊆ D_{Γ}^{A} × D̂_{Γ}^{A} for all Γ and A is Kripke.

We use the letters A, B, C for elements of 𝕂^{A}. We write Γ ⊢ d ∼ d′ ∈ A for (d, d′) ∈ A_{Γ}. 𝕂^{A} forms a complete lattice with ⊆, ∩, and ∪ defined pointwise.

A Kripke relation A is a Kripke PER (partial equivalence relation) if A_{Γ} is symmetric and transitive for any context Γ, i.e., Γ ⊢ d ∼ d′ ∈ A implies Γ ⊢ d′ ∼ d ∈ A and Γ ⊢ d_{1} ∼ d_{2} ∈ A and Γ ⊢ d_{2} ∼ d_{3} ∈ A imply Γ ⊢ d_{1} ∼ d_{3} ∈ A.

Constructing Kripke relations. In predicative type theories, such as Martin-Löf Type Theory, one can construct semantical types inductively, i. e., from below [ACD07], without reference to syntax. For impredicative systems, like System F or the Calculus of Constructions, this is not possible. Instead, for each type constructor one has to define a matching operation in the interpretation domain of types, in our case, 𝕂, and then define the interpretation of a type by induction on syntax, e. g., the size of the type expression [GLT89, Sec. 14.2] or its derivation of wellfoundedness [Str91]. In the following, we provide the necessary constructions to interpret function type and universal type.

Kripke relations are closed under arbitrary intersections. Further constructions on Kripke relations are function space and type abstraction:

→  ∈ 𝕂^{A} → 𝕂^{B} → 𝕂^{A→B}
(A → B)_{Γ} = {(f, f′) ∈ D_{Γ}^{A→B} × D̂_{Γ}^{A→B} | for all d, d′, Γ′ ≤ Γ,
Γ′ ⊢ d ∼ d′ ∈ A implies Γ′ ⊢ f · d ∼ f′ · d′ ∈ B}
( . )^{X.B} ∈ (A ∈ Ty) → 𝕂^{B[A/X]} → 𝕂^{∀XB}
(A.B)_{Γ}^{X.B} = {(d, d′) ∈ D_{Γ}^{∀XA} × D̂_{Γ}^{∀XA} | Γ ⊢ d · A ∼ d′ · A ∈ B}

The function space A → B is monotone (covariant) in B and antitone (contravariant) in A. The type abstraction operator (A.B)^{X.B} is monotone in B. In the following, we drop the superscript X.B

Lemma 1. If A, B are Kripke PERs, so are A → B and A.B.

Interpretation space. Depending on what result one wants to harvest from a model construction for System F, one has to impose restrictions on the interpretation domain of types. For example, in a Tait-style proof of strong normalization using saturated sets, one requires each semantical type to be below the set S of strongly normalizing terms and above the set N of neutral strongly normalizing terms. Vaux [Vau04] found an abstraction of (N , S) which he called stable pair. In the following, we present a further generalization which allows the restriction to be dependent on a syntactical type.

Definition 1 (Interpretation space). An interpretation space consists of two Kripke relations \underline{A} ⊆ \overline{A} ∈ 𝕂^{A} for each type A such that the following conditions hold.

k-fun-e  \underline{A → B} ⊆ \overline{A} → \underline{B}
k-fun-i  \underline{A} → \overline{B} ⊆ \overline{A → B}
k-all-e  \underline{∀Y A}  ⊆ B.\underline{A[B/Y]} for any B
k-all-i  X.\overline{A[X/Y]} ⊆ \overline{∀Y A}  for a new X

We write A ⊩ A (pronounced A realizes A) if \underline{A} ⊆ A ⊆ \overline{A}.

A trivial, not type-sensitive interpretation space is \underline{A}_{Γ} = N and \overline{A}_{Γ} = S. In this case, A ⊩ A just means A is saturated. An analogy of A ⊩ A can be found in Matthes’ proof of strong normalization of System F [Mat98, Sec. 9.1.2] where it means A is A-saturated. More examples of interpretation spaces can be found in this article.

In the following, we assume an interpretation space. We now introduce the last construction on semantical types, quantification, which is relative to an interpretation space. If F(B) ∈ 𝕂^{B} → 𝕂^{A[B/X]} for all B ∈ Ty, we let

⋂ F = ⋂{B.F(B, B) | B ⊩ B} ∈ 𝕂^{∀XA}.

Intersection is restricted to realizable semantical types. This has an analogue in other normalization proofs of System F, e. g., Girard [GLT89, Ch. 14] restricts quantification to reducibility candidates. The type constructions preserve realizability, thanks to the conditions imposed by Def. 1.

Lemma 2 (Realizability of type constructions).

1. If A ⊩ A and B ⊩ B then A → B ⊩ A → B.

2. If A[B/Y] ⊩ F(B, B) for all B ⊩ B, then ∀Y A ⊩ ⋂ F.

Proof. Directly, using the postulates on \underline{C} and \overline{C}.

1. First, we have \underline{A → B} ⊆ \overline{A} → \underline{B} by k-fun-e, and since A ⊆ \overline{A} and \underline{B} ⊆ B we obtain by contravariance of the function space \underline{A → B} ⊆ A → B. Secondly, since \underline{A} ⊆ A and B ⊆ \overline{B}, contravariance yields A → B ⊆ \underline{A} → \overline{B} ⊆ \overline{A → B} by k-fun-i.

2. First, for any B ⊩ B we have \underline{A[B/Y]} ⊆ F(B, B), thus by monotonicity of the abstraction operator, B.\underline{A[B/Y]} ⊆ B.F(B, B). By k-all-e it follows \underline{∀Y A} ⊆ B.F(B, B), and since B, B were arbitrary, \underline{∀Y A} ⊆ ⋂ F. Secondly, let X be a new type variable. We have X ⊩ \underline{X}, hence, A[X/Y] ⊩ F(X, \underline{X}) which implies F(X, \underline{X}) ⊆ \overline{A[X/Y]}. Thus, ⋂ F ⊆ X.F(X, \underline{X}) ⊆ X.\overline{A[X/Y]} ⊆ \overline{∀Y A} by k-all-i.

Type interpretation can now be defined mechanically, mapping the syntactic type constructors to the semantic ones. Let σ be a syntactical type substitution and ρ(X) ∈ 𝕂^{σ(X)} for all type variables X, which we write ρ ∈ 𝕂^{σ}. We define [[A]]_{ρ} ∈ 𝕂^{Aσ} by the following equations.

\begin{aligned}[[X]]_{ρ} & = & ρ(X) \\ [[A → B]]_{ρ} & = & [[A]]_{ρ} → [[B]]_{ρ} \\ [[∀XA]]_{ρ} & = & ⋂((B ∈ Ty) ↦ (B ∈ 𝕂^{B}) ↦ [[A]]_{ρ[X↦B]}) \end{aligned}

Note that ρ[X ↦ B] ∈ 𝕂^{σ[X↦B]} in the last line.

Lemma 3. If ρ(X) is a Kripke PER for all X, so is [[A]]_{ρ}.

Lemma 4 (Substitution). [[A[B/X]]]_{ρ} = [[A]]_{ρ[X↦[[B]]_{ρ}]}.

If ρ ∈ 𝕂^{σ}, we let σ ⊩ ρ if σ(X) ⊩ ρ(X) for all type variables X. It is now easy to show that types realize their own interpretations.

Theorem 1 (Type interpretation is realizable). If σ ⊩ ρ then Aσ ⊩ [[A]]_{ρ}.

4 Fundamental Lemma

A general model of System F can be given by interpreting terms in an applicative System F structure D and types as PERs over D. The fundamental theorem does not rely on types being PERs, thus, we can easily take Kripke relations instead.

Fix some context Δ. Let η map type variables to syntactical types and term variables to elements of D such that η ∈ D_{Δ}^{Γ}, meaning η(x) ∈ D_{Δ}^{B} for all (x:B) ∈ Γ. Let t ∈ Tm_{Γ}^{A}. We stipulate the existence of an evaluation function ⦇t⦈_{η} ∈ D_{Δ}^{A} with the following properties.

den-var  ⦇x⦈_{η} = η(x)
den-fun-e  ⦇r s⦈_{η} = ⦇r⦈_{η} · ⦇s⦈_{η}
den-all-e  ⦇r A⦈_{η} = ⦇r⦈_{η} · Aη
den-fun-i ⦇λx:A. t⦈_{η} · d = ⦇t⦈_{η[x↦d]} if d ∈ D_{Δ}^{A}
den-all-i  ⦇ΛXt⦈_{η} · A = ⦇t⦈_{η[X↦A]}

We call (D, · , ⦇ ⦈ ) a syntactical applicative System F structure (cf. Barendregt [Bar84, 5.3.1]).

Now we are ready to show the fundamental theorem. Let (D̂, · , ⦇ ⦈′) be another syntactical applicative System F structure. For η ∈ D_{Δ}^{Γ}, η′ ∈ D̂_{Δ}^{Γ} we define

Δ ⊢ η ∼ η′ ∈ [[Γ]]_{ρ} ⟺ Δ ⊢ η(x) ∼ η′(x) ∈ [[Γ (x)]]_{ρ} for all x ∈ dom(Γ).

Theorem 2 (Validity of typing). Let η ⊩ ρ and both η ↾ TyVar = η′ ↾ TyVar and Δ ⊢ η ∼ η′ ∈ [[Γ]]_{ρ}. If Γ ⊢ t : A then Δ ⊢ ⦇t⦈_{η} ∼ ⦇t⦈′_{η′} ∈ [[A]]_{ρ}.

Proof. By induction on Γ ⊢ t : A. Interesting are the System F specific cases.

Case

\frac{Γ ⊢ t : A}{Γ ⊢ ΛXt : ∀XA} X ∉ FV(Γ)

B ⊩ B  assumption
η[X ↦ B] ⊩ ρ[X ↦ B] =: ρ′  by def.
Δ ⊢ η[X ↦ B] ∼ η′[X ↦ B] ∈ [[Γ]]_{ρ} = [[Γ]]_{ρ′}  since X ∉ FV(Γ)
Δ ⊢ ⦇t⦈_{η[X↦B]} ∼ ⦇t⦈′_{η′[X↦B]} ∈ [[A]]_{ρ′}  by ind. hyp.
Δ ⊢ ⦇ΛXt⦈_{η} · B ∼ ⦇ΛXt⦈′_{η′} · B ∈ [[A]]_{ρ′}  den-all-i
Δ ⊢ ⦇ΛXt⦈_{η} ∼ ⦇ΛXt⦈′_{η′} ∈ B.[[A]]_{ρ′}  by def.
Δ ⊢ ⦇ΛXt⦈_{η} ∼ ⦇ΛXt⦈′_{η′} ∈ [[∀XA]]_{ρ}  since B ⊩ B arbitrary

Case

\frac{Γ ⊢ t : ∀XA}{Γ ⊢ t B : A[B/X]}

Δ ⊢ ⦇t⦈_{η} ∼ ⦇t⦈′_{η′} ∈ ⋂(X ↦ [[A]]_{ρ[X↦X]})  by ind.hyp.
Bη ⊩ [[B]]_{ρ}  by Thm. 1
Δ ⊢ ⦇t⦈_{η} · Bη ∼ ⦇t⦈′_{η′} · Bη ∈ [[A]]_{ρ[X↦[[B]]_{ρ}]}  by instantiation
Δ ⊢ ⦇t B⦈_{η} ∼ ⦇t B⦈′_{η′} ∈ [[A]]_{ρ[X↦[[B]]_{ρ}]}  den-all-e
Δ ⊢ ⦇t B⦈_{η} ∼ ⦇t B⦈′_{η′} ∈ [[A[B/X]]]_{ρ}  Substitution

5 Weak β-Normalization

From our general fundamental theorem we can recover a proof of β-normalization for System F. In this case, we construct an untyped interpretation space of discrete Kripke relations which ignores types and contexts. The following development is standard, we show here only that it fits into the abstractions we have chosen in sections 3 and 4.

Let \overline{r} denote the β-equivalence class of r. Let D_{Γ}^{A} = D̂_{Γ}^{A} = Tm/=_{β} for all Γ, A, with application defined by \overline{r} ·\overline{s} = \overline{r s} and \overline{r} ·A = \overline{r A}. Evaluation is defined by ⦇t⦈\overline{σ} = \overline{tσ}.

Lemma 5. Application and evaluation are well-defined and (D, · , ⦇ ⦈ ) forms a syntactical applicative System F structure.

Neutral terms are given by the grammar n ::= x | n s | n A. The interpretation space for β-normalization is untyped, i. e., we set

\overline{A}_{Γ} = W_{Γ} := \{(\overline{t}, \overline{t}) | t has a β-normal form \}
\underline{A}_{Γ} = N_{Γ} := \{(\overline{n}, \overline{n}) | n has a β-normal form \}

for all types A. To show that these settings really constitute an interpretation space is a standard exercise.

Let η_{id} be the identity map on term and type variables, and let ρ_{id}(X) = N for all X ∈ TyVar. Clearly, η_{id} ⊩ ρ_{id}.

Lemma 6 (Identity environment). Γ ⊢ \overline{η_{id}} ∼ \overline{η_{id}} ∈ [[Γ]]_{ρ_{id}}.

Theorem 3 (Weak β-normalization of System F). If Γ ⊢ t : A then t has a β-normal form.

Proof. By the fundamental theorem Γ ⊢ ⦇t⦈\overline{η_{id}} ∼ ⦇t⦈\overline{η_{id}} ∈ [[A]]_{ρ_{id}} which implies Γ ⊢ \overline{t} ∼ \overline{t} ∈ W, hence, t has a β-normal form.

6 Weak βη-Normalization

In this section, we instantiate Thm. 2 to prove weak βη-normalization for System F. In particular, we show that each well-typed term has a η-long β-normal form. In this, we will require the Kripke aspect of our type interpretation, since being η-long for open terms can only be defined in the presence of a typing context.

Let now \overline{r} denote the βη-equivalence class of r and set D_{Γ}^{A} = D̂_{Γ}^{A} = Tm/=_{βη}. Again, D, with application and evaluation defined as in the last section, constitutes a syntactical applicative System F structure.

Long normal forms are characterized by the two mutually defined judgments

Γ ⊢ t ⇑ A  t is a long normal form of type A
Γ ⊢ t ⇓ A  t is a neutral long normal form of type A

given by the following rules:

\overline{Γ ⊢ x ⇓ Γ (x)}  \frac{Γ ⊢ r ⇓ A → B  Γ ⊢ s ⇑ A}{Γ ⊢ r s ⇓ B}  \frac{Γ ⊢ r ⇓ ∀XA}{Γ ⊢ rB ⇓ A[B/X]}

\frac{Γ ⊢ r ⇓ X}{Γ ⊢ r ⇑ X} \frac{Γ, x:A ⊢ t ⇑ B}{Γ ⊢ λx:A. t ⇑ A → B} \frac{Γ ⊢ t ⇑ A}{Γ ⊢ ΛXt ⇑ ∀XA} X ∉ FV(Γ)

From the model construction of System F we want to harvest that each welltyped term has a η-long β-normal form. Thus, we define an interpretation space by setting

Γ ⊢ d ∼ d′ ∈ \overline{A} ⟺ exists r with d = d′ = \overline{r} and Γ ⊢ r ⇑ A,
Γ ⊢ d ∼ d′ ∈ \underline{A} ⟺ exists r with d = d′ = \overline{r} and Γ ⊢ r ⇓ A.

Lemma 7 (Weakening). \underline{A}, \overline{A} ∈ 𝕂^{A}. Indeed, \underline{A} and \overline{A} span an interpretation space, which we will prove in detail in the following. Lemma 8 (Interpretation space).

k-fun-e  \underline{A → B} ⊆ \overline{A} → \underline{B}
k-fun-i  \underline{A} → \overline{B} ⊆ \overline{A → B}
k-all-e  \underline{∀XA}  ⊆ B.\underline{A[B/X]}
k-all-i  X.\overline{A[X/Y]} ⊆ \overline{∀Y A}  for a new X

Proof. k-fun-e \underline{A → B} ⊆ \overline{A} → \underline{B}

Γ ⊢ f ∼ f′ ∈ \underline{A → B}  by hyp.
f = f′ = \overline{r} and Γ ⊢ r ⇓ A → B  by def.
Γ′ ≤ Γ and Γ′ ⊢ d ∼ d′ ∈ \overline{A}  assumption
d = d′ = \overline{s} and Γ′ ⊢ s ⇑ A  by def.
f · d = f′ · d′ = \overline{r s}  def. of application
Γ′ ⊢ r s ⇓ B  rule, Lemma 7
Γ′ ⊢ f · d ∼ f′ · d′ ∈ \underline{B}  by def.
Γ ⊢ f ∼ f′ ∈ \overline{A} → \underline{B}  since Γ′, d, d′ arb.

k-fun-i \underline{A} → \overline{B} ⊆ \overline{A → B}

Γ ⊢ \overline{r} ∼ \overline{r′} ∈ \underline{A} → \overline{B}  by hyp.
Γ, x:A ⊢ x ⇓ A  rule
Γ, x:A ⊢ \overline{x} ∼ \overline{x} ∈ \underline{A}  by def.
Γ, x:A ⊢ \overline{r} · \overline{x} ∼ \overline{r′} · \overline{x} ∈ \overline{B}  by def. →
\overline{r x} = \overline{r′ x} = \overline{t} and Γ, x:A ⊢ t ⇑ B  by def.
\overline{r} = \overline{λx:A. r x} = \overline{r′} = \overline{λx:A. r′ x} = \overline{λx:A. t}  η
Γ ⊢ λx:A. t ⇑ A → B  rule
Γ ⊢ \overline{r} ∼ \overline{r}′ ∈ \overline{A → B}  by def.

k-all-e \underline{∀XA} ⊆ B.\underline{A[B/X]}

Γ ⊢ d ∼ d′ ∈ \underline{∀XA}  assumption
d = d′ = \overline{r} and Γ ⊢ r ⇓ ∀XA  by def.
d · B = d′ · B = \overline{r B} and Γ ⊢ r B ⇓ A[B/X]  rule, app.
Γ ⊢ d · B ∼ d′ · B ∈ \underline{A[B/X]}  by def.
Γ ⊢ d ∼ d′ ∈ B.\underline{A[B/X]}  by def. B.A

k-all-i X.\overline{A[X/Y]} ⊆ \overline{∀Y A} for a new X.

Γ ⊢ \overline{r} ∼ \overline{r′} ∈ X.\overline{A[X/Y]}  assumption
Γ ⊢ \overline{r} · X ∼ \overline{r′} · X ∈ \overline{A[X/Y]}  by def. X.A
\overline{r X} = \overline{r′ X} = \overline{t} and Γ ⊢ t ⇑ A[X/Y]  by def.
\overline{r} = \overline{ΛX. r X} = \overline{r′} = \overline{ΛX. r′ X} = \overline{ΛXt}  η
X ∉ FV(Γ)  since X new
Γ ⊢ ΛXt ⇑ ∀X. A[X/Y] = ∀Y A  rule
Γ ⊢ \overline{r} ∼ \overline{r′} ∈ \overline{∀Y A}  by def.

The rest is just an application of the fundamental theorem. Recall that η_{id} is the identity map, and let this time ρ_{id}(X) = \underline{X} for all X ∈ TyVar. Again, η_{id} ⊩ ρ_{id}, and Γ ⊢ \overline{η_{id}} ∼ \overline{η_{id}} ∈ [[Γ]]_{ρ_{id}}.

Theorem 4 (Weak βη-normalization of System F). If Γ ⊢ t : A then t β-reduces η-expands to a long normal form t′.

Proof. Clearly, A ⊩ [[A]]_{ρ_{id}}. By Thm. 2, Γ ⊢ ⦇t⦈\overline{η_{id}} ∼ ⦇t⦈\overline{η_{id}} ∈ [[A]]_{ρ_{id}}, meaning t =_{βη} t′ with Γ ⊢ t′ ⇑ A. We conclude by Church-Rosser for β-reduction ηexpansion [Jay91].

7 Normalization by Evaluation

In this section we now define a normalization function which maps exactly the βη-equal terms of the same type to the same η-long β-normal form. To this end, we define judgmental βη-equality Γ ⊢ t = t′ : A and the function nf(Γ ⊢ t: A) such that it is

1. complete for judgmental equality, i. e., Γ ⊢ t = t′ : A implies nf(Γ ⊢t:A) ≡ nf(Γ ⊢t′:A), and

2. sound, i. e., if Γ ⊢ t : A then Γ ⊢ t = nf(Γ ⊢t:A) : A.

7.1 Judgmental Equality

Judgmental βη-equality Γ ⊢ t = t′ : A is defined inductively by the following axiom, plus congruence rules and equivalence rules (reflexivity, symmetry, and transitivity).

\frac{Γ, x:A ⊢ t : B  Γ ⊢ s : A}{Γ ⊢ (λx:A. t) s = t[s/x] : B}  \frac{Γ ⊢ t : A → B}{Γ ⊢ λx:A. t x = t : A → B} x ∉ FV(t)

\frac{Γ ⊢ t : A X ∉ FV(Γ)}{Γ ⊢ (ΛXt) B = t[B/X] : A[B/X]} \frac{Γ ⊢ t : ∀XA}{Γ ⊢ ΛX. t X = t : ∀XA} X ∉ FV(t)

A fundamental theorem for judgmental equality is of course not valid for arbitrary Kripke relations, it can only be shown for Kripke PERs, since symmetry and transitivity have to be modeled. Also, to model the above equations, the evaluation function must satisfy additional laws:

den-subst  ⦇t[s/x]⦈_{η} = ⦇t⦈_{η[x↦⦇s⦈_{η}]} if Γ, x:A ⊢ t : B and Γ ⊢ s : A
den-ty-subst ⦇t[A/X]⦈_{η} = ⦇t⦈_{η[X↦Aη]} if Γ ⊢ t : B and X ∉ FV(Γ)
den-irr  ⦇t⦈_{η} = ⦇t⦈_{η′}  if η(x) = η′(x) for all x ∈ FV(t)

If these laws are satisfied, (D, · , ⦇ ⦈ ) is called a syntactical combinatorial System F algebra (cf. [ACD07]).

For the following theorem, consider an interpretation space of Kripke-PERs over a syntactical combinatorial algebra.

Theorem 5 (Validity of equality). Let σ ⊩ ρ and Δ ⊢ η ∼ η′ ∈ [[Γ]]_{ρ}. If Γ ⊢ t = t′ : A then Δ ⊢ ⦇t⦈_{η} ∼ ⦇t′⦈_{η′} ∈ [[A]]_{ρ}.

Proof. By induction on Γ ⊢ t = t′ : A.

7.2 The normalization algorithm

Normalization by evaluation consist of two steps: first, evaluate the term in the identity environment, obtaining a semantic object, and then, reify the semantic object back to syntax, yielding a long normal form.

Evaluation. For the evaluation we need a combinatorial algebra Val with computable application and evaluation and with variables. One possibility is to let Val be the solution of the recursive domain equation:

Val = ((Var × (Val ∪ Ty)^{<ω}) + [Val → Val] + (Ty → Val))_{⊥}.

Then a semantic object d ∈ Val is either a neutral object e of the shape e ::= x | e d | e A, a continuous function f ∈ [Val → Val] on semantic objects, a function F ∈ Ty → Val from types to semantic objects, or undefined, ⊥.

Let D_{Γ}^{A} = Val for all Γ, A. Application is defined by

\begin{aligned}e · d & = & e d \\ f · d & = & f(d) \end{aligned}  \begin{aligned}e · A & = & e A \\ F · A & = & F (A), \end{aligned}

yielding ⊥ in all other cases, and evaluation by den-var, den-fun-e, den-all-e and

\begin{aligned}⦇λx:A. t⦈_{η}(d) & = & ⦇t⦈_{η[x↦d]} \\ ⦇ΛXt⦈_{η}(A) & = & ⦇t⦈_{η[X↦A]}. \end{aligned}

It is easy to check that (D, · , ⦇ ⦈ ) forms a syntactical combinatorial System F algebra.

Reification converts semantic objects back to expressions. Functions are reified by applying them to fresh variables. This is of course only possible if Val contains the variables.

We adapt contextual reification [ACD08] to System F and define inductively the mutual judgements

Γ ⊢ d ↘ t ⇑ A  d reifies to t at type A,
Γ ⊢ d ↘ t ⇓ A  d reifies to t, inferring type A.

These judgements enrich the corresponding judgements for long normal forms by the semantic object d to be reified to term t. As a consequence, the output t is trivially in long normal form.

\overline{Γ ⊢ x ↘ x ⇓ Γ (x)}

\frac{Γ ⊢ e ↘ r ⇓ A → B  Γ ⊢ d ↘ s ⇑ A}{Γ ⊢ e d ↘ r s ⇓ B}  \frac{Γ ⊢ e ↘ r ⇓ ∀XA}{Γ ⊢ e B ↘ r B ⇓ A[B/X]}

\frac{Γ ⊢ e ↘ r ⇓ X}{Γ ⊢ e ↘ r ⇑ X}

\frac{Γ, x:A ⊢ f · x ↘ t ⇑ B}{Γ ⊢ f ↘ λx:A. t ⇑ A → B} \frac{Γ ⊢ F · X ↘ t ⇑ A}{Γ ⊢ F ↘ ΛXt ⇑ ∀XA} X ∉ FV(Γ).

These rules can be interpreted computationally by considering them clauses of a logic program. Both judgements take Γ and d as input and return t. In the type-directed mode ⇑, type A is input, and in the inference mode ⇓, type A is output. It is easy to check that the associated logic program is well-moded [DW88]. Termination, however, will follow from the fundamental theorem.

Lemma 9 (Weakening). Let Γ′ ≤ Γ.

1. If Γ ⊢ e ↘ r ⇓ A then Γ′ ⊢ e ↘ r ⇓ A.

2. If Γ ⊢ d ↘ t ⇑ A then Γ′ ⊢ d ↘ t ⇑ A.

7.3 Completeness of NbE

We obtain completeness (and termination) of the normalization function as instance of the fundamental theorem for judgmental equality. Let an interpretation space be defined by

Γ ⊢ d ∼ d′ ∈ \overline{A} ⟺ exists t with Γ ⊢ d ↘ t ⇑ A and Γ ⊢ d′ ↘ t ⇑ A,
Γ ⊢ d ∼ d′ ∈ \underline{A} ⟺ exists t with Γ ⊢ d ↘ t ⇓ A and Γ ⊢ d′ ↘ t ⇓ A.

Lemma 10 (Interpretation space). \underline{A}, \overline{A} form an interpretation space of Kripke PERs.

Proof. Analogous to Lemma 8.

Theorem 6 (Completeness of NbE). If Γ ⊢ t = t′ : A then Γ ⊢ ⦇t⦈_{η_{id}} ↘ r ⇑ A and Γ ⊢ ⦇t′⦈_{η_{id}} ↘ r ⇑ A for some long normal form r.

Proof. Since Γ ⊢ η_{id} ∼ η_{id} ∈ [[Γ]]_{ρ_{id}}, by Thm. 5 Γ ⊢ ⦇t⦈_{η_{id}} ∼ ⦇t′⦈_{η_{id}} ∈ \overline{A}.

The normalization function nf(Γ ⊢ t: A) can now be defined to yield the t′ such that Γ ⊢ ⦇t⦈_{η_{id}} ↘ t′ ⇑ A.

7.4 Soundness of NbE

Soundness (and termination) of the normalization function is a consequence of the fundamental theorem for typing, applied to a Kripke relation between semantics and syntax. With D defined as above, we set D̂_{Γ}^{A} = Tm_{Γ}^{A}/(Γ ⊢ = : A), i.e., terms modulo judgmental equality, which forms a syntactical applicative System F structure by virtue of

\begin{aligned}app^{A,B}(\overline{r}, \overline{s}) & = & \overline{r s} \\ App^{X.A}(\overline{r}, B) & = & \overline{r A} \\ ⦇t⦈\overline{σ} & = & \overline{tσ} \end{aligned}

Note that the typed applicative structure is crucial here, on untyped terms modulo judgmental equality one cannot define a total application operation. We let

Γ ⊢ d ∼ \overline{t} ∈ \overline{A} ⟺ exists t′ with Γ ⊢ d ↘ t′ ⇑ A and Γ ⊢ t = t′ : A,
Γ ⊢ d ∼ \overline{t} ∈ \underline{A} ⟺ exists t′ with Γ ⊢ d ↘ t′ ⇓ A and Γ ⊢ t = t′ : A.

Lemma 11 (Interpretation space). \underline{A}, \overline{A} form an interpretation space.

Theorem 7 (Soundness of NbE). If Γ ⊢ t : A then Γ ⊢ ⦇t⦈_{η_{id}} ↘ t′ ⇑ A and Γ ⊢ t = t′ : A.

Proof. For all (x: B) ∈ Γ, it holds that Γ ⊢ x ∼ \overline{x} ∈ \underline{B}, hence, Γ ⊢ η_{id}(x) ∼ \overline{η_{id}}(x) ∈ [[B]]_{ρ_{id}}, thus, Γ ⊢ η_{id} ∼ \overline{η_{id}} ∈ [[Γ]]_{ρ_{id}}. By Thm. 2, Γ ⊢ ⦇t⦈_{η_{id}} ∼ \overline{t} ∈ [[A]]_{ρ_{id}}. We conclude by [[A]]_{ρ_{id}} ⊆ \overline{A}.

Summarizing this section, we have obtained a βη-normalization function for System F which is complete and sound for judgmental equality. We have crucially used that the fundamental theorem for typing is not restricted to PER semantics but has been formulated for Kripke relations between two different applicative System F structures.

8 Conclusion

We have introduced the concept of type interpretation space and proven generic fundamental theorems for typing and judgmental equality in System F. As instances, we obtained proofs of weak normalization for β and βη, and proofs of soundness and completeness for a normalization-by-evaluation algorithm based on contextual reification.

Further work. We seek to extend this work to type theories with non-trivial equality on the type level, like System F^{ω} and the Calculus of Constructions.

Acknowledgments. This work was carried out during a visit to Frédéric Blanqui and Cody Roux at LORIA, Nancy, France, financed by the Bayerisch-Französi-sches Hochschulzentrum. My gratitude extends also to Thierry Coquand and Peter Dybjer for discussions on the topic, and to Ralph Matthes, Cody Roux, and the anonymous referees for their suggestions which helped to improve this paper.

References

[ACD07] Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pages 3–12. IEEE Computer Soc. Press, 2007.

[ACD08] Andreas Abel, Thierry Coquand, and Peter Dybjer. Verifying a semantic βη-conversion test for Martin-Löf type theory. volume 5133 of Lect. Notes in Comput. Sci., pages 29–56. Springer-Verlag, 2008.

[ADHS01] Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In Proc. of the 16th IEEE Symp. on Logic in Computer Science (LICS 2001), pages 303–310. IEEE Computer Soc. Press, 2001.

[AHS96] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reductionfree normalisation for a polymorphic system. In Proc. of the 11th IEEE Symp. on Logic in Computer Science (LICS’96), pages 98–106. IEEE Computer Soc. Press, 1996.

[AHS97] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for System F. Available from

http://www.cs.nott.ac.uk/~txa/publ/f97.pdf, 1997.

[Bar84] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam, 1984.

[BJS07] Frédéric Blanqui, Jean-Pierre Jouannaud, and Pierre-Yves Strub. Building decision procedures in the Calculus of Inductive Constructions. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21th Int. Wksh., CSL 2007, 16th Annual Conf. of the EACSL, volume 4646 of Lect. Notes in Comput. Sci., pages 328–342. Springer-Verlag, 2007.

[Bla05] Frédéric Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1):37–92, 2005.

[BS91] Ulrich Berger and Helmut Schwichtenberg. An inverse to the evaluation functional for typed λ-calculus. In Proc. of the 6th IEEE Symp. on Logic in Computer Science (LICS’91), pages 203–211. IEEE Computer Soc. Press, 1991.

[Ct86] Robert Constable and team. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.

[CWC07] Jacek Chrzaszcz and Daria Walukiewicz-Chrzaszcz. Towards rewriting in Coq. In Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of Lect. Notes in Comput. Sci., pages 113–131. Springer-Verlag, 2007.

[Dan99] Olivier Danvy. Type-directed partial evaluation. In John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann, editors, Partial Evaluation – Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998, volume 1706 of Lect. Notes in Comput. Sci., pages 367–411. Springer-Verlag, 1999.

[DW88] Saumya K. Debray and David S. Warren. Automatic mode inference for logic programs. Journal of Logic Programming, 5:207–229, 1988.

[Fil99] Andrzej Filinski. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor, Proc. of the Int. Conf. on Principles and Practice of Declarative Programming, PPDP’99, volume 1702 of Lect. Notes in Comput. Sci., pages 378–395. Springer-Verlag, 1999.

[GLT89] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[INR07] INRIA. The Coq Proof Assistant, Version 8.1. INRIA, 2007. http://coq.inria.fr/.

[Jay91] Barry Jay. Long βη normal forms and confluence. Technical Report ECS-LFCS-91-183, University of Edinburgh, 1991.

[Mat98] Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. PhD thesis, Ludwig-Maximilians-University, May 1998.

[Nor07] Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden, September 2007.

[Pie02] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.

[Pol94] Randy Pollack. The Theory of LEGO. PhD thesis, University of Edinburgh, 1994.

[Str91] Thomas Streicher. Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhaeuser Verlag, Basel, 1991.

[Vau04] Lionel Vaux. A type system with implicit types. English version of his mémoire de maîtrise, June 2004.