A MODULAR TYPE-CHECKING ALGORITHM FOR TYPE THEORY WITH SINGLETON TYPES AND PROOF IRRELEVANCE

ANDREAS ABEL, THIERRY COQUAND, AND MIGUEL PAGANO

Ludwig-Maximilians-Universität München e-mail address: andreas.abel@ifi.lmu.de

Göteborg University e-mail address: coquand@chalmers.se

Universidad Nacional de Córdoba e-mail address: pagano@famaf.unc.edu.ar

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 [46], Coq [33], and Epigram [40] is to decide if a given term has some type (either checking for a given type or inferring one); i.e., if a term corresponds to a proof of a proposition [32]. 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 [2, 3] for Martin-Löf type theories [38, 45] by considering singleton types and proof-irrelevant propositions.

We consider a type theory with a universe, which allows large eliminations, i.e., types defined by recursion on natural numbers. The universe of small types was introduced by Martin-Löf [37] for formalising category theory. Martin-Löf presents universes in two different styles [38]: à la Russell (the one considered here), and à la Tarski.

1998 ACM Subject Classification: F.4.1. Key words and phrases: type theory, type-checking, normalisation-by-evaluation, singleton types, proof-

irrelevance.

The first author was supported by INRIA as guest researcher in the PI.R2 team, PPS, Paris, France, from October 2009 to March 2010.

The third author is partially supported by CONICET, Argentina.

LOGICAL METHODS IN COMPUTER SCIENCE  DOI:10.2168/LMCS-???  \begin{matrix}c \\ ◯ \end{matrix} A. Abel, T. Coquand, and M. Pagano Creative Commons

Singleton types were introduced by Aspinall [10] in the context of specification languages. An important use of singletons is as definitions by abbreviations (see [10, 21]); they were also used to model translucent sums in the formalisation of SML [34]. It is interesting to consider singleton types because beta-eta phase separation fails: one cannot do eta-expansion before beta-normalisation of types 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 eta-expansion at singleton type can trigger new betareductions. Stone and Harper [54] decide type checking in a logical framework (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 [18], for reducing the burden in the formalisation of mathematics. As shown by Werner [56], the use of proof-irrelevance types together with sigma types is one way to get subset types à la PVS [51] in type-theories having the eta rule. This style of subset types was also explored by Sozeau [53, Sec. 3.3]; for another presentation of subset types in Martin-Löf type-theory see [50]. Berardi conjectured that (impredicative) type-theory with proof-irrelevance is equivalent to constructive mathematics [14].

Checking dependent types relies on checking types for equality. To this end, we compute η-long normal forms using normalisation by evaluation (NbE) [39]. 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 [16], liftable de Bruijn terms [8], or Kripke semantics [5]. 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. In Section 2, we first present λ^{Sing}, Martin-Löf’s logical framework with one universe and singleton types, as a generalized algebraic theory [19]. Secondly, we introduce λ^{Irr}, Martin-Löf type theory with natural numbers, sigma types, and proof-irrelevant propositions. In Section 3, we show some examples using singleton types and proof-irrelevant types. In Section 4, we present briefly NbE for untyped and simply typed lambda calculi; in particular we illustrate our novel approach to generate fresh identifiers. In Section 5, we define the semantics of the type theories by a PER model and prove the soundness of the inference rules. We use this model to introduce a normalization algorithm nbe, for which we prove completeness (if t = t′ is derivable, then nbe(t) and nbe(t′) are identical). The soundness of the algorithm (i.e., t = nbe(t) is derivable) is proven by logical relations in Section 6. In Section 7, we define a bi-directional algorithm for checking the type of normal forms and inferring the type of neutral terms. More related work is discussed in Section 8.1. 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 this section, we introduce the type theory. In order to show the modularity of our approach, we present it as two calculi λ^{Sing} and λ^{Irr}: 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 natural numbers, sigma types, and proof-irrelevant propositions. However, this separation is not fundamental since the different features are orthogonal to each other. We could add singleton types to the second calculus without disrupting the structure of our algorithm and our proofs.

We present the calculi using the formalism proposed by Cartmell for generalised algebraic theories (GAT) [19]. A GAT consists of sort symbols and operator symbols, each with a dependent typing, and equations between sort expressions and terms (“operator expressions”). Following Dybjer [24], we are using “informal syntax” where redundant arguments to operators are left implicit.

2.1. Calculus λ^{Sing}with singleton types. We use capital Greek letters (Γ, Δ) for variables ranging over contexts; capital letters from the beginning of the Latin alphabet (A, B) for variables ranging over types; small Greek letters (δ, ρ, σ) are used for variables denoting substitutions; and minuscule Latin characters (r, s, t, u, a, b) for variables on terms. Words in sans face denote constants (e.g., Type, q).

2.1.1. Sorts. The set of sort symbols is {Ctx, →, Type, Term} and their formation rules, in the sense of Cartmell’s GATs, are:

\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. After we have defined the judgements, we will use the latter, more readable versions.

2.1.2. 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 the usual two operators for constructing contexts: S_{C} = {⋄, . }.

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

Substitutions. We have five operators for substitutions, which are the usual operators for explicit substitutions [1]: S_{S} = {⟨⟩, ( , ), id , , p}. Semantically, substitutions σ ∈ Γ → Δ are sequences of values, one for every variable declaration in Δ. The sequences are constructed from the empty sequence ⟨⟩ by sequence extension (σ, t). Substitutions form a category with identity id_{Γ} and composition σ δ. Finally, we have the first projection p on sequences.

\frac{Γ ∈ Ctx}{⟨⟩ ∈ Γ → ⋄} (empty-subs)  \frac{σ ∈ Γ → Δ  t ∈ Term(Γ, A σ)}{(σ, t) ∈ Γ → Δ.A} (ext-subs)

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

\frac{A ∈ Type(Γ)}{p ∈ Γ.A → Γ} (fst-subs)

Types. The set of operators for types is S_{T} = {U, Fun , , { } }. U is a universe of small types à la Russell, which means its elements are directly usable as types (u-el) without coercion. Besides dependent function types Fun A B we have the singleton type {t}_{A}—a subtype of A containing t as single inhabitant. Types A are closed under substitution A σ.

\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 , λ , app , , q, { } }. It includes function space Fun A B and singleton {t}_{A} as small-type constructors in U. Lambda terms with explicit substitutions are obtained via the constructions λt, app t u, q, and t σ. Since we have used juxtaposition for composition and application of substitutions, we have the explicit app for term application. Note that q stands for the top (0th) variable, the nth variable is expressed as q p^{n}.

\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{A ∈ Type(Γ)}{q ∈ Term(Γ.A, A p)} (hyp)  \frac{σ ∈ Γ → Δ  t ∈ Term(Δ, A)}{t σ ∈ Term(Γ, A σ)} (subs-term)

\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)

2.1.3. Axioms for Equational Theory. In the following, we present the axioms of the equational theory of λ^{Sing}. Equality is considered as the congruence closure of these axioms. Congruence rules, also called derived rules, are generated mechanically for each symbol from its typing. For instance, rule (subs-type) induces the derived rule

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

Another instance of a derived rule is conversion, it holds because equality between sorts, such as Term(Γ, A) = Term(Γ, A′):

\frac{t ∈ Term(Γ, A) A = A′ ∈ Type(Γ)}{t ∈ Term(Γ, A′)}

In the following, we present equality axioms without the premises concerning typing, except in the cases where they cannot be inferred.

Substitutions. The first two equations witness extensionality for the identity substitution, the next three the composition laws for the category of substitutions. Then there is a law for the first projection p, and the last two laws show how to propagate a substitution δ into a tuple.

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

Axioms for β and η, propagation and resolution of substitutions. An explicit substitution (id_{Γ}, r) is created by contracting a β-redex (first law). It is then propagated into the various term constructions until it can be resolved (last two laws).

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

Singleton types. All inhabitants of a singleton type are equal (sing-eq-i). We mention the important derived rule (sing-eq-el) here explicitly.

\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)

There is a choice how to express the last two rules; they could be replaced with

\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) : B (id, 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.

Conventions. We denote with |Γ| the length of the context Γ; and Γ!i is the projection of the i-th component of Γ, for 0 ⩽ i < |Γ|; i.e. if Γ = A_{n−1} … A_{0} and 0 ⩽ i < n, then Γ!i = A_{i}. We say Δ ⩽^{i} Γ if Δ ⊢ p^{i} : Γ; where p^{i} is the i-fold composition of p with itself. ^{1}

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 2.1. Note that if Δ ⊢ p^{i} : Γ, and Γ ⊢ p^{j} : Θ, then Δ ⊢ p^{i+j} : Θ.

Definition 2.2 (de Bruijn index). The ith de Bruijn index v_{i} is defined as

v_{i} = \{ \begin{matrix}q & if i ⩽ 0 \\ qp^{i} & if i > 0. \end{matrix}

For convenience, we identify negative indices with the 0th index.

The following grammar describes the set Nf of β-normal forms. As auxiliary notion, it uses the set Ne of neutral normal forms, i.e., normal forms with a variable in head position, which blocks reduction. A bit sloppily, we refer to elements of Ne as “neutral terms”; in general, the attribute neutral shall mean variable in head position (this is stricter than Girard’s concept of neutral [28]).

Definition 2.3 (Neutral terms, and normal forms).

Ne ∋ k ::= v_{i} | 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; for instance, some of the following inversion results, which are needed in the proof of completeness of the type-checking algorithm.

Remark 2.4 (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}.

1The direction Δ ⩽^{i} Γ (as opposed to Δ ⩾^{i} Γ) has been chosen to be compatible with subtyping A ⩽ B.

Weakening (Remark 2.4) is a special case of subsumption which states that Δ ⩽ Γ ⊢ t : A ⩽ B implies Δ ⊢ t : B.

Remark 2.5 (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 2.6 (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.

The following lemma can be proved directly by induction on derivations by checking the possibles rules used in the last step.

Lemma 2.7 (Inversion of typing).

(1) If Γ ⊢ Fun A′ B′ : A, then Γ ⊢ A = U, Γ ⊢ A′ : U, and also Γ.A′ ⊢ B′ : U;

(2) if Γ ⊢ {b}_{B} : A, then Γ ⊢ A = U, Γ ⊢ B : U, and also Γ ⊢ b : B;

(3) if Γ ⊢ λt : A, then either (a) Γ ⊢ A = Fun A′ B with Γ.A′ ⊢ t : B; or

(b) Γ ⊢ A = {a}_{A′} with Γ ⊢ λt = a : A′.

(4) if Γ ⊢ app t r : A, then Γ ⊢ t : Fun A′ B′, Γ ⊢ r : A′, and Γ ⊢ A = B′ (id, r′).

Proof. (1) The last rule used is one of (fun-u-i), (conv), (sing-i), or (sing-e). In the first case the premises of the rule are what is to be proved; in all other cases we have a premise with the form Γ ⊢ Fun A′ B′ : B, hence we can apply the i.h. (2-4) Analogously.

Remark 2.8 (Inversion of substitution). Any substitution Δ ⊢ σ : Γ.A is equal to some substitution Δ ⊢ (σ′, t) : Γ.A. It is enough to note id_{Γ.A} = (p, q), hence we have the equalities σ = id σ = (p, q) σ = (p σ, q σ).

2.2. λ^{Irr}: A type theory with proof-irrelevance. In this section we keep the basic rules of the previous calculus (those that do not refer to singleton types), and introduce types for natural numbers, enumeration sets, sigma types, and proof-irrelevant types. The main difference with other presentations [45, 38], on 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.

Sigma types. Both U and Type are closed under (strong) sigma-type formation; (a, b) introduces a dependent pair and fst t and snd t eliminate it.

\frac{A ∈ Term(Γ, U)  B ∈ Term(Γ.A, U)}{Σ A B ∈ Term(Γ, U)} (sum-u-i) \frac{A ∈ Type(Γ)  B ∈ Type(Γ.A)}{Σ A B ∈ Type(Γ)} (sum-f)

\frac{B ∈ Type(Γ.A)  a ∈ Term(Γ, A)  b ∈ Term(Γ, B (id, a))}{(a, 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)

The β- and η-laws for pairs are given by the first three equations to follow. The remaining equations propagate substitutions into the new term constructors.

fst (a, b) = a  snd (a, b) = b  (fst t, snd t) = t
(fst t) σ = fst (t σ)  (snd t) σ = snd (t σ)  (a, b) σ = (a σ, b σ)
(Σ A B) σ = Σ (A σ) (B (σ p, q))

Propagation laws can be obtained mechanically: to propagate σ into c t⃗, just compose it with each t_{i} that is not a binder (e.g., A in Σ A B), and compose its lifted version (σ p, q) with each t_{j} that is a binder (e.g., B in Σ A B). Binders are those formed in an extended context (here, B ∈ Type(Γ.A)). In the following, we will skip the propagation laws.

Natural numbers. We add an inductive type Nat with constructors zero and suc and primitive recursion natrec.

\frac{Γ ∈ Ctx}{Nat ∈ Term(Γ, U)} (nat-u-i) \frac{Γ ∈ Ctx}{zero ∈ Term(Γ, Nat)} (nat-z-i) \frac{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)

Here, we used Rec(B) as an abbreviation for Fun Nat (Fun B (B (p, suc q) p)) which in conventional notation reads Πx: Nat. B → B[suc x/x]. Since B is a big type, it can mention the universe U, thus, we can define small types by recursion via natrec. This so called large elimination excludes normalization proofs which use induction on type expressions [23, 22]. We add the usual computation laws for primitive recursion.

natrec B z s zero = z
natrec B z s (suc t) = app (app s t) (natrec B z s t)

Enumeration sets. The type N_{n} has the n canonical inhabitants c_{0}^{n}, …, c_{n−1}^{n}, which can be eliminated by the dependent case distinction case^{n} B t_{0} ⋯ t_{n−1} t with n branches.

\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 ∈ Term(Γ, N_{n}) t_{0} ∈ Term(Γ, B (id, c_{0}^{n})) ⋯ t_{n−1} ∈ Term(Γ, B (id, c_{n−1}^{n}))}{case^{n} B t_{0} ⋯ t_{n−1} t ∈ Term(Γ, B (id, t))} (n_{n}-e )

We add the usual computational law for case distinction, and weak extensionality, which for booleans (N_{2}) reads “if t then true else false = t”in sugared syntax.

case^{n} B t_{0} ⋯ t_{n−1} c_{i}^{n} = t_{i}
case^{n} N_{n} c_{0}^{n} ⋯ c_{n−1}^{n} t = t

For N_{0} and N_{1} we can formulate strong η-laws: all their inhabitants are considered equal, since there is at most one. To realize this, we introduce a new term ⋆ in N_{0} if it already has an inhabitant t; we consider ⋆ as normal form of t. Note that this seemingly paradoxical canonical form ⋆ ∈ N_{0} does not threaten consistency, since it cannot exist in the empty context Γ = ⋄; otherwise there would have already been a term t ∈ Term(⋄, N_{0}).

\frac{t ∈ Term(Γ, N_{0})}{⋆ ∈ Term(Γ, N_{0})} (n_{0}-tm) \frac{t, t′ ∈ Term(Γ, N_{0})}{t = t′ ∈ Term(Γ, N_{0})} (n_{0}-eq) \frac{t, t′ ∈ Term(Γ, N_{1})}{t = t′ ∈ Term(Γ, N_{1})} (n_{1}-eq)

On the one hand, rule (n_{0}-tm) destroys decidability of type checking: to check whether ⋆ ∈ Term(Γ, N_{0}) we would have to decide the consistency of Γ which is certainly impossible in a theory with natural numbers. On the other hand, it allows us to decide equality by computing canonical forms. We solve this dilemma by forbidding ⋆ in the user syntax which is input for the type-checker; ⋆ is only used internally in the NbE algorithm and in the canonical forms it produces. Formally this is reflected by having two calculi: one with the rule (n_{0}-tm) and one without it. For distinguishing the calculi, we decorate the turnstile (⊢^{⋆}) in judgements of the former and leave (⊢) for the calculus without (n_{0}-tm). We also use the different turnstiles for referring to each calculus. In Sect. 2.3 we prove that (⊢^{⋆}) is a conservative extension of (⊢).

Strong extensionality for booleans and larger enumeration sets is hard to implement [9, 12] and beyond the scope of this work.

In the sequel we use t⃗ for denoting the n terms t_{0} ⋯ t_{n−1} in case^{n} B t_{0} ⋯ t_{n−1} r. We will omit the superscript n in c_{i}, and in case B t⃗ r.

Proof irrelevance. Our treatment of proof-irrelevance is based on Awodey and Bauer [11] and Maillard [36]. The constructor Prf turns a type A into the proposition Prf A in the sense that only the fact matters whether A is inhabited, not by what. An inhabited proposition is regarded as true, an uninhabited as false. The proposition Prf A still has all inhabitants of A, but now they are considered equal. If A is not empty, we introduce a trivial proof ⋆ in Prf A which we regard as the normal form of any t ∈ Term(Γ, Prf A).

\frac{A ∈ Term(Γ, U)}{Prf A ∈ Term(Γ, U)} (prf-f)  \frac{A ∈ Type(Γ)}{Prf A ∈ Type(Γ)} (prf-f)

\frac{a ∈ Term(Γ, A)}{[a] ∈ Term(Γ, Prf A)} (prf-i)  \frac{a ∈ Term(Γ, A)}{⋆ ∈ Term(Γ, Prf A)} (prf-tm)

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

Note that (prf-tm) is analogous to (n_{0}-tm) and the same remarks apply; in particular, (prf-tm) is also a rule in (⊢^{⋆}) but not in (⊢).

We use Awodey and Bauer’s [11] elimination rule for proofs.

\frac{Γ ⊢ t : Prf A  Γ ⊢ B  Γ, x:A ⊢ b : B  Γ, x:A, y:A ⊢ b = b[y/x] : B}{Γ ⊢ b where [x] ← t : B}

The content x : A of a proof t : Prf A can be used in b via the elimination b where [x] = t if b does not actually depend on it, which is expressed via the hypothesis that b should be equal to b[y/x] for an arbitrary y. This elimination principle is stronger than “proofs can only be used inside of proofs” which is witnessed by the rule:

\frac{Γ ⊢ t : Prf A  Γ ⊢ B  Γ, x:A ⊢ b : Prf B}{Γ ⊢ b where [x] ← t : Prf B}

Note that this weaker elimination rule in the style of a bind operation for monads is an instance of the Awodey-Bauer rule, since the equation Γ, x:A, y:A ⊢ b = b[y/x] : Prf B holds trivially due to proof irrelevance. An example which is typable with the Awoday-Bauer rule but not the monadic rule is the term magic given in the next section.

The Awodey-Bauer where fulfills β-, η-, and associativity laws analogous to the ones of a monad.

b where [x] ← [a] = b[a/x]
b[[x]/y] where [x] ← t = b[t/y]
a where [x] ← (b where [y] ← c) = (a where [x] ← b) where [y] ← c  if y ∉ FV(a)

After this more readable presentation in named syntax, we add the eliminator and its equations to our GAT in de Bruijn style:

\frac{t ∈ Term(Γ, Prf A) B ∈ Type(Γ)  b ∈ Term(Γ.A, B p)  b p = b (p p, q) ∈ Term(Γ.A.A p, B p p)}{b where^{B} t ∈ Term(Γ, B)} (prf-el)
b where^{B} [a] = b (id, a)  (prf-β)
b (p, [q]) where^{B} t = b (id, t)  (prf-η)
a where^{A} (b where^{B} c) = (a (p p, q) where^{A p} b) where^{B} c  (prf-assoc)

After exposition of the formation, introduction, elimination, and equality rules for the types of λ^{Irr}, we continue with basic properties of derivations. From now, we use the more conventional notation for judgements.

Definition 2.9 (Neutral terms and normal forms).

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

Lemma 2.10 (Inversion of types).

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

(2) If Γ ⊢ Prf A, then Γ ⊢ A.

Lemma 2.11 (Inversion of typing).

(1) If Γ ⊢ Σ A′ B : A, then Γ ⊢ A = U, and Γ ⊢ A′ : U, and Γ.A′ ⊢ B : U.

(2) If Γ ⊢ Nat : A, then Γ ⊢ A = U.

(3) If Γ ⊢ N_{n} : A, then Γ ⊢ A = U.

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

(5) If Γ ⊢ fst t : A , then Γ ⊢ A = A′, and Γ ⊢ t : Σ A′ B, for some A′, and B.

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

(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), Γ ⊢ t : Nat, and Γ ⊢ A = B (id, t).

(10) if Γ ⊢ c_{i}^{n} : A, then Γ ⊢ A = N_{n}; (11) If Γ ⊢ case B t⃗ t′ : A, then Γ.N_{n} ⊢ B, Γ ⊢ t_{i} : B (id, c_{i}), Γ ⊢ 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 = B, Γ ⊢ t : Prf A′ for some A′, Γ.A′ ⊢ b : B p, and Γ.A′.A′ p ⊢ b p = b (pp, q) : B p.

2.3. Conservativity of ⋆. In this section we prove that (⊢^{⋆}) is a conservative extension of (⊢); i.e., any derivation in (⊢^{⋆}) has a counterpart derivation in (⊢) and the components of the conclusions of those derivations are judgmentally equal in (⊢^{⋆}).

Definition 2.12. A term is called pure if it does not contain any occurrence of ⋆. Let ν be a syntactical entity, if μ is obtained from ν by replacing all occurrences of ⋆ by pure terms, then μ is called a lifting of ν.

We will distinguish those liftings that are judgmentally equal to the lifted entity, these liftings are called good liftings.

Definition 2.13 (Good lifting).

(1) A context Γ′ ⊢ is a good lifting of Γ ⊢^{⋆} if Γ′ is a lifting of Γ, such that ⊢^{⋆} Γ = Γ′.

(2) A substitution Γ′ ⊢ σ′ : Δ′ is a good lifting of Γ ⊢^{⋆} σ : Δ if Γ′ ⊢ and Δ′ ⊢ are good liftings of Γ ⊢^{⋆} and Δ ⊢^{⋆}, resp., and σ′ is a lifting of σ, such that Γ ⊢^{⋆} σ = σ′ : Δ.

(3) A type Γ ⊢ A′ is a good lifting of Γ ⊢^{⋆} A if Γ′ ⊢ is a good lifting of Γ ⊢^{⋆} and A′ is a lifting of A, such that Γ ⊢^{⋆} A = A′.

(4) A term Γ ⊢ t′ : A′ is a good lifting of Γ ⊢^{⋆} t : A if Γ′ ⊢ A′ is a good lifting of Γ ⊢^{⋆} A and t′ is a lifting of t, such that Γ ⊢^{⋆} t = t′ : A.

Now we can prove that there is a good lifting for each syntactic entity; for proving this, we need the stronger condition that any pair of good liftings for some entity are judgmentally equal.

Theorem 2.14.

(1) Let Γ ⊢^{⋆}; then there is a good lifting Γ′ ⊢ of Γ ⊢^{⋆}; moreover if Γ′′ ⊢ is also a good lifting of Γ ⊢^{⋆} then ⊢ Γ′ = Γ′′.

(2) Let Γ ⊢^{⋆} σ : Δ; then there is a good lifting Γ′ ⊢ σ′ : Δ′ of Γ ⊢^{⋆} σ : Δ; moreover if Γ′′ ⊢ σ′′ : Δ′′ is also a good lifting of Γ ⊢^{⋆} σ : Δ then ⊢ Γ′ = Γ′′, ⊢ Δ′ = Δ′′, and Γ′ ⊢ σ′ = σ′′ : Δ′.

(3) Let Γ ⊢^{⋆} A; then there is a good lifting Γ′ ⊢ A′ of Γ ⊢^{⋆} A ; moreover if Γ′′ ⊢ A′′ is also a good lifting of Γ ⊢^{⋆} A then ⊢ Γ′ = Γ′′ and Γ′ ⊢ A′ = A′′.

(4) Let Γ ⊢^{⋆} t : A; then there is a good lifting Γ′ ⊢ t′ : A′ of Γ ⊢^{⋆} t : A ; moreover if Γ′′ ⊢ t′′ : A′′ is also a good lifting of Γ ⊢^{⋆} t : A then ⊢ Γ′ = Γ′′, Γ′ ⊢ A′ = A′′, and Γ′ ⊢ t′ = t′′ : A′.

Proof. By induction on derivations, 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 judgmental equal.

We show the case for (prf-tm). First we prove the existence of a good lifting.

Γ ⊢^{⋆} ⋆ : Prf A  hypothesis  (*)
Γ ⊢^{⋆} t : A  by inversion on (*)  (†)
Γ′ ⊢ t′ : A′  by ind. hyp. is a good lifting of (†)
Γ′ ⊢ [t′] : Prf A′  by (prf-i), is a good lifting of(*)

Now we prove the second half of the theorem.

Γ′′ ⊢ s : B  hypothesis, be other good lifting of (†)  (**)
Γ′′ ⊢ B  by inversion, good lifting of Γ ⊢^{⋆} Prf A
Γ′ ⊢ B′′ = Prf A′  by ind. hyp.
Γ′ ⊢ [t′] = s : Prf A′  by (prf-eq) and (conv).

Corollary 2.15. The calculus (⊢^{⋆}) is a conservative extension of (⊢).

3. Examples

3.1. Safe vector projection in λ^{Irr}. We give a short demonstration how to use proof irrelevance in λ^{Irr}: we define vectors and a type safe projection function. While de Bruijn style is good for implementation and reasoning, it is virtually unreadable for humans, so we allow ourselves named λ-terms here which can be mechanically converted into actual terms of λ^{Irr}. For instance, we write Fun A (x.B) instead of the de Buijn style Fun A B. For further convenience, let (x : A) → B = Fun A (x.B) and (x : A) × B = Σ A (x.B). The non-dependent versions are written A → B = ( :A) → B and A×B = ( :A)×B. The type Vec A n of vectors of length n over element type A can be defined recursively as follows.

Vec : (A:U) → (n:Nat) → U
Vec = λAλn. natrec U N_{1} (λn′λV. A × V) n

A more suggestive notation for definitions by recursion is pattern matching; in this the definition of Vec reads as follows:

Vec : (A:U) → (n:Nat) → U

Vec A zero  = N_{1}
Vec A (suc n′) = A × Vec A n′

In the following, we use pattern matching as syntactic sugar for natrec. Our language already has booleans, so let us define comparison of natural numbers.

leq : (m:Nat) → (n:Nat) → Bool

leq zero n  = true
leq (suc m) zero  = false
leq (suc m) (suc n) = leq m n

Bool = N_{2}
true = c_{0}^{2}
false = c_{1}^{2}

By reflecting booleans into U we can obtain witnesses of propositions.

True : (b:Bool) → U

True true = N_{1}
True false = N_{0}

True (leq m n) is inhabited if m ⩽ n, because then True (leq m n) simplifies to N_{1} with trivial inhabitant c_{0}^{1}. If not m ⩽ n then True (leq m n) simplifies to the empty type N_{0}. A proposition Lt for “less than” is obtained as:

Lt : (m:Nat) → (n:Nat) → U

Lt m n = True (leq (suc m) n)

We are now ready to define a safe projection operation for vectors.

lookup : (A:U) → (n:Nat) → (m:Nat) → (p:Prf (Lt m n)) → (v:Vec A n) → A

lookup A zero m  p v = magic A p
lookup A (suc n) zero p v = fst v
lookup A (suc n) (suc m) p v = lookup A n m p (snd v)

Since Lt (suc m) (suc n) = Lt m n we can simply pass p to the recursive call in the last equation. In the first line we have to magically conjure an element of A from a proof p : Prf (Lt m zero) = Prf (True (leq (suc m) zero)) = Prf (True false) = Prf N_{0}.

magic : (A:U) → (p:Prf N_{0}) → A magic A p = case^{0} A q where [q] ← p

This is well typed since all inhabitants of N_{0} are equal, thus, the Awodey-Bauer rule (prf-el) is applicable.

The benefit of proof irrelevance is that now for any p, q : Lt m n, lookup A n m p v = lookup A n m q v : A; for a more detailed discussion consult Werner [56].

3.2. Isomorphisms in λ^{Irr}. Any already irrelevant type is isomorphic to its Prf version, i.e., for A ∈ {N_{0}, N_{1}, Prf B, {t}_{B}} we have coercions

ϕ = λx. [x]  : A → Prf A
ψ = λx. y where [y] ← x : Prf A → A

with ψ ∘ ϕ = λx. x by (prf-β) and ϕ ∘ ψ = λx. x by proof irrelevance. How do these coercions extend to higher types? For arbitrary A, B we have.

ϕ^{Σ} : (x:Prf A) × Prf B → Prf ((x:A) × B)
ϕ^{Σ} = λp. [(a, b)] where [a] ← fst p where [b] ← snd p
ψ^{Σ} : Prf ((x:A) × B) → (x:Prf A) × Prf B
ψ^{Σ} = λq. ([fst p], [snd p]) where [p] ← q
ϕ^{Π} : ((x:A) → Prf B) → Prf ((x:A) → B)
ϕ^{Π} = λf. [λx.? where [y] ← f x]
ψ^{Π} : Prf ((x:A) → B) → (x:A) → Prf B
ψ^{Π} = λfλx. [g x] where [g] ← f

We would like to put y for the ? in ϕ^{Π}, but this is not well typed, since we do not have y = z : B for arbitrary z. It seems that ϕ^{Π} is not definable in λ^{Irr}, as it is not definable in computational lambda-calculus [44] for an arbitrary monad Prf. Awodey and Bauer also have only ϕ^{Π} : ((x:A) → Prf B) → Prf ((x:A) → Prf B), which is trivial.

For arbitrary p : (x:Prf A) × Prf B we have

(ψ^{Σ} ∘ ϕ^{Σ})(p) =_{β} ([a], [b]) where [a] ← fst p where [b] ← snd p
=_{η} (fst p, snd p) =_{η} p.

In the opposite direction, ϕ^{Σ} ∘ ψ^{Σ} = λq. q by proof irrelevance. Thus, ϕ and ψ establish an isomorphism, which means that Prf distributes over Σ.

3.3. On subtyping in λ^{Sing}. Subtyping can be defined in several ways, for instance, A is a subtype of A′ in Γ, written Γ ⊢ A <: A′, iff Γ, x:A ⊢ x:A′. Most presentations of singleton types include subtyping [10, 22, 54], so it is natural to ask whether the usual rules hold in our calculus. Using the principle u = t : A iff u : {t}_{A}, it is easy to see that we have Aspinall’s two axioms [10]:

\begin{aligned}x : \{t\}_{A} & ⊢ & x & : & A \\ x : \{t\}_{A} & ⊢ & x & : & \{t\}_{\{t\}_{A}} & since x = t : \{t\}_{A} \end{aligned}

Also, singleton formation is compatible with subtyping, if Γ ⊢ A <: B then Γ ⊢ {t}_{A} <: {t}_{B}. Contravariant subtyping, however, only holds up to η-equality. If we relax the definition of subtyping Γ ⊢ A <: A′ to Γ, x : A ⊢ η(x) : A′ where η(x) denotes any ηexpansion of x, then we get contravariant subtyping

\frac{Γ, x:A′ ⊢ η_{A}(x) : A Γ, x:A′, y:B[η_{A}(x)/x] ⊢ η_{B}(y) : B′}{Γ, f:(x:A) → B ⊢ λx. η_{B}(f(η_{A}(x))) : (x:A′) → B′} .

Furthermore, we have following two axioms, which hold definitionally in Stone and Harper’s system [54]

f : {t}_{(x:A)→B}  ⊢ λx. f x : (x:A) → {t x}_{B} since f = t : (x:A) → B
f : (x:A) → {t x}_{B} ⊢ λx. f x : {t}_{(x:A)→B}  since f x = t x : B

The first axiom is one of Courant’s subtyping rules [22].

4. From Untyped to Typed Normalisation by Evaluation

In this section, we give a short introduction into normalisation-by-evaluation for typed lambda calculi, with a special emphasis on our novel method for generation of fresh identifiers during reification.

4.1. Fresh Name Generation in NbE. The basic idea of NbE is to evaluate a term of type A into a suitable semantics [[A]] from which its normal form can be extracted by reification. In case of the simply-typed lambda-calculus, this is possible if we choose for base types [[o]] the set of terms of type o and for function types [[A → B]] a suitable subset of the function space [[A]] → [[B]]. During reification of a function f ∈ [[A → B]] to a term λx.t, the identifier x has to be chosen fresh to avoid capture of names in the body of the function f. However, since f is a semantic object, it is a non-trivial problem to compute a name which is fresh for f. Garillot and Werner [27] solve it by first letting x be a dummy identifier, computing the free variables in the reified function body t, and then reify f again with a name x which is fresh for t. This is, of course, horribly inefficient, and there are other solutions. In the original publication on NbE by Berger and Schwichtenberg [16], base types [[o]] = Λ̂ are interpreted by term families. These are functions g from the natural numbers into a de Bruijn level representation of terms such that all instances g(n) are α-equivalent but in g(n) the bound variables are levels starting with n. In this setting, the reification of a function f ∈ [[A → B]] is not a term but a term family, mapping f to the term family n ↦ λx_{n}.ϕ(f(x̂_{n}))(n + 1), where ϕ denotes the reification function and x̂_{n} is the variable x_{n} seen as an element in [[A]]. Note that every λ in ϕ(f(x̂_{n}))(n + 1), the body of the reified abstraction, will bind a variable from the set {x_{n+1}, x_{n+2}, …}.

When considering NbE for the untyped lambda calculus, the type semantics collapses to a single domain D ≅ Λ̂ + [D → D] which contains terms and functions,^{2} as observed by Filinski and Rhode [26]. Aehlig and Joachimski [8] replace term families by functions h from natural numbers to a de Bruijn index representation of terms, where h(n) shifts all free indices by n.

In this paper, instead of having term families Λ̂ in the semantics, we have a notion of neutral (“term-like”) value built up from free variables x_{i} and application of the free variables to sequences of values d⃗. The free variables are de Bruijn levels in spirit, thus, no shifting is needed, just like in the locally nameless approach [49]. The second author has given a semantics with neutrals before [20], calling the free variables generic values. Also, this approach has been used by the first two authors together with Dybjer [5] for NbE without a reflection operation, and independently by Löh, McBride, and Swierstra [35]. In this article, we put the technique to a novel use by defining typed reification and reflection for this semantics.

4.2. Untyped NbE. Let Var = {x_{0}, x_{1}, … } be a denumerable set of variables. We consider a set D and a notion of function space [D → D] with an embedding constructor Lam : [[D → D] → D] and two further constructors Var : Var → D and App : [D × D → D] for neutral values. An application function · : [D × D → D] is given by

(Lam f) · d = f(d)
e  · d = App(e, d) if e not a Lam.

Such a D can be realised by solving the recursive domain equation D ≅ [D → D] ⊕ Var_{⊥} ⊕ (D × D) or, for the practically minded, by defining a Haskell data type

    data D where
      Lam : (D -> D) -> D
      Var : Var -> D
      App : D -> D -> D

and programming · by pattern matching. Our definition of D is a bit “too big” since it does not restrict App to the construction of neutral values App(… App(Var x_{i}, d_{1}) …, d_{n}) but we have also App(Lam f, d). However, we can ignore these unwanted elements since our NbE algorithm never produces any.

Remark 4.1. The relationship between the denotational model D and the Haskell data type D is not without subtleties. Domain theoretic functions such as application · correspond to Haskell programs if our denotational semantics is computationally adequate for Haskell’s operational semantics [48]. Filinski and Rhode [26] formally relate a NbE function on a reflexive domain D to a NbE program written in an ML-like, call-by-value language, by exploiting computational adequacy. We do not formally prove this connection for Haskell in this article, this is deferred to future work.

2 Let us notice here the tagging introduced by the disjoint sum operator +. Indeed, in the absence of a type structure, tagless normalisation seems impossible.

Untyped NbE is now given by a standard evaluator [[t]]ρ ∈ D of terms t in environments ρ and a readback function R_{j} d from values d at de Bruijn level j to terms [31]. For the sake of readability, we use names instead of de Bruijn indices in the syntax of untyped terms.

\begin{aligned}[[x]]ρ & = & ρ(x) \\ [[r s]]ρ & = & [[r]]ρ · [[s]]ρ \\ [[λx.t]]ρ & = & Lam (d ↦ [[t]]ρ[d/x]) \end{aligned} R_{j} (Var x_{i})  = x_{i}

R_{j} (App(r, s)) = (R_{j} r) (R_{j} s)
R_{j} (Lam f)  = λx_{j}. R_{j+1} (f(Var x_{j}))

To normalise a closed term t, compute R_{0} [[t]]. To normalise an open term t with free variables y_{0}, … y_{n−1} compute R_{n} [[t]]ρ with environment ρ(y_{i}) = Var x_{i}.

To prepare for applying our method to λ^{Sing} and λ^{Irr}, let us switch to de Bruijn representation. Environments become tuples and variables de Bruijn indices v_{i}.

\begin{aligned}[[q]](ρ, d) & = & d \\ [[t p]](ρ, d) & = & [[t]]ρ \\ [[r s]]ρ & = & [[r]]ρ · [[s]]ρ \\ [[λt]]ρ & = & Lam (d ↦ [[t]](ρ, d)) \end{aligned} R_{j} (Var x_{i})  = v_{j−(i+1)}

R_{j} (App(r, s)) = (R_{j} r) (R_{j} s)
R_{j} (Lam f)  = λ (R_{j+1} (f(Var x_{j})))

To read back a de Bruijn level Var x_{i} as a de Bruijn index, we have to take the current length j of the variable context into account. While de Bruijn levels are absolute references, they are numbered x_{0}, x_{1}, …, x_{j−1} in a context of length j, de Bruijn indices are relative to the length of the context, they are enumerated from right to left: v_{j−1}, …, v_{1}, v_{0}. The formula j − (i + 1) (assuming i < j) converts level i into the corresponding index.

4.3. Typed NbE. While untyped NbE returns a β-normal form (if it exists), typed normalisation by evaluation yields a βη-normal form, usually the η-long form. To obtain the η-long form, we have to modify our reification procedure. One method is to make readback type directed [5], which corresponds to postponing η-expansion after β-normalisation. However, this strategy is not sufficient in the case of λ^{Sing}, because η-expansions at singleton types can trigger new β-reductions. The other method is to divide η-expansion into reflection and “reification”, the first expanding variables to enable new reductions, and the second expanding the result of β-normalisation to obtain an η-long form.^{3}

The novel approach of this article is to do reflection ↑ and “reification” ↓, hence, ηexpansion, completely at the level of the semantics D. Since our value domain D allows us to construct functions via Lam, the process of η-expansion is independent of any fresh name considerations.

\begin{aligned}↑_{o} & e & = & e \\ ↑_{A→B} & e & = & Lam (d ↦ ↑_{B} App(e, ↓_{A} d)) \end{aligned}  \begin{aligned}↓_{o} & d & = & d \\ ↓_{A→B} & d & = & Lam (e ↦ ↓_{B} (d · (↑_{A} e))) \end{aligned}

To compute the long normal form of a closed term t of type A, run R_{0} (↓_{A} [[t]]). For an open term y_{0} :A_{0}, …, y_{n−1} :A_{n−1} ⊢ t : A, execute R_{n} (↓_{A} [[t]]ρ), where ρ(y_{i}) = ↑_{A_{i}} (Var x_{i}).

3In tagless normalisers [16], reflection is necessary to inject variables x : A of non-base types A into the semantics [[A]]. However, for languages beyond pure type systems it is hard to obtain tagless normalisation.

Classic is the problem of disjoint sum types [9]: to display a free variable of type A + B as either a left or a right injection, we need control structures [12]. Alternatively, one can replace data types by their Church encodings. None of these approaches fit our purposes, thus, we are currently not aiming at tagless normalisation.

5. Semantics

In this section we define a domain D for denoting types, terms, and substitutions. Then we introduce a partial function R_{j} for reifying elements of the domain into the calculus; this function takes an extra argument j ∈ ℕ indicating the next free variable. We continue by defining PERs over the domain; these PERs denote the axioms for types, terms, and substitutions. We need PERs for the evaluation function is defined over syntactical entities and not for typing judgements. We also introduce PERs Nf and Ne whose elements are invariably, in every context, reified as normal forms and neutral terms respectively. Using these PERs we define a family (indexed by denotations of types) of functions for “normalising” in the domain. We conclude this section proving completeness for this family of normalisation functions; here completeness means that two terms in the theory are read back as the same normal form.

5.1. PER semantics. In this subsection we introduce the abstract notion of PER models for our theory. This subsection does not introduce any novelty (except for some notational issues). We refer the reader to [42] for a short report on the historical developments of PER models.

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

If R is a PER over A, and (a, a′) ∈ R then it is clear that (a, a) ∈ R. We define dom(R) = {a ∈ A | (a, a) ∈ R}; clearly, R is an equivalence relation over dom(R). If (a, a′) ∈ R, sometimes we will write a = a′ ∈ R, and a ∈ R if a ∈ dom(R). We denote with PER(A) the set of all PERs over A. Given two PERs R and R′ over A, we say R is included in R′ if (a, a′) ∈ R implies (a, a′) ∈ R′; we denote this inclusion with R ⊆ R′.

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

Definition 5.2 (Applicative structure). An applicative structure is given by a pair A = (A, ·), where A is a set and · is a binary operation on A.

The following definitions are standard (e.g. [10, 21]) in definitions of PER models for dependent types. The first one is even standard for non-dependent types (cf. [43]) and “F-bounded polymorphism” ([17]); its definition clearly shows that equality is interpreted extensionally for dependent function spaces. The second one is the PER corresponding to the interpretation of singleton types; it has as its domain all the elements related to the distinguished element of the singleton, and it relates everything in its domain.

Definition 5.3. Let A be an applicative structure, X ∈ PER(A), and F ∈ X → PER(A).

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

(2) {{a}}_{X} = {(b, b′) | a = b ∈ X and a = b′ ∈ X }.

Besides interpreting function spaces and singletons we need PERs for the denotation of the universe of small types, and for the set of large types; jointly with these PERs we need functions assigning a PER for each element in the domain of these universe PERs. Note that this forces the applicative structure to have some distinguished elements.

Definition 5.4 (Universe). Given an applicative structure A with distinguished elements Fun and Sing, a universe (U, [ ]) is a PER U over A and a family [ ]: U → Per(A) with the condition that U is closed under function and singleton types. This means:

(1) Whenever X = X′ ∈ U and for all a = a′ ∈ [X], F a = F′ a′ ∈ U, then Fun X F = Fun X′ F′ ∈ U, with [Fun X F] = ∏ [X] (a ↦ [F a]).

(2) Whenever X = X′ ∈ U and a = a′ ∈ [X], then Sing a X = Sing a′ X′ ∈ U and [Sing a X] = {{a}}_{[X]}.

An applicative structure paired with one universe for small types and one universe for large types is the minimal structure needed for having a model of our theory.

Definition 5.5 (PER model). Let A be an applicative structure with distinguished elements U, Fun, and Sing; a PER model is a tuple (A, U, T , [ ]) satisfying:

(1) U ⊂ T ∈ P ER(A), such that (T , [ ]) and (U, [ ]↾_{U}) are both universes, and

(2) U ∈ dom(T ), with [U] = U.

In the following definition we introduce an abstract concept for environments: since variables are represented as projection functions from lists (think of q as taking the head of a list, and p as taking the tail), it is enough having sequences together with projections.

Definition 5.6 (Sequences). Given a set A, a set A^{∗} has sequences over A if there are distinguished operations ⊤ : A^{∗}, Pair : A^{∗} × A → A^{∗}, fst : A^{∗} → A^{∗}, and snd : A^{∗} → A such that

fst (Pair a b) = a
snd (Pair a b) = b.

Now we need to extend the notion of PERs over A to PERs over A^{∗} for interpreting substitutions.^{4}

Definition 5.7. Let A be an applicative structure and let A^{∗} have sequences over A; moreover let X ∈ PER(A^{∗}) and F ∈ X → PER(A).

(1) 1 = {(⊤, ⊤)};

(2) ∐ X F = {(a, a′) | fst a = fst a′ ∈ X and snd a = snd a′ ∈ F (fst a)};

Until here we have introduced semantic concepts. Now we are going to axiomatise the notion of evaluation, connecting the syntactic realm with the semantic one.

Definition 5.8 (Environment model). Let (A, U, T , [ ]) be a PER model and let A^{∗} have sequences over A. We call M = (A, U, T , [ ], A^{∗}, [[ ]],^{s}[[ ]]) an environment model if the evaluation functions [[ ]] : Terms × A^{∗} → A and ^{s}[[ ]] : Terms × A^{∗} → A^{∗} satisfy:

s[[id]]a = a
s[[⟨⟩]]a = ⊤
s[[σ δ]]a = [[σ]]([[δ]]a)
s[[(σ, t)]]a = Pair ([[σ]]a) ([[t]]a)
s[[p]]a = fst a

[[U]]a = U
[[Fun A B]]a = Fun ([[A]]a) F, where F b = [[B]](Pair a b)
[[{t}_{A}]]a = Sing ([[t]]a) ([[A]]a)
[[t σ]]a = [[t]](^{s}[[σ]]a)
[[λt]]a = f, where f · b = [[t]](Pair a b)
[[app t u]]a = ([[t]]a) · ([[u]]a)
[[q]]a = snd a

Since no ambiguities arise, we shall henceforth write [[σ]] instead of ^{s}[[σ]].

4The reader is invited to think of 1 as the terminal object of the category of PERs over A^{∗} and PER preserving morphisms; looked this way our definition for 1 does not differ very much from others [10, 21].

Once we have an environment model M we can define the denotation for contexts. The second clause in the next definition is not well-defined a priori; its totality is a corollary of Thm. 5.11.

Definition 5.9. Given an environment model M, we define recursively the semantic of contexts ([ ]): Ctx → PER(A^{∗}):

(1) ([⋄]) = 1,

(2) ([Γ.A]) = ∐ ([Γ])(a ↦ [[[A]]a]) .

We use PERs for validating equality judgements and the domain of each PER for validating typing judgements.

Definition 5.10 (Validity). Let M be an environment model. We define inductively the predicate of satisfability of judgements by the model, denoted with Γ ⊨^{M} J:

(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 5.11 (Soundness of the Judgements). Let M be a model. If Γ ⊢ J, then Γ ⊨^{M} J.

Proof. By easy induction on Γ ⊢ J.

5.2. A concrete PER model. In this subsection we define a concrete PER model over a Scott domain. The definition of the evaluation function is post-poned to the next subsection after introducing the NbE machinery.

Definition 5.12. We define a domain

D = 𝕆 ⊕ Var_{⊥} ⊕ [D → D] ⊕ (D × D) ⊕ (D × D) ⊕ 𝕆 ⊕ (D × [D → D]) ⊕ (D × D) ,

where Var 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].

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} ∈ Var
Lam f  Fun d f  for d ∈ D, and f ∈ [D → D]
App d d′  Sing d d′  for d, d′ ∈ D.

Elements of the form Var x_{i} and App d d′ are called neutral; in this section, we reuse the letter k to denote neutral elements of D.

In order to define an environment model over D, we endow it with an applicative structure. Note also that D has pairing, letting us to take the set of sequences over D simply as D^{∗} = D with Pair a b = (a, b). We define application · : [D × D → D] and the projections fst, snd : [D → D] by

f · d = if f = Lam f′ then f′ d else ⊥,
fst d = if d = (d_{1}, d_{2}) then d_{1} else ⊥,
snd 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 Grégoire and Leroy’s read-back function [31].

Definition 5.13 (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}) = v_{j−(i+1)}

As explained in Sect. 4.2, the reification of variables turns de Bruijn levels into de Bruijn indices. Note that in case j < i + 1 we return the 0th de Bruijn index just not to be undefined; we will come back to this later.

The next PERs contain those elements of the domain D whose reification is defined for any context length. Moreover, their elements are reified as neutral terms and normal forms, respectively; allowing us to reason semantically about normal forms. Remember that t ≡_{T} t′ denotes that t is syntactically equal to t′ and t ∈ T.

Definition 5.14 ((Semantic) neutral terms and normal forms).

d = d′ ∈ Ne : ⟺ for all i ∈ ℕ, R_{i} d and R_{i} d′ are defined and R_{i} d ≡_{Ne} R_{i} d′
d = d′ ∈ Nf : ⟺ for all i ∈ ℕ, R_{i} d and R_{i} d′ are defined and R_{i} d ≡_{Nf} R_{i} d′

Notice that if the case j < i + 1 were undefined in the clause for variables in 5.13, then for any m the application R_{0} Var x_{m} would be undefined; hence Var x_{m} ∉ Ne and, consequently, Ne would be empty. Since we depend on having a semantic representation of variables and neutrals we add the case j < i + 1. This case will not arise in our use of the readback function.

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

Lemma 5.16 (Closure properties of Ne and Nf ).

(1) U = U ∈ Nf .

(2) Let X = X′ ∈ Ne. If F · k = F′ · k′ ∈ Nf for all k = k′ ∈ Ne, then Fun X F = Fun X′ F′ ∈ Nf .

(3) If d = d′ ∈ Nf and X = X′ ∈ Nf , then Sing d X = Sing d′ X′ ∈ Nf .

(4) If f · k = f′ · k′ ∈ Nf for all k = k′ ∈ Ne, then f = f′ ∈ Nf .

(5) Var x_{i} = Var x_{i} ∈ Ne for all i ∈ ℕ.

(6) If k = k′ ∈ Ne and d = d′ ∈ Nf , then App k d = App k′ d′ ∈ Ne.

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

Definition 5.17 (PER model).

(1) Inductive definition of U ∈ PER(D).

(a) Ne ⊆ U,

(b) if X = X′ ∈ U and d = d′ ∈ [X], then Sing d X = Sing d′ X′ ∈ U, (c) if X = X′ ∈ U and for all d = d′ ∈ [X], F d = F′ d′ ∈ U then Fun X F =

Fun X′ F′ ∈ U.

(2) Inductive definition of T ∈ PER(D).

(a) U ⊆ T ,

(b) U = U ∈ T ,

(c) if X = X′ ∈ T , and d = d′ ∈ [X] then Sing d X = Sing d′ X′ ∈ T ,

(d) if X = X′ ∈ T , and for all d = d′ ∈ [X], F d = F′ d′ ∈ T , then Fun X F =

Fun X′ F′ ∈ T .

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

(a) [U] = U,

(b) [Sing d X] = {{d}}_{[X]},

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

(d) [d] = Ne, in all other cases.

Remark 5.18. 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.19. The function [ ] : dom(T ) → PER(D) is a family of PER(D) over T , i.e., [ ] : T → PER(D).

Proof. By induction on X = X′ ∈ T . See Appendix C.1.

The previous lemma leads us to the definition of a PER model over D. Note also that D has all the distinguished elements needed to call it a syntactical applicative structure.

Corollary 5.20. The tuple (D, U, T , [ ]) is a PER model.

5.3. Normalisation and η-Expansion in the Model. In the following, we adopt the NbE algorithm outlined in Section 4 to the dependent type theory λ^{Sing}. Since read-back has already be defined, we only require reflection, reification and evaluation functions.

Definition 5.21 (Reflection and reification). The partial functions ↑ , ↓ : [D → [D → D]] and ⇓ : [D → D] are given as follows:

↑_{Fun X F} k = Lam (d ↦ ↑_{F d} (App k ↓_{X} d))
↑_{Sing d X} k = d
↑_{U} k = k
↑_{X} k = k, in all other cases.

↓_{Fun X F} d = Lam (e ↦ ↓_{F ↑_{X} e} (d · ↑_{X} e))
↓_{Sing d X} e = ↓_{X} d
↓_{U} d = ⇓ d
↓_{X} e = e, in all other cases.

⇓(Fun X F) = Fun (⇓ X) (d ↦ ⇓(F ↑_{X} d))

⇓(Sing d X) = Sing (↓_{X} d) (⇓ X)

⇓ U = U

⇓ X = X, in all other cases.

In the following lemma we show that reflection ↑ corresponds to Berger and Schwichtenberg’s “make self evaluating” and both reification functions ↓ and ⇓ correspond to“inverse of the evaluation function” [16]. Note that they are indexed by types values instead of syntactic types, since we are dealing with dependent instead of simple types.

Lemma 5.22 (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 . See C.2.

Let us recapitulate what we have achieved: we have defined a PER model over the domain D; then we defined a family of functions ↓_{X} indexed over denotation of types with the property that when applied to elements in the corresponding PER we get back elements which will be reified as normal forms. In fact, we have the stronger result that whenever we apply ↓_{X} to two related elements d = d′ ∈ [X] we get elements to be reified as the same term.

Now we define evaluation which clearly satisfies the environment model conditions in Def. 5.8; hence, we have a model and, using Thm. 5.11, we conclude completeness for our normalisation algorithm.

Definition 5.23 (Semantics). Evaluation of substitutions and terms into D is defined inductively by the following equations.

Substitutions.

[[⋄]]d = ⊤  [[id]]d = d
[[(γ, t)]]d = ([[γ]]d, [[t]]d)  [[p]]d = fst 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 = snd d

Theorem 5.24 (Completeness of NbE). Let Γ ⊢ t = t′ : A and let also d ∈ ([Γ]), then ↓_{[[A]]d} [[t]]d = ↓_{[[A]]d} [[t′]]d ∈ Nf .

Proof. By Thm. 5.11 we have [[t]]d = [[t′]]d ∈ [[[A]]d] and we conclude by Lem. 5.22.

5.4. Calculus λ^{Irr}with proof irrelevance. We extend all the definitions concerning the construction of the model.

Definition 5.25 (Extension of domain D).

D = … ⊕ D × [D → D] ⊕ D ⊕ D
⊕ 𝕆 ⊕ 𝕆 ⊕ D ⊕ [D → D] × D × [D → [D → D]] × D
⊕ D ⊕ 𝕆 ⊕ ℕ ⊕ ℕ × ℕ ⊕ ℕ × [D → D] × D^{ω} × D .

We use the following notations for the injections into D:

Sum d F  Fst d, Snd d  for d ∈ D, F ∈ [D → D]
zero  Nat  ⋆
suc d  Prf d  for d ∈ D
N_{n}  c_{i}^{n}  for i, n ∈ ℕ
Natrec(F, d, g, d′)  for d, d′ ∈ D, F ∈ [D → D], g ∈ [D → [D → D]]
Case^{n}(F, d⃗, d′)  for d, d′ ∈ D, F ∈ [D → D], d⃗ ∈ D^{ω}, n ∈ ℕ

In this extension, the injections Fst, Snd, Natrec, and Case construct neutral elements k. Soundness for the calculus (⊢^{⋆}) requires the canonical element for proof-irrelevant types (⋆) to be in every PER; thus we need to redefine application · to have ⋆ ∈ [Fun X F]:

⋆ · d = ⋆ .

We also redefine the projections fst and snd to account for neutrals and because they are used in the definition of ∐ XF, which will be used as the denotation of sigma types.

fst d = \begin{cases}d_{1} & if d = (d_{1}, d_{2}) \\ ⋆ & if d = ⋆ \\ Fst d & otherwise \end{cases} snd d = \begin{cases}d_{2} & if d = (d_{1}, d_{2}) \\ ⋆ & if d = ⋆ \\ Snd d & otherwise \end{cases}

Definition 5.26 (Read-back function).

R_{j} (Sum X F) = Σ (R_{j} X)
(R_{j+1} (F Var x_{j}))
R_{j} Nat = Nat
R_{j} zero = zero
R_{j} (suc d) = suc (R_{j} d)
R_{j} (Prf d) = Prf (R_{j} d)
R_{j} (N_{n}) = N_{n}

R_{j} (d, d′) = (R_{j} d, R_{j} d′)
R_{j} (Fst d) = fst (R_{j} d)
R_{j} (Snd d) = snd (R_{j} d)
R_{j} (Natrec(F, d, f, e)) = natrec (R_{j+1} (F Var x_{j}))
(R_{j} d) (R_{j} f) (R_{j} e)
R_{j} ⋆ = ⋆
R_{j} (c_{i}^{n}) = c_{i}^{n}
R_{j} (Case^{n}(F, ⟨d_{0}, …, d_{n−1}⟩, e)) = case^{n} (R_{j+1} (F Var x_{j})) (R_{j} d_{0}) ⋯ (R_{j} d_{n−1}) (R_{j} e)

We define inductively new PERs for interpreting naturals and finite types. Note that C_{0} and C_{1} are irrelevant, in this way we can model η-expansion for N_{0} and N_{1}; |X | is also irrelevant, even when X distinguishes its elements.

Definition 5.27 (More semantic types).

(1) N is the smallest PER over D, such that (a) Ne ⊆ N

(b) zero = zero ∈ N

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

(2) If X ∈ PER(D) then |X | := {(d, d′) | d, d′ ∈ dom(X) ∪ {⋆}} ∈ PER(D).

(3) C_{0} = |∅| = {(⋆, ⋆)},

(4) C_{1} = |{c_{0}^{1}}| = {(d, d′) | d, d′ ∈ {⋆, c_{0}^{1}}},

(5) C_{n} = {(c_{i}^{n}, c_{i}^{n}) | i < n} ∪ Ne, for n ⩾ 2.

We add new clauses in the definitions of the partial equivalences for universe and types, these clauses do not affect the well-foundedness of the order ⊏ defined in 5.18, but now we have that N_{n} and Nat are also minimal elements for that order.

Definition 5.28 (Extension of U and T ).

(1) Inductive definition of U ∈ PER(D).

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

(b) Nat = Nat ∈ U,

(c) N_{n} = N_{n} ∈ U,

(d) if X = X′ ∈ U, then Prf X = Prf X′ ∈ U.

(2) Inductive definition of T ∈ PER(D).

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

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

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

(a) [Sum X F] = ∐ [X] (d ↦ [F d]),

(b) [N_{n}] = C_{n}

(c) [Nat] = N,

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

Note that in the PER model, all propositions Prf X are inhabited. In fact, all types are inhabited, for 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 non-empty types.

Remark 5.29. It can be proved by induction on X ∈ T that ⋆ ∈ [X].

Definition 5.30 (Reflection and reification, cf. 5.21).

↑_{Sum X F} k = (↑_{X} Fst k, ↑_{F (↑_{X} Fst k)} Snd k)
↑_{Nat} k = k
↑_{N_{0}} k = ⋆
↑_{N_{1}} k = c_{0}^{1}
↑_{N_{n}} k = k  for n ⩾ 2
↑_{Prf X} k = ⋆

↓_{Sum X F} d = (↓_{X} fst d, ↓_{F (fst d)} snd d)
↓_{Nat} d = d
↓_{N_{0}} d = ⋆
↓_{N_{1}} d = c_{0}^{1}
↓_{N_{n}} d = d
↓_{Prf X} d = ⋆
⇓ Sum X F = Sum (⇓ X) (d ↦ ⇓(F ↑_{X} d))  ⇓ Nat = Nat
⇓ N_{n} = N_{n}  ⇓ Prf X = Prf (⇓ X)

For giving semantics to eliminators for data types we need to define partial functions natrec : [D → D] × D × D × D → D, and case : [D → D] × D × D × D → D.

Definition 5.31 (Eliminations on D).

(1) Elimination operator for naturals.

natrec(F, d, f, ⋆)  = ⋆
natrec(F, d, f, zero) = d
natrec(F, d, f, suc e) = (f · e) · natrec(F, d, f, e)
natrec(F, d, f, k)  = ↑_{F k} (Natrec(\begin{matrix}d′ ↦ ⇓ F d′, \\ ↓_{F zero} d, \\ Lam d′ ↦ (Lam e′ ↦ ↓_{F (suc d′)} f · d′ · e′), \\ k)) \end{matrix}

(2) Elimination operator for finite types.

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

Remark 5.32. 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 natrec(F, z, s, d) = natrec(F, z, s, d′) ∈ [F d].

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

Definition 5.33 (Extension of interpretation).

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

Lemma 5.34 (Laws of proof elimination). β, η, and associativity for where are modeled by the extended applicative structure.

Proof. See C.3.

Remark 5.35. All of lemmata 5.19, 5.22, and theorems 5.11, and 5.24 are valid for the extended calculus.

Note that we have defined a proof-irrelevant semantics for (⊢^{⋆}) that collapses all elements of Prf A to ⋆, which leads to a more efficient implementation of the normalisation function. However, this semantics is not sound if λ^{Irr} is extended with singleton types interpreted analogously to C_{1}, i.e., [Sing d X] = |{{d}}_{X}|, because it does not model (sing-eq-el). (We have d = ⋆ ∈ [Sing d X] for all d ∈ [X], but not necessarily d = ⋆ ∈ [X].) On the other hand, λ^{Irr} without ⋆ can be extended to singleton types as explained in the following remark.

Remark 5.36 (Extending λ^{Irr} by singleton types). Singleton types can be added straightforwardly if we employ a proof-relevant semantics:

The domain D is not changed; in particular we have ⋆ ∈ D, and it is readback as before, R_{j} ⋆ = ⋆; hence ⋆ ∈ dom(Nf ).

All the enumerated types are modelled in a uniform way: [N_{n}] = {(c_{i}^{n}, c_{i}^{n}) | i < n}∪Ne; proof-irrelevance types Prf A are interpreted as the irrelevant PER with the same domain as the PER for A: [Prf X] = {(d, d′) | d, d′ ∈ dom([X])}. Reflection and reification for Prf X are defined respectively as

↑_{Prf X} d = ↑_{X} d  and  ↓_{Prf X} d = ⋆ .

With these definitions it is clear that the corresponding result for Lem. 5.22 is still valid.

Since dom([Prf X]) = dom([X]), introduction and elimination of proofs can be interpreted as follows

[[[a]]]d = [[a]]d and [[b where^{B} t]]d = [[b]](d, [[t]]d) ;

this model is sound with respect to the calculus (⊢) extended with singleton types; hence Thm. 5.24 is valid.

Remark 5.37. As was previously said we cannot use this PER model for proving that there is no closed term in N_{0}. Instead, one can build up a PER model, in the sense of 5.1, of closed values, where [N_{0}] = ∅. By soundness (Thm. 5.11) it follows that there is no possible derivation of ⊢ t : N_{0}.

6. Correctness of NbE

In Thm. 5.24 we have proved that the NbE algorithm is complete with respect to the judgemntal equality of our calculi; a corollary of that fact is totality of NbE.

Remark 6.1. Let Γ ⊢ t : A. Given some d ∈ ([Γ]), we can conclude R_{i} (↓_{[[A]]d} [[t]]d) is a well-defined term in normal form.

In this section we prove correctness, with respect to the typing rules, for our NbE algorithm. This means that given a typing Γ ⊢ t : A, when NbE is applied to t, the resulting normal form v, is provable equal to t; i.e. Γ ⊢ t = v : A.

Let us anticipate the main results of this section. As a corollary of Thm. 6.11 we show that a term is related to its denotation with respect to some canonical environment (to be defined in Def. 6.12). Previously we prove in Lem. 6.6 that if a term is logically related with some semantic element, then its reification will be judgmentally equal to the term. Composing these facts we obtain correctness. As a consequence of having correctness and completeness for NbE, one gets decidability for judgmentally equality: normalise both terms and check they are syntactically the same. Another important corollary is injectivity for constructors.

6.1. Logical relations. In this subsection we define logical relations and prove some technical lemmas about them. As is standard with logical relations one defines them by induction on types (here we define by induction on semantics of types, i.e. elements of T ) and for basic types they are defined by prescribing the property to be proved; while for higher order types they are defined using the relations of the domain and image types.

Definition 6.2 (Logical relations). We define simultaneously two families of binary relations:

(a) If Γ ⊢ then (Γ ⊢ ∼ ∈ T ) ⊆ {A | Γ ⊢ A} × T shall be a Γ-indexed family of relations between well-formed syntactic types A and type values X.

(b) If Γ ⊢ A ∼ X ∈ T then (Γ ⊢ : A ∼ ∈ [X]) ⊆ {t | Γ ⊢ t : A} × [X] shall be a (Γ, A, X)-indexed family of relations between terms t of type A and values d in PER [X].

These relations are defined simultaneously by induction on X ∈ T .

(1) Neutral types: X ∈ Ne.

(a) Γ ⊢ A ∼ X ∈ T iff for all Δ ⩽^{i} Γ, Δ ⊢ A p^{i} = R_{|Δ|} ⇓ X.

(b) Γ ⊢ t : A ∼ d ∈ [X] iff Γ ⊢ A ∼ X ∈ T , and for all Δ ⩽^{i} Γ, Δ ⊢ t p^{i} = R_{|Δ|} ↓_{X} d :

A p^{i}.

(2) Universe.

(a) Γ ⊢ A ∼ U ∈ T iff Γ ⊢ A = U.

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

(3) Singletons.

(a) Γ ⊢ A ∼ Sing d X ∈ T iff Γ ⊢ A = {a}_{A′} and Γ ⊢ a : A′ ∼ d ∈ [X].

(b) Γ ⊢ t : A ∼ d′ ∈ [Sing d X] iff Γ ⊢ A = {a}_{A′} and Γ ⊢ t : A′ ∼ d ∈ [X], and

Γ ⊢ A′ ∼ X ∈ T .

(4) Function spaces.

(a) Γ ⊢ 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].

(b) Γ ⊢ 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 technical lemmata show that the logical relations are preserved by judgmental equality, weakening of the judgement, and the equalities on the corresponding PERs. These lemmata are proved simultaneously for types and terms.

Lemma 6.3 (Closure under conversion). Let Γ ⊢ A ∼ X ∈ T and Γ ⊢ A = A′. Then,

(a) Γ ⊢ A′ ∼ X ∈ T , and

(b) if Γ ⊢ t : A ∼ d ∈ [X] and Γ ⊢ t = t′ : A then Γ ⊢ t′ : A′ ∼ d ∈ [X].

Proof. By induction on X ∈ T . See C.4.

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

(a) if Γ ⊢ A ∼ X ∈ T , then Δ ⊢ A p^{i} ∼ X ∈ T ; and

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

Proof. By induction on X ∈ T . See C.5.

Lemma 6.5 (Closure under PERs). Let Γ ⊢ A ∼ X ∈ T , then

(a) if X = X′ ∈ T , then Γ ⊢ A ∼ X′ ∈ T ; and

(b) if Γ ⊢ t : A ∼ d ∈ [X] and d = d′ ∈ [X], then Γ ⊢ t : A ∼ d′ ∈ [X].

Proof. By induction on X = X′ ∈ T . See C.6.

The following lemma plays a key rôle 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 6.6. Let Γ ⊢ A ∼ X ∈ T . Then,

(a) Γ ⊢ A = R_{|Γ|} ⇓ X,

(b) if Γ ⊢ t : A ∼ d ∈ [X] then Γ ⊢ t = R_{|Γ|} ↓_{X} d : A; and

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

Proof. By induction on X ∈ T . See C.7.

In order to finish the proof of soundness we have to prove that each well-typed 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 6.7 (Logical relation for substitutions).

(1) Γ ⊢ σ : ⋄ ∼ d ∈ 1 always holds.

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

By the way this relation is defined, the counterparts of 6.3, 6.4, and 6.5 are easily proved by induction on the co-domain of the substitutions.

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

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

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

Theorem 6.11 (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. See C.9.

We define for each context Γ an element ρ_{Γ} of D. This environment will be used to define the normalisation function.

Definition 6.12 (Canonical environment). We define ρ_{Γ} by induction on Γ as follows:

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

By an immediate induction on contexts we can check the following.

Lemma 6.13. If Γ ⊢ then Γ ⊢ id_{Γ} : Γ ∼ ρ_{Γ} ∈ ([Γ]).

Proof. By induction on Γ ⊢. See C.8

6.2. Main results. Now we can define concretely the normalisation function as the composition of reification with normalisation after evaluation under the canonical environment. The following corollaries just instantiate previous lemmata and theorems concluding correctness of NbE.

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

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

Notice that if we instantiate Thm. 6.11 with ρ_{Γ}, then a well-typed term t under Γ will be logically related to its denotation. Finally, using the key lemma 6.6 we conclude correctness for NbE.

Corollary 6.15. Let Γ ⊢ A, and Γ ⊢ t : A, then by fundamental theorem of logical relations (and Lem. 6.3),

(1) Γ ⊢ A ∼ [[A]]ρ_{Γ} ∈ T ; and

(2) Γ ⊢ t : A ∼ [[t]]ρ_{Γ} ∈ [[[A]]ρ_{Γ}],

Corollary 6.16 (Soundness of NbE). By way of Lem. 6.6, it follows immediately

(1) Γ ⊢ A = nbe(A), and

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

We have now a decision procedure for judgmental equality; for deciding Γ ⊢ t = t′ : A, put both terms in normal formal and check if they are syntactically equal.

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

As a byproduct we can conclude that type constructors are injective; this result is exploited in the next section where we introduce the type-checking algorithm. Injectivity of Fun plays a key rôle in all versions of dependent type theory with equality as judgement; cf. Adams’ [7] proof of equivalence between PTS with equality as a judgement and equality taken as a relation between untyped terms, improved by Siles and Herbelin [52].

Remark 6.18. By expanding 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 6.19 (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.

6.3. Calculus λ^{Irr}with proof irrelevance. In this section we introduce the logical relations for the new types in λ^{Irr}. We skip the re-statement of the results given for λ^{Sing} in 6.1, instead we present in Appendix C the proof for some of the new cases arising in this calculus for each of lemmata 6.3, 6.4, 6.5, 6.6 and theorem 6.11.

Definition 6.20 (cf. 6.2).

(1) Sigma types.

(a) Γ ⊢ 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.

(b) Γ ⊢ t : A ∼ d ∈ [Sum X F] iff Γ ⊢ A = Σ A′ B′ and Γ ⊢ fst t : A′ ∼ fst d ∈ [X] and

Γ ⊢ snd t : B′ (id_{Γ}, fst t) ∼ snd d ∈ [F (fst d)].

(2) Natural numbers.

(a) Γ ⊢ A ∼ Nat iff Γ ⊢ A = Nat.

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

(3) Finite types.

(a) Γ ⊢ A ∼ N_{n} iff Γ ⊢ A = N_{n}.

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

(4) Proof-irrelevance types.

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

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

Remark 6.21.

(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 6.22. If Γ ⊢ Σ A B = Σ A′ B′, then Γ ⊢ A = A′, and Γ.A ⊢ B = B′.

7. Type-checking algorithm

In this section, we define a couple of judgements that represent a bidirectional type checking algorithm for terms in normal form; its implementation in Haskell can be found in the appendix. The algorithm is similar to previous ones [20, 4], in that it proceeds by analysing the possible types for each normal form, and succeeds only if the type’s shape matches the one required by the introduction 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 checks that the deepest tag of the normalised type (see Def. 7.2) has the form of the type of the introductory rule; or one adds 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.

Our algorithm depends on having a good normalisation function; note that this function does not need to be based on normalisation by evaluation. Also note that the second point asks for having correctness and completeness of the normalisation function.

Definition 7.1 (Good normalisation function).

(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.

From these properties we can prove the injectivity of Fun which is crucial for completeness of type checking λ-abstractions.

7.1. Type-checking λ^{Sing}. In this section, let V, V′, W, v, v′, w ∈ Nf , and k ∈ Ne. For obtaining the deepest tag of a singleton type, we define an operation on types, which is essentially the same as the one defined by Aspinall [10].

Definition 7.2 (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 7.3 (Type-checking and type-inference). We define three mutually inductive algorithmic judgements

Γ ⊢ V ⇐ in context Γ, normal type V checks
Γ ⊢ v ⇐ V in context Γ, normal term v checks against type V
Γ ⊢ k ⇒ V in context Γ, the type of neutral term k is inferred as V .

All three judgements presuppose and maintain the invariant the input Γ is a well-formed context. The procedures Γ ⊢ V ⇐ and Γ ⊢ v ⇐ V expect their inputs V and v in β-normal form. Inference Γ ⊢ k ⇒ V expects a neutral term k and returns its principal type V in long normal form.

Well-formedness checking of types Γ ⊢ V ⇐.

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

Type checking terms Γ ⊢ v ⇐ V.

\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.

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

Bidirectional type checking for dependent function types is well-understood [20, 35]; let us illustrate briefly how it works for singleton types, by considering the type checking problem {zero}_{Nat} ⊢ q ⇐ {zero}_{Nat}. Here is a skeletal derivation of this judgement, which is at the same time a execution trace of the type checker:

\{zero\}_{Nat} ⊢ q ⇒ \{zero\}_{Nat}  \{zero\}_{Nat} ⊢ \overline{\{zero\}_{Nat}} = Nat \{zero\}_{Nat} ⊢ q ⇐ Nat  \{zero\}_{Nat} ⊢ q = zero : Nat
{zero}_{Nat} ⊢ q ⇐ {zero}_{Nat}

Since the type to check against is a singleton, the algorithm proceeds by checking {zero}_{Nat} ⊢ q ⇐ Nat and {zero}_{Nat} ⊢ q = zero : Nat. Now the type of the neutral q is inferred and its tag compared to the given type Nat; as the tag is also Nat, the check succeeds. The remaining equation {zero}_{Nat} ⊢ q = zero : Nat is derivable by (sing-eq-el). Of course, the equations are checked by the nbe( ) function; for example, by using our own function for normalisation we have nbe_{{zero}_{Nat}}^{Nat}(q) = zero = nbe_{{zero}_{Nat}}^{Nat}(zero).

Theorem 7.4 (Correctness of type-checking).

(1) If Γ ⊢ V ⇐, then Γ ⊢ V.

(2) If Γ ⊢ v ⇐ V, then Γ ⊢ v : V.

(3) If Γ ⊢ k ⇒ V, then Γ ⊢ k : V.

Proof. By simultaneous induction on Γ ⊢ V ⇐, Γ ⊢ v ⇐ V, and Γ ⊢ V ⇒ k. See C.10.

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 7.5. 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 7.6 (Completeness of type-checking).

(1) If Γ ⊢ V, then Γ ⊢ V ⇐.

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

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

Proof. We prove these three statements simultaneously by well-founded induction on the order ≺. The respective measures are (1) (V, U), (2) (v, A), and (3) (k, A). Details are in the Appendix C.11.

7.2. Calculus λ^{Irr}with proof irrelevance. We give additional rules for type-checking and type-inference algorithms for the constructs added in Sect. 2.2. Remember that we distinguished two calculi: the calculus (⊢^{⋆}) has rules (n_{0}-tm) and (prf-tm); while (⊢) lacks those rules.

Definition 7.7 (Type-checking and type-inference). Σ-types.

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

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

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

Natural numbers.

\overline{Γ ⊢ Nat ⇐}

\overline{Γ ⊢ Nat ⇐ U}

Γ ⊢ zero ⇐ Nat

\frac{Γ ⊢ v ⇐ Nat}{Γ ⊢ suc v ⇐ Nat}

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

Finite types.

\overline{Γ ⊢ N_{n} ⇐}  \overline{Γ ⊢ N_{n} ⇐ U}  \frac{i < n}{Γ ⊢ c_{i}^{n} ⇐ N_{n}}

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

Proof types.

\frac{Γ ⊢ V ⇐}{Γ ⊢ Prf V ⇐}  \frac{Γ ⊢ V ⇐ U}{Γ ⊢ Prf V ⇐ U}  \frac{Γ ⊢ v ⇐ V}{Γ ⊢ [v] ⇐ Prf V}

\frac{Γ ⊢ W ⇐  Γ ⊢ k ⇒ Prf V  Γ.V ⊢ v ⇐ nbe(W p)  Γ.V.V p ⊢ vp = v(pp, q) : W pp}{Γ ⊢ v where^{W} k ⇒ W}

We do not show the proof for correctness, because nothing is to be gained from it; suffice it to say that we can prove correctness with respect to (⊢^{⋆}).

Theorem 7.8. The type-checking algorithm is sound with respect to the calculus ⊢^{⋆}.

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

It is clear that the given rules are not complete for checking (⊢^{⋆}), because there is no rule for checking Γ ⊢ ⋆ ⇐ A. Note that it is not possible to have a sound and complete type-checking algorithm with respect to (⊢^{⋆}), for it would imply the decidability of typeinhabitation. Since type checking happens always before normalisation, we can still use a good normalisation function with respect to the calculus (⊢^{⋆}) for normalising types or deciding equality. Indeed, if the term to type-check does not contain ⋆, the need of checking Γ ⊢ ⋆ ⇐ V will never arise; this is clearly seen by verifying that only sub-terms are typechecked in the premises.

Theorem 7.9. The type-checking algorithm is complete with respect to the calculus (⊢).

Proof. By simultaneous induction on the normal form of types and terms, using inversion on the typing judgement and correctness of nbe( ).

Corollary 7.10. The type-checking algorithm is correct (by Thm. 7.8 and Cor. 2.15) and complete with respect to the calculus (⊢).

8. Conclusion

The main contributions of the paper are the definition of a correct and complete typechecking algorithm, and a simpler solution to the problem of generating fresh identifiers in 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 NbE algorithm can be implemented fairly easily in Haskell (cf. Appendix A), but the correctness of the implementation depends on proving the computational adequacy of the domain semantics with respect to Haskell’s operational semantics. We have not developed this proof in this article and leave it for to future work.

8.1. Related and Further Work on Singleton Types. Singleton types are used to model the SML module system and records with manifest fields [21].

Aspinall [10] presents a logical framework with singleton types and subtyping and shows its consistency via a PER model, yet not decidability. The second author, Pollack, and Takeyama [21] extend the Aspinall’s framework by η-equality and records and a type checking algorithm which is correct wrt. the PER model. This work is unconventional since there is no complete syntactical specification of the LF in terms of syntax, typing and equality rules. Instead, in the style of Martin-Löf meaning explanations, they list a number of inference rules which are valid in the semantics and prove that type-checked expressions evaluate to values of the correct semantic type.

Courant [22] shows strong normalization for a variant of Aspinall’s system with equality defined by reduction. He uses a typed Kripke model of strongly normalizing terms, a variant of Goguen’s typed operational semantics [29].

Stone and Harper [54] extend Aspinall’s framework by sigma types and eta-equality, which allows them to reduce singletons at higher types to singletons at base type. Their decision procedure is type-directed, its completeness is shown via a Kripke model. Crary [23] gives a simplified decision procedure via hereditary substitutions and proves its correctness in Twelf, without the need for a model construction. His purely syntactical approach does not scale to universes, since he cannot handle types defined by recursion. Goguen [30] follows a similar agenda, he shows decidability for singleton types in the presence of eta by an eta-expanding translation into a logical framework with beta-equality only. He works with fully annotated terms in the sense of Streicher [55]. He stresses that his approach does not scale to computation on the type level.

In the continuation of this work we want to investigate whether our type-checking algorithm can be simplified if we implement Stone and Harper’s insight that singleton types at higher types can be defined in terms of singleton base types. Further, we would like to integrate subtyping in our calculus, which should not be too difficult, since the PER model already supports subtyping [10, 21].

8.2. Related and Further Work on Proof Irrelevance. Pfenning [47] presents a logical framework with proof irrelevance that supports irrelevant function arguments, with function introduction rule (writing (x:Prf A) → B in our syntax):

\frac{Γ, x ÷ A ⊢ B Γ, x ÷ A ⊢ t : B}{Γ ⊢ λxt : (x:Prf A) → B}

He proves decidability using erasure, mentioning that his technique does not scale to universes. Elimination of irrelevance is implicitly handled by annotating variables to ensure proof variables (x÷A) appear only in proofs, in contrast to our explicit use of where [ ] ← in the style of Awodey and Bauer [11]. However, we believe that Pfenning’s proof irrelevance can be modeled via bracket types Prf A, with the weaker “monadic” rule for where (see section 2).

Barras and Bernardo’s [13] presentation of proof irrelevant functions

\frac{Γ, x : A ⊢ B  Γ, x : A ⊢ t : B  x ∉ FV(t^{∗})}{Γ ⊢ λxt : (x:Prf A) → B}

diverges from Pfenning’s that they allow irrelevant variables x to be relevant in types B. (In t the variable x might only appear irrelevantly, expressed by the side condition that x may not be free in the relevant parts t^{∗} of t.) Barras and Bernardo justify their calculus by erasing into Miquel’s Implicit Calculus of Constructions (ICC) [41]. The ICC style irrelevance seems more expressive than Awodey and Bauer’s or Pfenning’s, but the exact relationship is unclear to us.

Berger’s Uniform Heyting Algebra [15] features uniform quantification {∀x}A (and {∃x}A) to obtain optimized programs by extraction from proofs. A proof of a uniform universal

\frac{Γ ⊢ M : A}{Γ ⊢ \{∀\}^{+}(λxM) : \{∀x\}A}

may not mention term variable x in a computational relevant position. Since the shape of formulas does not depend on terms, Berger’s calculus can be seen as logical counterpart of either Pfenning’s or Bruno and Bernardo’s type system.

We see two interesting questions about the different approaches to proof irrelevance above:

(1) How can Barras and Bernardo’s ICC^{∗} be understood in terms of judgmental equality à la Pfenning?

(2) How can ICC^{∗} and the calculus of Pfenning be extended to full bracket types à la Awodey and Bauer without explicit use of where.

Acknowledgments. The authors have led many discussions with Peter Dybjer on normalization by evaluation, generalized algebraic theories, and presentation of type theory as categories with families. The authors thank the referees of a previous version of this article for their helpful comments. The authors are also grateful for the suggestions made by the anonymous referees on this long version.

References

[1] Abadi, M., Cardelli, L., Curien, P. L., Lévy, J. J.: Explicit substitutions. In: POPL ’90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, NY, USA (1990), 31–46

[2] 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

[3] 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

[4] 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 (2008), 3–13

[5] Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic βη-conversion test for Martin-Löf type theory. In: Audebaud, P., Paulin-Mohring, C., eds., Proc. of the 9th Int. Conf. on Mathematics of Program Construction, MPC 2008, volume 5133 of Lect. Notes in Comput. Sci. Springer (2008), 29–56

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

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

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

[9] Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P. J.: Normalization by evaluation for typed lambda calculus with coproducts. In: Proc. of the 16th IEEE Symp. on Logic in Computer Science (LICS 2001). IEEE Computer Soc. Press (2001), 303–310 [10] 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 (1995), 1–15

[11] Awodey, S., Bauer, A.: Propositions as [Types]. J. Log. Comput. 14 (2004) 447–471

[12] Balat, V., Cosmo, R. D., Fiore, M. P.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In: Jones, N. D., Leroy, X., eds., Proc. of the 31st ACM Symp. on Principles of Programming Languages, POPL 2004. ACM Press (2004), 64–76

[13] Barras, B., Bernardo, B.: The implicit calculus of constructions as a programming language with dependent types. In: Amadio, R. M., ed., FoSSaCS, volume 4962 of Lecture Notes in Computer Science. Springer (2008), 365–379

[14] Berardi, S.: About the sets-as-propositions embedding of HOL in CC (2004)

[15] Berger, U.: Uniform Heyting arithmetic. Ann. Pure Appl. Logic 133 (2005) 125–148

[16] 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

[17] Bruce, K., Mitchell, J. C.: Per models of subtyping, recursive types and higher-order polymorphism. In: POPL ’92: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, NY, USA (1992), 316–327

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

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

[20] Coquand, T.: An algorithm for type-checking dependent types. In: Proc. of the 3rd Int. Conf. on Mathematics of Program Construction, MPC ’95, volume 26 of Sci. Comput. Program. Elsevier (1996), 167–177

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

[22] Courant, J.: Strong normalization with singleton types. In: Intersection Types and Related Systems (ITRS 2002), volume 70 of Electr. Notes in Theor. Comp. Sci. Elsevier (2002)

[23] Crary, K.: A syntactic account of singleton types via hereditary substitution. In: Cheney, J., Felty, A., eds., 4th Int. Wksh. on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2009). ACM Press (2009), 21–29

[24] Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M., eds., Types for Proofs and Programs, Int. Wksh., TYPES’95, volume 1158 of Lect. Notes in Comput. Sci. Springer (1996), 120–134

[25] Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Logic 65 (2000) 525–549

[26] Filinski, A., Rohde, H. K.: A denotational account of untyped normalization by evaluation. In: Walukiewicz, I., ed., Proc. of the 7th Int. Conf. on Foundations of Software Science and Computational Structures, FoSSaCS 2004, volume 2987 of Lect. Notes in Comput. Sci. Springer (2004), 167–181

[27] Garillot, F., Werner, B.: Simple types in type theory: Deep and shallow encodings. In: Schneider, K., Brandt, J., eds., Theorem Proving in Higher Order Logics, TPHOLs 2007, volume 4732 of Lect. Notes in Comput. Sci. Springer (2007), 368–382

[28] Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types, volume 7 of Cambridge Tracts in Theoret. Comput. Sci. Cambridge University Press (1989)

[29] Goguen, H.: A Typed Operational Semantics for Type Theory. Ph.D. thesis, University of Edinburgh (1994). Available as LFCS Report ECS-LFCS-94-304

[30] Goguen, H.: A syntactic approach to eta equality in type theory. In: Palsberg, J., Abadi, M., eds., Proc. of the 32nd ACM Symp. on Principles of Programming Languages, POPL 2005. ACM Press (2005), 75–84

[31] 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

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

[33] INRIA: The Coq Proof Assistant, Version 8.1. INRIA (2007). http://coq.inria.fr/ [34] 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

[35] Löh, A., McBride, C., Swierstra, W.: A tutorial implementation of a dependently typed lambda calculus. Fundam. Inform. 102 (2010) 177–207

[36] Maillard, O.-A.: Proof-irrelevance, strong-normalisation in Type-Theory and PER. Technical report, Chalmers Institute of Technology (2006)

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

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

[39] 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

[40] 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 (2005), 130–170

[41] Miquel, A.: The implicit calculus of constructions. In: Abramsky, S., ed., Proc. of the 5th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2001, volume 2044 of Lect. Notes in Comput. Sci. Springer (2001), 344–359

[42] Mitchell, J. C.: A type-inference approach to reduction properties and semantics of polymorphic expressions (summary). In: LFP ’86: Proceedings of the 1986 ACM conference on LISP and functional programming. ACM, New York, NY, USA (1986), 308–319

[43] Mitchell, J. C.: Type systems for programming languages. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) (1990), 365–458

[44] Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in computer science. IEEE Press, Piscataway, NJ, USA (1989), 14–23

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

[46] Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis, Dept of Comput. Sci. and Engrg., Chalmers, Göteborg, Sweden (2007)

[47] Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: LICS 2001: IEEE Symposium on Logic in Computer Science (2001)

[48] Plotkin, G.: LCF considered as a programming language. Theor. Comput. Sci. 5 (1977) 223–255

[49] Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T., eds., Types for Proofs and Programs (TYPES’93), Nijmegen, The Netherlands, volume 806 of Lect. Notes in Comput. Sci. Springer (1994), 313–332

[50] 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

[51] 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

[52] Siles, V., Herbelin, H.: Equality is typable in semi-full pure type systems. In: LICS (2010), 21–30

[53] 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 (2007), 237–252

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

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

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

Appendix A. Normalisation by evaluation

type Type = Term
data Term = U  -- universe

| Fun Type Type  -- dependent function space
| Singl Term Type  -- singleton type ({a}_{A})
| App Term Term  -- application
| Lam Term  -- abstraction
| Q  -- variable
| Sub Term Subst  -- substitution
| Sigma Type Type  -- dependent pair type
| Fst Term  -- first projection
| Snd Term  -- second projection
| Pair Term Term  -- dependent pair
| Nat  -- naturals
| Zero  -- 0
| Suc Term  -- +1
| Natrec Type Term Term Term -- elimination for Nat
| Prf Type  -- proof (with proof irrelevance)
| Box Term  -- a term in Prf A
| Star  -- canonical element of Prf A
| Where Type Term Term  -- Box elimination
| Enum Int  -- Enum n has n elements
| Const Int Int  -- Const n i is the ith element
| Case Int Type [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)

type DT = D  -- semantic types
data D = T  -- terminal object (empty context)
| Ld (D → D)  -- function
| FunD DT (D → DT )  -- dependent function type
| UD  -- universe
| SingD D DT  -- singleton type
| Vd Int  -- free variable
| AppD D D  -- neutral application
| SumD DT (D → DT )  -- dependent pair type
| PairD D D  -- context comprehension
| FstD D  -- first projection of neutral
| SndD D  -- second projection of neutral
| NatD  -- natural number type
| ZeroD  -- 0
| SucD D  -- +1

| NatrecD (D → DT ) D D D  -- recursion on neutrals
| PrfD DT  -- proof type
| StarD  -- don’t care
| EnumD Int  -- enumeration type
| ConstD Int Int  -- constants in EnumD
| CaseD Int (D → DT ) [D ] D -- elimination on neutrals
type Ctx = [Type ]
pi1 , pi2 :: D → D
pi1 (PairD d d′) = d
pi1 StarD  = StarD
pi1 k  = FstD k
pi2 (PairD d d′) = d′
pi2 StarD  = StarD
pi2 k  = SndD k

ap :: D → D → D ap (Ld f ) d = f d

ap StarD = StarD

neutralD :: D → Bool

neutralD (Vd )  = True
neutralD (AppD )  = True
neutralD (FstD )  = True
neutralD (SndD )  = True
neutralD (NatrecD  ) = True
neutralD (CaseD  ) = True
neutralD StarD  = True
neutralD  = False

natrec :: (D → DT ) → D → D → D → D

natrec b z s StarD  = StarD
natrec b z s ZeroD  = z
natrec b z s (SucD e)  = (s ‘ap‘ e) ‘ap‘ (natrec b z s e)
natrec b z s d | neutralD d = up (b d)
(NatrecD (λe → downT (b e))

(down (b ZeroD) z) downSuc d)

where downSuc = down (FunD NatD

(λn → FunD (b n) (λe → b (SucD n))))

s

downs :: Int → (D → DT ) → [D ] → Int → [D ]

downs [ ] = [ ]
downs n f (d : ds) i = down (f (ConstD n i)) d : downs n f ds (i + 1)

constD :: Int → Int → D → Bool
constD n i (ConstD m j ) = m ≡ n ∧ i ≡ j
constD  = False

caseD :: Int → (D → DT ) → [D ] → D → D

caseD n b ds StarD  = StarD
caseD n b ds (ConstD m i) | n ≡ m ∧ i < n  = ds !! i
caseD n b ds d | neutralD d ∧
and [constD n i (ds !! i) | i ← [0 . . n − 1]] = up (b d) d
caseD n b ds d | neutralD d  = up (b d)
(CaseD n (λe → downT (b e))

(downs n b ds 0) d)

up :: DT → 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 (FstD k))

(up (f (up a (FstD k))) (SndD k))

up (PrfD a)  k = StarD
up (EnumD 0) k = StarD
up (EnumD 1) k = ConstD 1 0
up d  k = k

down :: DT → 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 (pi1 a)) (down (b (pi1 d)) (pi2 d))
down (PrfD a) d = StarD
down (EnumD 1) d = ConstD 1 0
down d  e = e

downT :: DT → DT

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)  = App  (readback i k) (readback i d)
readback i (FstD d)  = Fst  (readback i d)

readback i (SndD 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 (NatrecD b z s e) = Natrec (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  = Star
readback i (EnumD n)  = Enum n
readback i (ConstD n j )  = Const n j
readback i (CaseD n b ds d) = Case n (readback (i + 1) (b (Vd i)))

(map (readback i) ds) (readback i d)

-- Evaluation type Env = D eval :: Term → Env → 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 (App 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 = pi1 (eval t d)
eval (Snd t)  d = pi2 (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 (Natrec b z s t) d = natrec (λ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 = StarD
eval Star  d = StarD
eval (Where t b p) d = eval b (PairD d StarD)

eval (Enum n)  d = EnumD n
eval (Const n i)  d = ConstD n i
eval (Case n b ts t) d = caseD n (λe → eval b (PairD d e))

(map ((flip eval) d) ts) (eval t d)

evalS :: Subst → Env → Env

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 :: Type → Term → Term nbe ty t = readback 0 (down (eval ty T ) (eval t T )) nbeTy :: Type → Type nbeTy ty = readback 0 (downT (eval ty T )) nbeOpen :: Ctx → Type → Term → Term

nbeOpen ctx ty t = readback n (down (eval ty env) (eval t env))
where n  = length ctx
env  = mkenv n ctx

nbeOpenTy :: Ctx → Type → Type

nbeOpenTy ctx ty = readback n (downT (eval ty env))
where n  = length ctx
env  = mkenv n ctx

mkenv :: Int → Ctx → Env

mkenv 0 [ ]  = T
mkenv n (t : ts) = PairD d′ (up td (Vd (n − 1)))
where d′  = mkenv (n − 1) ts
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))

Appendix B. Type-checking algorithm

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

Checking well-formedness of types. chkType :: Ctx → Type → 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@(App 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@(Natrec t′ v v′ k) = chkNeTerm ts U w
chkType  = False

Checking the types of terms. sgSub :: Term → Term → Term sgSub t t′ = Sub t (Ext Is t′) chkTerm :: Ctx → Type → 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 (sgSub 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 (App k v)  = True
neutral (Fst k)  = True
neutral (Snd k)  = True
neutral (Natrec t′ v v′ k) = True

neutral (Case n b ts t) = True
neutral (Where t b p) = True
neutral  = False

erase :: Type → Type

erase (Singl e t) = erase t
erase t  = t

maybeEr :: Maybe Type → Maybe Type maybeEr = maybe Nothing (Just ∘ erase) chkNeTerm :: Ctx → Type → 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 → Type → Maybe Type nbeType ctx t = Just (nbeOpenTy ctx t) infType :: Ctx → Term → Maybe Type

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 (App e e′)  = case maybeEr (infType ts e) of

Just (Fun t t′) → if chkTerm ts t e′ then nbeType ts (sgSub 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 (sgSub t′ (Fst e))

→ Nothing

infType ts (Natrec t v w k) = case maybeEr (infType ts k) of

Just Nat → if chkType (Nat : ts) t ∧ chkTerm ts (nbeOpenTy ts (sgSub t Zero)) v ∧ chkTerm (Nat : ts)

(Fun (sgSub t Q)

(sgSub t (Suc (Sub Q P)))) w then nbeType ts (sgSub 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 ∧ nbeOpen ts′ w (Sub b (Ext (subs 1) Q)) ≡ nbeOpen ts′ w (Sub b P)

then Just t

else Nothing

where ts′ = Sub t′ P : t′ : ts

w = Sub t (subs 1)

→ Nothing

infType ts (Case 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 (sgSub b k)

else Nothing

→ Nothing

infType  = Nothing

chkList :: Ctx → Int → Type → Int → [Term ] → Bool

chkList ts [ ] = True
chkList ts n b i (e : es) = chkTerm ts (nbeOpenTy ts (sgSub 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

Appendix C. Proofs

C.1. Proof of Lemma 5.19. By induction on X = X′ ∈ T . We do not show the base cases, for they are trivial.

(1) Let Sing d X = Sing d′ X′ ∈ T .

[X] = [X′]  by ind. hyp.
d = d′ ∈ [X]  by ind. hyp.
e = d ∈ [X] and e′ = d ∈ [X]  hypothesis
e = d′ ∈ [X] and e′ = d′ ∈ [X]  by transitivity
{{d}}_{X} = {{d′}}_{X′}  by definition.

46 A. ABEL, T. COQUAND, AND M. PAGANO

(2) Let Fun X F = Fun X′ F′ ∈ T .

[X] = [X′]  by ind. hyp.
for all d ∈ dom([X]), F d = F′ d ∈ T by definition (*)
for all d = d′ ∈ [X], f · d = f′ · d′ ∈ [F d]  hypothesis
f · d = f′ · d′ ∈ [F′ d]  by ind. hypothesis in (*).

C.2. Proof of Lemma 5.22. By induction on X = X′ ∈ T .

(a) Case Sing d X = Sing d′ X′ ∈ T .

(1) The partial function ↑ maps neutrals to related elements in the corresponding PER.

k = k ∈ Ne  hypothesis
d = d′ ∈ [X] and X = X′ ∈ T  by inversion
↑_{Sing d X} k = d and ↑_{Sing d′ X′} k′ = d′  by def.
d = d′ ∈ {{d}}_{X}  by def. of this PER.

(2) The partial function ↓ maps related elements to related normal forms.

d_{1} = d_{2} ∈ {{d}}_{X}  hypothesis
d_{1} = d_{2} = d = d′ ∈ [X] and X = X′ ∈ T  by inversion
↓_{X} d = ↓_{X′} d′ ∈ Nf  by ind. hyp.
↓_{Sing d X} d_{1} = ↓_{Sing d′ X′} d_{2} ∈ Nf  by def.

(3) The function ⇓ maps related elements in T to normal forms.

⇓ Sing d X = Sing (↓_{X} d) (⇓ X)  by def.
⇓ Sing d′ X′ = Sing (↓_{X′} d′) (⇓ X′)  by def.
↓_{X} d = ↓_{X′} d′ ∈ Nf  by ind. hyp.
⇓ X = ⇓ X′ ∈ Nf  by ind. hyp.
Sing (↓_{X} d) (⇓ X) = Sing (↓_{X} d) (⇓ X) ∈ Nf  by Lem. 5.16.

(b) Case Fun X F = Fun X′ F′ ∈ T . (1) The partial function ↑ maps neutrals to related elements in the corresponding PER.

k = k′ ∈ Ne  hypothesis
d = d′ ∈ [X]  hypothesis  (*)
X = X′ ∈ T  by inversion  (†)
F d = F′ d′ ∈ T  by inversion  (**)
↓_{X} d = ↓_{X′} d′ ∈ Nf  by ind. hyp. on (*) and (†)
App k (↓_{X} d) = App k′ (↓_{X′} d′) ∈ Ne by Lem. 5.16 (‡)
↑_{F d} (App k (↓_{X} d)) = ↑_{F′ d′} (App k′ (↓_{X′} d′)) ∈ [F d] by ind. hyp. on (**) and (‡)
↑_{Fun X F} k = ↑_{Fun X′ F′} k′ ∈ [Fun X F]  by def.

A MODULAR TYPE-CHECKING ALGORITHM FOR TYPE THEORY 47

(2) The partial function ↓ maps related elements to related normal forms.

X = X′ ∈ T by inversion (*)
f = f′ ∈ [Fun X F]  hypothesis
k = k′ ∈ Ne  hypothesis
↑_{X} k = ↑_{X′} k′ ∈ [X] by ind. hyp. on (*) (†)
d := ↑_{X} k  abbreviation
d′ := ↑_{X′} k′  abbreviation
F d = F′ d′ ∈ T  by inversion and (†)  (**)
f · d = f′ · d′ ∈ [F d]  definition of [Fun X F]  (‡)
↓_{F d} (f · d) = ↓_{F′ d′} (f′ · d′) ∈ Nf  by ind. hyp. on (‡)
(↓_{Fun X F} f) · k = (↓_{Fun X′ F′} f′) · k′ ∈ Nf  by def.
↓_{Fun X F} f = ↓_{Fun X′ F′} f′ ∈ Nf  by Lem. 5.16

(3) The function ⇓ maps related elements in T to normal forms.

X = X′ ∈ T  by inversion  (*)
⇓ X = ⇓ X′ ∈ Nf  by ind. hyp. on (*)  (**)
k = k′ ∈ Ne  hypothesis.
↑_{X} k = ↑_{X′} k′ ∈ [X] by ind. hyp. on (*) (†)
d := ↑_{X} k  abbr.
d′ := ↑_{X′} k′  abbr.
F d = F′ d′ ∈ T by inversion and (†) (‡)
⇓(F d) = ⇓(F′ d′) ∈ Nf  by ind. hyp. on (‡)
⇓(Fun X F) = ⇓(Fun X′ F′) ∈ Nf  by Lem. 5.16

C.3. Proof of Lemma 5.34. The proofs of soundness for (prf-β) and (prf-η) have the same structure, so we show only the first one.

(prf-β) b where^{B} [a] = b (id, a) [[b where^{B} [a]]]d

= [[b]](d, ⋆)  def. of semantics for b where^{B} [a]
= [[b]](d, [[a]]d)  ind. hypothesis on Γ.A.A p ⊢ b p = b (p p, q) : B p p
= [[b]]([[(id, a)]]d)  def. of semantics for substitutions

= [[b (id, a)]]d (prf-assoc) a where^{A} (b where^{B} c) = (a (p p, q) where^{A p} b) where^{B} c

[[a where^{A} (b where^{B} c)]]d = [[a]](d, ⋆)
= [[a]](d, [[b]](d, ⋆))
= [[a (p p, q)]]((d, ⋆), [[b]](d, ⋆))
= [[a (p p, q) where^{A p} b)]](d, ⋆)
= [[(a (p p, q) where^{A p} b) where^{B} c]]d

C.4. Proof of Lemma 6.3. By induction on X ∈ T .

(a) Types; in all cases we use symmetry and transitivity to show the conditions. We only show the case for Fun X F.

(1) X = Fun X′ F:

Γ ⊢ A = Fun B C  by definition  (*)
Γ ⊢ B ∼ X′  by definition
Δ ⊢ C (p^{i}, s) ∼ F d ∈ T  by definition
for all Δ ⩽^{i} Γ and Δ ⊢ s : B p^{i} ∼ d ∈ [X′]
Γ ⊢ A′ = Fun B C  by sym. and trans. on (*)

(2) N_{n} ∈ T .

Γ ⊢ t : A ∼ d ∈ [N_{1}]  hypothesis  (*)
Γ ⊢ t = t′ : A  hypothesis  (†)
Δ ⊢ t p^{i} = R_{i} d : A p^{i}  by inversion on (*)  (**)
Δ ⊢ t p^{i} = t′ p^{i} : A p^{i}  by congruence on (†)  (‡)
Δ ⊢ t′ p^{i} = R_{i} d : A p^{i}  by sym. and trans. on (**) and (‡)

(b) Terms. As in the case for types, we use symmetry and transitivity. We show only the case for singletons and functions.

(1) X = Sing d X′:

Γ ⊢ A = {b}_{B}  by hypothesis  (*)
Γ ⊢ B ∼ X′ ∈ T  by hypothesis
Γ ⊢ t : B ∼ d ∈ [X′]  by hypothesis  (†)
Γ ⊢ A′ = {b}_{B}  by sym. and trans. on (*)
Γ ⊢ t′ : B ∼ d ∈ [X′]  By i.h. on (†)

(2) X = Fun X′ F:

Γ ⊢ A = Fun B C  by hypothesis  (*)
Γ ⊢ B ∼ X′  by hypothesis
Δ ⊢ app t p^{i} s : C (p^{i}, s) ∼ f · d ∈ [F d]  by hypothesis
for all Δ ⩽^{i} Γ and Δ ⊢ s : B p^{i} ∼ d ∈ [X′]
Γ ⊢ A′ = Fun B C  by sym. and trans. on (*) (†)
Δ ⊢ app t p^{i} s = app t′ p^{i} s : C (p^{i}, s)  by congruence on (†)  (‡)
Δ ⊢ app t′ p^{i} s : C (p^{i}, s) ∼ f · d ∈ [F d]  by i.h. on (‡)

C.5. Proof of Lemma 6.4. By induction on X ∈ T . This property is trivial for the base cases; for singletons is obtained by applying the i.h. We show two cases.

(1) Let X = Fun X′ F.

Γ ⊢ A = Fun B C  by hypothesis  (*)
Γ ⊢ B ∼ X′  (†)
Θ ⊢ C (p^{i}, s) ∼ F d ∈ T  by hypothesis
for all Θ ⩽^{i} Γ and Θ ⊢ s : B p^{i} ∼ d ∈ [X′]
Δ ⊢ A p^{i} = Fun (B p^{i}) (C (p^{i} p, q))  by congruence on (*)
Δ ⊢ B p^{i} ∼ X  by i.h. on (†)
Θ′ ⊢ s : (B p^{i}) p^{j} ∼ d ∈ [X], with Θ′ ⩽^{j} Δ  hypothesis
Θ′ ⊢ s : B p^{i+j} ∼ d ∈ [X]  by rem. 2.1 and 6.3  (‡)
Θ′ ⊢ C (p^{i+j} q, s) ∼ F d  by hyp. using (‡)
Θ′ ⊢ C (p^{i} p, q) (p^{j}, s) ∼ F d  By congruence and 6.3

(2) Prf X ∈ T . As mentioned earlier if Γ ⊢ A ∼ Prf X ∈ T then Γ ⊢ : A ∼ ∈ [Prf X] is non-empty if and only if Γ ⊢ : A is not empty.

Γ ⊢ t : A ∼ d ∈ [Prf X]  hypothesis  (*)
Γ ⊢ t : A  by inversion on (*)  (†)
Γ ⊢ A ∼ Prf X ∈ T  by inversion on (*)  (**)
Δ ⊢ t p^{i} : A p^{i}  by weakening on (†)
Δ ⊢ A p^{i} ∼ Prf X ∈ T  by monotonicity for types on (**)
Δ ⊢ t p^{i} : A p^{i} ∼ d ∈ [Prf X]  by definition of log. rel.

We do not show proofs for the second part, since the most involved case is dealt analogously to the case for Fun X′ F.

C.6. Proof of Lemma 6.5. By induction on X = X′ ∈ T . Note that the first part for the base cases is trivial; the second point is also trivial for X ∈ Ne. Thus we do not show those parts of the proof.

(a) Types.

(1) Sing d X = Sing d′ X′.

Γ ⊢ A = {b}_{B}  by hypothesis  (*)
Γ ⊢ B ∼ X ∈ T  by hypothesis
Γ ⊢ t : B ∼ d ∈ [X]  by hypothesis  (†)
Γ ⊢ t : B ∼ d′ ∈ [X′]  By i.h. on (*) and (†)

(2) Fun X F = Fun X′ F′.

Γ ⊢ A = Fun B C  by hypothesis
Γ ⊢ B ∼ X′  by hypothesis (*)
Θ ⊢ C (p^{i}, s) ∼ F d ∈ T  by hypothesis (†)
for all Θ ⩽^{i} Γ and Θ ⊢ s : B p^{i} ∼ d ∈ [X′]
Γ ⊢ B ∼ X′ ∈ T  By i.h. on (*)
Θ ⊢ B (p^{i}, s) ∼ F′ d ∈ T  by i.h. on (†)

(b) Terms. (1) e = e′ ∈ [Sing d X].

Γ ⊢ A = {b}_{B}  by hypothesis
Γ ⊢ B ∼ X ∈ T  by hypothesis  (*)
Γ ⊢ t : B ∼ d ∈ [X]  by hypothesis  (†)
e′ = d ∈ [X]  by def. of e = e′ ∈ [Sing d X]  (**)
Γ ⊢ t : B ∼ e′ ∈ [X]  by i.h. on (*), (†), and (**),

(2) f = f′ ∈ [Fun X F].

Γ ⊢ A = Fun B C

Γ ⊢ B ∼ X  (*)
Δ ⊢ app t p^{i} s : C (p^{i}, s) ∼ f · d ∈ [F d]  (†)
for all Δ ⩽^{i} Γ and Δ ⊢ s : B p^{i} ∼ d ∈ [X] .  (**)

By i.h. on (*) and (**) and monotonicity 6.4

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

By i.h. on (†)

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

(3) d = d′ ∈ [Sum X F].

d = d′ ∈ [Sum X F]  hypothesis  (*)
Γ ⊢ t : A ∼ d ∈ [Sum X F]  hypothesis  (**)
Γ ⊢ A = Σ A′ B  by inversion on (**)
Γ ⊢ Σ A′ B ∼ Sum X F ∈ T  by inversion on (**)
Γ ⊢ fst t : A′ ∼ fst d ∈ [X]  by inversion on (*)  (†)
Γ.A′ ⊢ snd t : B (id, fst t) ∼ snd d ∈ [F fst d]  by inversion on (**)  (‡)
fst d = fst d′ ∈ [X]  by definition of (*)  (††)
snd d = snd d′ ∈ [F fst d]  by definition of (*)  (‡‡)
Γ ⊢ fst t : A′ ∼ fst d′ ∈ [X]  by ind. hyp. on (†) and (††)
Γ.A′ ⊢ snd t : B (id, fst t) ∼ snd d′ ∈ [F fst d′]  by ind. hyp. on (‡) and (‡‡).

C.7. Proof of Lemma 6.6. By induction on X ∈ T . By induction on X ∈ T . For a better organisation of the proof we show the proofs for each point separately.

(a) Γ ⊢ A = R_{|Γ|} ⇓ X. We skip the part for the minimal elements in T .

(1) Sing d X:

Γ ⊢ A′ = R_{|Γ|} ⇓ X  by ind. hyp.
Γ ⊢ t = R_{|Γ|} ↓_{X} d : A′  by ind. hyp.
Γ ⊢ {a}_{A′} = {R_{|Γ|} ↓_{X} d}_{R_{|Γ|} ⇓ X}  by congruence and transitivity

(2) Fun X F:

Γ ⊢ A′ = R_{|Γ|} ⇓ X  by ind. hyp.
Δ ⊢ B (p^{i}, s) = R_{|Δ|} ⇓ F d  (*)
for any Δ ⩽^{i} Γ and Δ ⊢ s : A′ p^{i} ∼ d ∈ [X]
Γ.A′ ⊢ q : A′ p ∼ ↑_{X} Var x_{|Γ|}  by ind. hyp.  (†)
Γ.A′ ⊢ B (p, q) = R_{|Γ.A′|} ⇓ F ↑_{X} Var x_{|Γ|}  by instantiating (*) with (†)
Γ.A′ ⊢ B = R_{|Γ.A′|} ⇓ F ↑_{X} Var x_{|Γ|}  by 6.3.

(b) Γ ⊢ t = R_{|Γ|} ↓_{X} d : A. We skip the part for the minimal elements in T . (1) d′ ∈ [Sing d X]:

Γ ⊢ A = {b}_{B}  (*)

Γ ⊢ B ∼ X ∈ T

Γ ⊢ t : B ∼ d ∈ [X]  (†)
Γ ⊢ t = R_{|Γ|} ↓_{X} d : B  by ind. hyp. in (†)
Γ ⊢ t = R_{|Γ|} ↓_{X} d : {t}_{B}  by conversion and (sing-eq-i)
Γ ⊢ t = R_{|Γ|} ↓_{X} d : A  by conversion

(2) f ∈ [Fun X F]:

Γ.A′ ⊢ q : A′ p ∼ ↑_{X} Var x_{|Γ|} ∈ [X]  by ind. hyp. on the third part
d := ↑_{X} Var x_{|Γ|}  abbreviation
Γ.A′ ⊢ app (t p) q : B (p, q) ∼ f · d ∈ [F d]  by definition of the logical relation
Γ.A′ ⊢ app (t p) q = R_{|Γ.A|} ↓_{F d} f · d : B (p, q)  by ind. hyp.
Γ.A′ ⊢ app (t p) q = R_{|Γ.A|} ↓_{F d} f · d : B  by (conv)
Γ ⊢ λ(app (t p) q) = λ(R_{|Γ.A|} ↓_{F d} f · d) : Fun A′ B by congruence
Γ ⊢ t = λ(app (t p) q) : Fun A′ B  by (eta)
Γ ⊢ t = R_{|Γ|} ↓_{Fun X F} f : Fun A′ B  by trans.

(c) (1) Sing d X:

Γ ⊢ A = {a}_{B}  by hypothesis
Γ ⊢ B ∼ X ∈ T  by hypothesis
Γ ⊢ t : B ∼ d ∈ [X]  by hypothesis
Γ ⊢ B ∼ X ∈ T  by monotonicity 6.4
Δ ⊢ t p^{i} : B p^{i} ∼ d ∈ [X]  by monotonicity 6.4
Δ ⊢ A p^{i} = {a p^{i}}_{B p^{i}}  by congruence

(2) Fun X F:

Δ ⊢ s : A′ p^{i} ∼ d′ ∈ [X]  hypothesis  (*)
Δ ⊢ s = R_{|Δ|} ↓_{X} d′ : A′ p^{i}  by ind. hyp. on (*)
Δ ⊢ app (t p^{i}) s = app ((R_{|Γ|} d) p^{i}) (R_{|Δ|} (↓_{X} d′)) : B (p^{i}, s)  by congruence
R_{|Δ|} App d ↓_{X} d′ = app ((R_{|Γ|} d) p^{i}) (R_{|Δ|} (↓_{X} d′))  by definition
Δ ⊢ app (t p^{i}) s : B (p^{i}, s) ∼ ↑_{F d′} App d ↓_{X} d′ ∈ [F d′]  by ind. hyp.

C.8. Proof of Lemma 6.13. By induction on Γ ⊢; we show only the inductive case. Let Γ.A ⊢.

d := ρ_{Γ}  definition
Γ ⊢ id : Γ ∼ d ∈ ([Γ])  by inversion and i.h.  (*)
Γ.A ⊢ id p : Γ ∼ d ∈ ([Γ])  from (*) by Rem. 6.9  (†)
Γ.A ⊢ p : Γ ∼ d ∈ ([Γ])  from (†) by Rem. 6.8  (**)
Γ.A ⊢ A p ∼ [[A]]d ∈ T  by inversion and Thm. 6.11
Γ.A ⊢ q : A p ∼ ↑_{[[A]]d} Var x_{n} ∈ [[[A]]d]  by Thm. 6.11
Γ.A ⊢ (p, q) : Γ.A ∼
(d, ↑_{[[A]]d} Var x_{n}) ∈ ∐ ([Γ]) (e ↦ [[[A]]e])  by Def. 6.7  (‡)
Γ.A ⊢ id : Γ.A ∼ ρ_{Γ.A} ∈ ([Γ.A])  from (‡) by Rem. 6.8

C.9. Proof of Theorem 6.11. 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; for the case of the conversion rule, we can conclude by i.h., and lemma 6.3.

(a) Types. We show only the case for (fun-f).

Δ ⊢ s : A′ p^{i} ∼ e ∈ [X]  hypothesis  (*)
Θ ⊢ δ p^{i} : Γ ∼ d ∈ ([Γ])  By monotonicity for substitutions 6.9  (†)
Θ ⊢ (δ p^{i}, s) : Γ.A ∼ (d, e) ∈ ([Γ.A]) From (*) and (†)
Θ ⊢ B (δ p^{i}, s) ∼ [[B]](d, e) ∈ T  by ind. hyp. on Γ.A ⊢ B and using 6.3 and 6.5

(b) Terms. We show the case for application (fun-el) and for (n_{n}-e). The case for abstraction (fun-i) is analogous to (fun-f).

(1) (fun-el)

Γ ⊢ app t r : B (id, r)  hypothesis
Δ ⊢ r δ : A δ ∼ [[r]]d ∈ [[[A]]d]  by ind. hyp.  (*)
Δ ⊢ t δ : Fun A B δ ∼ [[t]]d ∈ [[[Fun A B]]d]  by ind. hyp.  (†)

Δ ⊢ app (t δ) (r δ) : B (id, r δ) ∼

[[t]]d · [[r]]d ∈ [[[B]](d, [[r]]d)]  by def. of log. rel. for (†) with (*)

Δ ⊢ (app t r) δ : B (id, r δ) ∼

[[app t r]]d ∈ [[[B]](d, [[r]]d)]  by 6.3 and 6.5

(2) (n_{n}-e)

Γ ⊢ case^{B} t_{0} ⋯ t_{n−1} t : B (id, t)  hypothesis
Δ ⊢ t δ : N_{n} ∼ [[t]]d ∈ [N_{n}]  by inversion and by ind. hyp.
Δ ⊢ t δ = R_{|Δ|} [[t]]d : N_{n}  by 6.6
Δ ⊢ t_{i} δ : B (δ, c_{i}) ∼ [[t_{i}]]d ∈ [[[B]](d, [[t]]d)]  by inversion and by ind. hyp.

if R_{|Δ|} [[t]]d ≡ c_{i}:

Δ ⊢ (case B t_{0} ⋯ t_{n−1} c_{i}) δ = t_{i} δ : B (id, t)  by subst.

Δ ⊢ (case B t_{0} ⋯ t_{n−1} c_{i}) δ : B (id, t) ∼

[[case^{B} t_{0} ⋯ t_{n−1} t ]]d ∈ [[[B (id, t)]]d]  by 6.3 and 6.5

if R_{|Δ|} [[t]]d ∈ Ne:

Δ.N_{n} ⊢ B (δ p, q) = R_{|Δ|+1} ⇓[[B]](d, Var x_{|Δ|})

Δ ⊢ t_{i} δ = R_{|Δ|} [[t_{i}]]d : B (δ, c_{i})  by 6.6
t′_{i} := R_{|Δ|} [[t_{i}]]d  abbreviation
t′ := R_{|Δ|} ↓_{[[B]](d,c_{i})} [[t]]d  abbreviation
B′ := R_{|Δ|+1} [[B]](d, Var x_{|Δ|})  abbreviation

Δ ⊢ (case B t_{0} ⋯ t_{n−1} t) δ =

case B′ t′_{0} ⋯ t′_{n−1} t′ : B (δ, t)  congruence

Δ ⊢ (case B t_{0} ⋯ t_{n−1} t) δ : B (δ, t) ∼

↑_{[[B]](d,[[t]]d)} (case B′ t′_{0} ⋯ t′_{n−1} t′ ∈ [[B]](d, [[t]]d)) by 6.6 and 6.4

Δ ⊢ (case B t_{0} ⋯ t_{n−1} c_{i}) δ : B (id, t) ∼

[[case^{B} t_{0} ⋯ t_{n−1} t ]]d ∈ [[[B (id, t)]]d]  by 6.3 and 6.5

(c) Substitutions. Only the proof for (ext-subs) is shown.

Γ ⊢ Θ.A : (γ, t)  hypothesis
Δ ⊢ γ δ : Θ ∼ [[γ]]d ∈ ([Θ]) by ind. hyp. (*)
Δ ⊢ t δ : (A γ) δ ∼ [[t]]d ∈ [[[A γ]]d]  (†)
([[γ]]d, [[t]]d) ∈ ∐ ([Θ]) (e ↦ [[[A γ]]e])  from (*) and (†)
Δ ⊢ (γ, t) δ : Θ.A ∼ [[(γ, t)]]d ∈ ([Θ.A])  by 6.8 and 6.10

C.10. Proof of Theorem 7.4. By simultaneous induction on Γ ⊢ V ⇐, Γ ⊢ v ⇐ V, and Γ ⊢ V ⇒ k.

(1) Types:

• 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).

(2) 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 latter case, the derivation is obtained directly from the correctness of type-inference. In the first case we use the rule (sing-el), with the derivation obtained by i.h. and then we conclude with conversion.

(3) 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 correctness of nbe( ) and by 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 by conversion and correctness of nbe( ).

C.11. Proof of Theorem 7.6. We prove simultaneously all the points. The first point is by induction on the structure of the type. In the last two points we use well-founded induction on the order ≺.

(1) Types:

• Γ ⊢ 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 2.7, we know Γ ⊢ k : U; hence by i.h.

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

(2) 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:

(a) 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.

(b) 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}:

(a) Γ ⊢ 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

(b) Γ ⊢ 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′

(a) Γ ⊢ V = Fun A′ B, and Γ.A′ ⊢ v′ : B; from this we can conclude Γ.nbe(A′) ⊢ v′ : B by ind. hyp. we get Γ.nbe(A′) ⊢ v′ ⇐ nbe(B); therefore Γ ⊢ λv′ ⇐ Fun nbe(A′) nbe(B′).

(b) 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).

(a) 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).

(b) 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.

(3) 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)) (by correctness of the nbe( ) algorithm).