Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements

Andreas Abel^{∗} Institut für Informatik

Ludwig-Maximilians-Universität Oettingenstr. 67, D-80538 München

abel@tcs.ifi.lmu.de

Thierry Coquand

Department of Computer Science and Engineering Chalmers University of Technology Rännvägen 6, S-41296 Göteborg

coquand@cs.chalmers.se

Peter Dybjer^{†}

Department of Computer Science and Engineering Chalmers University of Technology Rännvägen 6, S-41296 Göteborg

peterd@cs.chalmers.se

Abstract

The decidability of equality is proved for Martin-Löf type theory with a universe á la Russell and typed betaeta-equality judgements. A corollary of this result is that the constructor for dependent function types is injective, a property which is crucial for establishing the correctness of the type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first interprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this algorithm is established using a PER-model and a logical relation between syntax and semantics.

1. Introduction

The most important metatheorems of Martin-Löf’s intensional intuitionistic type theory [21, 26] (and related intensional type theories such as the Calculus of Constructions) state that its judgements are decidable. These theorems are fundamental both philosophically and practically. They are the main reasons for preferring intensional to extensional type theory [22, 11]. It is a tenet of the philosophy of constructivism that it should be mechanically decidable whether a certain construction a is a witness to the truth of a given proposition A. Moreover, proof checkers for intensional type theories such as Coq, Agda, and Epigram, all rely on the decision algorithm for a : A using normalization: the user attempts to prove the theorem A by building a construction a, and the system checks that a is indeed a proof of A.

Typed equality judgements. In spite of many years of research into the metatheory of type theory a completely satisfactory story has yet to be told. Systems with an untyped notion of conversion, such as Barendregt’s pure type systems, are well-understood, but there are reasons why theories with a typed notion of conversion (equality judgements) are more fundamental. Firstly, the constructive meaning of equality in the sense of Martin-Löf [22, 23] is relative to a type; two objects are not just equal, they are equal with respect to a type. For this reason all systems of Martin-Löf type theory from 1973 and onwards [21, 22, 26] use equality judgements rather than untyped conversion. Secondly, systems with a typed notion of conversion have clearer mathematical semantics: we can compute the semantics of an element a : A in an arbitrary model of type theory, for example, defined as a category with families [15].

Although some authors have studied the decidability problem for various systems with typed conversion (Martin-Löf [21], Coquand [12], Altenkirch [7], Adams [4]), there is still a need for a clear treatment of the main system of Martin-Löf type theory. Goguen [17] uses typed operational semantics to develop the metatheory of Luo’s system UTT including normalization and Church-Rosser. UTT is an impredicative system having a predicative subsystem which is a version of Martin-Löf type theory. It differs from our system since UTT’s rules for the universe are formulated à la Tarski rather than à la Russell. Moreover, unlike our system, UTT does not have η-conversion on the universe level. More recently, Harper and Pfenning [18] have addressed the problem for the logical framework (LF), with the aim of finding a simpler treatment of its metatheory. However, their method requires injectivity of the dependent function type constructor to be proved early in the development of LF’s metatheory. It is not clear how to extend this method to a system of dependent type theory with a universe of small types. The reader is referred to Harper and Pfenning [18] for discussion and references to related work.

∗Research partially supported by the EU coordination action TYPES (510996).

†Research partially supported by VR-project Typed Lambda Calculus and Applications.

Normalization by evaluation (nbe). We shall employ this method for proving the main decidability theorems for the theory λ^{ΠUN} of Martin-Löf type theory with one universe and natural numbers and typed equality judgements. An important advantage of nbe is that it bypasses the need for a separate proof of the Church-Rosser property, a discovery due to Peter Hancock [21]. Instead it follows directly from the model construction that convertible terms have equal normal forms.

The nbe-method has previously been used for the combinatory version of Martin-Löf type theory [21] with a weak notion of conversion. This theory was however abandoned, and the most recent version of Martin-Löf type theory is based on a logical framework with a type of “sets” (a universe of small types) and dependent function types with β and η-conversion. In recent unpublished work Martin-Löf [24] has shown how to construct an nbe-algorithm for this system, incorporating the technique developed by Berger and Schwichtenberg [10] for the simply-typed λ-calculus. Martin-Löf did however not consider a system with a universe of small types closed under dependent function sets which is the main difficulty here. Such a system was instead considered by Abel, Aehlig, and Dybjer [1] who used ideas from Aehlig and Joachimski’s work on untyped nbe [5]. However, the system in [1] has an untyped notion of conversion and thus differs from the present one; it was not known whether the two systems are equivalent.

The use of nbe has made it possible both to strengthen and to simplify previous treatments of the metatheory of Martin-Löf type theory with a universe and typed equality judgements. Furthermore, our method generalizes to dependent product types (Σ-types) and also to singleton types, and thus generalizes results by Stone and Harper [30].

We expect that our results will play a key role in the theoretical justification of proof systems for Martin-Löf type theory, including the new version of the Agda system currently being developed in Göteborg.

Plan of the paper. In Section 2 we introduce our version of Martin-Löf type theory λ^{ΠUN} with typed equality judgements. The main point here is to give an nbe-algorithm for this theory and to prove it correct. This algorithm consists of an evaluation function given in 3.1 and reification and reflection functions given in 3.2, and studied further as a system of rewrite rules in 3.3. The central property of the nbe-algorithm is that it returns unique representatives (normal forms) for equivalence class of convertible terms and convertible types. We prove this property in two steps: completeness in Section 3 and soundness in Section 4.

By completeness we mean that terms or types which are convertible (we can prove the respective equality judgements) map to identical normal forms. We establish this in Section 3 by defining a family of PERs expressing a notion of typed equality in the model. We then show that the interpretation function maps convertible terms and types to equivalent elements in the model and that reification maps equivalent elements to equal normal forms.

By soundness we mean that a term or type is convertible to its normal form as returned by the nbe-algorithm. To this end we define a logical relation between syntactic expressions and elements in the model in Section 4. Having proved both soundness and completeness the two main results of the paper (decidability of equality and injectivity of Π) follow as corollaries.

In Section 5 we explain how our method extends if we add unit types and dependent product types (Σ-types), and also can be adapted to some other variations of the theory.

2. Syntax and inference rules

In this section we introduce a version of Martin-Löf type theory λ^{ΠUN} with a type of natural numbers N and a universe U of small types. In this system we can build families of small types (elements of U) by primitive recursion. As a consequence, we cannot erase type dependencies, a technique which can otherwise be used in the metatheoretic analysis of the system [18].

The inference rules of the theory are quite standard: we have the usual rules for the dependently typed lambda calculus formulated with equality judgements, the usual rules for N, and the usual rules for a universe U à la Russell. We remark that we have both β and η-conversion for Πtypes. Moreover, the substitution rule is primitive rather than admissible, and thus standard properties of the system are proved easily. We also remark that the nbe-method is quite robust and not so dependent on the precise formulation of the inference rules. It is only when proving decidability of type-checking that we need to know that typing rules are invertible (see Lemma 2), something we can show for our system, even though we have a primitive substitution rule.

Expressions (terms and types). Since we work with Russell-style universes it is natural to have a common syntactic category Λ for terms and types:

Var ∋ x, y, z
Const ∋ c  ::= Fun | U | N | s | z | rec
Λ  ∋ r, s, t ::= c | x | λx.t | r s

The contexts are generated by

Cxt ∋ Γ, Δ ::= ⋄ | Γ, x:A

To aid the reader, we use the letters A, B, C for expressions which are to be understood as types and r, s, t for terms. Dependent function types, usually written Πx : A. B, are written Fun A (λx.B). When B does not depend on x we have a non-dependent function type and write A → B.

We identify expressions up to α-conversion and adopt the convention that in contexts Γ all variables must be distinct. Hence, we can view Γ as a map from variables to types with finite domain dom(Γ) and let Γ(x) = A iff (x: A) ∈ Γ. In context extensions Γ, x: A we presuppose x ∉ dom(Γ). As usual FV(t) is the set of free variables of t. We let FV(t_{1}, …, t_{n}) = FV(t_{1}) ∪ ⋯ ∪ FV(t_{n}) and FV(Γ) = ⋃_{x∈dom(Γ)} FV(Γ(x)).

Simultaneous substitutions σ, τ ∈ Var → Λ are mappings from variables to expressions where the set {x | σ(x) ≠ x}, called dom(σ), is finite. We set FV(σ) = ⋃_{x∈dom(σ)} FV(σ(x)). The identity substitution is denoted by σ_{id}. When f ∈ Var → S for some set S, x ∈ Var and a ∈ S, let f[x ↦ a] be the function f′ defined by f′(x) = a and f′(y) = f(y) for y ≠ x. This update operation will be used for substitutions and later also for environments mapping variables to elements of a semantic domain.

The term t[σ] is the result of substituting σ(x) for x in t for all x ∈ FV(t) in parallel. Parallel substitution Δ[σ] into contexts is defined by (Δ[σ])(x) = (Δ(x))[σ] and composition of substitutions σ[σ′] by (σ[σ′])(x) = (σ(x))[σ′].

Judgements. The type theory λ^{ΠUN} has the following forms of judgement:

Γ ⊢  Γ is a well-formed context
Γ ⊢ A  A is a well-formed type in Γ
Γ ⊢ t : A  t has type A in Γ
Γ ⊢ σ : Δ  σ is a well-formed substitution in Γ
Γ ⊢ A = A′  A and A′ are equal types in Γ
Γ ⊢ t = t′ : A  t and t′ are equal terms of type A in Γ
Γ ⊢ σ = σ′ : Δ σ and σ′ are equal substitutions in Γ

Note that the judgement Γ ⊢ A : U stating that A is a wellformed small type in Γ, is a special case of the third form.

For an arbitrary judgement, we write Γ ⊢ J, where J is a collection of the syntactic entities (terms, contexts, substitutions) to the right of ⊢ in a judgement. The notation J[σ] is understood as the substitution of σ into all entities in J, and FV(J) is the union of the free variable sets of all entities in J. Exceptions are FV(σ : Δ), which is defined as ⋃_{x∈dom(Δ)} FV(Δ(x), σ(x)), and FV(σ = σ′ : Δ) = ⋃_{x∈dom(Δ)} FV(Δ(x), σ(x), σ′(x)).

In our inference rules, we use the abbreviation Rec (λx.C) for the type of the primitive recursion combinator rec with the result type C depending on x : N.

Rec (λx.C) = C[z/x] →

(Fun N (λn. C[n/x] → C[s n/x])) →

Fun N (λx.C)

The inference rules are given in Figure 1.

In the following, we state some simple syntactic properties of λ^{ΠUN} which will be needed in Section 4. Since substitution is a primitive rule these properties are easier to establish than in systems without this primitive rule [18, 2]. On the other hand, if substitution is a primitive rule, the injectivity of Π does not follow easily by syntactic considerations. Instead, this will be one of our main results.

Lemma 1 (Basic properties)

1. (Scope:) If Γ ⊢ J then FV(J) ⊆ dom(Γ).

2. (Context well-formedness:) If Γ, x : A, Γ′ ⊢ J, then Γ ⊢ A.

3. (Weakening:) If Γ, Γ′ ⊢ J and both Γ ⊢ A and x ∉ dom(Γ, Γ′), then Γ, x:A, Γ′ ⊢ J.

4. (Context conversion:) Let Γ ⊢ B = A and Γ ⊢ B. If Γ, x:A, Γ′ ⊢ J then Γ, x:B, Γ′ ⊢ J.

5. (Substitution:)

(a) If Γ ⊢ σ : Δ and x ∈ dom(Δ) then Γ ⊢ σ(x) : Δ(x)[σ].

(b) Γ ⊢ = : Δ is an equivalence relation.

(c) If Γ ⊢ then Γ ⊢ σ_{id} : Γ and Γ ⊢ σ_{id} = σ_{id} : Γ.

Lemma 2 (Inversion)

1. If Γ ⊢ z : C then Γ ⊢ N = C.

2. If Γ ⊢ s : C then Γ ⊢ N → N = C.

3. If Γ ⊢ rec (λx.A) : C then Γ ⊢ Rec (λx.A) = C.

4. If Γ ⊢ x : C then Γ ⊢ Γ(x) = C.

5. If Γ ⊢ λx.t : C then Γ ⊢ Fun A (λx.B) = C and Γ, x:A ⊢ t : B.

6. If Γ ⊢ r s : C then Γ ⊢ r : Fun A (λx.B) with Γ ⊢ s : A and Γ ⊢ B[s/x] = C.

7. If Γ ⊢ Fun A (λx.B) : C then Γ ⊢ A : U and Γ, x: A ⊢ B : U with Γ ⊢ U = C.

8. If Γ ⊢ Fun A (λx.B) then Γ ⊢ A and Γ, x:A ⊢ B.

Well-formed contexts Γ ⊢.

cxt-empty \overline{⋄ ⊢}  cxt-ext \frac{Γ ⊢ A}{Γ, x:A ⊢}

Well-formed types Γ ⊢ A.

n-f \frac{Γ ⊢}{Γ ⊢ N}  univ-f \frac{Γ ⊢}{Γ ⊢ U}  fun-f \frac{Γ ⊢ A  Γ, x:A ⊢ B}{Γ ⊢ Fun A (λx.B)}  univ-e \frac{Γ ⊢ A : U}{Γ ⊢ A}

Well-typed terms Γ ⊢ t : A.

hyp \frac{Γ ⊢  (x:A) ∈ Γ}{Γ ⊢ x : A}  conv \frac{Γ ⊢ t : A  Γ ⊢ A = A′}{Γ ⊢ t : A′}
univ-i-n \frac{Γ ⊢}{Γ ⊢ N : U}  univ-i-fun \frac{Γ ⊢ A : U  Γ, x:A ⊢ B : U}{Γ ⊢ Fun A (λx.B) : U}
fun-i \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λx.t : Fun A (λx.B)}  fun-e \frac{Γ ⊢ r : Fun A (λx.B)  Γ ⊢ s : A}{Γ ⊢ r s : B[s/x]}
n-i-z \frac{Γ ⊢}{Γ ⊢ z : N}  n-i-s \frac{Γ ⊢}{Γ ⊢ s : N → N}  n-e \frac{Γ, x:N ⊢ C}{Γ ⊢ rec (λx.C) : Rec (λx.C)}

Well-formed substitutions Γ ⊢ σ : Δ and parallel substitution.

subst-empty \frac{Γ ⊢}{Γ ⊢ σ : ⋄}  subst-ext \frac{Γ ⊢ σ : Δ  Δ ⊢ A  Γ ⊢ σ(x) : A[σ]}{Γ ⊢ σ : (Δ, x:A)}  subst \frac{Γ ⊢ σ : Δ  Δ ⊢ J}{Γ ⊢ J[σ]}

Equal types Γ ⊢ A = A′. (Congruence and equivalence rules which are omitted.) Equal terms Γ ⊢ t = t′ : A. (Congruence and equivalence rules and the type conversion rule are omitted.)

eq-fun-β \frac{Γ, x:A ⊢ t : B  Γ ⊢ s : A}{Γ ⊢ (λx.t) s = t[s/x] : B[s/x]}  eq-fun-η \frac{Γ ⊢ t : Fun A (λx.B)}{Γ ⊢ (λx. t x) = t : Fun A (λx.B)} x ∉ dom(Γ)
eq-n-ι-z \frac{Γ, x:N ⊢ C  Γ ⊢ z : C[z/x]  Γ ⊢ s : Fun N (λn. C[n/x] → C[s n/x])}{Γ ⊢ rec (λx.C) z s z = z : C[z/x]}
eq-n-ι-s \frac{Γ, x:N ⊢ C  Γ ⊢ z : C[z/x]  Γ ⊢ s : Fun N (λn. C[n/x] → C[s n/x])  Γ ⊢ n : N}{Γ ⊢ rec (λx.C) z s (s n) = s n (rec (λx.C) z s n) : C[s n/x]}

Equal substitutions Γ ⊢ σ = σ′ : Δ and functionality.

eq-subst-empty \frac{Γ ⊢}{Γ ⊢ σ = σ′ : ⋄}  eq-subst-ext \frac{Γ ⊢ σ = σ′ : Δ  Δ ⊢ A  Γ ⊢ σ(x) = σ′(x) : A[σ]}{Γ ⊢ σ = σ′ : (Δ, x:A)}
eq-func-ty \frac{Γ ⊢ σ = σ′ : Δ  Δ ⊢ A}{Γ ⊢ A[σ] = A[σ′]}  eq-func \frac{Γ ⊢ σ = σ′ : Δ  Δ ⊢ t : A}{Γ ⊢ t[σ] = t[σ′] : A[σ]}

Figure 1. Inference rules for λ^{ΠUN}.

Lemma 3 (Syntactic validity)

1. Typing: If Γ ⊢ t : A then Γ ⊢ A.

2. Equality: If Γ ⊢ t = t′ : A then Γ ⊢ A and both Γ ⊢ t : A and Γ ⊢ t′ : A.

3. Type equality: If Γ ⊢ A = A′ then Γ ⊢ A and Γ ⊢ A′.

3. Models and Completeness of NbE

We now show that if we can prove an equality judgement expressing that two types or terms are equal, then they have the same normal form, as computed by our algorithm. To this end, we build a model of λ^{ΠUN} over a model of the untyped λ-calculus.

In 3.1 we consider the class of all PER models of λ^{ΠUN} and show soundness of the inference rules. In 3.2 we add a few new operations and equations to our notion of syntactic combinatory algebra. One of these operations is reification. An abstract nbe-algorithm can be obtained by composing evaluation with the reification function of that algebra. To establish the completeness of this nbe-algorithm we define a residualizing PER-model. Completeness of nbe follows from the facts that (i) provably equal syntactic terms and types are evaluated to PER-equivalent elements in the model, and (ii) PER-equivalent elements in the model are reified to identical normal forms.

In 3.3 we show a new way to instantiate the underlying syntactic combinatorial algebra of the residualizing PERmodel by an extended lambda calculus.

3.1. PER models

A syntactical combinatory algebra consists of a set D with an application operation (juxtaposition) ∈ D×D → D, constructor constants Fun, U, N, z, s and a constant for primitive recursion rec. Each constructor c is injective: c d⃗ = c e⃗ implies d⃗ = e⃗. Primitive recursion satisfies the usual equations:

den-ι-z  rec F d_{z} d_{s} z = d_{z}
den-ι-s  rec F d_{z} d_{s} (s e) = d_{s} e (rec F d_{z} d_{s} e)

Note that the first argument of rec is a dependent type, the type of the result of the function defined by rec. Furthermore, there is an evaluation function [[ ]] ∈ Λ × Env → D satisfying

den-const  [[c]]_{ρ} = c  (c constant)
den-var  [[x]]_{ρ} = ρ(x)
den-fun-e  [[r s]]_{ρ} = [[r]]_{ρ} [[s]]_{ρ}
den-β  [[λx.t]]_{ρ} d = [[t]]_{ρ[x↦d]}
den-subst  [[t[σ]]]_{ρ} = [[t]]_{[[σ]]_{ρ}}

In the following, we let ρ range over environments in Env := Var → D. We use X, Y, F to range over elements of D which denote types. The denotation [[σ]]_{ρ} of a substitution σ is the environment [[σ]]_{ρ}(x) = [[σ(x)]]_{ρ}.

PER models. Let Per(D) denote the set of all partial equivalences over D. If A ∈ Per(D) we write d = d′ ∈ A for (d, d′) ∈ A and |A| = {d | d = d ∈ A} for the domain of A. We often simply write d ∈ A for d ∈ |A|. If A ∈ Per(D), let Fam(A) be the set of functions F ∈ |A| → Per(D) such that F(d) = F′(d′) for all d = d′ ∈ A.

A PER model of λ^{ΠUN} consists of a syntactic combinatory algebra and two PERs U ⊂ Type ∈ Per(D) and a family of PERs [ ] ∈ Fam(Type) with the following closure conditions. The first two conditions express that the PER U of small types contains N and is closed under Π:

per-1 N = N ∈ U; then z = z ∈ [N], and s d = s d′ ∈ [N] if d = d′ ∈ [N].

per-2 Fun X F = Fun X′ F′ ∈ U if X = X′ ∈ U and F d = F′ d′ ∈ U for all d = d′ ∈ [X]; then f = f′ ∈ [Fun X F] if f d = f′ d′ ∈ [F d] for all

d = d′ ∈ [X].

Moreover, the PER Type of all types contains all small types and U, and is closed under Π:

per-3 Type ⊃ U.

per-4 U = U ∈ Type; then [U] = U.

per-5 Fun X F = Fun X′ F′ ∈ Type if X = X′ ∈ Type and F d = F′ d′ ∈ Type for all d = d′ ∈ [X]; then f = f′ ∈ [Fun X F] if f d = f′ d′ ∈ [F d] for all

d = d′ ∈ [X].

Finally, since the first argument of the recursion-constant rec is a family of types it is not covered by the rules for Π above. Hence to validate the rule eq-n-e it is necessary to stipulate separately that it preserves PER-equalities:

per-6 If F d = F′ d′ ∈ Type for all d = d′ ∈ [N], d_{z} = d′_{z} ∈ [F z], d_{s} d_{n} d_{r} = d′_{s} d′_{n} d′_{r} ∈ [F (s d_{n})] for all d_{n} = d′_{n} ∈ [N] and d_{r} = d′_{r} ∈ [F d_{n}], and e = e′ ∈

[N] then rec F d_{z} d_{s} e = rec F′ d′_{z} d′_{s} e′ ∈ [F e].

From now on we often write d = d′ ∈ X for d = d′ ∈ [X].

Validity of the judgements in λ^{ΠUN}. Let ρ = ρ′ ∈ Γ hold if ρ(x) = ρ′(x) ∈ [[A]]_{ρ} for all (x: A) ∈ Γ. Define Γ ⊧ J, meaning that Γ ⊢ J is valid in a given PER-model, as follows:

⊧  :⟺ true
Γ, x:A ⊧  :⟺ Γ ⊧ A
Γ ⊧ A  :⟺ Γ ⊧ A = A
Γ ⊧ A = A′  :⟺ Γ ⊧ and

∀ρ = ρ′ ∈ Γ. [[A]]_{ρ} = [[A′]]_{ρ′} ∈ Type

Γ ⊧ t : A  :⟺ Γ ⊧ t = t : A
Γ ⊧ t = t′ : A :⟺ Γ ⊧ A and

∀ρ = ρ′ ∈ Γ. [[t]]_{ρ} = [[t′]]_{ρ′} ∈ [[A]]_{ρ}

Γ ⊧ σ : Δ  :⟺ Γ ⊧ σ = σ : Δ
Γ ⊧ σ = σ′ : Δ :⟺ Γ ⊧ and Δ ⊧ and

∀ρ = ρ′ ∈ Γ. [[σ]]_{ρ} = [[σ′]]_{ρ′} ∈ Δ

Lemma 4 (Soundness of eq-fun-η ) If Γ ⊧ t : Fun A (λx.B) and x ∉ dom(Γ) then Γ ⊧ λx. t x = t : Fun A (λx.B).

Proof. Assume ρ = ρ′ ∈ Γ and d = d′ ∈ [[A]]_{ρ}. By the laws of the syntactic combinatory algebra, [[λx. t x]]_{ρ} d = [[t x]]_{ρ[x↦d]} = [[t]]_{ρ[x↦d]} d. Since x ∉ dom(Γ) we have ρ[x ↦ d] = ρ′ ∈ Γ, hence, [[λx. t x]]_{ρ} d = [[t]]_{ρ[x↦d]} d = [[t]]_{ρ′} d′ ∈ [[B]]_{ρ[x↦d]}. □

Lemma 5 (Soundness of eq-func-ty ) If Γ ⊧ σ = σ′ : Δ and Δ ⊧ A then Γ ⊧ A[σ] = A[σ′].

Proof. Assume ρ = ρ′ ∈ Γ. Then [[σ]]_{ρ} = [[σ′]]_{ρ′} ∈ Δ and [[A]]_{[[σ]]_{ρ}} = [[A]]_{[[σ′]]_{ρ′}} ∈ Type which implies [[A[σ]]]_{ρ} = [[A[σ′]]]_{ρ′} ∈ Type by den-subst . □

Theorem 6 (Soundness of the inference rules) If Γ ⊢ J then Γ ⊧ J.

Proof. Standard, by induction on the derivation of Γ ⊢ J. This proof is straightforward since the inference rules were designed with the PER model in mind. □

3.2 An abstract nbe-algorithm and its completeness

We shall now extend our syntactical combinatory algebras with a new constructor Up which maps neutral terms (see below) to elements in D and operations for reification and reflection. Then we can define a normalization by evaluation function by composing the evaluation function with the reification function. To prove the completeness of this algorithm we define a residualizing PER-model. We emphasize again that in this section we only define an “abstract” nbe-algorithm, which leaves the choice of the exact implementation of D open. In Section 3.3 we will instantiate D with an extended lambda calculus Λ^{↓↑}.

We define the set Nf ⊆ Λ of βι-normal forms simultaneously with the set Ne ⊆ Λ of neutral terms (normal forms with a head variable).

Nf ∋ v, w, V, W ::= λx.v | z | s v | U | Fun V λx.W | u
Ne ∋ u  ::= x | u v | rec V v w u

A residualizing PER-model. Given a syntactical combinatory algebra with an additional injective constructor Up : Ne → D, we define a residualizing PER model as follows.

First define N ∈ Per(D) inductively by the following rules.

\overline{z = z ∈ N}  \frac{d = d′ ∈ N}{s d = s d′ ∈ N}  \overline{Up u = Up u ∈ N}

We then give a simultaneous inductive-recursive definition [16] of the PERs U and [d]. There are several ways to understand such definitions set-theoretically [28, 3, 9]. If Rel(D) is the set of relations on D, we can e. g. follow [6, 1] and inductively define the graph of a partial function [ ] : D ⇀ Rel(D) such that the following equations hold:

[Up u]  = {(Up u′, Up u′) | u′ ∈ Ne}
[N]  = N
[Fun X F] = {(f, f′) | (f d, f′ d′) ∈ [F d]
for all (d, d′) ∈ [X]}

To prove univalence of this relation we use that Up, N, and Fun are constructors. Then we define the universe of small types U ∈ Rel(D) inductively (using PER notation, although we have not yet proved that it is a PER):

\overline{Up u = Up u ∈ U}  \overline{N = N ∈ U}

\frac{X = X′ ∈ U F d = F′ d′ ∈ U for all d = d′ ∈ X}{Fun X F = Fun X′ F′ ∈ U}

We then show by induction on this relation that if X = X′ ∈ U then [X] and [X′] are well-defined and equal PERs. It follows that U ∈ Per(D). We extend the partial function by [U] = U and define the universe of all types Type ∈ Rel(D) inductively.

U ⊆ Type \overline{U = U ∈ Type}

\frac{X = X′ ∈ Type F d = F′ d′ ∈ Type for all d = d′ ∈ X}{Fun X F = Fun X′ F′ ∈ Type}

As for U, we can now show that [ ] ∈ Fam(Type) and Type ∈ Per(D), and it is immediate to check that (U, Type, [ ]) constitutes a PER model of λ^{ΠUN}, validating per-1-5 . The remaining requirement per-6 will be fulfilled in the next section.

Reflection and reification. Assume furthermore, that for each X ∈ Type there are functions

↑^{X} ∈ Ne → |[X]| reflection,
↓^{X} ∈ |[X]| → Nf reification,
⇓ ∈ |Type| → Nf type reification,

such that the following equations in D hold:

\begin{aligned}(↑^{Fun X F} u) d & = & ↑^{F d}(u ↓^{X}d) \\ ↑^{X} u & = & Up u \end{aligned}

where X in the second equation is a term beginning with a constructor different from Fun. Moreover, we have the following syntactical identities in Λ:

↓^{Fun X F} f  = λx. ↓^{F (↑^{X}x)}(f (↑^{X}x))  (*)
↓^{N}z  = z
↓^{N}(s d)  = s (↓^{N}d)
↓^{N}(Up u)  = u
↓^{Up u′}(Up u) = u
↓^{U}X  = ⇓X
⇓(Fun X F) = Fun (⇓X) (λx. ⇓(F (↑^{X}x))) (*)
⇓N  = N
⇓(Up u)  = u
⇓U  = U

The equations (*) shall hold for all but finitely many x ∈ Var. Since we consider λ-terms modulo α-equivalence, this is equivalent to postulating them for some “fresh” x. One way to make this precise is to require D to be a nominal set [27] or FM-domain [29]. We let D be the λ-calculus modulo β and rewrite rules for recursion, reflection and reification. We come to that later, for now let us just assume that the reification functions always choose fresh variables x.

The following central lemma shows that the above equations define total reflection and reification functions on the PERs of our model, and their result does not depend on the choice of representative for each equivalence class.

Lemma 7 (Characterization of reflection and reification) Let X = X′ ∈ Type. Then ↑^{X}u = ↑^{X′}u ∈ X and ⇓X = ⇓X′, and if d = d′ ∈ X then ↓^{X}d = ↓^{X′}d′.

Proof. Simultaneously by induction on X = X′ ∈ Type, showing the lemma for X = X′ ∈ U first. In case of function types Fun X F = Fun X′ F′ ∈ U and f = f′ ∈ Fun X F we have by induction hypothesis ↑^{X}x = ↑^{X′}x ∈ X for a fresh x, hence, f ↑^{X}x = f′ ↑^{X′}x ∈ F ↑^{X}x. Since F ↑^{X}x = F′ ↑^{X′}x ∈ U, by induction hypothesis ↓^{F ↑^{X}x}(f ↑^{X}x) and ↓^{F′ ↑^{X′} x}(f′ ↑^{X′}x) are identical βιnormal forms. Hence, we can abstract x in both terms, which shows that ↓^{Fun X F} f = ↓^{Fun X′ F′}f′ ∈ Nf. This was the most interesting case. □

Since we have a new constructor e = Up r for neutral values, we need to add a new equation for rec:

rec F d_{z} d_{s} (Up r) =

↑^{F (Up r)}(rec \begin{matrix}(λx. ⇓(F (↑^{N}x))) \\ (↓^{F z}d_{z}) \\ (λnλy. ↓^{F (s n)}(d_{s} (↑^{N}n) (↑^{F n}y))) \\ r) \end{matrix}

The variables x, n, y must be fresh for F, s. We can now prove per-6 , the totality of rec, by induction on N.

Summarizing the developments in this section, we have a complete method for checking judgmental equality:

Corollary 8 (Completeness of NbE) Let ρ = ρ ∈ Γ.

1. If Γ ⊢ A = A′ then ⇓[[A]]_{ρ} = ⇓[[A′]]_{ρ}.

2. If Γ ⊢ t = t′ : A then ↓^{[[A]]_{ρ}}[[t]]_{ρ} = ↓^{[[A]]_{ρ}}[[t′]]_{ρ}.

Proof. We have [[A]]_{ρ} = [[A′]]_{ρ} ∈ Type by Thm. 6, hence ⇓[[A]]_{ρ} is syntactically equal to ⇓[[A′]]_{ρ} by the lemma. Analogously for term equality. □

3.3 Extended λ-calculus

We shall now instantiate the domain D with a lambda calculus Λ^{↓↑} ⊇ Λ extended by four new constants Up, up, down, Down. On Λ^{↓↑} we consider βι-reduction ⟶, given as the reflexive-transitive compatible closure of the β-axiom (λx.t) s ⟶ t[s/x] and the ι-axioms listed in Figure 2.

In the three rules which create an abstraction, x ∉ FV(A, C, t). Under this assumption, each of the ιreductions preserves the set of free variables. Since there are no reductions for terms headed by constants c ∈ {Fun, N, z, s, U, Up}, these c are constructors, whereas the other constants f ∈ {rec, up, down, Down} satisfy pattern matching equations. The left hand sides of all ι-rules are algebraic, linear, and non-overlapping. Reduction ⟶ is a orthogonal constructor combinatory reduction system [20], hence, it is confluent. Thus, ⟶ ∘ ⟵ is an equivalence, which we denote by =_{βι}. Reduction is also standardizing; one can apply the call-by-name strategy to find the normal form, if it exists.

Let \overline{r} denote the equivalence class of r modulo =_{βι}. The set of equivalence classes D = Λ^{↓↑}/=_{βι} forms a syntactical combinatory algebra with application operation \overline{r} · \overline{s} = \overline{r s} and denotation operation [[r]]_{ρ} = \overline{r[σ]} where σ is arbitrary with \overline{σ(x)} = ρ(x) for all x ∈ Var. (D is even a syntactical λ-model [8].)

One easily checks that all equations assumed in the last section are satisfied by D. Since recursion is well-defined by induction on N and ↑^{X}, ↓^{X}, ⇓X are well-defined by induction on X ∈ Type, the implementation of these function by rewriting is terminating on arguments which inhabit the PERs of our model. Also, for X ∈ Type, the free variables of the normal form of up X u for u ∈ Ne are exactly the free variables of u, the free variables of the normal form of down X v for v ∈ X normal are exactly the free variables of v, and for X ∈ Type normal the free variables of the normal form of Down X are exactly the free variables of X. This simplifies the task of finding fresh variables during reflection and reification, since suitable candidates can be fixed in the beginning.

rec C z s z  ⟶ z
rec C z s (s n)  ⟶ s n (rec C s z n)
rec C z s (Up r) ⟶ up (C (Up r))
(rec (down (N → U) C) (down (C z) z) (down (Fun N (λn. C n → C (s n))) s) r)

up (Fun A C) t ⟶ λx. up (C x) (t (down A x))
up N t  ⟶ Up t
up (Up r) t  ⟶ Up t
up U t  ⟶ Up t
down (Fun A C) t ⟶ λx. down (C (up A x))
(t (up A x))
down N z  ⟶ z
down N (s n)  ⟶ s (down N n)
down N (Up t)  ⟶ t
down (Up r) (Up t) ⟶ t
down U  ⟶ Down
Down (Fun A C) ⟶ Fun (Down A)
(λx. Down (C (up A x)))
Down N  ⟶ N
Down (Up t)  ⟶ t
Down U  ⟶ U

Figure 2. ι-reduction in Λ^{↓↑}.

Our solution to freshness is similar to the work of Danvy [14] and Aehlig and Joachimski [5] who introduce a secondlevel lambda-calculus to model computation in D. However, our approach is simpler, we do not need two levels, so we can apply standard results of λ-calculus. Furthermore, in our case recursion, reflection, and reification are always terminating, which is not the case in untyped NbE.

4 Logical Relations and Soundness of NbE

In this section we show soundness of NbE for λ^{ΠUN}, that is, that a term (or type) is provably equal to its normal form as computed by the nbe-algorithm: Γ ⊢ a = ⇓[[a]] : A. Decidability of judgmental equality is then a direct corollary of soundness and completeness.

Let Ty(Γ) = {C | Γ ⊢ C} be the set of well-formed types in context Γ and Tm(Γ, C) = {t | Γ ⊢ t : C} be the set of terms of type C in Γ. We say that Δ extends a wellformed context Γ, written Δ ≥ Γ, if Δ ⊢ and Γ(x) = Δ(x) for all x ∈ dom(Γ).

By induction on X ∈ Type, we simultaneously define relations

\begin{matrix}⊢ ◯^{R} X \\ ⊢ : ◯^{R} ∈ X \end{matrix}

such that (Γ ⊢ ◯^{R} X) ⊆ Ty(Γ) and (Γ ⊢ : C ◯^{R} ∈ X) ⊆ Tm(Γ, C) × [X]. We always assume that Γ is well-formed.

Γ ⊢ C ◯^{R} Fun X F :⟺

Γ ⊢ C = Fun A (λx.B) for some A, B and

Γ ⊢ A ◯^{R} X and

Δ ⊢ B[s/x] ◯^{R} F d for all Δ ≥ Γ

and Δ ⊢ s : A ◯^{R} d ∈ X

Γ ⊢ C ◯^{R} X :⟺ Γ ⊢ C = ⇓X for X ≠ Fun Y F

Γ ⊢ r : C ◯^{R} f ∈ FunXF :⟺

Γ ⊢ C = Fun A (λx.B) for some A, B and

Γ ⊢ A ◯^{R} X and

Δ ⊢ r s : B[s/x] ◯^{R} f d ∈ F d for all Δ ≥ Γ

and Δ ⊢ s : A ◯^{R} d ∈ X

Γ ⊢ A : C ◯^{R} X ∈ U :⟺ Γ ⊢ C = U and Γ ⊢ A ◯^{R} X

Γ ⊢ r : C ◯^{R} d ∈ X :⟺ Γ ⊢ r = ↓^{X}d : C

for X = N, Up u

Note that these definitions do not depend on the choice of the representative X, the relations are invariant under replacement of X by X′ if X = X′ ∈ Type.

Lemma 9 Let X = X′ ∈ Type.

1. If Γ ⊢ C ◯^{R} X then Γ ⊢ C ◯^{R} X′.

2. If Γ ⊢ t : C ◯^{R} d ∈ X and d = d′ ∈ X then Γ ⊢ t :

C ◯^{R} d′ ∈ X′.

Simultaneously with the definition one proves the following lemma.

Lemma 10 (Properties of the logical relations) Let X ∈ Type, Γ ⊢ C ◯^{R} X, and Γ ⊢ t : C ◯^{R} d ∈ X.

1. (Monotonicity:) If Δ ≥ Γ then Δ ⊢ C ◯^{R} X and

Δ ⊢ t : C ◯^{R} d ∈ X.

2. (In:) If Γ ⊢ r = u : C then Γ ⊢ r : C ◯^{R} ↑^{X}u ∈ X.

3. (Out:) Γ ⊢ C = ⇓X and Γ ⊢ t = ↓^{X}d : C.

A consequence of Out is that the choice of A, B in the defining clauses of the relations for Fun X F does not matter, since A is determined by X up to judgmental equality uniquely, and B by F. Hence, the following lemma is easily proved by induction on X ∈ Type:

Lemma 11 Let X ∈ Type and Γ ⊢ C = C′.

1. If Γ ⊢ C ◯^{R} X then Γ ⊢ C′ ◯^{R} X.

2. If Γ ⊢ t : C ◯^{R} d ∈ X and Γ ⊢ t = t′ : C then

Γ ⊢ t′ : C′ ◯^{R} d ∈ X.

We relate substitutions Δ ⊢ σ : Γ to environments ρ ∈ Γ by the following definition:

Δ ⊢ σ : Γ ◯^{R} ρ :⟺ for all x ∈ dom(Γ),

Δ ⊢ σ(x) : Γ(x)[σ] ◯^{R} ρ(x) ∈ [[Γ(x)]]_{ρ}

We define the propositions Γ ⊩ J as follows:

⊩  :⟺ true
Γ, x:A ⊩  :⟺ Γ ⊩ A
Γ ⊩ A  :⟺ Γ ⊩ A = A
Γ ⊩ A = A′  :⟺ Γ ⊩ and

Δ ⊢ A[σ] ◯^{R} [[A′]]_{ρ}

for all Δ ⊢ σ : Γ ◯^{R} ρ.

Γ ⊩ t : A  :⟺ Γ ⊩ t = t : A
Γ ⊩ t = t′ : A :⟺ Γ ⊩ A and

Δ ⊢ t[σ] : A[σ] ◯^{R} [[t′]]_{ρ} ∈ [[A]]_{ρ}

for all Δ ⊢ σ : Γ ◯^{R} ρ.

Γ ⊩ τ : Γ′  :⟺ Γ ⊩ τ = τ : Γ′
Γ ⊩ τ = τ′ : Γ′ :⟺ Γ ⊩ and Γ′ ⊩ and

Δ ⊢ τ[σ] : Γ′ ◯^{R} [[τ′]]_{ρ}

for all Δ ⊢ σ : Γ ◯^{R} ρ

Theorem 12 (Fundamental theorem of logical relations) If Γ ⊢ J then Γ ⊩ J.

Proof. By induction on Γ ⊢ J. □

We define a special valuation ρ_{Γ} by induction on Γ, where ρ_{⋄}(x) is arbitrary and ρ_{(Γ,x:A)} = ρ_{Γ}[x ↦ ↑^{[[A]]_{ρ_{Γ}}} x]. It follows that ρ_{Γ} ∈ Γ and Γ ⊢ σ_{id} : Γ ◯^{R} ρ_{Γ}.

Corollary 13 (Soundness of NbE)

1. If Γ ⊢ t : A then Γ ⊢ t = ↓^{[[A]]_{ρ_{Γ}}} [[t]]_{ρ_{Γ}} : A.

2. If Γ ⊢ A then Γ ⊢ A = ⇓[[A]]_{ρ_{Γ}}.

Corollary 14 (Decidability of equality)

1. If Γ ⊢ t, t′ : A we can decide whether Γ ⊢ t = t′ : A.

2. If Γ ⊢ A, A′ we can decide whether Γ ⊢ A = A′.

Proof. It follows from soundness and completeness that two terms or types are equal (in the sense of judgmental equality) iff their normal forms, as computed by the nbefunction, are equal. □

Corollary 15 (Injectivity of Π) If Γ ⊢ Fun A (λx.B) = Fun A′ (λx.B′) then Γ ⊢ A = A′ and Γ, x:A ⊢ B = B′.

Proof. Let ρ = ρ_{Γ}. By Thm. 6, [[Fun A (λx.B)]]_{ρ} = [[Fun A′ (λx.B′)]]_{ρ} ∈ Type. First, this implies [[A]]_{ρ} = [[A′]]_{ρ} ∈ Type by inversion on Type, hence, ⇓[[A]]_{ρ} and ⇓[[A′]]_{ρ} are syntactically identical. With soundness of NbE, this implies Γ ⊢ A = A′. Secondly, since d := ↑^{[[A]]_{ρ}}x ∈ [[A]]_{ρ}, we get [[λx.B]]_{ρ} d = [[λx.B′]]_{ρ} d ∈ Type. With ρ′ = ρ[x ↦ ↑^{[[A]]_{ρ}}x] = ρ_{(Γ,x:A)} this implies that [[B]]_{ρ′} = [[B′]]_{ρ′} ∈ Type, so with soundness we get Γ, x: A ⊢ B = B′. □

5 Extensions

Since we work with judgmental equality it is simple to extend our method to a system with a unit type 1 with inhabitant Γ ⊢ () : 1 and η-law Γ ⊢ t = () : 1 for Γ ⊢ t : 1. In the PER model, we simply let d = d′ ∈ [1] for all d, d′. Reification ↓^{1}d = () and reflection ↑^{1}u = () return both the constant (), so the result of nbe never depends on a particular inhabitant t of the unit type.

Similarly, we can extend our method to deal with Σtypes and singleton types, constructions which present problems in systems with untyped conversion. Such types are handled by Harper and Pfenning’s [18] type-directed algorithmic equality. However, their method is based on erasure of type dependencies and fails for systems which also include universes like λ^{ΠUN}.

Finally, our approach is robust to changes of syntax. For instance, it can deal with typed abstraction λx: A.t. In the PER model, which is based on the untyped λ-calculus, A is simply ignored. The reification function ↓^{Fun X F} t then returns an abstraction annotated with type ⇓X. We could also adapt it to the more explicit syntax for abstraction and application suggested in [31]. Yet another possibility is to use our method for proving the basic properties of the initial category with families (cwf) [15, 19], which is a more algebraic way to present type theory.

We can now prove the correctness of a standard bidirectional type checking algorithm [18] for normal terms. This proof is a corollary of decidability of judgmental equality together with the syntactical inversion properties (Lemma 2). Such algorithms are currently used in the core languages of the dependently typed languages Agda [13] developed at Chalmers and Epigram [25] developed at Nottingham University. With typed abstraction, type checking is decidable also for non-normal terms.

References

[1] A. Abel, 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, volume 173 of Electronic Notes in Theoretical Computer Science, pages 17–39. Elsevier, 2007.

[2] A. Abel and T. Coquand. Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Fundamenta Informaticae, 77(4):345–395, 2007. TLCA’05 special issue.

[3] P. Aczel. Frege Structures and the Notions of Proposition, Truth, and Set, pages 31–59. North-Holland, 1980.

[4] R. Adams. Pure type systems with judgemental equality. Journal of Functional Programming, 16(2):219–246, 2006.

[5] K. Aehlig and F. Joachimski. Operational aspects of untyped normalization by evaluation. Mathematical Structures in Computer Science, 14(4):587–611, Aug. 2004.

[6] S. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Department of Computer Science, Cornell University, 1987.

[7] T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, Nov. 1993.

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

[9] M. Beeson. Foundations of constructive mathematics. Metamathematical studies, volume 6 of Ergebnisse der Mathematik und ihrer Grenzgebiete, 3. Folge [A Series of Modern Surveys in Mathematics]. Springer-Verlag, 1985.

[10] U. Berger and H. Schwichtenberg. An inverse to the evaluation functional for typed λ-calculus. In Sixth Annual Symposium on Logic in Computer Science (LICS ’91), July, 1991, Amsterdam, The Netherlands, Proceedings, pages 203–211. IEEE Computer Society Press, 1991.

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

[12] T. Coquand. An algorithm for testing conversion in type theory. In Logical Frameworks, pages 255–279. Cambridge University Press, 1991.

[13] T. Coquand. An algorithm for type-checking dependent types. In Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), volume 26 of Science of Computer Programming, pages 167–177. Elsevier, May 1996.

[14] O. Danvy. Type-directed partial evaluation. In J. Hatcliff, T. Æ. Mogensen, and P. Thiemann, editors, Partial Evaluation – Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998, volume 1706 of Lecture Notes in Computer Science, pages 367–411. Springer-Verlag, 1999.

[15] P. Dybjer. Internal type theory. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120–134. Springer-Verlag, 1996.

[16] P. Dybjer. A general formulation of simultaneous inductiverecursive definitions in type theory. Journal of Symbolic Logic, (2):525–549, June 2000.

[17] H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, The University of Edinburgh, Department of Computer Science, 1994.

[18] R. Harper and F. Pfenning. On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic, 6(1):61–101, 2005.

[19] M. Hofmann. Syntax and semantics of dependent types. In A. Pitts and P. Dybjer, editors, Semantics and Logics of Computation. Cambridge University Press, 1996.

[20] J. W. Klop. Combinatory reduction systems. Mathematical Center Tracts, 27, 1980.

[21] P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium ‘73, pages 73–118. North-Holland, 1975.

[22] P. Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153–175. North-Holland, 1982.

[23] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[24] P. Martin-Löf. Normalization by evaluation and by the method of computability. Talk at JAIST, Japan Advanced Institute of Science and Technology, Kanazawa, June 2004.

[25] C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 2004.

[26] B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin Löf’s Type Theory: An Introduction. Clarendon Press, Oxford, 1990.

[27] A. M. Pitts. Alpha-structural recursion and induction. In J. Hurd and T. F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 17–34. Springer-Verlag, 2005.

[28] D. S. Scott. Combinators and classes. In C. Böhm, editor, Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, March 25-27, 1975, volume 37 of Lecture Notes in Computer Science, pages 1– 26. Springer-Verlag, 1975.

[29] M. R. Shinwell and A. M. Pitts. On a monadic semantics for freshness. Theoretical Computer Science, 342(1):28–55, 2005.

[30] C. A. Stone and R. Harper. Extensional equivalence and singleton types. ACM Transactions on Computational Logic, 7(4):676–722, 2006.

[31] T. Streicher. Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhäuser Verlag, Basel, 1991.