A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

Andreas Abel^{1}, Thierry Coquand^{2}, and Miguel Pagano^{3}

1 Ludwig-Maximilians-Universität München, abel@informatik.uni-muenchen.de

                2 Göteborg University, coquand@cs.chalmers.se

3 Universidad Nacional de Córdoba, miguel.pagano@gmail.com

Abstract. We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.

1 Introduction and Related Work

One of the raisons d’être of proof-checkers like Agda [28], Coq [20], and Epigram [25] is to decide if a given term has some type; i.e., if a term corresponds to a proof of a proposition [19]. Hence, the convenience of such a system is, in part, determined by the types for which the system can check membership. We extend the decidability of type-checking done in previous works [1, 2] for Martin-Löf type-theories [23, 27] by considering singleton types and proof-irrelevant propositions.

The universe of small types was introduced by Martin-Löf [22] for formalising category theory (in mathematics, universes were introduced by Grothendieck [18] for giving a set-theoretical foundation of category theory[11]); in [23] two different styles of universes are introduced which are called à la Russell (the one considered here), and à la Tarski.

Singleton types were introduced by Aspinall [8] in the context of specification languages. An important use of singletons is as definitions by abbreviations (see [8, 15]); they were also used to model translucent sums in the formalisation of SML [21]. It is interesting to consider singleton types because beta-eta phase separation fails: one cannot do eta-expansion before beta-normalisation because the shape of the types at which to eta-expand is still unknown at this point; and one cannot postpone eta-expansion after beta-normalisation, because etaexpansion can trigger new beta-reductions. Stone and Harper [33] decide type checking in a LF with singleton types and subtyping. Yet it is not clear whether their method extends to computation on the type level. As far as we know, our work is the first where singleton types are considered together with a universe.

De Bruijn proposed the concept of irrelevance of proofs [12], for reducing the burden in the formalisation of mathematics. As shown by Werner [34], the use of proof-irrelevance types together with sigma types is one way to get subset types à la PVS [30] in type-theories having the eta rule—this direction was explored by Sozeau [31, Sec. 3.3] (for other presentation of subset types in Martin-Löf typetheory see [29]). Berardi conjectured in an unpublished work that (impredicative) type-theory with proof-irrelevance is equivalent to constructive mathematics [9].

Checking dependent types relies on checking types for equality. To this end, we compute η-long normal forms using normalisation by evaluation (NbE) [24]. Syntactic expressions are evaluated into a semantic domain and then reified back to expressions in normal form. To handle functional and open expressions, the semantic domain has to be equipped with variables; a major challenge in rigorous treatments of NbE has been the problem to generate fresh identifiers. Solutions include term families [10], liftable de Bruijn terms [7], or Kripke semantics [4]. In this work we present a novel formulation of NbE which avoids the problem completely: reification is split into an η-expansion phase (↓) in the semantics, followed by a read back function (R) into the syntax which is indexed by the number of already used variables. This way, a standard PER model is sufficient, and technical difficulties are avoided.

Outline. The definitions of two calculi are presented in section 2. In section 3 we define the semantics of this LF in a PER model, and we show soundness of the model wrt. the derived rules of the calculus. We use this model to introduce a NbE algorithm, for which we prove completeness (if t = s is derivable, then nbe(t) and nbe(s) are identical). In section 4 we prove, using logical relations, the soundness of the algorithm (i.e., t = nbe(t) is derivable). In section 5 we define a bi-directional algorithm for checking the type of normal forms and inferring the type of neutral terms. The Haskell programs corresponding to the NbE, and type-checking algorithms are shown in the appendices A, and B, respectively.

2 The calculus as a Generalised Algebraic Theory

In the section, we introduce the calculus. For ease of reading, and for showing the modularity of our approach, we present it as two calculi: the first one has dependent function spaces, singleton types, and a universe closed under function spaces and singletons. In the second calculus we leave out singleton types and we add proof-irrelevant types.

We present the calculi using the formalism proposed by Cartmell for generalised algebraic theories (GAT) [13]; however, our calculi are not proper GATs (the rules are written in the so-called “informal syntax” and the rule for application is ambiguous). We give only the introductory rules and the axioms; the rules stating that equality is a congruence relation, called derived rules, are omitted. An example of a derived rule is

\frac{A = B ∈ Type(Γ) γ = δ ∈ Δ → Γ}{A γ = B δ ∈ Type(Δ)} .

2.1 Calculus with singleton types

Notation. We use capital Greek letters for variables ranging over Ctx; capital letters from the beginning of the Latin alphabet for variables ranging on Type(Γ); small Greek letters are used for variables ranging on Γ → Δ; and minuscule Latin characters, for variables on Term(Γ, A). Words in sans face denote constants.

Sorts. The set of sort symbols is {Ctx, →, Type, Term}.

\overline{Ctx is a type} (ctx-sort)  \frac{Γ, Δ ∈ Ctx}{Γ → Δ is a type} (subs-sort)
\frac{Γ ∈ Ctx}{Type(Γ) is a type} (type-sort) \frac{Γ ∈ Ctx  A ∈ Type(Γ)}{Term(Γ, A) is a type} (term-sort)

In the following, whenever a rule has a hypothesis A ∈ Type(Γ), then Γ ∈ Ctx shall be a further, implicit hypothesis. Similarly, σ ∈ Γ → Δ presupposes Γ ∈ Ctx and Δ ∈ Ctx, and t ∈ Term(Γ, A) presupposes A ∈ Type(Γ), which in turn presupposes Γ ∈ Ctx. Note that judgements of the form Γ ∈ Ctx, A ∈ Type(Γ), t ∈ Term(Γ, A), and σ ∈ Γ → Δ correspond to the more conventional forms Γ ⊢, Γ ⊢ A, Γ ⊢ t : A, and Γ ⊢ σ : Δ, resp. In the rest of the paper we use the latter.

Operators. The set of operators is quite large and instead of giving it at once, we define it as the union of the disjoint sets of operators for contexts, substitutions, types, and terms.

Contexts. There are two operators for contexts: S_{C} = {⋄, . }.

\overline{⋄ ∈ Ctx} (empty-ctx)  \frac{Γ ∈ Ctx  A ∈ Type(Γ)}{Γ.A ∈ Ctx} (ext-ctx)

Substitutions. For substitutions we have five operators: S_{S} = {id , ⟨⟩, ( , ), , p}.

\frac{Γ ∈ Ctx}{id_{Γ} ∈ Γ → Γ} (id-subs)  \frac{Γ ∈ Ctx}{⟨⟩ ∈ Γ → ⋄} (empty-subs)

\frac{δ ∈ Γ → Θ  σ ∈ Θ → Δ}{σ δ ∈ Γ → Δ} (comp-subs)

\frac{σ ∈ Γ → Δ  t ∈ Term(Γ, A σ)}{(σ, t) ∈ Γ → Δ.A} (ext-subs)  \frac{A ∈ Type(Γ)}{p ∈ Γ.A → Γ} (fst-subs)

Types. The set of operators for types is S_{T} = {U, Fun , , { } }.

\frac{Γ ∈ Ctx}{U ∈ Type(Γ)} (u-f) \frac{A ∈ Term(Γ, U)}{A ∈ Type(Γ)} (u-el) \frac{A ∈ Type(Γ)  B ∈ Type(Γ.A)}{Fun A B ∈ Type(Γ)} (fun-f)

\frac{A ∈ Type(Γ)  t ∈ Term(Γ, A)}{\{t\}_{A} ∈ Type(Γ)} (sing-f) \frac{A ∈ Type(Δ)  σ ∈ Γ → Δ}{A σ ∈ Type(Γ)} (subs-type)

Terms. The set of operators for terms is S_{E} = {Fun , { } , , q, λ , App }.

\frac{A ∈ Term(Γ, U)  B ∈ Term(Γ.A, U)}{Fun A B ∈ Term(Γ, U)} (fun-u-i) \frac{t ∈ Term(Γ.A, B)}{λt ∈ Term(Γ, Fun A B)} (fun-i)

\frac{B ∈ Type(Γ.A)  t ∈ Term(Γ, Fun A B)  u ∈ Term(Γ, A)}{App t u ∈ Term(Γ, B (id_{Γ} , u))} (fun-el)

\frac{σ ∈ Γ → Δ  t ∈ Term(Δ, A)}{t σ ∈ Term(Γ, A σ)} (subs-term) \frac{A ∈ Type(Γ)}{q ∈ Term(Γ.A, A p)} (hyp)

\frac{A ∈ Term(Γ, U)  t ∈ Term(Γ, A)}{\{t\}_{A} ∈ Term(Γ, U)} (sing-u-i) \frac{t ∈ Term(Γ, A)}{t ∈ Term(Γ, \{t\}_{A})} (sing-i)

\frac{a ∈ Term(Γ, A)  t ∈ Term(Γ, \{a\}_{A})}{t ∈ Term(Γ, A)} (sing-el)

Axioms. We give the axioms without the premises, except in the cases where they can not be inferred.

Substitutions.

(σ δ) γ = σ (δ γ)  ⟨⟩ σ = ⟨⟩
id_{Γ} σ = σ  σ id_{Γ} = σ
id_{⋄} = ⟨⟩  id_{Γ.A} = (p, q)
p (σ, t) = σ  (σ, t) δ = (σ δ, t δ)

Substitutions on types, and terms; η and β-axioms.

U γ = U  {t}_{A} σ = {t σ}_{A σ}
(Fun A B) σ = Fun (A σ) (B (σ p, q))  q (σ, t) = t
t (σ δ) = (t σ) δ  t id_{Γ} = t
(λt) σ = λ(t (σ p, q))  (App r s) σ = App (r σ) (s σ)
App (λt) r = t (id_{Γ} , r)  λ(App (t p) q) = t

\frac{t, t′ ∈ Term(Γ, \{a\}_{A})}{t = t′ ∈ Term(Γ, \{a\}_{A})} (sing-eq-i) \frac{t = t′ ∈ Term(Γ, \{a\}_{A})}{t = t′ ∈ Term(Γ, A)} (sing-eq-el)

In the last two rules we have a choice on how to express them, we could replace them with the rules

\frac{t ∈ Term(Γ, \{a\}_{A})}{t = a ∈ Term(Γ, \{a\}_{A})} (sing-eq-i’) \frac{t ∈ Term(Γ, \{a\}_{A})}{t = a ∈ Term(Γ, A)} (sing-eq-el’)

The rule sing-eq-el is essential; in fact, since we have eta-expansion for singletons, we would like to derive

Γ.{λt}_{Fun A B} ⊢ App q a = t (id, a) : A

from Γ.{λt}_{Fun A B} ⊢ q = λt : {λt}_{Fun A B}, and Γ ⊢ a : A. Which would be impossible if sing-eq-el were not a rule.

Notation. We denote with |Γ | the length of the context Γ; and Γ!i is the projection of the i-th component of Γ, for 0 ⩽ i < |Γ |. We say Δ ⩽^{i} Γ if Δ ⊢ p^{i} : Γ; where p^{i} is the i-fold composition of p with itself. We write D :: J, to denote that D is a derivation with conclusion J. We denote with Terms the set of words freely generated using symbols in S_{S} ∪ S_{T} ∪ S_{E}. We write t ≡_{T} t′ for denoting syntactically equality of t and t′ in T ⊆ Terms. We call A the tag of {a}_{A}.

Remark 1. Note that if Δ ⊢ p^{i} : Γ, and Γ ⊢ p^{j} : Θ, then Δ ⊢ p^{i+j} : Θ.

Definition 1 (Neutral terms, and normal forms).

Ne ∋ k ::= q | qp^{i+1} | App k v
Nf ∋ v, V, W ::= U | Fun V W | {v}_{V} | λv | k

An advantage of introducing the calculus as a GAT is that we can derive several syntactical results from the meta-theory of GATs.

Remark 2 (Weakening of judgements). Let Δ ⩽^{i} Γ, Γ ⊢ A = A′, and Γ ⊢ t = t′ : A; then Δ ⊢ A p^{i} = A′ p^{i}, and Δ ⊢ t p^{i} = t′ p^{i} : A p^{i}.

Remark 3 (Syntactic validity).

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

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

3. If Γ ⊢ A = A′, then both Γ ⊢ A, and Γ ⊢ A′.

Lemma 1 (Inversion of types).

1. If Γ ⊢ Fun A B, then Γ ⊢ A, and Γ.A ⊢ B.

2. If Γ ⊢ {a}_{A}, then Γ ⊢ A, and Γ ⊢ a : A.

3. If Γ ⊢ k, then Γ ⊢ k : U.

Because of the presence of singletons the proof of inversion of the typing rule is more involved than usual. We first show a weaker version of the inversion lemma; and then we prove the usual one.

Let D be a derivation, then P (D) denotes the predicate “if D :: Γ ⊢ t : A, then there exists a derivation D′ :: Γ ⊢ A = {a}_{A′}, and three sub-derivations of D, such that D^{1} :: Γ ⊢ a : A′, D^{2} :: Γ ⊢ t : A′, and D^{3} :: Γ ⊢ a = t : A′, respectively”.

Lemma 2 (Inversion of terms).

1. If D :: Γ ⊢ Fun A′ B′ : A, then

(a) either there exist a derivation D′ :: Γ ⊢ A = U, and two sub-derivations of D, such that D^{1} :: Γ ⊢ A′ : U, and also D^{2} :: Γ.A′ ⊢ B′ : U;

(b) or P (D).

2. If D :: Γ ⊢ {b}_{B} : A, then

(a) either there exist a derivation D′ :: Γ ⊢ A = U, and two sub-derivations of D, such that D^{1} :: Γ ⊢ B : U, and also D^{2} :: Γ ⊢ b : B;

(b) or P (D).

3. If D :: Γ ⊢ λt : A, then

(a) either there exist a derivation D′ :: Γ ⊢ A = Fun A′ B′, and a subderivations of D, such that D^{1} :: Γ.A′ ⊢ t : B′;

(b) or P (D).

4. If D :: Γ ⊢ App t r : A, then

(a) either there exist a derivation D′ :: Γ ⊢ A = B′ (id, r), and sub-derivations of D, such that D^{1} :: Γ ⊢ t : Fun A′ B′, and D^{2} :: Γ ⊢ r : A′;

(b) or P (D).

Proof. (By induction on D.) We show the proof only for D :: Γ ⊢ Fun A B : C, for the other cases are very similar.

We should consider only three cases fun-u-i, sing-i, and conv.

1. It is immediate for fun-u-i, we prove the first disjunct; the only missing derivation is obtained by reflexivity.

2. It is also trivial for sing-i.

3. The most tedious case is conv. We have a derivation D

\frac{D_{1} :: Γ ⊢ Fun A B : C D_{2} :: Γ ⊢ C = C′}{Γ ⊢ Fun A B : C′}

We can apply the inductive hypothesis on D_{1}; from that we know

(a) either there are sub-derivations of D_{1}, such that D_{1}^{1} :: Γ ⊢ A : U, and D_{1}^{2} :: Γ.A ⊢ B : U, and a derivation D∗ :: Γ ⊢ C = U;

(b) or there are a derivation D∗ :: Γ ⊢ C = {a}_{A′}, and three sub-derivations of D_{1}, such that D_{1}^{1} :: Γ ⊢ a : A′, and D_{1}^{2} :: Γ ⊢ Fun A B : A′, and D_{1}^{3} :: Γ ⊢ a = Fun A B : A′.

In either case D_{1}^{i} is a sub-derivation of D. And from D∗ and D_{2}, we can conclude by symmetry and transitivity Γ ⊢ C′ = U, or Γ ⊢ C′ = {a}_{A′}, respectively.

From the last lemma we can conclude, using the fact that derivations are well-founded, the stronger inversion lemma.

Corollary 1 (Inversion of typing).

1. If D :: Γ ⊢ Fun A′ B′ : A, then there exist two sub-derivations of D, such that D^{1} :: Γ ⊢ A′ : U, and also D^{2} :: Γ.A′ ⊢ B′ : U;

2. If D :: Γ ⊢ {b}_{B} : A, then there exist two sub-derivations of D, such that D^{1} :: Γ ⊢ B : U, and also D^{2} :: Γ ⊢ b : B;

3. If D :: Γ ⊢ λt : A, then there exists a sub-derivation of D, such that D^{1} :: Γ.A′ ⊢ t : B′.

Proof. First we note that, albeit not formally done in this work, derivations are defined inductively. Hence the induced order on derivations (D′ < D if and only if D′ is a sub-derivation of D) is well-founded.

We make the reasoning for the first clause; all the rest are similar. Let D :: Γ ⊢ Fun A B : C

Suppose 1 is false, hence by lemma 2, there exists a sub-derivation D′ :: Γ ⊢ Fun A B : C′. And we can continue ad-infinitum, hence the order on derivations is not well-founded.

Remark 4 (Inversion of substitution). It is clear that any substitution Δ ⊢ σ : Γ.A is equal to some substitution Δ ⊢ (σ′, t) : Γ.A

Calculus with Proof-Irrelevance.

In this section we keep the basic rules, and introduce types for natural numbers, enumeration sets, and proof-irrelevant types. The main difference with other presentations [27, 23], in the syntactic level, is that the eliminator operator (for each type) has as an argument the type of the result. The presence of the resulting type in the eliminator is needed in order to define the normalisation function; it is also necessary for the type-inference algorithm.

The lost of decidability of type-checking is because we should decide the inhabitation of a type in order to check that O has some type Prf A^{1}.

Introductory rules.

\frac{Γ ∈ Ctx  A ∈ Type(Γ)  B ∈ Type(Γ.A)}{Σ A B ∈ Type(Γ)} (sum-i)
\frac{t ∈ Term(Γ, A)  b ∈ Term(Γ, B (id, t))}{(t, b) ∈ Term(Γ, Σ A B)} (sum-in)
\frac{t ∈ Term(Γ, Σ A B)}{fst t ∈ Term(Γ, A)} (sum-el1) \frac{t ∈ Term(Γ, Σ A B)}{snd t ∈ Term(Γ, B (id, fst t))} (sum-el2)
\frac{B ∈ Term(Γ, U)  B ∈ Term(Γ.A, U)}{Σ A B ∈ Term(Γ, U)} (sum-u-i)
\frac{Γ ∈ Ctx}{Nat ∈ Type(Γ)} (nat-i)  \frac{Γ ∈ Ctx}{Nat ∈ Term(Γ, U)} (nat-u-i)
\frac{Γ ∈ Ctx}{zero ∈ Term(Γ, Nat)} (nat-z-i) \frac{Γ ∈ Ctx  t ∈ Term(Γ, Nat)}{suc(t) ∈ Term(Γ, Nat)} (nat-s-i)

\frac{B ∈ Type(Γ.Nat)  t ∈ Term(Γ, Nat) z ∈ Term(Γ, B (id, zero))  s ∈ Term(Γ, Rec(B))}{natrec(B, z, s, t) ∈ Term(Γ, B (id, t))} (nat-el)
\frac{Γ ∈ Ctx}{N_{n} ∈ Type(Γ)} (n_{n}-f)  \frac{Γ ∈ Ctx}{N_{n} ∈ Term(Γ, U)} (n_{n}-u-i)
\frac{Γ ∈ Ctx  i < n}{c_{i}^{n} ∈ Term(Γ, N_{n})} (n_{n}-i)

\frac{B ∈ Type(Γ.N_{n})  t_{0} ∈ Term(Γ, B (id, c_{0}^{n})) ⋯ t_{n−1} ∈ Term(Γ, B (id, c_{n−1}^{n}))  t ∈ Term(Γ, N_{n})}{elim^{n}(B, t_{0}, …, t_{n−1}, t) ∈ Term(Γ, B (id, t))} (n_{n}-e)

1 Another possibility is to consider type-checking as an interactive process. For ex-

ample, we could use the same approach as in [32], and introduce proof-obligations

when type-checking O.

\frac{A ∈ Type(Γ)}{Prf A ∈ Type(Γ)} (prf-f) \frac{a ∈ Term(Γ, A)}{[a] ∈ Term(Γ, Prf A)} (prf-i) \frac{t ∈ Term(Γ, A)}{O ∈ Term(Γ, Prf A)} (prf-tm)

\frac{A ∈ Type(Γ)  t, t′ ∈ Term(Γ, Prf A)}{t = t′ ∈ Term(Γ, Prf A)} (prf-eq)

\frac{B ∈ Type(Γ)  b ∈ Term(Γ.A, B p)  t ∈ Term(Γ, Prf A)}{b where^{B} t ∈ Term(Γ, Prf B)} (prf-el)

Axioms.

Σ A B σ = Σ (A σ) (B (σ p, q))
Nat σ = Nat
N_{i} σ = N_{i}
fst t σ = fst t σ
snd t σ = snd t σ
(t, b) σ = (t σ, b σ)
zero δ = zero
suc(t) δ = suc(t δ)
natrec(B, z, s, t) δ = natrec(B (δ p, q), z δ, s δ, t δ)
(Prf A) δ = Prf (A δ)  [t] δ = [t δ]  O δ = O
(b where^{B} t) δ = b (δ p, q) where^{B δ} (t δ)  c_{i}^{n} δ = c_{i}^{n}
elim^{n}(B, t_{0}, …, t_{n−1}, t) δ = elim^{n}(B δ, t_{0} δ, …, t_{n−1} δ, t δ)
fst (t, b) = t
snd (t, b) = b
(fst t, snd t) = t
natrec(B, z, s, zero) = z
natrec(B, z, s, suc(t)) = App (App s t) natrec(B, z, s, t)
elim^{n}(B, t_{0}, …, t_{n−1}, c_{i}^{n}) = t_{i}
b where^{B} [t] = [b (id, t)]

Notation In the sequel we will be (more) flexible with the notation, and we will omit the indices in c_{i}, and in elim(B, t, r).

Lemma 3 (Inversion).

1. If Γ ⊢ Σ A B, then Γ ⊢ A, and Γ.A ⊢ B.

2. If Γ ⊢ Σ A′ B : A, then Γ ⊢ A = U, and Γ ⊢ A : U, and Γ.A ⊢ B : U;

3. If Γ ⊢ (t, b) : A , then Γ ⊢ A = Σ A′ B, and Γ ⊢ t : A′, and Γ ⊢ b : B (id, t);

4. If Γ ⊢ fst t : A , then Γ ⊢ A = A′, and Γ ⊢ t : Σ A′ B, for some A′, and B;

5. If Γ ⊢ snd t : B, then Γ ⊢ B = B′ (id, fst t), and Γ ⊢ t : Σ A B′, for some A, and B′; 6. If Γ ⊢ Nat : A, then Γ ⊢ A = U.

7. If Γ ⊢ zero : A, then Γ ⊢ A = Nat;

8. If Γ ⊢ suc(t) : A, then Γ ⊢ t : Nat, and Γ ⊢ A = Nat;

9. If Γ ⊢ natrec(B, z, s, t) : A , then Γ.Nat ⊢ B, Γ ⊢ z : B (id, zero), Γ ⊢ s : Rec(B), and Γ ⊢ t : Nat, and Γ ⊢ A = B (id, t);

10. if Γ ⊢ c_{i}^{n} : A, then Γ ⊢ A = N_{n};

11. If Γ ⊢ elim(B, t, t′) : A, then Γ.N_{n} ⊢ B, Γ ⊢ t_{i} : B (id, c_{i}), and Γ ⊢ t′ : N_{n}, and Γ ⊢ A = B (id, t).

12. If Γ ⊢ [t] : A, then Γ ⊢ A = Prf A′ and Γ ⊢ t′ : A′.

13. If Γ ⊢ b where^{B} t : A, then Γ ⊢ A = Prf B, and Γ ⊢ t : Prf A′, and Γ.A′ ⊢ b : B p.

As is expected we have now more normal forms, and more neutral terms:

Ne ∋ k ::= … | fst k | snd k | natrec(V, v, v, k) | O
| v where^{V} k | elim^{n}(V, v_{0}, …, v_{n−1}, k)
Nf ∋ v, V ::= … | Σ V W | Nat | N_{n} | Prf V | (v, v′) |
zero | suc(v) | [v] | O | c_{i}^{n}

The problem of losing decidability of type-checking for the calculus with the rule prf-tm does not affect the usability of a system based on a calculus without it. In fact we can consider two calculi, one which is used internally by the system, and one another on which the user writes proofs.

Now we prove that the calculus with prf-tm is a conservative extension of the one without it. We decorate the turnstile, and the equality symbol with ^{∗} for referring to judgements in the extended calculus.

Definition 2. A term t′ is called a lifting of a term t, if all the occurrences of O in t have been replaced by terms s_{0}, …, s_{n−1}, and O does not occur in any s_{i}. We extend this definition to substitutions, contexts, and equality judgements.

If Γ′ is a lifting of Γ, and Γ =^{∗} Γ′, and also Γ′ ⊢ then we say that Γ′ is a good-lifting of Γ. We extend the definition of good-lifting to the others kinds of judgement.

For example, Γ′ ⊢ t′ : A′ is a good-lifting of Γ ⊢ t : A, if Γ′ is a good-lifting of Γ, and A′ is a lifting of A, such that Γ ⊢ A = A′, and t′ is a lifting of t, such that Γ ⊢ t = t′ : A.

Lemma 4. Let Γ ⊢^{∗} J, then there exists a good-lifting Γ′ ⊢ J′; moreover for any other good-lifting Γ′′ ⊢ J′′ of Γ ⊢^{∗} J, we have Γ′ = Γ′′, and Γ′ ⊢ J′ = J′′.

Proof. By induction on Γ ⊢ J, in each rule we use i.h., and build up the corresponding entity to the good-lifting for each part of the judgement; then, given any other good-lifting of the whole judgement, we do inversion on the definition of good-lifting, and get the equalities for each part; we finish using congruence for showing that both good-lifting are judgemental equal.

We show the case for prf-tm. Let

Γ ⊢ O : Prf A,  (1)

then we know Γ ⊢ t : A; hence, by i.h. there is a good-lifting Γ′ ⊢ t′ : A′, and we can conclude Γ′ ⊢ [t′] : Prf A′, which is a good-lifting of 1. Now suppose Γ′′ ⊢ s : B is another good-lifting of 1, then, by inversion, we know Γ′′ is a goodlifting of Γ, B is a good-lifting of Prf A, hence B ≡ Prf A′′, and A′′ is a goodlifting of A; moreover we know s is a good-lifting of O, hence s ≡ [t′′]; therefore we can conclude Γ′ ⊢ [t′] = [t′′] : Prf A′, by prf-eq, after using conversion.

Corollary 2. The calculus ⊢^{∗} is a conservative extension of ⊢.

3 Semantics

In this section we define a PER model of the calculus presented in the previous section. The model is used to define a normalisation function later.

3.1 PER semantics

Definition 3. We define a domain D = 𝕆 ⊕ X_{⊥} ⊕ [D → D] ⊕ D × D ⊕ D × D ⊕ 𝕆 ⊕ D × [D → D] ⊕ D × D, where X is a denumerable set of variables (as usual we write x_{i} and assume x_{i} ≠ x_{j} if i ≠ j, for i, j ∈ ℕ), E_{⊥} = E ∪ {⊥} is lifting, 𝕆 = {⊤}_{⊥} is the Sierpinski space, [D → D] is the set of continuous functions from D to D, ⊕ is the coalesced sum (this is the disjoint union where all the bottoms elements are identified), and D × D is the Cartesian product of D [6]. The injections are:

ι_{O} : 𝕆 → D  ι_{Pair} : D × D → D
ι_{Var} : X → D  ι_{U} : 𝕆 → D
ι_{Lam} : [D → D] → D  ι_{Fun} : D × [D → D] → D
ι_{App} : D × D → D  ι_{Sing} : D × D → D

An element of D which is not ⊥ can be of one of the forms:

⊤  (d, d′)  for d, d′ ∈ D
Var x_{i}  U  for x_{i} ∈ X
Lam f  Fun d f  for d ∈ D, and f ∈ [D → D]
App d d′  Sing d d′  for d, d′ ∈ D .

We define application · : [D × D → D] and the projections p, q : [D → D] by

f · d = if f = Lam f′ then f′ d else ⊥,
p d = if d = (d_{1}, d_{2}) then d_{1} else ⊥,
q d = if d = (d_{1}, d_{2}) then d_{2} else ⊥.

We define a partial function R : ℕ → D → Terms which reifies elements from the model into terms; this function is similar to the read-back function of Gregoire and Leroy’s [17].

Definition 4 (Read-back function).

R_{j} U = U
R_{j} (Fun X F) = Fun (R_{j} X)
(R_{j+1} (F (Var x_{j})))
R_{j} (Sing d X) = {R_{j} d}_{R_{j} X}

R_{j} (App d d′) = App (R_{j} d) (R_{j} d′)
R_{j} (Lam f) = λ(R_{j+1} (f(Var x_{j})))
R_{j} (Var x_{i}) = \begin{cases}q & if j ⩽ i \\ q p^{j−i−1} & if j > i \end{cases}

Partial Equivalence Relations. A partial equivalence relation (PER) over a set D is a binary relation over D which is symmetric and transitive.

If R is a PER over D, and (d, d′) ∈ R then it is clear that (d, d) ∈ R. We define dom(R) = {d ∈ D | (d, d) ∈ R} ; clearly, R is an equivalence relation over dom(R). If (d, d′) ∈ R, sometimes we will write d = d′ ∈ R, and d ∈ R if d ∈ dom(R). We denote with PER(D) the set of all PERs over D.

If R ∈ PER(D) and F : dom(R) → PER(D), we say that F is a family of PERs indexed by R iff for all d = d′ ∈ R, F d = F d′. If F is a family indexed by R, we write F : R → PER(D).

We define two binary relations over D: one for neutral terms and the other for normal forms.

d = d′ ∈ Ne : ⟺ ∀i ∈ ℕ. R_{i} d and R_{i} d′ are defined and R_{i} d ≡_{Ne} R_{i} d′
d = d′ ∈ Nf : ⟺ ∀i ∈ ℕ. R_{i} d and R_{i} d′ are defined and R_{i} d ≡_{Nf} R_{i} d′

Remark 5. These are clearly PERs over D: symmetry is trivial and transitivity follows from transitivity of the syntactical equality.

The following definitions are standard [8, 15] (except for 1); they will be used in the definition of the model.

Definition 5. Let X ∈ PER(D) and F ∈ X → PER(D).

– 1 = {(⊤, ⊤)};

– ∐ X F = {(d, d′) | p d = p d′ ∈ X and q d = q d′ ∈ F (p d)};

– ∏ X F = {(f, f′) | f · d = f′ · d′ ∈ F d, for all d = d′ ∈ X };

– {{d}}_{X} = {(e, e′) | d = e ∈ X and d = e′ ∈ X }.

We define U, T ∈ PER(D) and [ ] : dom(T ) → PER(D) using Dybjer’s schema of inductive-recursive definition [16]. We show then that [ ] is a family of PERs over D.

Definition 6 (PER model).

– Inductive definition of U ∈ PER(D).

• Ne ⊆ U,

• if X = X′ ∈ U and d = d′ ∈ [X], then Sing d X = Sing d′ X′ ∈ U,

• if X = X′ ∈ U and for all d = d′ ∈ [X], F d = F′ d′ ∈ U then

Fun X F = Fun X′ F′ ∈ U.

– Inductive definition of T ∈ PER(D).

• U ⊂ T , • U = U ∈ T ,

• if X = X′ ∈ T , and d = d′ ∈ [X] then Sing d X = Sing d′ X′ ∈ T ,

• if X = X′ ∈ T , and for all d = d′ ∈ [X], F d = F′ d′ ∈ T , then

Fun X F = Fun X′ F′ ∈ T .

– Recursive definition of [ ] ∈ dom(T ) → PER(D).

• [U] = U,

• [Sing d X] = {{d}}_{[X]},

• [Fun X F] = ∏ [X] (d ↦ [F d]),

• [d] = Ne, in all other cases.

Remark 6. The generation order ⊏ on T is well-founded. The minimal elements are U, and elements in Ne; X ⊏ Fun X F, and for all d ∈ [X], F d ⊏ Fun X F; and, finally, X ⊏ Sing d X.

Lemma 5. The function [ ] : dom(T) → PER(D) is a family of PER(D) over T, i.e., [ ] : T → PER(D).

Proof. We prove, by induction on X = X′ ∈ T , that [X] = [X′].

– It is trivial for d = d′ ∈ Ne.

– It is also trivial for U = U.

– Let Sing d X = Sing d′ X′ ∈ U, show {{d}}_{X} = {{d′}}_{X′}. By i.h. we have [X] = [X′], hence d = d′ ∈ [X]. Now let e = d ∈ [X] and e′ = d ∈ [X], by transitivity we have e = d′ ∈ [X] and e′ = d′ ∈ [X]; therefore {{d}}_{X} = {{d′}}_{X′}. Note that this arguments is the same for Sing d X = Sing d′ X′ ∈ T .

– Let Fun X F = Fun X′ F′ ∈ U. By i.h. we know [X] = [X′], and by definition we have F d = F′ d, for all d ∈ dom([X]); hence if f · d = f′ · d′ ∈ F d, for all d = d′ ∈ [X], then also f · d = f′ · d′ ∈ F′ d. As in the last case this reasoning applies for Fun X F = Fun X′ F′ ∈ T .

Remark 7. If d = d′ ∈ Nf and X = X′ ∈ Nf, then Sing d X = Sing d′ X′ ∈ Nf. Also, if d = d′ ∈ Ne and e = e′ ∈ Nf, then App d e = App d′ e′ ∈ Ne.

3.2 Normalisation and η-Expansion in the Model

The usual way to define NbE [7] is to introduce a reification function which maps elements from the model into normal forms; and a function mapping neutral terms to elements of the model (the former function is called the inverse of the evaluation function, and the later “make self evaluating” in [10]). A tricky point of the algorithm is to find a new variable when reifying functions as abstractions.

In this work we do not need to worry about variable capturing when reifying, because we can define functions corresponding to reification, and lifting of neutrals in the model avoiding completely the need to deal with fresh variables.

Definition 7. The partial functions ↑ , ↓ : D → D → D and ⇓ : D → D are given as follows:

↑_{Fun X F} d = Lam (e ↦ ↑_{F e} App d ↓_{X} e)
↑_{Sing d X} e = d
↑_{U} d = d
↑_{d} e = e, for all d ∈ Ne

↓_{Fun X F} d = Lam (e ↦ ↓_{F ↑_{X} e} d · ↑_{X} e)
↓_{Sing d X} e = ↓_{X} d
↓_{U} d = ⇓ d
↓_{d} e = e, for all d ∈ Ne

⇓(Fun X F) = Fun (⇓ X) (d ↦ ⇓(F ↑_{X} d))
⇓(Sing d X) = Sing (↓_{X} d) (⇓ X)
⇓ U = U
⇓ d = d, for all d ∈ Ne

We will show that ↑_{X} : Ne → [X] and ↓_{X} : [X] → Nf. As usual, we need to make it stronger and get that as a corollary of the following lemma.

Lemma 6 (Characterisation of ↑, ↓, and ⇓). Let X = X′ ∈ T , then

1. if k = k′ ∈ Ne then ↑_{X} k = ↑_{X′} k′ ∈ [X];

2. if d = d′ ∈ [X], then ↓_{X} d = ↓_{X′} d′ ∈ Nf;

3. and also ⇓ X = ⇓ X′ ∈ Nf.

Proof. (By induction on X = X′ ∈ T )

– U = U: the first and third parts are clearly seen to hold. The second part is shown by induction on d = d′ ∈ U, and is proved by the third point in the following three cases.

– Sing d X = Sing d′ X′: by the rule we have d = d′ ∈ [X], and X = X′ ∈ T ; hence [X] = [X′]. The first part follows directly from those facts. The second part is by i.h. on d = d′ ∈ [X]. The third part follows from the i.h. and from Rem. 7.

– d = d′ ∈ Ne: trivial.

– Fun X F = Fun X′ F′:

• let k = k′ ∈ Ne, for showing the first part we need to take d = d′ ∈ [X] and show ↑_{Fun X F} App k ↓_{X} d = ↑_{Fun X′ F′} App k′ ↓_{X′} d′ ∈ [F d]. By i.h. on X we have ↓_{X} d = ↓_{X′} d′ ∈ Nf, hence by Rem. 7 and i.h. on F d, we have ↑_{F d} App k ↓_{X} d = ↑_{F′ d′} App k′ ↓_{X′} d′ ∈ [F d].

• Let f = f′ ∈ [Fun X F], for showing ↓_{Fun X F} f = ↓_{Fun X′ F′} f′ ∈ Nf we should prove that R_{i} (↓_{Fun X F} f) and R_{i} (↓_{Fun X F′} f′) are both defined and syntactically equal normal forms. From Rem. 7 and by i.h. on X we have ↑_{X} Var x_{j} = ↑_{X} Var x_{j} ∈ [X] and then f · Var x_{j} = f′ · Var x_{j} ∈ [F ↑_{X} Var x_{j}], therefore we conclude (by i.h. on the second part) ↓_{F ↑_{X} Var x_{j}} f · Var x_{j} = ↓_{F′ ↑_{X} Var x_{j}} f′ · Var x_{j} ∈ Nf. So, by definition of Nf they are syntactically equal once read back, finally we end using congruence of equality under λ.

• let’s show ⇓ Fun X F = ⇓ Fun X′ F′ ∈ Nf . By definition we have ⇓ Fun X F = Fun ⇓ X e ↦ ⇓(F ↑_{X} e). By i.h. on X, we have ⇓ X = ⇓ X′ ∈ Nf. Moreover if k = k′ ∈ Ne, ⇓ F ↑_{X} k = ⇓ F′ ↑_{X′} k′ ∈ Nf (this is again by i.h. and by definition of T ). Now we need to show that R_{i} (Fun X F) and R_{i} (Fun X′ F′) are both defined, and they are syntactically equal in T . We can conclude that by the fact that the syntactically equality is a congruence for Fun ; the only thing that remains to be proved is that R_{i+1} F (↑_{X} Var x_{i}) and R_{i+1} F′(↑_{X′} Var x_{i}) are both syntactically equal, which follows from ⇓ F ↑_{X} k = ⇓ F′ ↑_{X′} k′ ∈ Nf instantiating k and k′ with Var x_{i}.

Definition 8 (Semantics).

Contexts.

[[⋄]] = 1  [[Γ.A]] = ∐ [[Γ]] (d ↦ [[[A]]d])

Substitutions.

[[⋄]]d = ⊤  [[id]]d = d
[[(γ, t)]]d = ([[γ]]d, [[t]]d)  [[p]]d = p d
[[γ δ]]d = [[γ]]([[δ]]d)

Terms (and types).

[[U]]d = U  [[Fun A B]]d = Fun ([[A]]d) (e ↦ [[B]](d, e))
[[{a}_{A}]]d = Sing ([[a]]d) ([[A]]d)  [[App t u]]d = [[t]]d · [[u]]d
[[λt]]d = Lam (d′ ↦ [[t]](d, d′))  [[t γ]]d = [[t]]([[γ]]d)
[[q]]d = q d

Definition 9 (Validity). We define inductively the notion of validity of judgements in a model.

1. ⋄ ⊨ iff true

2. Γ.A ⊨ iff Γ ⊨ A

3. Γ ⊨ A iff Γ ⊨ A = A

4. Γ ⊨ A = A′ iff Γ ⊨ and for all d = d′ ∈ [[Γ]], [[A]]d = [[A′]]d′ ∈ T

5. Γ ⊨ t : A iff Γ ⊨ t = t : A 6. Γ ⊨ t = t′ : A iff Γ ⊨ A and for all d = d′ ∈ [[Γ]], [[t]]d = [[t′]]d′ ∈ [[[A]]d]

7. Γ ⊨ σ : Δ iff Γ ⊨ σ = σ : Δ

8. Γ ⊨ σ = σ′ : Δ iff Γ ⊨, Δ ⊨, and for all d = d′ ∈ [[Γ]], [[σ]]d = [[σ′]]d′ ∈ [[Δ]].

Theorem 1 (Soundness of the Judgements). if Γ ⊢ J, then Γ ⊨ J.

Proof. By induction on Γ ⊢ J.

Theorem 2 (Completeness of NbE). If ⊢ t = t′ : A, then ↓_{[[A]]} [[t]] = ↓_{[[A]]} [[t′]] ∈ Nf.

Proof. By Thm. 1 we have [[t]] = [[t′]] ∈ [[[A]]] and we conclude by Lem. 6.

Calculus with Proof-Irrelevance.

We extend all the definition concerning the construction of the model.

D = … ⊕ D × [D → D] ⊕ 2 × D
⊕ 𝕆 ⊕ 𝕆 ⊕ D ⊕ [D → D] × D × [D → [D → D]] × D
⊕ D ⊕ 𝕆 ⊕ ℕ ⊕ ℕ × ℕ ⊕ ℕ × [D → D] × D^{∗} × D ;

the corresponding injections are

ι_{Sum} : D × [D → D] → D  ι_{P roj} : 2 × D → D
ι_{Nat} : 𝕆 → D  ι_{Zero} : 𝕆 → D
ι_{Suc} : D → D  ι_{Rec} : [D → D] × D × [D → [D → D]] × D → D
ι_{Prf} : D → D  ι_{⋆} : 𝕆 → D
ι_{N} : ℕ → D  ι_{c} : ℕ × ℕ → D
ι_{elim}ℕ × [D → D] × D^{∗} × D → D

As before we use a more convenient notation for the injections, let F, f ∈ [D → D], d, d′ ∈ D, g ∈ [D → D] × D × [D → [D → D]] × D, n, i ∈ ℕ, and d ∈ D^{∗}.

Sum(d, f)  Proj_{{1,2}}d
zero  Nat
suc(d)  nrec(F, d, g, d′)
⋆  Prf(d)
N_{n}  c_{i}^{n}
elim^{n}(F, d, d′)

In preparation for giving the semantics of the new constructs, we define a new extension for functions defined only on pairs to any element of D. If g : D ×D → D, then g : 2 → D → D, as follows:

g^{i}d = \begin{cases}g (e, e′) & if d = (e, e′) \\ Proj_{i}(d) & if d ∈ Ne \\ ⊥ & otherwise \end{cases}

We will use this extension for defining the semantics of fst and snd :

p^{∗} = π_{1}^{1}
q^{∗} = π_{2}^{2}

Definition 10.

R_{j} Sum(X, F) = Σ (R_{j} X) (R_{j+1} F Var x_{j})
R_{j} (d, d′) = (R_{j} d, R_{j} d′)
R_{j} Proj_{1}(d) = fst R_{j} d
R_{j} Proj_{2}(d) = snd R_{j} d
R_{j} Nat = Nat
R_{j} zero = zero
R_{j} suc(d) = suc(R_{j} d)
R_{j} nrec(F, d, f, e) = natrec(R_{j+1} F Var x_{j}, R_{j} d, R_{j} f, R_{j} e)
R_{j} Prf(d) = Prf R_{j} d
R_{j} ⋆ = O
R_{j} N_{n} = N_{n}
R_{j} c_{i}^{n} = c_{i}^{n}  if i < n
R_{j} elim^{n}(F, ⟨d_{0}, …, d_{n−1}⟩, e) = elim^{n}(R_{j+1} F Var x_{j}, R_{j} d_{0}, …, R_{j} d_{n−1}, R_{j} e)

Note that if d = d′ ∈ Ne, e = e′ ∈ Nf, f = f′ ∈ Nf, and F = F′ ∈ Nf, then nrec(F, d, f, e) = nrec(F′, d′, f′, e′) ∈ Ne.

We define inductively a new PER for interpreting natural numbers:

Definition 11 (PER for natural numbers).

– Ne ⊂ N

– zero = zero ∈ N

– suc(d) = suc(d′) ∈ N, if d = d′ ∈ N

Definition 12. Let n ∈ ℕ, then Const_{n} = {(c_{i}^{n}, c_{i}^{n}) | i < n} ∪ Ne.

Remark 8. The operator \overline{X} is a closure operator; i.e.,

1. it is extensive, X ⊆ \overline{X};

2. it is monotonic, if X ⊆ X′, then \overline{X} ⊆ \overline{X′}; and

3. it is idempotent, \overline{\overline{X}} = \overline{X}.

Definition 13.

– If X = X′ ∈ U, and for all d = d′ ∈ [X], F d = F′ d′ ∈ U, then Sum(X, F) = Sum(X′, F′) ∈ U.

– If X = X′ ∈ T , and for all d = d′ ∈ [X], F d = F′ d′ ∈ T , then Sum(X, F) = Sum(X′, F′) ∈ T .

– finally we add the corresponding PER, [Sum(X, F)] = ∐ X F

– Nat = Nat ∈ U,

– [Nat] = N

– N_{n} = N_{n} ∈ U,

– [N_{n}] = Const_{n}

– if X = X′ ∈ T , then Prf(X) = Prf(X′) ∈ T .

– if X ∈ dom(T ), then [Prf(X)] = {(⋆, ⋆)}

Not that in the PER model, all propositions Prf(X) are inhabited. In fact, all types are inhabited, since there is a reflection from variables into any type, be it empty or not. So, the PER model is unsuited for refuting propositions. However, the logical relation we define in the next section will only be inhabited for nonempty types.

Definition 14.

↑_{Sum(X,F)} d = (↑_{X} p^{∗} d, ↑_{F ↑_{X} (p^{∗} d)} q^{∗} d)
↓_{Sum(X,F)} d = (↓_{X} p^{∗} d, ↓_{F (p^{∗} d)} q^{∗} d)
↑_{Nat} k = k  ↓_{Nat} suc(d) = suc(↓_{Nat} d)
↓_{Nat} d = d
↑_{Prf(X)} d = ⋆  ↓_{Prf(X)} d = ⋆
↑_{N_{n}} k = k  ↓_{N_{n}} d = d
⇓ Sum(X, F) = Sum(⇓ X, d ↦ ⇓ F ↑_{X} d)  ⇓ Nat = Nat
⇓ Prf(X) = Prf(⇓ X)  ⇓ N_{n} = N_{n}

↑_{Prf(X)} d = ⋆  ↓_{Prf(X)} d = ⋆  ⇓ Prf(X) = Prf(⇓ X)

Proof ( 6 on page 13).

1. let k = k′ ∈ Ne, then ↑_{Nat} k = ↑_{Nat} k′ ∈ [Nat]. Trivial, since Ne ⊂ N.

2. Let d = d′ ∈ [Nat], and show ↓_{Nat} d = ↓_{Nat} d′ ∈ Nf. By induction on d = d′ ∈ N.

3. We have to show ⇓ Nat = ⇓ Nat ∈ Nf. Trivial.

4. It is immediate that if k = k′ ∈ Ne, then ↑_{Prf(X)} k = ↑_{Prf(X′)} k′ ∈ [Prf(X)], because both sides are by definition ⋆, and ⋆ = ⋆ ∈ [Prf(X)].

5. Since O ∈ Nf , and R_{i} ⋆ = O, then ⋆ = ⋆ ∈ Nf; hence if d = d′ ∈ [Prf(X)], ↓_{Prf(X)} d = ↓_{Prf(X′)} d.

6. by i.h. we have ⇓ X = ⇓ X′ ∈ Nf, and clearly Prf(⇓ X) = Prf(⇓ X′) ∈ Nf.

We define a partial function rec : [D → D] × D × D × D → D as:

Definition 15.

rec(F, d, f, zero) = d
rec(F, d, f, suc(e)) = (f · e) · rec(F, d, f, e)
rec(F, d, f, k) = ↑_{F k} (nrec(d′ ↦ ⇓ F d′,
↓_{F zero} d,
Lam d′ ↦ (Lam e′ ↦ ↓_{F suc(d′)} f · d′ · e′),
k))

Definition 16.

case^{n}(F, ⟨d_{0}, …, d_{n−1}⟩, c_{i}^{n}) = d_{i}
case^{n}(F, ⟨d_{0}, …, d_{n−1}⟩, k) = ↑_{F k} elim^{n}(e ↦ ⇓ F e, ⟨↓_{F c_{0}^{n}} d_{0}, …, ↓_{F c_{n−1}^{n}} d_{n−1}⟩, k)

Remark 9. If for all d = d′ ∈ N, F d = F′d′ ∈ T , and z = z′ ∈ [F zero], and for all d = d′ ∈ N, and e = e′ ∈ [F d], s · d · e = s′ · d′ · e′ ∈ [F suc(d)], and d = d′ ∈ N then rec(F, z, s, d) = rec(F, z, s, d′) ∈ [F d].

With these new definitions we can now give the semantic equations for the new constructs.

Definition 17.

[[Σ A B]]d = Sum([[A]]d, d′ ↦ [[B]]((d, d′)))
[[fst t]]d = p^{∗} [[t]]d
[[snd t]]d = q^{∗} [[t]]d
[[(t, t′)]]d = ([[t]]d, [[t′]]d)
[[Nat]]d = Nat
[[zero]]d = zero
[[suc(t)]]d = suc([[t]]d)
[[natrec(B, z, s, t)]]d = rec(e ↦ [[B]](d, e), [[z]]d, [[s]]d, [[t]]d)
[[Prf A]]d = Prf([[A]]d)
[[[a]]]d = ⋆
[[O]]d = ⋆
[[b where^{B} t]]d = ⋆
[[N_{n}]]d = N_{n}
[[c_{i}^{n}]]d = c_{i}^{n}
[[elim^{n}(B, t_{0}, …, t_{n−1}, t)]]d = case^{n}(e ↦ [[B]](d, e), ⟨[[t_{0}]]d, …, [[t_{n−1}]]d⟩, [[t]]d)
[[Prf A]]d = Prf([[A]]d)  [[[a]]]d = ⋆
[[b where^{B} t]]d = ⋆  [[O]]d = ⋆

Remark 10. All of lemmata 5, 6, and theorems 1, and 2 are valid for the calculus with proof-irrelevance.

4 Logical relations

In order to prove soundness of our normalisation algorithm we define logical relations [?] between types and elements in the domain of T , and between terms and elements in the domain of the PER corresponding to elements of T .

These relations are defined inductively on the structure of the elements in the domain of T .

Definition 18 (Logical relations). The relations Γ ⊢ A ∼ X ∈ T (ternary) and Γ ⊢ t : A ∼ d ∈ [X] are defined simultaneously by induction on X ∈ T .

– Neutral types: X ∈ Ne. • Γ ⊢ A ∼ X ∈ T iff for all Δ ⩽^{i} Γ, Δ ⊢ A p^{i} = R_{|Δ|} ⇓ X.

• Γ ⊢ t : A ∼ d ∈ [X] iff Γ ⊢ A ∼ X ∈ T , and for all Δ ⩽^{i} Γ,

Δ ⊢ t p^{i} = R_{|Δ|} ↓_{X} d : A p^{i}.

– Universe X = U.

• Γ ⊢ A ∼ U ∈ T iff Γ ⊢ A = U.

• Γ ⊢ t : A ∼ X ∈ [U] iff Γ ⊢ A = U, and Γ ⊢ t ∼ X ∈ T .

– Singletons.

• Γ ⊢ A ∼ Sing d X ∈ T iff Γ ⊢ A = {a}_{A′} for some A′, a, and Γ ⊢ a : A′ ∼ d ∈ [X].

• Γ ⊢ t : A ∼ d′ ∈ [Sing d X] iff Γ ⊢ A = {a}_{A′} for some A′, a, such that

Γ ⊢ t : A′ ∼ d ∈ [X], and Γ ⊢ A′ ∼ X ∈ T .

– Function spaces.

• Γ ⊢ A ∼ Fun X F ∈ T iff Γ ⊢ A = Fun A′ B, and Γ ⊢ A′ ∼ X ∈ T , and Δ ⊢ B (p^{i}, s) ∼ F d ∈ T for all Δ ⩽^{i} Γ and Δ ⊢ s : A′ p^{i} ∼ d ∈ [X].

• Γ ⊢ t : A ∼ f ∈ [Fun X F] iff Γ ⊢ A = Fun A′ B, Γ ⊢ A′ ∼ X, and Δ ⊢ App (t p^{i}) s : B (p^{i}, s) ∼ f · d ∈ [F d] for all Δ ⩽^{i} Γ and Δ ⊢ s : A′ p^{i} ∼ d ∈ [X].

The following lemmata show that the logical relations are preserved by judgemental equality, weakening of the judgement, and the equalities on the corresponding PERs.

Lemma 7. Let Γ ⊢ A = A′, Γ ⊢ t = t′ : A, Γ ⊢ A ∼ X ∈ T , and Γ ⊢ t : A ∼ d ∈ [X]; then Γ ⊢ A′ ∼ X ∈ T , and Γ ⊢ t′ : A′ ∼ d ∈ [X].

Proof. By induction on X ∈ T .

– Types.

• X = U: by hypothesis Γ ⊢ A = U, hence by symmetry and transitivity Γ ⊢ A′ = U.

• X ∈ Ne: by hypothesis Γ ⊢ A = R_{|Γ |} X, again by symmetry and transitivity Γ ⊢ A′ = R_{|Γ |} X.

• X = Sing d X: by hypothesis Γ ⊢ A = {a}_{B}, and Γ ⊢ a : B ∼ d ∈ [X]. As before we use symmetry and transitivity, and conclude Γ ⊢ A′ = {a}_{B}.

• X = Fun X′ F: by hypothesis Γ ⊢ A = Fun B C, Γ ⊢ B ∼ X′, and Δ ⊢ C (p^{i}, s) ∼ F d ∈ T for all Δ ⩽^{i} Γ and Δ ⊢ s : B p^{i} ∼ d ∈ [X′]. Using symmetry and transitivity, we have Γ ⊢ A′ = Fun B C.

– Terms. • X = U: proved by the three last cases in the previous part.

• X ∈ Ne: by hypothesis Γ ⊢ t = R_{|Γ |} d : A; and by conversion Γ ⊢ t′ = t′ : A′, and Γ ⊢ t = R_{|Γ |} d : A′ from which we easily conclude Γ ⊢ t′ = R_{|Γ |} d : A′.

• X = Sing d X: we have to show Γ ⊢ t′ : A′ ∼ d′ ∈ {{d}}_{X}. From the hypothesis we know Γ ⊢ t : A ∼ d′ ∈ {{d}}_{X}, hence there exist B and a, such that Γ ⊢ t : {a}_{B}, and Γ ⊢ t : B ∼ d ∈ [X]. As Γ ⊢ t = t′ : B, we can use the i.h. and conclude Γ ⊢ t′ : B ∼ d ∈ [X].

• X = Fun X′ F: we need to show Γ ⊢ t′ : A′ ∼ f ∈ [Fun X F]. From the hypothesis we have Γ ⊢ A = Fun B C, and Γ ⊢ B ∼ X ∈ T ; by symmetry and transitivity we conclude Γ ⊢ A′ = Fun B C. Now we have to show Δ ⊢ App (t′ p^{i}) s : C (p^{i}, s) ∼ f · d ∈ [F d]. Which can be derived using the i.h. on Δ ⊢ C (p^{i}, s) = C (p^{i}, s), Δ ⊢ App (t p^{i}) s = App (t′ p^{i}) s : C (p^{i}, s), and Δ ⊢ App (t p^{i}) s : C (p^{i}, s) ∼ f· ∈ [F d].

Lemma 8 (Monotonicity). Let Δ ⩽^{i} Γ, then

1. if Γ ⊢ A ∼ X ∈ T , then Δ ⊢ A p^{i} ∼ X ∈ T ; and

2. if Γ ⊢ t : A ∼ d ∈ [X], then Δ ⊢ t p^{i} : A p^{i} ∼ d ∈ [X].

Proof. By induction on X ∈ T . We will show first the proof of the first point, and then the proof of the second point.

– Types: • U: the first part is trivial because U p^{i} = U for any i.

• Var x_{j} and App k v: by definition, and remark 1.

• Sing d X: by 2 we have Δ ⊢ A p^{i} = {a}_{A′} p^{i}, hence Δ ⊢ A p^{i} = {a p^{i}}_{A′ p^{i}}. And by i.h. we have Δ ⊢ a p^{i} : A′ p^{i} ∼ d ∈ [X].

• Fun X F: by the congruence of equality with respect to the application of substitutions, we know Δ ⊢ A p^{i} = Fun (A′ p^{i}) (B (p^{i} p, q)). By i.h. we have Δ ⊢ A′ p^{i} ∼ X. For the second part, let Θ ⩽^{j} Δ and Θ ⊢ s : (A′ p^{i}) p^{j} ∼ d ∈ [X]; then we have to prove Θ ⊢ B (p^{i} p, q) (p^{j}, s) ∼ F d; and that follows from the definition, because B (p^{i} p, q) (p^{j}, s) = B (p^{i+j}, s).

– Terms: • U: By the last three cases for the first part.

• Var x_{j} and App k v: The first part to show, namely Δ ⊢ A ∼ Var x_{i}, was shown in the previous point; for showing Δ ⊢ t p^{i} = R_{|Δ|} d : A, we use the same reasoning used in the previous paragraph.

• Sing d X: We have Δ ⊢ A p^{i} = {a p^{i}}_{A′ p^{i}} and by i.h. we have Δ ⊢ t p^{i} : A′ p^{i} ∼ d ∈ [X].

• Fun X F: For proving Δ ⊢ λt p^{i} : A p^{i} ∼ f ∈ [Fun X F], first we note that Δ ⊢ A p^{i} = Fun (A′ p^{i}) (B (p^{i+1}, q)). The second thing to show is that Θ ⊢ App ((λt p^{i}) p^{j}) s : B (p^{i+1}, q) (p^{j}, s) ∼ f · d ∈ [F d], for any Θ ⩽^{j} Δ, and Δ ⊢ s : A′ p^{j} ∼ d ∈ [X], which follows from the definition of Γ ⊢ λt : Fun A′ B ∼ f ∈ [Fun X F].

Lemma 9. Let Γ ⊢ A ∼ X ∈ T and Γ ⊢ t : A ∼ d ∈ [X], then

1. if X = X′ ∈ T , then Γ ⊢ A ∼ X′ ∈ T ; and

2. if d = d′ ∈ [X], then Γ ⊢ t : A ∼ d′ ∈ [X].

Proof. By induction on X = X′ ∈ T .

– U = U: trivial for the first part. The second part is proved in the first part of the following cases.

– X = X′ ∈ Ne: by definition of Ne, we know that R_{|Γ |} X = R_{|Γ |} X′ (this is syntactically equal), from that is trivial to deduce Γ ⊢ A = R_{|Γ |} X′. By definition [X] = Ne, then we can use the same reasoning as before: d = d′ ∈ Ne, hence Γ ⊢ a = R_{|Γ |} d : A imply Γ ⊢ R_{|Γ |} d = R_{|Γ |} d′ : A; by transitivity we have: Γ ⊢ a = R_{|Γ |} d′ : A.

– Sing d X = Sing d′ X′. By hypothesis, Γ ⊢ A = {a}_{A′}, Γ ⊢ A′ ∼ X, and also Γ ⊢ a : A′ ∼ d ∈ [X]. By i.h. we have Γ ⊢ A′ ∼ X, and Γ ⊢ a : A′ ∼ d′ ∈ [X]; by [X] = [X′] we conclude Γ ⊢ a : A′ ∼ d′ ∈ [X′]. Let e = e′ ∈ {{d}}_{X} and Γ ⊢ a : A ∼ e ∈ {{d}}_{X}, show Γ ⊢ a : A ∼ e′ ∈ {{d′}}_{X′}. By hypothesis we know Γ ⊢ A = {a′}_{A′}, and Γ ⊢ a′ : A′ ∼ d ∈ [X] and by i.h. we conclude Γ ⊢ a′ : A′ ∼ d′ ∈ [X′], because we have d = d′ ∈ [X] and X = X′ ∈ T .

– Fun X F = Fun X′ F′. By hypothesis, Γ ⊢ A = Fun A′ B, Γ ⊢ A′ ∼ X ∈ T , and hence by i.h. Γ ⊢ A′ ∼ X′ ∈ T . We need to prove Δ ⊢ B (p^{i}, s) ∼ F′ d ∈ T , where Δ ⩽^{i} Γ, and Δ ⊢ s : A p^{i} ∼ d ∈ [X]; that is proved by mean of the i.h. with Δ ⊢ B (p^{i}, s) ∼ F d ∈ T and Δ ⊢ s : A p^{i} ∼ d ∈ [X′]. Let Γ ⊢ t : A ∼ f ∈ ∏ X F, and f = f′ ∈ ∏ X F, show Γ ⊢ t : A ∼ f′ ∈ ∏ X′ F′. By hypothesis we know Γ ⊢ A = Fun A′ B, and

Δ ⊢ App (t p^{i}) s : B (p^{i}, s) ∼ f · d ∈ [F d]  (*)

for any Δ ⩽^{i} Γ and

Δ ⊢ s : A′ p^{i} ∼ d ∈ [X]  (**)

By i.h. on (**), we have Δ ⊢ s : A′ p^{i} ∼ d′ ∈ [X′]. And we also know that f · d = f′ · d ∈ [F d]; hence by i.h. on (*), we conclude Δ ⊢ App (t p^{i}) s : B (p^{i}, s) ∼ f′ · d ∈ [F′ d].

The following lemma plays a key role in the proof of soundness. It proves that if a term is related to some element in (some PER), then it is convertible to the reification of the corresponding element in the PER of normal forms.

Lemma 10. Let Γ ⊢ A ∼ X ∈ T , Γ ⊢ t : A ∼ d ∈ [X], and k ∈ Ne, then

1. Γ ⊢ A = R_{|Γ |} ⇓ X,

2. Γ ⊢ t = R_{|Γ |} ↓_{X} d : A; and

3. if for all Δ ⩽^{i} Γ, Δ ⊢ t p^{i} = R_{|Δ|} k : A p^{i}, then Γ ⊢ t : A ∼ ↑_{X} k ∈ [X].

Proof. By induction on X ∈ T . For organising better the proof we show the proofs for each point separately.

– Γ ⊢ A = R_{|Γ |} ⇓ X • X = U: trivial for the first part.

• X ∈ Ne: also trivial.

• X = Sing d X: by induction hypothesis we have Γ ⊢ A′ = R_{|Γ |} ⇓ X, and Γ ⊢ t = R_{|Γ |} ↓_{X} d : A′. By congruence we conclude Γ ⊢ {a}_{A′} = {R_{|Γ |} ↓_{X} d}_{R_{|Γ |} ⇓ X}.

• X = Fun X F: by i.h. we have Γ ⊢ A′ = R_{|Γ |} ⇓ X, and Δ ⊢ B (p^{i}, s) = R_{|Δ|} ⇓ F d, for any Δ ⩽^{i} Γ and Δ ⊢ s : A′ p^{i} ∼ d ∈ [X]. By ?? and i.h. on the third part we have Γ.A′ ⊢ q : A′ p ∼ ↑_{X} Var x_{|Γ |}. Hence we conclude Γ.A′ ⊢ B (p, q) = R_{|Γ.A′|} ⇓ F ↑_{X} Var x_{|Γ |}, hence Γ.A′ ⊢ B = R_{|Γ.A′|} ⇓ F ↑_{X} Var x_{|Γ |}, because (p, q) = id_{Γ.A′}. From this we conclude Γ ⊢ Fun A′ B = R_{|Γ |} Fun X F.

– Γ ⊢ t = R_{|Γ |} ↓_{X} d : A • d ∈ U: this is shown by the previous part.

• d ∈ [X], and X ∈ Ne: also trivial.

• d′ ∈ [Sing d X]: let Γ ⊢ A ∼ Sing d X, and (∗) Γ ⊢ t : A ∼ d′ ∈ Sing d X; show Γ ⊢ t = R_{|Γ |} ↓_{Sing d X} d′ : A. From (∗), we get Γ ⊢ A = {a}_{A′}, hence Γ ⊢ t = A : {a}_{A′}, and Γ ⊢ A′ : t ∼ d ∈ [X]; by i.h. in the last fact, we know Γ ⊢ t = R_{|Γ |} ↓_{X} d : A′, hence Γ ⊢ t = R_{|Γ |} ↓_{X} d : {t}_{A′}, and using conversion twice we conclude Γ ⊢ t = R_{|Γ |} ↓_{X} d : A.

• f ∈ [Fun X F]: let Γ ⊢ t : A ∼ f ∈ [Fun X F], show Γ ⊢ t = R_{|Γ |} ↓_{Fun X F} f : A. First note that Γ ⊢ q : A′ ∼ ↑_{X} Var x_{|Γ |}, by i.h. on the third part. Hence by definition of the logical relation: Γ.A′ ⊢ App (t p) q : B (p, q) ∼ f · ↑_{X} Var x_{|Γ |} ∈ [F ↑_{X} Var x_{|Γ |}]. Therefore by i.h. we conclude: Γ.A′ ⊢ App (t p) q = R_{|Γ.A|} ↓_{F ↑_{X} Var x_{|Γ |}} f · ↑_{X} Var x_{|Γ |} : B (p, q). By conversion we have Γ.A′ ⊢ App (t p) q = R_{|Γ.A|} ↓_{F ↑_{X} Var x_{|Γ |}} f · ↑_{X} Var x_{|Γ |} : B, and by congruence we have Γ ⊢ λ(App (t p) q) = λ(R_{|Γ.A|} ↓_{F ↑_{X} Var x_{|Γ |}} f · ↑_{X} Var x_{|Γ |}) : Fun A′ B; and by transitivity we conclude Γ ⊢ t = R_{|Γ |} ↓_{Fun X F} f : Fun A′ B.

– • X = U: we have to show Γ ⊢ t : A ∼ ↑_{U} k. the first part Γ ⊢ A = U, is obtained from the hypothesis. The second part Γ ⊢ t ∼ d ∈ T , is trivial from the hypothesis.

• X ∈ Ne: by hypothesis.

• X = Sing d X: we need to show Γ ⊢ t : A′ ∼ d ∈ [X]. From the hypothesis we know: Γ ⊢ t : {a}_{A′} and Γ ⊢ a : A′ ∼ d ∈ [X]; hence we have Γ ⊢ a = t : A′. By lemma 7, we conclude Γ ⊢ t : A′ ∼ d ∈ [X].

• X = Fun X F: let Δ ⩽^{i} Γ, and (∗) Δ ⊢ s : A′ p^{i} ∼ d′ ∈ [X]. We have to show Δ ⊢ App t p^{i} s : B (p^{i}, s) ∼ ↑_{F d′} App d ↓_{X} d′. From (∗), using the i.h., we have Δ ⊢ s = R_{|Δ|} ↓_{X} d′ : A′ p^{i}. Hence we can use that and the hypothesis (after lifting) to deduce Δ ⊢ App (t p^{i}) s = App ((R_{|Γ |} d) p^{i}) (R_{|Δ|} (↓_{X} d′)) : B (p^{i}, s). The r.h.s. of the equality is equal by definition to R_{|Δ|} App d ↓_{X} d′; hence using the i.h. we conclude Δ ⊢ App (t p^{i}) s : B (p^{i}, s) ∼ ↑_{F d′} App d ↓_{X} d′ ∈ [F d′].

In order to finish the proof of soundness we have to prove that each welltyped term (and each well-formed type) is logically related to its denotation; with that aim we extend the definition of logical relations to substitutions and prove the fundamental theorem of logical relations.

Definition 19 (Logical relation for substitutions).

– Γ ⊢ σ : ⋄ ∼ d ∈ 1.

– Γ ⊢ (σ, t) : Δ.A ∼ (d, d′) ∈ ∐ X (d ↦ [F d]) iff Γ ⊢ σ : Δ ∼ d ∈ X and Γ ⊢ t : A σ ∼ d′ ∈ [F d].

By the way this relation is defined, the counterparts of 7, 8 and 9 are easily proved by induction on the co-domain of the substitutions.

Remark 11. If γ = δ : Γ → Δ, and Γ ⊢ γ : Δ ∼ d ∈ X, then Γ ⊢ δ : Δ ∼ d ∈ X.

Remark 12. If Δ ⊢ δ : Γ ∼ d ∈ [[Γ]], then for any Θ ⩽^{i} Δ, Θ ⊢ δ p^{i} : Γ ∼ d ∈ [[Γ]].

Remark 13. If Γ ⊢ γ : Δ ∼ d ∈ X, and d = d′ ∈ X, then Γ ⊢ γ : Δ ∼ d′ ∈ X.

Theorem 3 (Fundamental theorem of logical relations). Let Δ ⊢ δ : Γ ∼ d ∈ [[Γ]].

1. if Γ ⊢ A, then Δ ⊢ A δ ∼ [[A]]d ∈ T ;

2. if Γ ⊢ t : A, then Δ ⊢ t δ : A δ ∼ [[t]]d ∈ [[[A]]d]; and

3. if Γ ⊢ γ : Θ then Δ ⊢ γ δ : Θ ∼ [[γ]]d ∈ [[Θ]].

Proof. By mutual induction on the derivations. We note that for terms we show only the cases when the last rule used was the introductory rule, or the rule for introducing elements in singletons; the case when the last rule used was the conversion rule, we can conclude by i.h., and lemma 7.

– Types:

• ⋄ ⊢ U: trivial using 7 and 9.

• Γ ⊢ Fun A B: we will show Θ ⊢ B (δ p^{i}, s) ∼ [[B]](d, e) ∈ T , for any Θ ⩽^{i} Δ, and (∗) Θ ⊢ s : (A δ) p^{i} ∼ e ∈ [[[A]]d]. By 12 we have Θ ⊢ δ p^{i} : Γ ∼ d ∈ [[Γ]], and from (∗) we conclude Θ ⊢ (δ p^{i}, s) : Γ.A ∼ (d, e), hence we can use the i.h. on Γ.A ⊢ B and the rest is by 7 and 9.

• Γ ⊢ A (by Γ ⊢ A : U): by i.h. Δ ⊢ A δ : U ∼ [[A]]d ∈ U.

• Γ ⊢ {t}_{A}: by i.h. Δ ⊢ t δ : A δ ∼ [[t]]d ∈ [[A]]d.

• Γ ⊢ A σ: by i.h. Δ ⊢ σ δ : Θ ∼ [[σ]]d ∈ [[Θ]]; and, again by i.h., Δ ⊢

A σ δ ∼ [[A]]([[σ]]d) ∈ T .

– Terms:

• Γ ⊢ Fun A B : U and Γ ⊢ {t}_{A} : U are the same as before.

• Γ ⊢ λt : Fun A B: we will show Θ ⊢ t (δ p^{i}, s) : B (δ p^{i}, s) ∼ [[λt]]d · e ∈ [[[B]](d, e)], for any Θ ⩽^{i} Δ, and (∗) Θ ⊢ s : (A δ) p^{i} ∼ e ∈ [[[A]]d]. By 12 we have Θ ⊢ δ p^{i} : Γ ∼ d ∈ [[Γ]], and from (∗) we conclude Θ ⊢ (δ p^{i}, s) : Γ.A ∼ (d, e), hence we can use the i.h. on Γ.A ⊢ t : B and the rest is by 7 and 9.

• Γ ⊢ App t r : B (id_{Γ} , r): by i.h. we have Δ ⊢ r δ : A δ ∼ [[r]]d ∈ [[[A]]d] and, Δ ⊢ t δ : Fun A B δ ∼ [[t]]d ∈ [[[Fun A B]]d]; hence Δ ⊢ App t δ r δ : B (id_{Δ}, r δ) ∼ [[t]]d · [[r]]d ∈ [[[B]](d, [[r]]d)]. The rest is again using 7 and 9.

• Γ.A ⊢ q : A p: by remark 4 we know δ = (γ, t), for some γ and t; hence d = (e, e′), Δ ⊢ γ : Γ ∼ e ∈ [[Γ]], and Δ ⊢ t : A δ ∼ e′ ∈ [[[A]]e]. Now we know that q (γ, t) = t, and [[A p]](e, e′) = [[A]]e. Hence we are done by 7 and 9.

• Γ ⊢ t σ : A σ: by i.h. Δ ⊢ σ δ : Θ ∼ [[σ]]d ∈ [[Θ]]; and, again by i.h., Δ ⊢ t σ δ : A σ δ ∼ [[t]]([[σ]]d) ∈ [[[A]]([[σ]]d)].

• Γ ⊢ t : {a}_{A}: by i.h. we have Δ ⊢ t δ : A δ ∼ [[t]]d ∈ [[[A]]d], and by

soundness [[t]]d = [[a]] ∈ [[[A]]d], hence Δ ⊢ t δ : A δ ∼ [[a]]d ∈ [[[A]]d].

– Substitutions:

• Γ ⊢ t σ : A σ: by i.h. Δ ⊢ σ δ : Θ ∼ [[σ]]d ∈ [[Θ]]; and, again by i.h., Δ ⊢ t σ δ : A σ δ ∼ [[t]]([[σ]]d) ∈ [[[A]]([[σ]]d)].

• Γ ⊢ id_{Γ} : Γ: show that Δ ⊢ id_{Γ} δ : Γ ∼ [[id_{Γ}]]d ∈ [[Γ]]. First note that id_{Γ} δ = δ and [[id_{Γ}]]d = d, hence using 11 and 13 we conclude what was needed.

• Γ ⊢ ⟨⟩ : ⋄: Again we use 11 and 13 to conclude .

• Γ ⊢ (γ, t) : Θ.A: we use the i.h. on Γ ⊢ γ : Θ and Γ ⊢ t : A γ; so we have Δ ⊢ γ δ : Θ ∼ [[γ]]d ∈ [[Θ]], and Δ ⊢ t δ : (A γ) δ ∼ [[t]]d ∈ [[[A γ]]d]. From that we get that ([[γ]]d, [[t]]d) ∈ ∐ [[Θ]] (e ↦ [[[A γ]]e]). Finally (γ, t) δ = (γ δ, t δ) and [[(γ, t)]]d = ([[γ]]d, [[t]]d), hence we use 11 and 13 and we are done.

• Γ ⊢ γ′ γ : Θ′: by i.h. Δ ⊢ γ δ : Γ ∼ [[γ]]d ∈ [[Γ]], and using this we conclude by i.h. Δ ⊢ γ′ (γ δ) : Θ′ ∼ [[γ′]]([[γ]]d) ∈ [[Θ′]]. The rest is by 11 and 13.

• Γ.A ⊢ p : Γ: by remark 4 we know δ = (γ, t), for some γ and t; hence d = (e, e′), and Δ ⊢ γ : Γ ∼ e ∈ [[Γ]]. Finally, p (γ, t) = γ, and [[p]](e, e′) = e.

At this point we have all the ingredients to define a normalisation algorithm for our calculus. First we define recursively on the structure of contexts an element of D, which is related with the identity substitution of that context; then we use that value for calculating the semantics of well-typed term t : A (resp. well-formed type A); by the last theorem the value of t is in the PER corresponding to the value of A (resp. the value of A is in T ), and is related to t (resp. to A). Then we can use the key lemma 10 and conclude that t (resp. A) is provable equal to the reification of the normalised value of t (resp. A).

Definition 20. We define ρ_{Γ} = P_{Γ} ⊤, where

P_{⋄} d = d
P_{Γ.A} d = (d′, ↑_{[[A]]d′} Var x_{n})  where n = |Γ |, and d′ = P_{Γ} d.

Then Γ ⊢ id_{Γ} : Γ ∼ ρ_{Γ} ∈ [[Γ]] for Γ ∈ Ctx.

Definition 21 (Normalisation algorithm). Let Γ ⊢ A, and Γ ⊢ t : A.

nbe_{Γ} (A) = R_{|Γ |} ⇓[[A]]ρ_{Γ}
nbe_{Γ}^{A}(t) = R_{|Γ |} ↓_{[[A]]ρ_{Γ}} [[t]]ρ_{Γ}

If Γ, and A are clear from the context, then we will omit them and write nbe(A), and nbe(t), respectively.

Remark 14. Let Γ ⊢ A, and Γ ⊢ t : A, then

1. by fundamental theorem of logical relations (and lemma 7), – Γ ⊢ A ∼ [[A]]ρ_{Γ} ∈ T ; and

– Γ ⊢ t : A ∼ [[t]]ρ_{Γ} ∈ [[[A]]ρ_{Γ}],

2. then it is immediate using lemma 10, that – Γ ⊢ A = nbe(A), and

– Γ ⊢ t = nbe(t) : A.

Remark 15. By expanding the definitions, we easily check

1. nbe_{Γ} (Fun A B) = Fun (nbe_{Γ} (A)) (nbe_{Γ.A}(B)), and

2. nbe_{Γ} ({a}_{A}) = {nbe_{Γ}^{A}(a)}_{nbe_{Γ} (A)}.

Corollary 3. If Γ ⊢ A, and Γ ⊢ A′, then we can decide Γ ⊢ A = A′. Also if Γ ⊢ t : A, and Γ ⊢ t′ : A, we can decide Γ ⊢ t = t′ : A.

Corollary 4 (Injectivity of Fun and of { } ). If Γ ⊢ Fun A B = Fun A′ B′, then Γ ⊢ A = A′, and Γ.A ⊢ B = B′. Also Γ ⊢ {t}_{A} = {t′}_{A′}, then Γ ⊢ A = A′, and Γ ⊢ t = t′ : A.

Calculus with Proof-Irrelevance.

Logical relations

Definition 22.

– Γ ⊢ A ∼ Sum(X, F), iff Γ ⊢ A = Σ A′ B′, and Γ ⊢ A′ ∼ X, and for all Δ ⩽^{i} Γ, and Δ ⊢ s : A′ p^{i} ∼ d ∈ [X], Δ ⊢ B′ (p^{i}, s) ∼ F d.

– Γ ⊢ t : A ∼ d ∈ [Sum(X, F)], iff Γ ⊢ A = Σ A′ B′, and Γ ⊢ fst t : A′ ∼ p^{∗} d ∈ [X], and Γ ⊢ snd t : B′ (id_{Γ} , fst t) ∼ q^{∗} d ∈ [F p^{∗} d].

– Γ ⊢ A ∼ Nat, iff Γ ⊢ A = Nat.

– Γ ⊢ t : A ∼ d ∈ [Nat], iff Γ ⊢ A ∼ Nat, and for all Δ ⩽^{i} Γ, Δ ⊢ t p^{i} = R_{|Δ|} d : A p^{i}.

– Γ ⊢ A ∼ N_{n}, iff Γ ⊢ A = N_{n}.

– Γ ⊢ t : A ∼ d ∈ [N_{n}], iff Γ ⊢ A ∼ N_{n}, and for all Δ ⩽^{i} Γ, Δ ⊢ t p^{i} = R_{|Δ|} d : A p^{i}.

– Γ ⊢ A ∼ Prf(X) ∈ T , iff Γ ⊢ A = Prf A′, and Γ ⊢ A′ ∼ X ∈ T .

– Γ ⊢ t : A ∼ d ∈ [Prf(X)], iff Γ ⊢ A ∼ Prf(X).

Lemma 11. 1. nbe_{Γ} (Σ A B) = Σ nbe_{Γ} (A) nbe_{Γ.A}(B);

2. nbe_{Γ}^{Σ A B}((t, b)) = (nbe_{Γ}^{A}(t), nbe_{Γ}^{B (id,t)}(b));

3. nbe(suc(t)) = suc(nbe(t)).

4. nbe(Prf A) = Prf nbe(A).

Corollary 5 (). If Γ ⊢ Σ A B = Σ A′ B′, then Γ ⊢ A = A′, and Γ.A ⊢ B = B′.

5 Type-checking algorithm

In this section we define three predicates that represent algorithms for checking the well formation of contexts in normal form, the derivability of a type under a certain context, the typing of a normal form, and a partial function from contexts and neutral terms to types, that represents the algorithm for inferring types of neutral terms. We implemented them in Haskell (see the appendix B).

The algorithm is similar to previous ones [14, 3], in that it proceeds by analysing the possible types for each normal form, and succeeds only if the type corresponds to the type corresponding to the type of the introductory rule of the term. The only difference is introduced by the presence of singleton types; now we should take into account that a normal form can also have a singleton as its type.

This situation can be dealt in two possible ways; either one check that the deepest tag of the normalised type (see 24) has the form of the type of the introductory rule; or one add a rule for checking any term against singleton types. The first approach requires to have more rules (this is due to the combination of singletons and a universe). We take the second approach, which requires to compute the eta-long normal form of the type before type-checking. We also note that the proof of completeness is more involved, because now the algorithm is not only driven by the term being checked, but also by the type.

In both cases it is crucial to have a normalisation function with the following properties.

Definition 23 (Properties for normalisation).

1. nbe({a}_{A}) = {nbe(a)}_{nbe(A)}, and nbe(Fun A B) = Fun nbe(A)nbe(B) ;

2. nbe_{Γ} (A) = nbe_{Γ} (B) if and only if Γ ⊢ A = B, and nbe_{Γ}^{A}(t) = nbe_{Γ}^{A}(t′), if and only if Γ ⊢ t = t′ : A.

Notation. In this section, we fix C for a context where all the types are in normal form; V, V′, W, v, v′, w ∈ Nf , and k ∈ Ne. For obtaining the deepest tag, we define an operation on types, which is essentially the same as the one defined in [8]

Definition 24 (Singleton’s tag).

\overline{V} = \begin{cases}\overline{W} & if V ≡ \{w\}_{W} \\ V & otherwise. \end{cases}

The predicates for type-checking are defined mutually inductively, together with the function for inferring types.

Definition 25 (Type-checking and type-inference). Contexts Γ ⇐.

\overline{⋄ ⇐} \frac{Γ ⇐  Γ ⇐ V}{Γ.V ⇐}

Types Γ ⇐ V. We presuppose Γ ⊢.

\overline{Γ ⇐ U} \frac{Γ ⇐ V  Γ.V ⇐ W}{Γ ⇐ Fun V W} \frac{Γ ⇐ V  Γ ⊢ v ⇐ nbe(V)}{Γ ⇐ \{v\}_{V}} \frac{Γ ⊢ k ⇐ U}{Γ ⇐ k}

Terms Γ ⊢ v ⇐ V. We presuppose Γ ⊢ V, and V in η-long normal form with respect to Γ.

\frac{Γ ⊢ V ⇐ U  Γ.V ⊢ W ⇐ U}{Γ ⊢ Fun V W ⇐ U}  \frac{Γ.V ⊢ v ⇐ W}{Γ ⊢ λv ⇐ Fun V W}

\frac{Γ ⊢ V ⇐ U  Γ ⊢ v ⇐ nbe(V)}{Γ ⊢ \{v\}_{V} ⇐ U}  \frac{Γ ⊢ v ⇐ V′  Γ ⊢ v′ = v : V′}{Γ ⊢ v ⇐ \{v′\}_{V′}}

\frac{Γ ⊢ k ⇒ V′  Γ ⊢ \overline{V′} = V}{Γ ⊢ k ⇐ V} V ≢ \{w\}_{W}

Type inference Γ ⊢ k ⇒ V. We presuppose Γ ⊢.

\overline{Γ.A_{i}…. A_{0} ⊢ q p^{i} ⇒ nbe(A_{i} p^{i+1})} \frac{Γ ⊢ k ⇒ V  Γ ⊢ \overline{V} = Fun V′ W  Γ ⊢ v ⇐ V′}{Γ ⊢ App k v ⇒ nbe(W (id, v))}

Theorem 4 (Correctness of type-checking).

1. If Γ ⇐, then Γ ⊢.

2. If Γ ⇐ V, then Γ ⊢ V.

3. If Γ ⊢ v ⇐ V, then Γ ⊢ v : V.

4. If Γ ⊢ k ⇒ V, then Γ ⊢ k : V.

Proof. By simultaneous induction on Γ ⇐, Γ ⇐ V, and Γ ⊢ v ⇐ A.

– Contexts: • For the empty context the proof is trivial: the derivation is ⋄ ⊢.

• For the case of an extension, we know Γ ⇐, and also Γ ⇐ V; hence by i.h. we have derivations with conclusions Γ ⊢, and Γ ⊢ V, so we can derive Γ.V ⊢ .

– Types:

• the case for U is trivial.

• the case for Fun V W is also obtained directly from the derivations we get using the i.h. on Γ ⇐ V, and Γ.V ⇐ W; and use them for deriving Γ ⊢ Fun V W

• for {v}_{V}, we can apply the same reasoning as before: by i.h. on Γ ⇐ V, and Γ ⊢ v ⇐ nbe(V) we know that there are, respectively, derivations with conclusions Γ ⊢ V, and Γ ⊢ v : V; from which we can conclude Γ ⊢ {v}_{V}

• here we’ll consider the three cases when V is a neutral term, because the reasoning is the same. By i.h. on Γ ⊢ V ⇐ U, we have a derivation with conclusion Γ ⊢ V : U; hence we use u-el.

– Terms:

• let V = U, and v = Fun V′ W. By i.h. Γ ⊢ V′ : U, and Γ.V′ ⊢ W : U, and using both derivations we can derive Γ ⊢ Fun V W : U.

• consider V = U, and v = {v′}_{V′}. by i.h. on Γ ⊢ V′ ⇐ U, and Γ ⊢ v′ ⇐ nbe(V), we have Γ ⊢ V : U, and Γ ⊢ v′ : nbe(V), and using conversion we derive Γ ⊢ v′ : V; and these are the premises we need to show Γ ⊢ {v′}_{V} : U.

• V = Fun V′ W, and v = λv′: we have Γ.V′ ⊢ v′ ⇐ W. From this we can conclude by i.h. Γ.V′ ⊢ v′ : W; and this is the key premise for concluding Γ ⊢ λv′ : Fun V′ W.

• V = {w}_{W}: by hypothesis we know Γ ⊢ w : W, and Γ ⊢ v ⇐ W, and Γ ⊢ w = v : W; by the i.h. on the second one we get Γ ⊢ v : W; then we can conclude using sing-i.

• v = k ∈ Ne, and V ≢ {w}_{W}: let Γ ⊢ k ⇒ V′, then we distinguish the cases when V′ is a singleton, and when V′ is not a singleton. In the later case, the derivation is obtained directly from the correctness of typeinference. In the first case we use the rule sing-el, with the derivation obtained by i.h. and then we conclude with conversion.

– Inference:

• for q p^{i}, if i = 0, then we use hyp, and conversion; if i > 0, then we have a derivation with conclusion Γ ⊢ q : A_{i} p, and clearly Γ ⊢ p^{i} : Γ.A_{i} ….A_{0}, hence by subs-term, we have Γ.A_{i} ….A_{0} ⊢ q p^{i} : A_{i} p^{i+1}, we conclude by the fact Γ ⊢ nbe(A) = A, and conversion.

• by i.h. we have derivations with conclusions Γ ⊢ k : V′, with \overline{V′} = Fun V W, hence we have a derivation Γ ⊢ k : Fun V W (using sing-el if necessary) and Γ ⊢ v : V, hence by the rule fun-el, we have Γ ⊢ App k v : W (id, v). We conclude with conversion and the fact that Γ ⊢ A = nbe(A).

In order to prove completeness we define a lexicographic order on pairs of terms and types, in this way we can make induction over the term, and the type.

Definition 26. Let v, v′ ∈ Nf , and A, A′ ∈ Type(Γ), then (v, A) ≺ (v′, A′) is the lexicographic order on Nf × Type(Γ). The corresponding orders are v ≺ v′ iff v is an immediate sub-term of v′; and A ≺^{Γ} A′, iff nbe(A′) ≡ {w}_{nbe(A)}.

Theorem 5 (Completeness of type-checking).

1. If C ⊢, then C ⇐.

2. If Γ ⊢ V, then Γ ⇐ V.

3. If Γ ⊢ v : A, then Γ ⊢ v ⇐ nbe(A).

4. If Γ ⊢ k : A, and Γ ⊢ k ⇒ V′, then Γ ⊢ \overline{nbe(A)} = \overline{V′}.

Proof. We prove simultaneously all the points. The first two points are by induction on the structure of the context, and the type, respectively. In the last two points we use well-founded induction on the order ≺.

– Contexts:

• the case for ⋄ is trivial;

• for C = C′.V, we have by i.h. C′ ⇐, and C′ ⇐ V; hence C′.V ⇐.

– Types:

• U, trivial.

• Γ ⊢ Fun V′ W; by inversion we know Γ ⊢ V′, and Γ.V′ ⊢ W; hence by i.h. we have respectively Γ ⇐ V′, and Γ.V′ ⇐ W.

• V = {v}_{V′}: by inversion we have Γ ⊢ V′, and Γ ⊢ v : nbe(V′), hence by i.h. we have both Γ ⇐ V′, and Γ ⊢ v ⇐ V′.

• Γ ⊢ k, we have to show Γ ⇐ k. By lemma ??, we know Γ ⊢ k : U; hence

by i.h. we have Γ ⊢ k ⇒ A, and Γ ⊢ A = U, hence Γ ⊢ k ⇐ U.

– Terms: We omit the trivial cases, e.g. (U, A); we have re-arranged the order of the cases for the sake of clarity.

• v = Fun V′ W:

1. either Γ ⊢ A = U, Γ ⊢ V′ : U, and Γ.V′ ⊢ W : U; hence, by i.h. we know both Γ ⊢ V′ ⇐ U, and Γ.V′ ⊢ W ⇐ U; hence we can conclude Γ ⊢ Fun V W ⇐ U.

2. Or Γ ⊢ A = {a}_{A′}, Γ ⊢ v : A′, and Γ ⊢ v = a : A′, hence by i.h. we know Γ ⊢ v ⇐ nbe(B), by conversion we also have and transitivity of the equality Γ ⊢ nbe(a) = v : nbe(B), hence Γ ⊢ v ⇐ {nbe(a)}_{nbe(B)}.

• v = {v′}_{V}:

1. Γ ⊢ V : U, and Γ ⊢ v′ : V. From those derivations we have by i.h. Γ ⊢ V ⇐ U, and Γ ⊢ v′ ⇐ nbe(V), respectively; from which we conclude Γ ⊢ {v′}_{V} ⇐ U

2. Γ ⊢ A = {a}_{A′}, with Γ ⊢ v : A′, and Γ ⊢ v = a : A′, hence by i.h. we know Γ ⊢ v ⇐ nbe(B). We can also derive Γ ⊢ nbe(a) = v : nbe(B), hence Γ ⊢ v ⇐ {nbe(a)}_{nbe(B)}.

• v = λv′

1. Γ ⊢ V = Fun A′ B, and Γ.A′ ⊢ v′ : B; from this we can conclude Γ.nbe(A′) ⊢ v′ : B by i.h. we get Γ.nbe(A′) ⊢ v′ ⇐ nbe(B); hence Γ ⊢ λv′ ⇐ Fun nbe(A′) nbe(B′).

2. Or Γ ⊢ A = {a}_{A′}, Γ ⊢ v : A′, and Γ ⊢ v = a : A′, hence by i.h. we know Γ ⊢ v ⇐ nbe(B), by conversion we also have and transitivity of the equality Γ ⊢ nbe(a) = v : nbe(B), hence Γ ⊢ v ⇐ {nbe(a)}_{nbe(B)}.

• v ∈ Ne: then we do case analysis on nbe(A).

1. If nbe(A) = {w}_{W}, then by soundness of nbe( ), and conversion we have Γ ⊢ k : {w}_{W}; and by inversion of singletons we have Γ ⊢ k : W, and also Γ ⊢ k = w : W (∗). Clearly (k, W) ≺ (k, A), hence we can apply the inductive hypothesis and conclude Γ ⊢ k ⇐ W; from that and (∗), we conclude Γ ⊢ k ⇐ {w}_{W}, i.e., Γ ⊢ k ⇐ nbe(A).

2. If V ≢ \{w\}_{W}, then \overline{V} ≡ V. We use the last clause for concluding Γ ⊢ k ⇐ nbe(A); but we need to show that if Γ ⊢ k ⇒ V′, then Γ ⊢ \overline{V} = \overline{V′}; we show this in the next point.

– Inference: let Γ ⊢ k : A, Γ ⊢ k ⇒ V′, and V = nbe(A). Show Γ ⊢ \overline{V} = \overline{V′}.

• let us consider first the case when V = {w}_{W}; by inversion we have derivations Γ ⊢ k : W, and Γ ⊢ k = w : W. Hence by i.h. we know that Γ ⊢ \overline{V′} = \overline{W}, and \overline{W} = \overline{\{w\}_{W}}.

• Now we consider the case when V is not a singleton, and k = q p^{i}; this case is trivial because by inversion we know that Γ ⊢ V = nbe((Γ!i) p^{i+1}).

• the last case to consider is k = App k′ v and V not a singleton. By inversion we know Γ ⊢ App k v : B (id, v), and Γ ⊢ k : Fun A B, hence Γ ⊢ k : Fun nbe(A) nbe(B), and Γ ⊢ v : A, hence Γ ⊢ v : nbe(A). By i.h. we know that if Γ ⊢ k ⇒ V′, then \overline{V′} = Fun nbe(A) nbe(B), and also Γ ⊢ v ⇐ nbe(A). Hence we can conclude Γ ⊢ App k v ⇒ nbe(nbe(B) (id, v)). And Γ ⊢ nbe(nbe(B) (id, v)) = nbe(B (id, v)) (using the derived rule shown in example ?? together with the correctness of the nbe( ) algorithm).

Calculus with Proof-Irrelevance.

We give the additional rules for type-checking, and type-inference algorithms for the new constructs of the calculus. We show that the type-checking algorithm is correct and complete for the calculus without prf-tm.

Definition 27 (Type-checking and type-inference).

Types Γ ⇐ V. We presuppose Γ ⊢.

\frac{Γ ⇐ V  Γ.V ⇐ W}{Γ ⇐ Σ V W} \overline{Γ ⇐ Nat}

\overline{Γ ⇐ N_{n}} \frac{Γ ⇐ V}{Γ ⇐ Prf V}

Terms Γ ⊢ v ⇐ V.

\frac{Γ ⊢ V ⇐ U Γ.V ⊢ W ⇐ U}{Γ ⊢ Σ V W ⇐ U}

\frac{Γ ⊢ v ⇐ V Γ ⊢ v′ ⇐ nbe(W (id_{Γ} , v))}{Γ ⊢ (v, v′) ⇐ Σ V W}

\overline{Γ ⊢ Nat ⇐ U}

\overline{Γ ⊢ zero ⇐ Nat} \frac{Γ ⊢ v ⇐ Nat}{Γ ⊢ suc(v) ⇐ Nat}

\overline{Γ ⊢ N_{n} ⇐ U}

\frac{i < n}{Γ ⊢ c_{i}^{n} ⇐ N_{n}} \frac{Γ ⊢ v ⇐ V}{Γ ⊢ [v] ⇐ Prf V}

Type inference Γ ⊢ k ⇒ V. We presuppose Γ ⊢.

\frac{Γ ⊢ k ⇒ Σ V W}{Γ ⊢ fst k ⇒ V} \frac{Γ ⊢ k ⇒ Σ V W}{Γ ⊢ snd k ⇒ nbe(W (id_{Γ} , fst k))}

\frac{Γ ⊢ k ⇒ Prf V′ Γ.V′ ⊢ v ⇐ nbe(V p)}{Γ ⊢ v where^{V} k ⇒ Prf V}

\frac{Γ.Nat ⇐ V  Γ ⊢ k ⇒ Nat  Γ ⊢ v ⇐ nbe(V (id_{Γ} , zero)) Γ.Nat ⊢ v′ ⇐ nbe(Fun V (id, q) V (id, suc(q p)))}{Γ ⊢ natrec(V, v, v′, k) ⇒ nbe(V (id, k))}

\frac{Γ.N_{n} ⇐ V  Γ ⊢ k ⇒ N_{n}  Γ ⊢ v_{i} ⇐ nbe(V (id_{Γ} , c_{i}^{n}))}{Γ ⊢ elim^{n}(V, v_{0}, …, v_{n−1}, k) ⇒ nbe(V (id, k))}

Theorem 6. The type-checking algorithm is correct with respect to the calculus with prf-tm.

Proof. By simultaneous induction on the derivability of the type-checking judgements.

Corollary 6. The type-checking algorithm is sound with respect to the calculus without prf-tm.

Lemma 12. The type-checking algorithm is complete with respect to the calculus with prf-tm if we add the axiom Γ ⊢ O ⇐ Prf V .

Proof. We need to consider the typing rules introduced in this section.

– let Γ ⊢ Prf V, then by inversion we know Γ ⊢ V, hence by i.h. Γ ⇐ V, and we are done.

– if Γ ⊢ A : [v], we know by inversion Γ ⊢ A′ : v, and Γ ⊢ A = Prf A′, and by i.h. we have Γ ⊢ v ⇐ nbe(A′), and by 15 we know nbe(A) ≡ Prf nbe(A′), hence Γ ⊢ [v] ⇐ nbe(A) (we don’t consider the case when by inversion we have that Γ ⊢ A = {a}_{A′}, for it is not different to other similar cases).

– if Γ ⊢ O : A, then we use the inversion lemma and we conclude by using the axiom considered in this lemma, and 15.

Remark 16. If we consider context, types, and terms where O does not occur, then we can drop the axiom for prf-ax. Indeed, we prove by inspecting the typechecking rules that we never normalise a term in the type-checking algorithms (except for deciding equalities); hence we do not need to type-check O if it does not occur in the term being checked.

Corollary 7. The type-checking algorithm is correct (by Cor. 2) and complete (by last remark) with respect to the calculus without prf-tm.

6 Conclusion

The main contributions of the paper are the definition of a correct and complete type-checking algorithm, and the simplification of the NbE algorithm for a calculus with singletons, one universe, and proof-irrelevant types. The type-checker is based on the NbE algorithm which is used to decide equality and to prove the injectivity of the type constructors. We emphasise that the type-checking algorithm is modular with respect to the normalisation algorithm. All the results can be extended to a calculus with annotated lambda abstractions, yielding a type-checking algorithm for terms not necessarily in normal forms.

The full version [5] extends this work by sigma-types and data types and an implementation of the type checker in Haskell.

6.1 Future work

Mention Sozeau’s work, use Prf A to model uniformity (as in [?,?], this was suggested by Baas), using the same technique for adding more equalities (this is Miguel thesis, hopefully), relation with program extraction facilities (adding Prop?), how to handle functions defined by pattern-matching (cite the calculus of definitions by Thierry?). Prove that the model is a CwF(?).

References

1. Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for Martin-Löf type theory with one universe. In: Fiore, M., ed., Proc. of the 23rd Conf. on the Mathematical Foundations of Programming Semantics (MFPS XXIII), volume 173 of Electr. Notes in Theor. Comp. Sci. Elsevier (2007), 17–39

2. Abel, A., Coquand, T., Dybjer, P.: 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). IEEE Computer Soc. Press (2007), 3–12

3. Abel, A., Coquand, T., Dybjer, P.: On the algebraic foundation of proof assistants for intuitionistic type theory. In: Garrigue, J., Hermenegildo, M. V., eds., Proc. of the 9th Int. Symp. on Functional and Logic Programming, FLOPS 2008, volume 4989 of Lect. Notes in Comput. Sci. Springer-Verlag (2008), 3–13

4. Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic βη-conversion test for Martin-Löf type theory. volume 5133 of Lect. Notes in Comput. Sci. Springer-Verlag (2008), 29–56

5. Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance (full version) (2009). Available on http://www.tcs.ifi.lmu.de/˜ abel/singleton.pdf

6. Abramsky, S., Jung, A.: Handbook of Logic in Computer Science, chapter Domain Theory. Oxford University Press (1994), 1–168

7. Aehlig, K., Joachimski, F.: Operational aspects of untyped normalization by evaluation. Math. Struct. in Comput. Sci. 14 (2004) 587–611

8. Aspinall, D.: Subtyping with singleton types. In: Pacholski, L., Tiuryn, J., eds., Computer Science Logic, 8th Int. Wksh., CSL ’94, volume 933 of Lect. Notes in Comput. Sci. Springer-Verlag (1995), 1–15 9. Berardi, S.: About the sets-as-propositions embedding of HOL in CC (2004)

10. Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed λcalculus. In: Proc. of the 6th IEEE Symp. on Logic in Computer Science (LICS’91). IEEE Computer Soc. Press (1991), 203–211

11. Blass, A.: The interaction between category theory and set theory. Contemporary Mathematics (1984)

12. Bruijn, N. G. d.: Some extensions of Automath : the AUT-4 family (1994)

13. Cartmell, J.: Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic (1986) 32–209

14. Coquand, T.: An algorithm for type-checking dependent types. Science of Computer Programming 26 (1996) 167–177

15. Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundam. Inform. 65 (2005) 113–134

16. Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic 65 (2000) 525–549

17. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proc. of the 7th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP ’02), volume 37 of SIGPLAN Notices. ACM Press (2002), 235–246

18. Grothendieck, A.: Séminaire de Géométrie Algébrique du Bois Marie - 1963-64 - Théorie des topos et cohomologie étale des schémas, volume 269 of Lecture notes in mathematics. Springer-Verlag, Berlin; New York (1972)

19. Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the Association of Computing Machinery 40 (1993) 143–184

20. INRIA: The Coq Proof Assistant, Version 8.1. INRIA (2007). http://coq.inria.fr/ 21. Lee, D. K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard

ML. In: Hofmann, M., Felleisen, M., eds., Proc. of the 34th ACM Symp. on Principles of Programming Languages, POPL 2007. ACM Press (2007), 173–184

22. Martin-Löf, P.: An Intuitionistic Theory of Types. Technical report (1972)

23. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)

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

25. McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T., eds., 5th Int. School on Advanced Functional Programming, AFP 2004, Revised Lectures, volume 3622 of Lect. Notes in Comput. Sci. Springer-Verlag (2005), 130–170

26. Mitchell, J. C., Moggi, E.: Kripke-Style models for typed lambda calculus. In: LICS (1987), 303–314

27. Nordström, B., Petersson, K., Smith, J. M.: Programming in Martin Löf’s Type Theory: An Introduction. Clarendon Press, Oxford (1990)

28. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden (2007)

29. Sambin, G., Valentini, S.: Building up a toolbox for Martin-Löf’s type theory: subset theory. In: Twenty-five years of constructive type theory (Venice, 1995), volume 36, chapter Oxford Logic Guides. Oxford University Press, New York (1998), 221–244

30. Shankar, N., Owre, S.: Principles and Pragmatics of Subtyping in PVS. In: WADT ’99: Selected papers from the 14th International Workshop on Recent Trends in Algebraic Development Techniques. Springer-Verlag, London, UK (2000), 37–52 31. Sozeau, M.: Subset coercions in Coq. In: Altenkirch, T., McBride, C., eds., Types

for Proofs and Programs, Int. Wksh., TYPES 2006, volume 4502 of Lect. Notes in Comput. Sci. Springer-Verlag (2007), 237–252

32. Sozeau, M.: Un environnement pour la programmation avec types dépendants. Ph.D. thesis, Université Paris 11, Orsay, France (2008)

33. Stone, C. A., Harper, R.: Extensional equivalence and singleton types. ACM Trans. Comput. Logic 7 (2006) 676–722

34. Werner, B.: On the strength of proof-irrelevant type theories. Logical Meth. in Comput. Sci. 4 (2008)

A Normalisation by evaluation

data Term = U                -- Universe
| Fun Term Term    -- dependent function space
| Singl Term Term  -- Singleton type ({a}_A)
| Term :@ Term     -- application
| Lam Term         -- abstraction
| Q                -- variable
| Sub Term Subst   -- substitution
| Sigma Term Term  -- dependent pair type
| Fst Term         -- first projection
| Snd Term         -- second projection
| Pair Term Term   -- dependent pair
| Nat              -- Naturals
| Zero             --
| Suc Term         --
| Rec Term Term Term Term -- Elimination for Nat
| Prf Term         -- Proof (with Proof-Irrelevance)
| Box Term         -- A term in Prf
| Oh               -- Canonical element of Prf t
| Where Term Term Term
| Enum Int         -- Enum n has n elements
| Const Int Int    --
| Elim Int Term [Term] Term -- Elimination for (Enum n)
  deriving (Eq,Show)
data Subst = E                 -- empty substitution
 | Is                -- identity substitution
 | Ext Subst Term    -- extension
 | P                 -- weakening
 | Comp Subst Subst  -- composition
   deriving (Eq,Show)
data D = T                     -- terminal object (empty context)
| Ld (D -> D)           -- curryfication
| FunD D (D -> D)        -- dependent products

       | UD                    -- Universe
       | SingD D D             -- Singleton
       | PairD D D              -- context comprehension
       | Vd Int                -- variables
       | AppD D D              -- neutrals
       | SumD D (D -> D)       -- dependent products
       | Proj Bool D           -- projections of neutrals
       | NatD
       | ZeroD
       | SucD D
       | RecD (D -> D) D D D
       | PrfD D
       | StarD
       | EnumD Int
       | ConstD Int Int
       | ElimD Int (D -> D) [D] D

type Ctx = [Term]
pi1,pi2 :: D -> D
pi1 (PairD d d') = d
pi2 (PairD d d') = d'
app :: D -> D
app (PairD (Ld f) d) = f d
ap :: D -> D -> D
ap f d = app (PairD f d)
neutralD :: D -> Bool
neutralD (Vd _) = True
neutralD (AppD __) = True
neutralD (Proj __) = True
neutralD (RecD ____) = True
neutralD (ElimD ____) = True
neutralD _= False
dec :: (D -> D) -> Bool -> D -> D
dec f b (PairD d d')  = f (PairD d d')
dec f b d | neutralD d = Proj b d
p = dec pi1 False
q = dec pi2 True

rec :: (D -> D) -> D -> D -> D -> D
rec b z s ZeroD    = z
rec b z s (SucD e) = (s `ap` e) `ap` (rec b z s e)
rec b z s d | neutralD d = up (b d)
                           (RecD (\e -> (downT (b e)))
                              (down (b ZeroD) z)
                              (down
                               (FunD NatD (\n -> FunD (b n) (\e -> b (SucD n)))) s)
                              d)
downs :: Int -> (D -> D) -> [D] -> Int -> [D]
downs __[]     _= []
downs n f (d:ds) i = (down (f (ConstD n i)) d):(downs n f ds (i+1))
elim :: Int -> (D -> D) -> [D] -> D -> D
elim n b ds (ConstD m i) | n == m && i < n = ds!!i
elim n b ds d | neutralD d = up (b d)
                                (ElimD n (\e -> (downT (b e)))
                                       (downs n b ds 0)
                                       d
                                )
up :: D -> D -> D
up (SingD a x) k = a
up (FunD a f)  k = Ld (\d -> up (f d) (AppD k (down a d)))
up (SumD a f)  k = PairD (up a (p k)) (up (f (up a (p k))) (q k))
up NatD        k = k
up (PrfD a)    k = StarD
up d           k = k
down :: D -> D -> D
down UD d          = downT d
down (SingD a x) d = down x a
down (FunD a f)  d = Ld (\e -> down (f (up a e)) (d `ap` (up a e)))
down (SumD a b)  d = PairD (down a (p a)) (down (b (p d)) (q d))
down NatD        (SucD e) = SucD (down NatD e)
down (PrfD a)    d = StarD
down d           e = e
downT (SingD a x) = SingD (down x a) (downT x)
downT (FunD a f)  = FunD (downT a) (\d -> downT (f (up a d)))
downT (SumD a b)  = SumD (downT a) (\d -> downT (b (up a d)))
downT (PrfD a)    = PrfD (downT a)
downT d           = d
readback :: Int -> D -> Term

readback i UD             = U
readback i (FunD a f)     = Fun (readback i a) $ readback (i+1) (f (Vd i))
readback i (SingD a x)    = Singl (readback i a) (readback i x)
readback i (Ld f)         = Lam $ readback (i+1) (f (Vd i))
readback i (Vd n)         = mkvar (i-n-1)
readback i (AppD k d)     = (readback i k) :@ (readback i d)
readback i (Proj False d) = Fst (readback i d)
readback i (Proj True d)  = Snd (readback i d)
readback i (PairD d e)    = Pair (readback i d) (readback i e)
readback i (SumD a b)     = Sigma (readback i a) $ readback (i+1) (b (Vd i))
readback i NatD           = Nat
readback i ZeroD          = Zero
readback i (SucD e)       = Suc (readback i e)
readback i (RecD b z s e) = Rec (Fun Nat (readback (i+1) (b (Vd i))))
                             (readback i z)
                             (readback i s)
                             (readback i e)
readback i (PrfD d)        = Prf (readback i d)
readback i StarD           = Oh
readback i (EnumD n)       = Enum n
readback i (ConstD n j)    = Const n j
readback i (ElimD n b ds d) = Elim n (readback (i+1) (b (Vd i)))
                                  (map (readback i) ds) (readback i d)
-- Evaluation
eval :: Term -> D -> D
eval U           d = UD
eval (Fun t f)   d = FunD (eval t d) (\d' -> eval f (PairD d d'))
eval (Singl t a) d = SingD (eval t d) (eval a d)
eval (Lam t)     d = Ld (\d' -> eval t (PairD d d'))
eval (t :@ r)    d = (eval t d) `ap` (eval r d)
eval Q           d = pi2 d
eval (Sub t s)   d = eval t (evalS s d)
eval (Sigma t r) d = SumD (eval t d) (\e -> eval r (PairD d e))
eval (Fst t)     d = p (eval t d)
eval (Snd t)     d = q (eval t d)
eval (Pair t r)  d = PairD (eval t d) (eval r d)
eval Nat         d = NatD
eval Zero        d = ZeroD
eval (Suc t)     d = SucD (eval t d)
eval (Rec b z s t) d = rec (\e -> eval b (PairD d e))

                           (eval z d)
                           (eval s d)
                           (eval t d)

eval (Prf t)     d = PrfD (eval t d)
eval (Box t)     d = eval t d
eval Oh          d = StarD
eval (Where t b p) d   = eval b (PairD d (eval t d))
eval (Enum n)        d = EnumD n
eval (Const n i)     d = ConstD n i
eval (Elim n b ts t) d = elim n (\e -> eval b (PairD d e))
                              (map ((flip eval) d) ts) (eval t d)
evalS :: Subst -> D -> D
evalS E           d = T
evalS Is          d = d
evalS (Ext s t)   d = PairD (evalS s d) (eval t d)
evalS P           d = pi1 d
evalS (Comp s s') d = (evalS s . evalS s') d
nbe :: Term -> Term -> Term
nbe ty t = readback 0 . down (eval ty T) $ eval t T
nbeTy :: Term -> Term
nbeTy ty = readback 0 $ downT (eval ty T)
nbeOpen :: Ctx -> Term -> Term -> Term
nbeOpen ctx ty t = readback n . down (eval ty env) $ eval t env
    where n   = length ctx
          env = mkenv n ctx T

nbeOpenTy :: Ctx -> Term -> Term
nbeOpenTy ctx ty = readback n $ downT (eval ty env)
    where n   = length ctx
          env = mkenv n ctx T

mkenv :: Int -> Ctx -> D -> D
mkenv 0 []     d = d
mkenv n (t:ts) d = PairD d' (up td (Vd (n-1)))
    where d' = mkenv (n-1) ts d
          td = eval t d'

mkvar :: Int -> Term
mkvar n | n == 0    = Q
        | otherwise = Sub Q $ subs (n-1)
subs n | n == 0    = P
subs n | otherwise = Comp P $ subs (n-1)

B Type-checking algorithm

Type checking algorithm for normal forms, and type inference algorithm for neutral terms.

Checking contexts

chkCtx :: Ctx -> Bool
chkCtx [] = True
chkCtx (t:ts) = chkCtx ts && chkType ts t

Checking types

chkType :: Ctx -> Term -> Bool
chkType ts U                 = True
chkType ts (Fun t r)         = chkType ts t && chkType (t:ts) r
chkType ts (Singl a t)       = chkType ts t && chkTerm ts t a
chkType ts (Sigma t r)       = chkType ts t && chkType (t:ts) r
chkType ts Nat               = True
chkType ts (Prf t)           = chkType ts t
chkType ts (Enum n)          = True
chkType ts Q                 = chkNeTerm ts U Q
chkType ts w@(Sub Q s)       = chkNeTerm ts U w
chkType ts w@(k :@ v)        = chkNeTerm ts U w
chkType ts w@(Fst k)         = chkNeTerm ts U w
chkType ts w@(Snd k)         = chkNeTerm ts U w
chkType ts w@(Rec t' v v' k) = chkNeTerm ts U w
chkType __= False

Checking the types of terms

idsub :: Term -> Term -> Term
idsub t t' = Sub t (Ext Is t')

chkTerm :: Ctx -> Term -> Term -> Bool
chkTerm ts U           (Fun t t')   = chkTerm ts U t &&
                                      chkTerm (t:ts) U t'
chkTerm ts U           (Singl e t)  = chkTerm ts U t &&
                                      chkTerm ts t e
chkTerm ts U           (Sigma t t') = chkTerm ts U t &&
                                      chkTerm (t:ts) U t'
chkTerm ts U            Nat         = True
chkTerm ts (Fun t t')  (Lam e)      = chkTerm (t:ts) t' e
chkTerm ts (Singl e t) e'           = chkTerm ts (nbeOpenTy ts t) e' &&
                                     (nbeOpen ts e t) == (nbeOpen ts e' t)
chkTerm ts (Sigma t r) (Pair e e')  = chkTerm ts t e &&
                                      chkTerm ts (nbeOpenTy ts (idsub r e)) e'
chkTerm ts Nat         Zero         = True
chkTerm ts Nat         (Suc t)      = chkTerm ts Nat t
chkTerm ts (Prf t)     (Box e)      = chkTerm ts t e
chkTerm ts (Enum n)    (Const m i)  = m == n && i < n
chkTerm ts t e | neutral e          = chkNeTerm ts t e
chkTerm ___= False
neutral :: Term -> Bool
neutral Q               = True
neutral (Sub Q s)       = True
neutral (k :@ v)        = True
neutral (Fst k)         = True
neutral (Snd k)         = True
neutral (Rec t' v v' k) = True
neutral (Elim n b ts t) = True
neutral (Where b t p)   = True
neutral _= False
maybeEr :: Maybe Term -> Maybe Term
maybeEr = maybe Nothing (Just . erase)
chkNeTerm :: Ctx -> Term -> Term -> Bool
chkNeTerm ts t e = case maybeEr (infType ts e) of
                     Just t' -> t == t'
                     Nothing -> False

Inferring the types of neutral terms

nbeType :: Ctx -> Term -> Maybe Term
nbeType ctx t = Just (nbeOpenTy ctx t)
infType :: Ctx -> Term -> Maybe Term

infType (t:ts) Q         = nbeType (t:ts) (Sub t P)
infType ts     (Sub Q s) = case infType (infCtx ts s) Q of
                             Just t -> nbeType ts (Sub t s)
                             _-> Nothing
infType ts (e :@ e') = case maybeEr (infType ts e) of
                         Just (Fun t t') ->
                             if chkTerm ts t e'
                             then nbeType ts (idsub t' e')
                             else Nothing
                         _-> Nothing
infType ts (Fst e)   = case maybeEr(infType ts e) of
                         Just (Sigma t t') ->  Just t
                         _-> Nothing
infType ts (Snd e)   = case maybeEr (infType ts e) of
                         Just (Sigma t t') -> nbeType ts (idsub t' (Fst e))
                         _-> Nothing
infType ts (Rec t v w k) = case maybeEr (infType ts k) of
                             Just Nat -> if
                                 chkType (Nat:ts) t &&
                                 chkTerm ts (nbeOpenTy ts (idsub t Zero)) v &&
                                 chkTerm (Nat:ts)
                                           (Fun (idsub t Q)
                                                (idsub t (Suc (Sub Q P)))) w
                                 then nbeType ts (idsub t k)
                                 else Nothing
                             _-> Nothing
infType ts (Where t b k) = case maybeEr (infType ts k) of
                             Just (Prf t') -> if chkType ts t &&
                                                 chkTerm (t':ts) t b
                                              then Just (Prf t)
                                              else Nothing
                             _-> Nothing
infType ts (Elim n b cs k) = case maybeEr (infType ts k) of
                               Just (Enum m) -> if m == n &&
                                                   chkType (Enum n:ts) b &&
                                                   chkList ts n b 0 cs
                                                then nbeType ts (idsub b k)
                                                else Nothing
                               _-> Nothing
infType __= Nothing
chkList :: Ctx -> Int -> Term -> Int -> [Term] -> Bool

chkList ts ___[]     = True
chkList ts n b i (e:es) = chkTerm ts (nbeOpenTy ts (idsub b (Const n i))) e &&
                          chkList ts n b (i+1) es
infCtx :: Ctx -> Subst -> Ctx
infCtx  (t:ts) P          = ts
infCtx  (t:ts) (Comp P s) = infCtx ts s
erase :: Term -> Term
erase (Singl e t) = erase t
erase t           = t