An Adequacy Theorem for Dependent Type Theory

This paper has two main contributions. The first one is to present a domain model of dependent type theory where a type is interpreted as a finitary projection on one “universal” domain. We believe this model to be quite natural and canonical, and it can be presented as a simple decidable typing system on finite elements.^{Footnote 1} While this model is based on a “universal” domain, two convertible terms have the same semantics, like for the set-theoretic model [3]. This is to be contrasted with an “untyped” semantics, like the one used in [1] and where one needs to quotient by an extra partial equivalence relation. The second contribution is to show, using this model, purely syntactical properties of dependent type theory. In particular, we can show that dependent product is one-to-one for conversion in a constructive metatheory, involving only induction and recursion on finite objects,^{Footnote 2} a property which is crucial in establishing subject reduction [4, 17]. Furthermore, the technique that is used is similar to the use of “inclusive predicates”, fundamental in domain theory [12, 15]. Another technical advantage of our approach is that we don’t need to use contexts as Kripke worlds as in previous arguments [2, 6]. We also establish that two convertible terms in type theory (maybe partial [10, 11, 13, 14]) have the same Böhm tree.

In this paper, we work in a constructive metatheory, and when we write that a propoosition P is decidable, we mean that P ∨¬P is provable.

We shall use the following Scott domain, least solution of a recursive domain equation (see [18, 19] for a lively description of Scott domains and solutions to domain equations):

In this equation, + denotes the coalesced sum [18] and i = 0,1,2,…

We write a,b,u,v,… for the elements of this domain. We define u(v) for u and v in D as follows: it is the application of u to v if u belongs to D → D and it is ⊥ otherwise.

A fundamental result of domain theory is that the finite/compact elements of this domain can be described in a purely syntactical way, and both the order and the compatibility relations on these finite elements are decidable [16, 18, 19]. It also has been noticed [16] that this domain is coherent in the sense that a finite set is compatible (i.e. has a least upper bound) if, and only if, it is pairwise compatible.

Here is an inductive description of the finite elements

• ⊥ or

• U_i, N or 0 or

• Su where u is finite

• π af where a is finite and f is a finite function or

• a finite function

and a finite function f is a least upper bound of basic step functions and is of the form ⊥ or u₁↦v₁,…,u_n↦v_n (with \(n\geqslant 1\) and all u_i,v_i finite) such that whenever u_i and u_j are compatible then so are v_i and v_j. Such a function sends an element u to the element f(u) = ∨{v_i | u_i ≤ u}.

The order relation on finite elements can then be described by the rules

• ⊥≤ u,

• N ≤N and 0 ≤0 and U_i ≤U_i,

• Su ≤Sv if u ≤ v,

• π af ≤π bg if a ≤ b and f ≤ g, and

• (u₁↦v₁,…,u_p↦v_p) ≤ f if v_i ≤ f(u_i) for all i.

In general there are different possible ways to write a finite function f as a least upper bound of step functions. For instance, we have (⊥↦N) = (U₃↦N,⊥↦N). We say that a description f = (u₁↦v₁,…,u_n↦v_n) is minimal if we cannot remove some u_i↦v_i in this description. An important property is the following.

Lemma 1

Iff = (u₁↦v₁,…,u_n↦v_n) is minimal, we havefu < fu_iwheneveru < u_i.

Proof

If we have u < u_i and fu_i = fu, then \(\vee \{v_{j} \mid u_{j}<u_{i}\} \geqslant f~u = f~u_{i}\) and we can remove u_i↦v_i from the given description of f . □

Corollary 1

If we have a minimal description off = (u₁↦v₁,…,u_n↦v_n) and another descriptionf = (a₁↦b₁,…,a_m↦b_m) (not necessarily minimal), thenu_i = ∨{a_j∣a_j ≤ u_i}.

Proof

Indeed, if u = ∨{a_j∣a_j ≤ u_i} we have u ≤ u_i and f(u) = ∨{b_j ∣ a_j ≤ u} = ∨{b_j∣a_j ≤ u_i} = f(u_i), so we cannot have u < u_i by the previous lemma. □

We define the rank rk(u) of the finite element u by the equations

and rk(f) = 1 + max(rk(u_i),rk(f(u_i))) if f = (u₁↦v₁,…,u_l↦v_l) is minimal and l > 0. The rank measures the first time an element u appears in the inductive generation of finite elements. An important property of the rank is that rk(u ∨ v) ≤ max(rk(u),rk(v)) and rk(f(u)) < rk(f) for all u.

Working with universes, we want to consider that U_i is more “complex” than any given finite element which only mentions U_j for j < i. In order to capture this notion of complexity, we define

and lv(f) = max(lv(u_i),lv(f(u_i))) if f = (u₁↦v₁,…,u_k↦v_k) is minimal. An important property of the (universe) level is that lv(u ∨ v) ≤ max(lv(u),lv(v)) and lv(f(u)) ≤ lv(f) for all u.

Finally we define the complexity of a finite element a as the pair lv(a),rk(a) with the lexicographic ordering.

A finitary projection [18, 19] of a Scott domain E is a map p : E → E such that p ∘ p = p and pa ≤ a and the image of p, which is also the set of fixed-points of p, is a Scott domain. If pu = u and pv = v and u,v are compatible then p (u ∨ v) = u ∨ v since both u and v are ≤ p (u ∨ v). A finitary projection is thus completely determined by a set of finite elements which is closed by compatible sups. If F,E are two Scott domains, we write \(F\lhd E\) and say that F is a subdomain of E if F is the image of a finitary projection of E. Equivalently F is the set of directed sups of a given subset of finite elements of E which is closed by compatible binary sups, and this set is exactly the set of finite elements of F. A fundamental result [18] is that the poset of finitary projections of a Scott domain E is itself a Scott domain, which is a subdomain of E → E.

We now describe a type system on finite elements.

Lemma 2

Ifu : aanda ≤ b,thenu : b.Ifu : a,v : a,and u and v are compatible, thenu ∨ v : a.

Proof

The first statement is by induction on the derivation of u : a. For the second statement, we look at the case where a = U_k and u = π b (u₁↦t₁,…,u_n↦t_n) and v = π b^′ (v₁↦l₁,…,v_m↦l_m). By induction, we have b ∨ b^′ : U_k. Also u_i : b and hence u_i : b ∨ b^′ by the first statement and similarly v_j : b ∨ b^′. The other cases are similar. □

Corollary 2

Ifw : π afandu : a,thenw(u) : f(u).

Proof

We can write w = (u₁↦v₁,…,u_n↦v_n) with v_i : f(u_i). We have v_i : f(u) if u_i ≤ u by Lemma 2. We then have w(u) = ∨{v_i∣u_i ≤ u} : f(u) by Lemma 2. □

Lemma 3

If π af : U_kandf = (u₁↦t₁,…,u_n↦t_n) is minimal, thenu_i : aandf(u_i) : U_k.

Proof

We have f = (u₁↦t₁,…,u_n↦t_n) = (v₁↦l₁,…,v_m↦l_m) with v_j : a and l_j : U_k. Since f(u_i) = ∨{l_j∣v_j ≤ u_i} we have f(u_i) : U_k by Lemma 2. Also u_i = ∨{v_j∣v_j ≤ u_i} and so u_i : a by Lemma 2. □

Lemma 4

Ifw : π afandw = (u₁↦t₁,…,u_n↦t_n) is minimal, thenu_i : aandw(u_i) : f(u_i).

Proof

We have w = (u₁↦t₁,…,u_n↦t_n) = (v₁↦l₁,…,v_m↦l_m) with v_j : a and l_j : f(v_j). It follows from Corollary 1 that we have u_i = ∨{v_j∣v_j ≤ u_i} and so u_i : a by Lemma 2. Using Corollary 2, we get w(u_i) : f(u_i). □

Note that if u : a then lv(u) ≤ lv(a) and if u : U_k then lv(u) < k, by induction on the derivation.

Corollary 3

The relationu : ais decidable.

Proof

By induction on the complexity of u and a. □

The following Lemma will be useful when connecting syntax and semantics.

Lemma 5

Ifw : π bfandb ≤ a,then for anyu : athere existsv : bsuch thatv ≤ uandw(u) = w(v).

Proof

We write w = (u₁↦l₁,…,u_n↦l_n) with u_i : b and l_i : f(u_i). We then have w(u) = w(v) with v = ∨{u_i∣u_i ≤ u} and v : b by Lemma 2. □

We now introduce the predicate atype by the rules:

Lemma 6

Ifa : U_j,thenatype.Ifatype,btype,anda,bare compatible, thena ∨ btype.If π a (u₁↦t₁,…,u_n↦t_n) typeandu₁↦t₁,…,u_n↦t_nis a minimal description, thenu_i : aandt_itype.

Proof

The first statement is by induction on the derivation of a : U_j. The second statement is proved as in Lemma 2, and the last statement as in the proof of Lemma 3. □

Corollary 4

The predicate a t y p e is decidable.

Given a finite element a, the set of finite elements u such that u : a is closed by compatible binary sups by Lemma 2. Hence it defines a finitary projection pa. Similarly the set of finite elements a such that atype defines a finitary projection p_type. We write \({\mathsf {Type}}\lhd D\) for the corresponding subdomain.

By Lemma 2, we have pa ≤ pb if a ≤ b and we can hence define the finitary projection pa for an arbitrary element a of D, not necessarily finite, as the directed sup of all pa₀ for a₀ ≤ a finite, in the Scott domain of finitary projections of D. We write \(El~a\lhd D\) for the image of pa.

We have \(El~\mathsf {U}_{i}\lhd El~\mathsf {U}_{i + 1}\) and \(El~\mathsf {U}_{i}\lhd {\mathsf {Type}}\).

Let us write a → b for π a (⊥↦b). The domain \(El~\mathsf {N}\lhd D\) is exactly the domain of “lazy” natural numbers, that are elements of the form S^k0 or S^k⊥. The poset of finite elements w such that w : N →N is exactly the poset of finite element of the domain of continuous functions ElN → ElN.

Lemma 7

Iff = (u₁↦v₁,…,u_n↦v_n) is minimal andf = f ∘ pwhere p is a finitary projection, thenpu_i = u_ifor all i.

Proof

We have fu_i = f (pu_i) and so we cannot have pu_i < u_i since the description is minimal using Corollary 1, and so pu_i = u_i. □

Proposition 1

We have

andpab = ⊥ in all other cases. We also have

andp_typeb = ⊥ in all other cases.

Proof

Let qa be the function defined by these recursive equations. We show by induction on the complexity of a finite that we have qau = u, for u finite, if, and only if, u : a. This is clear if a = N. If a = π bf and u : a, then using Lemma 4, we can write u = (u₁↦v₁,…,u_n↦v_n) with u_i : a and v_i : f(u_i). We then have u(x) = u(qbx) : f (qbx) and so u(x) = (q (π bf) u)(x) for any x and so u = qau. Conversely, if u = qau, we have u = u ∘ (qb), and if u = (u₁↦v₁,…,u_n↦v_n) is a minimal description of u, we have qbu_i = u_i by Lemma 7. So u_i : b by induction. We then have v_i = q (f(u_i)) v_i and so v_i : f(u_i) by induction.

Finally we prove qU_ka = a if, and only if, a : U_k by induction on the complexity of a finite. We cover the case a = π bf where u₁↦l₁,…,u_n↦l_n is a minimal description of f .

If a : U_k, then b : U_k and so qU_kb = b by induction and u_i : b and l_i : U_k. Since b is strictly less complex than U_k, we have by induction qbu_i = u_i and qU_kf(u_i) = f(u_i). It follows that we have qU_ka = a.

Conversely, if qU_ka = a then qU_kb = b and so b : U_k by induction and we have (qU_k) ∘ f ∘ (qb) = f. It follows that we have f(u_i) = qU_k (f(qbu_i)) for all i and we have qbu_i = u_i by Lemma 7. So u_i : b since b is simpler than U_k. We then get f(u_i) = qU_kf(u_i) and so f(u_i) : U_k by induction. □

We can now consider the continuous families of domains Ela and Ela →Type indexed over a in Type. We can form their carteisan products and get a continuous family Ela × (Ela →Type) indexed over a in Type. We consider then the sum of this family, which is itself a Scott domain [7]

and we have an evaluation function E →Type, (a,v,f)↦f(v). This evaluation function is continuous. So, if we have w₀ ≤ f(v) in Type then we can find a₀ ≤ a finite in Type, and u₀ ≤ u finite in Ela₀ and f₀ ≤ f finite in Ela₀ →Type such that w₀ ≤ f(v). This remark will be used in a crucial way in connecting syntax and semantics of type theory.

The syntax of type theory is defined as follows.

We write F(x/M) the substitution of M for x in F. We may write simply F(M) if x is clear from the context.

The semantics can be defined at this purely untyped syntactic level, exactly like for the set-theoretic semantics presented in [3]. This semantics is described in Fig. 1 where we define ρ,x : a = u to be the update of ρ with the assignment x = pau.

Denotational semantics of type theory

Full size image

The semantics of rec is the usual lazy semantics of primitive recursion. We define rec(d₀,d₁) in D → D by the recursive equations

and rec(d₀,d₁) u = ⊥ in the other cases, and then

(The extra argument λx.T is used in Section 7.)

The typing and conversion rules are in the Appendix. There are two judgments for types, of the form Atype and AconvA^′, and two judgments for elements, of the form M : A and MconvM^′ : A. Such a judgment is stated in a context, which is a list of typing declarations x : A. As in [9], we may not write the context explicitly.

We say that ρfits Γ if for all x : A in Γ we have ⟦A⟧ρ in Type and ρ(x) in El(⟦A⟧ρ).

Theorem 1

Ifρfits Γ,then:

1. 1.

   Γ ⊩ Atypeimplies ⟦A⟧ρ ∈Type,

2. 2.

   Γ ⊩ AconvA^′implies ⟦A⟧ρ = ⟦A^′⟧ρ,

3. 3.

   Γ ⊩ M : Aimplies ⟦M⟧ρ ∈ El (⟦A⟧ρ),and

4. 4.

   Γ ⊩ MconvM^′ : Aimplies ⟦M⟦ρ = ⟧M^′⟧ρ.

Proof

Direct by induction on the derivation. □

Note that the use of finitary projections takes care of η-conversion in the semantics. For instance, we have ⟦λ(x : N →N)x⟧ = ⟦λ(x : N →N)λ(y : N)xy⟧. Indeed, both are equal to the function u↦v↦pN (u(pNv)).

The main difference with the semantics suggested in [11] and in [13] is that abstraction is not interpreted as a constructor. This is crucial in order to validate the rule of η-conversion that NconvN^′ : π(x : A)B as soon as NxconvN^′x : B (x : A). If we represent abstraction by a constructor, we would have w = λ(⊥)≠⊥ = w^′ but also w(u) = ⊥ = w^′(u) for any u in D, and so the rule for η-conversion cannot be valid in this case.

We write M → M^′ for weak-head reduction. This is defined at a purely syntactical level. The rules are the following.

We write M →_AM^′ for M → M^′ and MconvM^′ : A and write \(M\rightarrow ^{*}_{A} M^{\prime }\) for the corresponding transitive reflexive closure. We write A →_typeA^′ to mean that A → A^′ and AconvA^′, and we write \(A \rightarrow _{\mathsf {type}}^{*} A^{\prime }\) the corresponding transitive reflexive closure. These relations are similar to the relations used in [2, 6].

In this section, we will consider only closed terms. The relation AconvB defines an equivalence relation on the set of terms A such that Atype. If Atype, then, similarly, the relation MconvN : A defines an equivalence relation on the set of terms M satisfying M : A.

The main goal of this section is to analyze relations refining these predicates. We define Atype∣_a and AconvB∣_a for a ≤⟦A⟧ in Type and, if we have Atype∣_a, we define M : A∣_u:a and MconvM^′ : A∣_u:a for u ≤⟦M⟧ in Ela. The relation AconvB∣_a will be an equivalence relation on the set of terms satisfying the predicate ∣_a, while, if Atype∣_a, the relation MconvM^′ : A∣_u:a will be an equivalence relation on the set of terms M such that M : A∣_u:a.

These relations are defined first for finite elements a, by recursion on the complexity of a in Type. More precisely, we define all the relations Atype∣_a, AconvB∣_a, M : A∣_u:a, and MconvM^′∣_u:a by recursion on the complexity of the finite element a. In particular, this definition is not an inductive-recursive one. To incorporate universes we also define at the same time the relations \(A~{\mathsf {type}\mid ^{i}_{a}}\) and \(A~\mathsf {conv}~A'{\mid ^{i}_{a}}\) for i = 0,1,2,… in the clauses 5-8. In each of the clauses of the definition below we will have some tacit assumptions suppressed for readability: Atype∣a assumes Atype and atype; AconvA^′∣_a assumes both Atype∣_a and A^′type∣_a and further AconvA^′; M : A∣_u:a assumes Atype∣_a, M : A, and u : a; MconvM^′ : A∣_u:a assumes M : A∣_u:a, M^′ : A∣_u:a, and MconvM^′ : A.

We distinguish the shape of a.

1. 1.

   Case ⊥. Atype∣_⊥, AconvA^′∣_⊥, M : A∣_u:⊥, and MconvM^′∣_u:⊥ all hold by definition.

2. 2.

   Case πbf. We define:

   • Atype∣_πbf means \(A\rightarrow _{\mathsf {type}}^{*} {\Pi } (x:B)F\) for some B and F with Btype∣_b and x : B ⊩ Ftype and

     1. (a)

        N : B∣_v:b implies F(N) type∣_f(v), and

     2. (b)

        NconvN^′ : B∣_v:b implies F(N) convF(N^′)∣_f(v).

   • Given A^′ with \(A^{\prime }\rightarrow _{\mathsf {type}}^{*} {\Pi } (x:B^{\prime })F^{\prime }\) and A as above, then AconvA^′∣_πbf means BconvB^′∣_b and

     $$N:B\mid_{v:b} \quad \text{implies} \quad F(N)~\mathsf{conv}~F^{\prime}(N)\mid_{f(v)}. $$

   • M : A∣_u:πbf is defined as (A as above):

     1. (a)

        N : B∣_v:b implies MN : F(N)∣_u(v):f(v), and

     2. (b)

        NconvN^′ : B∣_v:b implies MNconvMN^′ : F(N)∣_u(v):f(v).

   • MconvM^′ : A∣_u:πbf is defined as

     $$N:B\mid_{v:b} \quad \text{implies} \quad M~N~\mathsf{conv}~M^{\prime}~N : F(N) \mid_{u(v) : f(v)}. $$
3. 3.

   CaseN. We define:

   • Atype∣_N means that \(A\rightarrow _{\mathsf {type}}^{*} \mathsf {N}\).

   • AconvA^′∣_N is always satisfied.

   • M : A∣_u:N is defined by induction on u:

     1. (a)

        M : A∣_⊥:N holds by definition,

     2. (b)

        M : A∣_0:N if \(M\rightarrow _{\mathsf {N}}^{*} \mathsf {0}\), and

     3. (c)

        M : A∣_Sv:N if \(M\rightarrow _{\mathsf {N}}^{*} \mathsf {S}~N\) and N : A∣_v:N.

   • MconvM^′ : A∣_u:N is defined by induction on u:

     1. (a)

        MconvM^′ : A∣_⊥:N and MconvM^′ : A∣_0:N hold by definition, and

     2. (b)

        MconvM^′ : A∣_Sv:N if \(M\rightarrow _{\mathsf {N}}^{*} \mathsf {S}~N\), \(M^{\prime }\rightarrow _{\mathsf {N}}^{*} \mathsf {S}~N^{\prime }\) and NconvN^′ : A∣_v:N.

The rest of the definition involves universes, so let us interrupt the definition to look at an example: Atype∣_a, for a = π N (0↦N, S0↦N), means \(A\rightarrow _{\mathsf {type}}^{*}{\Pi }(x:B)F\) with Btype∣_N, that is, \(B\rightarrow _{\mathsf {type}}^{*}\mathsf {N}\), and

• if \(M\rightarrow _{\mathsf {N}}^{*}\mathsf {0}\), then F(M)type∣_N, that is, \(F(M)\rightarrow _{\mathsf {type}}^{*}\mathsf {N}\), and

• if \(M\rightarrow _{\mathsf {N}}^{*}\mathsf {S}~\mathsf {0}\), then F(M)∣_N, that is, \(F(M)\rightarrow _{\mathsf {type}}^{*}\mathsf {N}\).

We now continue the definition to incorporate universes:

1. 4.

   CaseU_j. We define:

   • \(A~\mathsf {type}\mid _{\mathsf {U}_{j}}\) means \(A\rightarrow _{\mathsf {type}}^{*} \mathsf {U}_{j}\), and

   • \(A~\mathsf {conv}~A^{\prime }\mid _{\mathsf {U}_{j}}\) is always satisfied.

   • \(M:A\mid _{u:\mathsf {U}_{j}}\) means \(M~\mathsf {type} {\mid ^{j}_{u}}\), and

   • \(M~\mathsf {conv}~M^{\prime }\mid _{u:\mathsf {U}_{j}}\) means \(M~\mathsf {conv}~M'{\mid ^{j}_{u}}\).

Where the relations \(A~{\mathsf {type}\mid ^{i}_{a}}\) and \(A~\mathsf {conv}~A'{\mid ^{i}_{a}}\) used above are simultaneously defined by recursion on the complexity of a : U_i according to the following cases. We have similar tacit assumptions in the definition: \(A~{\mathsf {type}\mid ^{i}_{a}}\) always additionally assumes a : U_i (as finite elements) and A : U_i. And \(A~\mathsf {conv}~A^{\prime }{\mid ^{i}_{a}}\) assumes \(A~{\mathsf {type}\mid ^{i}_{a}}\), \(A^{\prime }~{\mathsf {type}\mid ^{i}_{a}}\), and AconvA^′ : U_i.

1. 5.

   Case ⊥. \(A~\mathsf {type}\mid ^{i}_{\bot }\) and \(A~\mathsf {conv}~A^{\prime }\mid ^{i}_{\bot }\) hold by definition.

2. 6.

   Case πbf. We define:

   • \(A~\mathsf {type}\mid ^{i}_{{\Pi }bf}\) means \(A\rightarrow _{\mathsf {U}_{i}}^{*} {\Pi } (x:B)F\) for some B and F with \(B~{\mathsf {type}\mid ^{i}_{b}}\) and x : B ⊩ F : U_i and

     1. (a)

        N : B∣_v:b implies \(F(N)~\mathsf {type}\mid ^{i}_{f(v)}\), and

     2. (b)

        NconvN^′ : B∣_v:b implies \(F(N)~\mathsf {conv}~F(N^{\prime })\mid ^{i}_{f(v)}\).

   • Given A^′ with \(A^{\prime }\rightarrow _{\mathsf {U}_{i}}^{*} {\Pi } (x:B^{\prime })F^{\prime }\) and A as above, then \(A~\mathsf {conv}~A^{\prime }\mid ^{i}_{{\Pi }bf}\) means that \(B~\mathsf {conv}~B^{\prime }{\mid ^{i}_{b}}\) and

     $$N:B\mid_{v:b} \quad \text{implies} \quad F(N)~\mathsf{conv}~F^{\prime}(N)\mid^{i}_{f(v)}. $$
3. 7.

   CaseN. We define:

   • \(A~\mathsf {type} \mid ^{i}_{\mathsf {N}}\) means that \(A\rightarrow _{\mathsf {U}_{i}}^{*} \mathsf {N}\).

   • \(A~\mathsf {conv}~A^{\prime }\mid ^{i}_{\mathsf {N}}\) is always satisfied.

4. 8.

   CaseU_j with j < i. We define:

   • \(A~\mathsf {type}\mid ^{i}_{\mathsf {U}_{j}}\) means \(A\rightarrow _{\mathsf {U}_{i}}^{*} \mathsf {U}_{j}\), and

   • \(A~\mathsf {conv}~A^{\prime }\mid ^{i}_{\mathsf {U}_{j}}\) is always satisfied.

This concludes the definition of the predicates.

Lemma 8

Each relationAconvA^′∣_ais an equivalence relation on the set of terms A such thatA∣_a.Furthermore, ifAconvA^′∣_athen we haveM : A∣_u:aiffM : A^′∣_u:aandMconvM^′ : A∣_u:aiffMconvM^′ : A^′∣_u:afor any u inEla.

Proof

This is clear if a = ⊥ or a = N. If a = π bf, let us prove for instance that the relation AconvA^′∣_a is symmetric. We assume Atype∣_a and A^′type∣_a and AconvA^′ ∣_a, and we prove A^′convA ∣_a.

We have \(A\rightarrow ^{*}_{\mathsf {type}}{\Pi } (x:B)F\) and \(A^{\prime }\rightarrow ^{*}_{\mathsf {type}}{\Pi } (x:B^{\prime })F^{\prime }\) and BconvB^′∣_b. By induction, we have B^′convB∣_b. Also, we have N : B^′∣_v:b iff N : B∣_v:b and this implies F(x/N) convF^′(x/N)∣_f(v) and so F(x/N^′) convF(x/N)∣_f(v) by induction. So we get A^′convA∣_a as required. □

Lemma 9

1. 1.

   IfJ∣_aanda^′≤ ainType,then\(J\mid _{a^{\prime }}\)where J isAtypeorAconvB.

2. 2.

   If\(J{\mid ^{i}_{a}}\)anda^′≤ ainElU_i,then\(J\mid ^{i}_{a^{\prime }}\)where J isAtypeorAconvB.

3. 3.

   IfAtype∣_aanda^′≤ ainTypeand\(J\mid _{u^{\prime }:a^{\prime }}\),then\(J\mid _{u^{\prime }:a}\)where J isM : AorMconvM^′ : A.

4. 4.

   Finally, ifAtype∣_aanda^′≤ ainTypeandJ∣_u:aandu^′ : a^′andu^′≤ u,then\(J\mid _{u^{\prime }:a^{\prime }}\)where J isM : AorMconvM^′ : A.

Proof

We prove simultaneously the assertions by induction on the complexity of a in Type. We explain two representative cases.

In case a = π bf and a^′ = π b^′f^′≤ a and Atype∣_a, we assume Atype∣_a and we show \(A~\mathsf {type}\mid _{a^{\prime }}\). We first have \(A\rightarrow _{\mathsf {type}}^{*} {\Pi } (x:B)F\) and Btype∣_b and N : B∣_v:b implies F(N) type∣_f(v) and NconvN^′ : B∣_v:b implies F(N) convF(N^′)∣_f(v). By induction we have \(B~\mathsf {type}\mid _{b^{\prime }}\). Also if \(N:B\mid _{v:b^{\prime }}\) then N : B∣_v:b by induction and so F(N) type∣_f(v) and so \(F(N)~\mathsf {type}\mid _{f^{\prime }(v)}\) by induction. Similarly, \(N~\mathsf {conv}~N^{\prime }B\mid _{v:b^{\prime }}\) implies F(N) convF(N^′)∣_f(v) and so \(F(N)~\mathsf {conv}~F(N^{\prime })\mid _{f^{\prime }(v)}\) by induction.

If a = π bf and a^′ = π b^′f^′≤ a and Atype∣_a and \(M:A\mid _{u:a^{\prime }}\), then we claim that M : A∣_u:a. We know \(A\rightarrow _{\mathsf {type}}^{*} {\Pi }(x:B)F\) with Btype∣_b. We have to show that N : B∣_v:b implies MN : F(N)∣_u(v):f(v). By induction, we know that if v^′≤ v and v^′ in Elb^′ then \(N:B\mid _{v^{\prime }:b^{\prime }}\). Since \(M:A\mid _{u:a^{\prime }}\) we have \(M~N:F(N)\mid _{u(v^{\prime }):f^{\prime }(v^{\prime })}\). Since u : a^′ we have v^′≤ v in Elb^′ such that u(v) = u(v^′) by Lemma 5. For this v^′ we have \(M~N:F(N)\mid _{u(v):f^{\prime }(v^{\prime })}\) and then MN : F(N)∣_u(v):f(v) by induction, since F(N) type∣_f(v) and f^′(v^′) ≤ f(v). We prove similarly that NconvP : B∣_v:b implies MNconvMP : F(N)∣_u(v):f(v). □

We use this result to extend the relation Atype∣_a for a arbitrary (possibly infinite) in Type.

Definition 1

Atype∣_ameans\(A~\mathsf {type}\mid _{a_{0}}\)for all finite a₀ ≤ ainType.If J isM : AorMconvM^′ : Athen the relationsJ∣_u:afor u arbitrary inElais defined as follows: for all u₀ ≤ ufinite inElathere exists a₀ ≤ afinite inTypesuch that\(J\mid _{u_{0}:a_{0}}\).

Note that if we have \(J\mid _{u_{0}:a_{0}}\) then we also have \(J\mid _{u_{0}:a_{1}}\) for any finite a₁ such that a₀ ≤ a₁ ≤ a in Type by Lemma 9.

Proposition 2

We haveAtype∣_{π bf}if,and only if,\(A\rightarrow ^{*}_{\mathsf {type}} {\Pi }(x:B)F\)for B and F withBtype∣_band

1. 1.

   N : B∣_v:bimpliesF(N) type∣_f(v),and

2. 2.

   NconvN^′ : B∣_v:bimpliesF(N) convF(N^′)∣_f(v).

Proof

We assume \(A~\mathsf {type}\mid _{{\Pi }~b~f}\). This means \(A~\mathsf {type}\mid _{{\Pi }~b_{0}~f_{0}}\) for all finite \({\Pi }~b_{0}~f_{0}\leqslant {\Pi }~b~f\) in Type, and, in particular, we have \(A~\mathsf {type}\mid _{{\Pi }~b_{0}~f_{0}}\) for b₀ = ⊥ and f₀ = ⊥. This implies \(A\rightarrow ^{*}_{\mathsf {type}} {\Pi }(x:B)F\) for some Btype and \(F~\mathsf {type}~(x:B)\).

If \(b_{0}\leqslant b\) in Type is finite we have \(A~\mathsf {type}\mid _{{\Pi }~b_{0}~\bot }\) and so \(B~\mathsf {type}\mid _{b_{0}}\). So we have \(B~\mathsf {type}\mid _{b}\).

For N : B∣_v:b we show \(F(N)~\mathsf {type}\mid _{f(v)}\) by showing that \(F(N)~\mathsf {type}\mid _{w_{0}}\) for any \(w_{0}\leqslant f(v)\) finite in Type. By the remark on continuity of evaluation at the end of Section 2, we can find \(b_{0}\leqslant b\) finite in \({\mathsf {Type}}\) and \(v_{0}\leqslant v\) finite in Elb₀ and \(f_{0}\leqslant f\) finite in \(El~b_{0}\rightarrow {\mathsf {Type}}\) such that \(w_{0}\leqslant f_{0}(v_{0})\) in Type. We then have \(A~\mathsf {type}\mid _{{\Pi }~b_{0}~f_{0}}\) and \(N:B\mid _{v_{0}:b_{1}}\) for some \(b_{1}\leqslant b\) finite in Type. We can assume \(b_{0}\leqslant b_{1}\), maybe changing b₁ to b₀ ∨ b₁, and using Lemma 9.3. By Lemma 9.4, we also have \(N:B\mid _{v_{0}:b_{0}}\) and hence \(F(N)\mid _{f_{0}(v_{0})}\) as needed to be shown.

The last assertion about conversion has a similar proof.

Conversely assume \(A\rightarrow ^{*}_{\mathsf {type}} {\Pi }(x:B)F\) with Btype∣_b and N : B∣_v:b implies F(N)∣_f(v) and \(N~\mathsf {conv}~N^{\prime }:B\mid _{v:b}\) implies \(F(N)~\mathsf {conv}~F(N^{\prime })\mid _{f(v)}\). We show that \(A~\mathsf {type}\mid _{{\Pi }~b_{0}~f_{0}}\) for all finite \({\Pi }~b_{0}~f_{0}\leqslant {\Pi }~b~f\) in Type. We have \(B~\mathsf {type}\mid _{b_{0}}\) by definition, and if \(N:B\mid _{v:b_{0}}\) with v in Elb₀ finite, then N : B∣_v:b and so F(N) type∣_f(v) and hence \(F(N)~\mathsf {type}\mid _{f_{0}(v)}\). We prove similarly that \(N~\mathsf {conv}~N^{\prime } : B\mid _{v:b_{0}}\) with v finite implies \(F(N)~\mathsf {conv}~F(N^{\prime })\mid _{f_{0}(v)}\). □

Proposition 3

GivenAtype∣_{π bf}and\(A\rightarrow ^{*}_{\mathsf {type}} {\Pi }(x:B)F\),we haveM : A∣_{w:π bf}if, and only if,N : B∣_v:bimpliesMN : F(N)∣_w(v):f(v)andNconvN^′ : B∣_v:bimpliesMNconvMN^′ : F(N)∣_w(v):f(v).

Proof

Similar to the proof of Proposition 2. □

The two last propositions hold by definition if π bf is a finite element of Type. Note that we could not have used these propositions directly on general, maybe infinite, element as a definition of Atype∣_{π bf} since it might be that f(v) is as complex as π bf. The method we have used instead was thus first to define the relation Atype∣_{π bf} for π bffinite, and then extend this relation by “continuity” on general elements. This is similar to the use of “inclusive predicates” [12, 15], fundamental in denotational semantics.

Lemma 10

1. 1.

   IfA →_typeA^′andA^′type∣_a,thenAtype∣_aandAconvA^′∣_a.

2. 2.

   IfAtype∣_aandM →_AM^′andM^′ : A∣_u:a,thenM : A∣_u:aandMconvM^′ : A∣_u:a.

Proof

Both properties are shown by induction on a. The most interesting case is for the second assertion when a = π bf. We then have \(A\rightarrow _{\mathsf {type}}^{*} {\Pi }(x:B)F\) with Btype∣_b. If N : B∣_v:b, we have MN →_F(N)M^′N and M^′N : F(N)∣_u(v):f(v). By induction, we have MN : F(N)∣_u(v):f(v) and MNconvM^′N : F(N)∣_u(v):f(v). Similarly, if NconvN^′∣_v:b, we get MN^′convM^′N^′ : F(N)∣_u(v):f(v). Since M^′ : A∣_u:a we have M^′NconvM^′N^′ : F(N)∣_u(v):f(v) and we get by transitivity and symmetry MNconvMN^′ : F(N)∣_u(v):f(v). □

We write σ : Γ∣_ρ to mean that we have Aσtype∣_⟦A⟧ρ and \(\sigma (x):A\sigma \mid _{\rho (x):\llbracket A \rrbracket \rho }\) for all x : A in Γ. Note that, in particular, this implies that ρ fits Γ.

Similarly, we write σconvσ^′ : Γ∣_ρ to mean that we have AσconvAσ^′∣_⟦A⟧ρ and σ(x) convσ^′(x) : Aσ∣_{ρ(x):⟦A⟧ρ} for all x : A in Γ.

Theorem 2

The following properties hold, givenσ : Γ∣_ρandσconvσ^′ : Γ∣_ρ.

1. 1.

   If Γ ⊩ Atype,thenAσtype∣_⟦A⟧ρ.

2. 2.

   If Γ ⊩ M : A,thenMσ : Aσ∣_{⟦M⟧ρ:⟦A⟧ρ}.

3. 3.

   If Γ ⊩ AconvA^′,thenAσconvA^′σ∣_⟦A⟧ρ.

4. 4.

   If Γ ⊩ MconvM^′ : A,thenMσconvM^′σ : Aσ∣_{⟦M⟧ρ:⟦A⟧ρ}.

5. 5.

   If Γ ⊩ Atype,thenAσconvAσ^′∣_⟦A⟧ρ.

6. 6.

   If Γ ⊩ M : A,thenMσconvMσ^′ : Aσ∣_⟦A⟧ρ.

Proof

This follows from Propositions 2 and 3 and Lemma 10, and the fact that weak-head reduction is stable under substitution. □

Corollary 5

If0convM : N,then\(M\rightarrow _{\mathsf {N}}^{*} \mathsf {0}\).IfSM₀convM : N,then\(M\rightarrow _{\mathsf {N}}^{*} \mathsf {S}~M_{1}\)withM₀convM₁ : N.IfA₀conv π(x : B₁)F₁,then\(A_{0}\rightarrow _{\mathsf {type}}^{*} {\Pi }(x:B_{0})F_{0}\)withB₀convB₁andN : B₀impliesF₀(N) convF₁(N).

Proof

For the first statement, we have ⟦M⟧ = ⟦0⟧ = 0. Using the previous theorem, we get \(M:\mathsf {N}\mid _{\llbracket M \rrbracket :\mathsf {N}}\) that is M : N∣_0:N, which means precisely \(M\rightarrow _{\mathsf {N}}^{*} \mathsf {0}\). The proof of the second statement is similar.

If A₀conv π(x : B₁)F₁, then \(\llbracket A_{0} \rrbracket = \llbracket {\Pi }(x:B_{1})F_{1} \rrbracket = {\Pi }~\llbracket B_{1} \rrbracket ~\llbracket \lambda (x:B_{1})F_{1} \rrbracket \) and we have \(A_{0}~\mathsf {conv}~{\Pi }(x:B_{1}){F_{1}}\mid _{\llbracket A_{0} \rrbracket }\) by Theorem 2. It follows that \(A_{0}\rightarrow _{\mathsf {type}}^{*} {\Pi }(x:B_{0})F_{0}\) and \(B_{0}~\mathsf {conv}~{B_{1}}\mid _{\llbracket B_{0} \rrbracket }\) and \(N:B_{0}\mid _{v:\llbracket B_{1} \rrbracket }\) implies \(F_{0}(N)~\mathsf {conv}~F_{1}(N)\mid _{\llbracket F_{0} \rrbracket (x=v)}\). In particular, we have B₀convB₁ and, for v = ⊥, we have F₀(N) convF₁(N) if N : B₀. □

Note that we cannot conclude that dependent product is one-to-one for conversion yet, since in the last case we get only that N : B₀ implies F₀(N) convF₁(N), for N : B₀closed, which is not enough to conclude F₀convF₁ (x : B₀). A simple modification of our argument will apply however, as we shall see in the next section.

We fix a context Δ = x₁ : T₁,x₂ : T₂(x₁),…,x_n : T_n(x₁,…,x_n− 1). Working in this context Δ corresponds to extend the type system with constants c₁ : T₁,c₂ : T₂(c₁),…,c_n : T_n(c₁,…,c_n− 1). We define the interpretation of these constants by taking ⟦c_i⟧ = ⊥.

We then have \(c_{1}:{T_{1}}\mid _{\llbracket c_{1} \rrbracket :\llbracket T_{1} \rrbracket },~c_{2}:{T_{2}(c_{1})}\mid _{\llbracket c_{2} \rrbracket :\llbracket T_{2}(c_{1}) \rrbracket },~\dots \). All the reasoning of the previous section applies with this addition of constants c_i. Moving between constants and variables, we deduce the following proposition, which does not mention constants:

Proposition 4

If Δ ⊩ A₀conv π(x : B₁)F₁,then\(A_{0}\rightarrow ^{*}_{\mathsf {type}} {\Pi }(x:B_{0})F_{0}\)withΔ ⊩ B₀convB₁and Δ ⊩ N : B₀implies Δ ⊩ F₀(N/x) convF₁(N/x).

Note that for this proposition, the context Δ is completely arbitrary. We can thus deduce the following fact:

Corollary 6

If Δ ⊩ A₀conv π(x : B₁)F₁,then\(A_{0}\rightarrow ^{*}_{\mathsf {type}} {\Pi }(x:B_{0})F_{0}\)suchthat Δ ⊩ B₀convB₁and Δ,x : B₀ ⊩ F₀convF₁.

Proof

Since all judgments stay valid by extension of the context, we not only have Δ ⊩ A₀conv π(x : B₁)F₁. but also Δ,x : B₀ ⊩ A₀conv π(x : B₁)F₁. We can then apply the previous proposition, using Δ,x : B₀ instead of Δ and taking x for u. □

As in [2], an important application of the injectivity of dependent product for conversion is subject-reduction, i.e. the following result.

Corollary 7

IfAtypeandA → A^′thenA^′typeandAconvA^′.IfM : AandM → M^′thenM^′ : AandMconvM^′ : A.

We refine the domain as follows

and we add the following typing rules:

We extend the application operation u(v) by taking T(v) to be T for any value T. An operational intuition about T is that it represents the semantics of an “exception”. We also extend the definition of rec by rec(d₀,d₁) T = T. We finally refine the definition of the projection function by adding the clauses

We now introduce the special class of “neutral” terms

and the predicate G(k) of “typable” neutral terms, which is defined by the following clauses, where we define at the same time the type function τ(k):

1. 1.

   Any constant c_i is typable, G(c_i), and τ(c_i) = T_i is the given type of c_i.

2. 2.

   If G(k) and \(\tau (k)\rightarrow _{\mathsf {type}}^{*} {\Pi } (x:B)F\) and N : B, then G(kN) and τ(kN) = F(N)

3. 3.

   If G(k) and \(\tau (k)\rightarrow _{\mathsf {type}}^{*} \mathsf {N}\) and Ttype (x : N) and M₀ : T(0) and M₁ : π(x : N)(T → T(Sx)), then G(rec(λxT,M₀,M₁) k) and τ(rec(λxT,M₀,M₁) k) = T(k)

We define next an equivalence relation Q(k,k^′) on elements satisfying G by the clauses:

1. 1.

   Q(c_i,c_i)

2. 2.

   Q(kN,k^′N^′) if Q(k,k^′) and \(\tau (k)\rightarrow _{\mathsf {type}}^{*} {\Pi } (x:B)F\) and N : B and \(\tau (k^{\prime })\rightarrow _{\mathsf {type}}^{*} {\Pi } (x:B^{\prime })F^{\prime }\) and N^′ : B^′ and BconvB^′ and FconvF^′ (x : B)

3. 3.

   \(Q(\mathsf {rec}(\lambda x~T,M_{0},M_{1})~k,\mathsf {rec}(\lambda x~T^{\prime },M_{0}^{\prime },M_{1}^{\prime })~k^{\prime })\) if Q(k,k^′) and \(\tau (k)\rightarrow _{\mathsf {type}}^{*} \mathsf {N}\) and \(\tau (k^{\prime })\rightarrow _{\mathsf {type}}^{*} \mathsf {N}\) and TconvT^′ (x : N) and \(M_{0}~\mathsf {conv}~M^{\prime }_{0}:T(\mathsf {0})\) and \(M_{1}~\mathsf {conv}~ M_{1}^{\prime }:{\Pi } (x:\mathsf {N})(T\rightarrow T(\mathsf {S}~x))\).

We refine then the definitions of J∣_a and J∣_u:a by the clauses:

1. 1.

   Atype∣_T means that \(A\rightarrow _{\mathsf {type}}^{*} k\) for some k

2. 2.

   AconvA^′∣_T means that AconvA^′

3. 3.

   M : A∣_T:a, where a is T or U_i or N, means \(M\rightarrow _{A}^{*} k\) for some k

4. 4.

   MconvM^′ : A∣_T:a, where a is T or U_i or N, means MconvM^′ : A

Lemma 11

IfG(k) andτ(k) type∣_a,thenk : τ(k)∣_paT:a.IfQ(k,k^′) andτ(k) type∣_a,thenkconvk^′ : τ(k)∣_paT:a.

Proof

By induction on atype. Let us for instance prove the first assertion in the case where a = π bf. We have \(\tau (k)\rightarrow _{\mathsf {type}}^{*} {\Pi } (x:B)F\) with Btype∣_b and N : B∣_v:b implies F(N) type∣_f(v) and NconvN^′ : B∣_v:b implies F(N) convF(N^′)∣_f(v). It follows that N : B∣_v:b implies G(kN) and τ(kN) = F(N), so that kN : F(N)∣_{p (f(v)) T:f(v)} by induction. Similarly we show that NconvN^′∣_v:b implies Q(kN,kN^′) and so kNconvkN^′ : F(N)∣_{p (f(v)) T:f(v)} by induction. □

We explain now the semantics of the constants c₁ : T₁, c₂ : T₂(c₁),…. We take \(\llbracket c_{1} \rrbracket = p~\llbracket T_{1} \rrbracket ~\mathsf {T}\) and then ⟦c₂⟧ = p ⟦T₂(c₁)⟧ T and so on. This is justified since T₁ does not refer to any constant, and T₂ refers at most to the constant c₁, and so on. It follows from the last lemma that we have \(T_{i}~\mathsf {type}\mid _{\llbracket T_{i} \rrbracket }\) and \(c_{i}:T_{i}\mid _{\llbracket c_{i} \rrbracket :\llbracket T_{i} \rrbracket }\).

Theorem 2 holds then with this semantics, since it holds for the constants c_i.

We then have the following application, using as in the previous section the fact that the context Δ is arbitrary.

Theorem 3

If Δ ⊩ MconvN : A,thenM : AandN : Ahave the same Böhm tree.

Proof

Corollary 7 implies that a term is convertible to (and hence as the same semantics as) its weak head normal form. Theorem 2 shows then that, given any two convertible terms, if one has a weak head normal form, so does the other term and these weak head normal form have the same shape. □

We have shown that constructors are one-to-one for dependent type theory with conversion as judgment andη-conversion in a weak metatheory, while all existing proofs [2] use strong logical principles. Our argument applies as well to partial type theory, where we may have non terminating computations. An example is given in the reference [11]: one introduces a new base type Ω, which is like the type of natural numbers N with 0 deleted, and an element ω : Ω such that ωconvSω : Ω. The type Ω will be represented by a new finite element of the domain, while the element ω will be the least upper bound of the sequence ⊥, S ⊥, S (S ⊥),…

Using strong logical principles, it should be possible to define a semantical notion of totality on elements of the domain, and prove that a total element corresponds to a finite Böhm tree. If we are only interested in the evaluation of closed expressions, the techniques we have presented are enough to show canonicity of type theory extended with bar recursion, as in [8], but with η-conversion in the type system.

On the other hand it is not clear how to extend the present method to a type system with a type of all types. Do we still have adequacy in this case?