# Embedding Pure Type Systems in the lambda-Pi-calculus modulo

Denis Cousineau, Gilles Dowek

<figure><img src="image_1.png" /></figure>

## To cite this version:

Denis Cousineau, Gilles Dowek. Embedding Pure Type Systems in the lambda-Pi-calculus modulo. 2007. hal-04245478

HAL Id: hal-04245478

https://inria.hal.science/hal-04245478v1

Preprint submitted on 17 Oct 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Embedding Pure Type Systems in the lambda-Pi-calculus modulo

Denis Cousineau and Gilles Dowek

École polytechnique and INRIA
LIX, École polytechnique, 91128 Palaiseau Cedex, France.

Cousineau@lix.polytechnique.fr, http://www.lix.polytechnique.fr/~cousineau
Gilles.Dowek@polytechnique.edu, http://www.lix.polytechnique.fr/~dowek

**Abstract.** The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calculus modulo. We show in this paper that this simple extension is surprisingly expressive and, in particular, that all functional Pure Type Systems, such as the system F, or the Calculus of Constructions, can be embedded in it. And, moreover, that this embedding is conservative under termination hypothesis.

The $\lambda\Pi$-calculus is a dependently typed lambda-calculus that allows to express proofs of minimal predicate logic through the Brouwer-Heyting-Kolmogorov interpretation and the Curry-de Bruijn-Howard correspondence. It can be extended in several ways to express proofs of some theory. A first solution is to express the theory in Deduction modulo [7, 9], i.e. to orient the axioms as rewrite rules and to extend the $\lambda\Pi$-calculus to express proofs in Deduction modulo [3]. We get this way the $\lambda\Pi$-calculus modulo. This idea of extending the dependently typed lambda-calculus with rewrite rules is also that of Intuitionistic type theory used as a logical framework [13].

A second way to extend the $\lambda\Pi$-calculus is to add typing rules, in particular to allow polymorphic typing. We get this way the *Calculus of Constructions* [4] that allows to express proofs of simple type theory and more generally the *Pure Type Systems* [2, 15, 1]. These two kinds of extensions of the $\lambda\Pi$-calculus are somewhat redundant. For instance, simple type theory can be expressed in deduction modulo [8], hence the proofs of this theory can be expressed in the $\lambda\Pi$-calculus modulo. But they can also be expressed in the Calculus of Constructions. This suggests to relate and compare these two ways to extend the $\lambda\Pi$-calculus.

We show in this paper that all functional Pure Type Systems can be embedded in the $\lambda\Pi$-calculus modulo using an appropriate rewrite system. This rewrite system is inspired both by the expression of simple type theory in Deduction modulo and by the mechanisms of universes à la Tarski [12] of Intuitionistic type theory. In particular, this work extends Palmgren's construction of an impredicative universe in type theory [14].
# 1 The $\lambda\Pi$-calculus

The $\lambda\Pi$-calculus is a dependently typed lambda-calculus that permits to construct types depending on terms, for instance a type *array* $n$, of arrays of size $n$, that depends on a term $n$ of type *nat*. It also permits to construct a function $f$ taking a natural number $n$ as an argument and returning an array of size $n$. Thus, the arrow type *nat* $\Rightarrow$ *array* of simply typed lambda-calculus must be extended to a dependent product type $\Pi x : \text{nat} \; (\text{array} \; x)$ where, in the expression $\Pi x : A B$, the occurrences of the variable $x$ are bound in $B$ by the symbol $\Pi$ (the expression $A \Rightarrow B$ is used as a shorter notation for the expression $\Pi x : A B$ when $x$ has no free occurrence in $B$). When we apply the function $f$ to a term $n$, we do not get a term of type *array* $x$ but of type *array* $n$. Thus, the application rule must include a substitution of the term $n$ for the variable $x$. The symbol *array* itself takes a natural number as an argument and returns a type. Thus, its type is *nat* $\Rightarrow$ *Type*, i.e. $\Pi x : \text{nat Type}$. The terms *Type*, *nat* $\Rightarrow$ *Type*, ... cannot have type *Type*, because Girard's paradox [10] could then be expressed in the system, thus we introduce a new symbol *Kind* to type such terms. To form terms, like $\Pi x : \text{nat Type}$, whose type is *Kind*, we need a rule expressing that the symbol *Type* has type *Kind* and a new product rule allowing to form the type $\Pi x : \text{nat Type}$, whose type is *Kind*. Besides the variables such as $x$ whose type has type *Type*, we must permit the declaration of variables such as *nat* of type *Type*, and more generally, variables such as *array* whose type has type *Kind*. This leads to introduce the following syntax and typing rules.

**Definition 1 (The syntax of $\lambda\Pi$).** The syntax of the $\lambda\Pi$-calculus is

$$t = x \mid \text{Type} \mid \text{Kind} \mid \Pi x : t t \mid \lambda x : t t \mid t t$$

The $\alpha$-equivalence and $\beta$-reduction relations are defined as usual and terms are identified modulo $\alpha$-equivalence.

**Definition 2 (The typing rules of $\lambda\Pi^-$).**

```
[] well-formed Empty
```

$$\frac{\Gamma \vdash A : \text{Type}}{\Gamma[x : A] \text{ well-formed}} \quad \text{Declaration } x \text{ not in } \Gamma$$

$$\frac{\Gamma \vdash A : \text{Kind}}{\Gamma[x : A] \text{ well-formed}} \quad \text{Declaration2 } x \text{ not in } \Gamma$$

$$\frac{\Gamma \text{ well-formed}}{\Gamma \vdash \text{Type} : \text{Kind}} \quad \text{Sort}$$

$$\frac{\Gamma \text{ well-formed} \quad x : A \in \Gamma}{\Gamma \vdash x : A} \quad \text{Variable}$$

$$\frac{\Gamma \vdash A : \text{Type} \quad \Gamma[x : A] \vdash B : \text{Type}}{\Gamma \vdash \Pi x : A B : \text{Type}} \quad \text{Product}$$
$$ \frac{\Gamma \vdash A : \mathit{Type} \quad \Gamma[x : A] \vdash B : \mathit{Kind}}{\Gamma \vdash \Pi x : A B : \mathit{Kind}} \quad \mathbf{Product2} $$

$$ \frac{\Gamma \vdash A : \mathit{Type} \quad \Gamma[x : A] \vdash B : \mathit{Type} \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash \lambda x : A t : \Pi x : A B} \quad \mathbf{Abstraction} $$

$$ \frac{\Gamma \vdash t : \Pi x : A B \quad \Gamma \vdash u : A}{\Gamma \vdash (t \ u) : (u/x) B} \quad \mathbf{Application} $$

It is useful, in some situations, to add a rule allowing to build type families by abstraction, for instance $\lambda x : nat (array (2 \times x))$ and rules asserting that a term of type $(\lambda x : nat (array (2 \times x)) n)$ also has type $array (2 \times n)$. This leads to introduce the following extra typing rules.

**Definition 3 (The typing rules of $\lambda\Pi$).** The typing rules of $\lambda\Pi$ are those of $\lambda\Pi^-$ and

$$ \frac{\Gamma \vdash A : \mathit{Type} \quad \Gamma[x : A] \vdash B : \mathit{Kind} \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash \lambda x : A t : \Pi x : A B} \quad \mathbf{Abstraction2} $$

$$ \frac{\Gamma \vdash A : \mathit{Type} \quad \Gamma \vdash B : \mathit{Type} \quad \Gamma \vdash t : A}{\Gamma \vdash t : B} \quad \mathbf{Conversion} \ A \equiv_{\beta} B $$

$$ \frac{\Gamma \vdash A : \mathit{Kind} \quad \Gamma \vdash B : \mathit{Kind} \quad \Gamma \vdash t : A}{\Gamma \vdash t : B} \quad \mathbf{Conversion2} \ A \equiv_{\beta} B $$

where $\equiv_{\beta}$ is the $\beta$-equivalence relation.

It can be proved that types are preserved by $\beta$-reduction, that $\beta$-reduction is confluent and strongly terminating and that each term has a unique type modulo $\beta$-equivalence.

The $\lambda\Pi$-calculus, and even the $\lambda\Pi^-$-calculus, can be used to express proofs of minimal predicate logic, following the Brouwer-Heyting-Kolmogorov interpretation and the Curry-de Bruijn-Howard correspondence. Let $\mathcal{L}$ be a language in predicate logic, we consider a context $\Gamma$ formed with a variable $\iota$ of type $\mathit{Type}$ – or variables $\iota_1, \dots, \iota_n$ of type $\mathit{Type}$ when $\mathcal{L}$ is many-sorted –, for each function symbol $f$ of $\mathcal{L}$, a variable $f$ of type $\iota \Rightarrow \dots \Rightarrow \iota \Rightarrow \iota$ and for each predicate symbol $P$ of $\mathcal{L}$, a variable $P$ of type $\iota \Rightarrow \dots \Rightarrow \iota \Rightarrow \mathit{Type}$.

To each formula $P$ containing free variables $x_1, \dots, x_p$ we associate a term $P^\circ$ of type $\mathit{Type}$ in the context $\Gamma, x_1 : \iota, \dots, x_p : \iota$ translating each variable, function symbol and predicate symbol by itself and the implication symbol and the universal quantifier by a product.

To each proof $\pi$, in minimal natural deduction, of a sequent $A_1, \dots, A_n \vdash B$ with free variables $x_1, \dots, x_p$, we can associate a term $\pi^\circ$ of type $B^\circ$ in the context $\Gamma, x_1 : \iota, \dots, x_p : \iota, \alpha_1 : A_1^\circ, \dots, \alpha_n : A_n^\circ$. From the strong termination of the $\lambda\Pi$-calculus, we get cut elimination for minimal predicate logic. If $B$ is an atomic formula, there is no cut free proof, hence no proof at all, of $\vdash B$.
## 2 The $\lambda\Pi$-calculus modulo

The $\lambda\Pi$-calculus allows to express proofs in pure minimal predicate logic. To express proofs in a theory $\mathcal{T}$, we can declare a variable for each axiom of $\mathcal{T}$ and consider proofs-terms containing such free variables, this is the idea of the Logical Framework [11]. However, when considering such open terms most benefits of termination, such as the existence of empty types, are lost.

An alternative is to replace axioms by rewrite rules, moving from predicate logic to *Deduction modulo* [7, 9]. Such extensions of type systems with rewrite rules to express proofs in Deduction modulo have been defined in [3] and [13]. We shall present now an extension of the $\lambda\Pi$-calculus: the $\lambda\Pi$-calculus modulo.

Recall that if $\Sigma$, $\Gamma$ and $\Delta$ are contexts, a substitution $\theta$, binding the variables declared in $\Gamma$, is said to be of type $\Gamma \rightsquigarrow \Delta$ in $\Sigma$ if for all $x$ declared of type $T$ in $\Gamma$, we have $\Sigma\Delta \vdash \theta x : \theta T$, and that, in this case, if $\Sigma\Gamma \vdash u : U$, then $\Sigma\Delta \vdash \theta u : \theta U$.

A *rewrite rule* is a quadruple $l \to^{\Gamma, T} r$ where $\Gamma$ is a context and $l, r$ are $\beta$-normal terms. Such a rule is said to be *well-typed* in the context $\Sigma$ if, in the $\lambda\Pi$-calculus, the context $\Sigma\Gamma$ is well-formed and the terms $l$ and $r$ have type $T$ in this context.

If $\Sigma$ is a context, $l \to^{\Gamma, T} r$ is a rewrite rule well-typed in $\Sigma$ and $\theta$ is a substitution of type $\Gamma \rightsquigarrow \Delta$ in $\Sigma$ then the terms $\theta l$ and $\theta r$ both have type $\theta T$ in the context $\Sigma\Delta$. We say that the term $\theta l$ *rewrites* to the term $\theta r$.

If $\Sigma$ is a context and $\mathcal{R}$ a set of rewrite rules well-typed in the $\lambda\Pi$-calculus in $\Sigma$, then the *congruence generated by* $\mathcal{R}$, $\equiv_{\mathcal{R}}$, is the smallest congruence such that if $t$ rewrites to $u$ then $t \equiv_{\mathcal{R}} u$.

**Definition 4 ($\lambda\Pi$-modulo).** Let $\Sigma$ be a context and $\mathcal{R}$ a rewrite system in $\Sigma$. Let $\equiv_{\mathcal{R}}$ be the congruence of terms generated by the rules of $\mathcal{R}$ and the rule $\beta$.

The $\lambda\Pi$-calculus modulo $\mathcal{R}$ is the extension of the $\lambda\Pi$-calculus obtained by replacing the relation $\equiv_{\beta}$ by $\equiv_{\beta\mathcal{R}}$ in the conversion rules

$$ \frac{\Gamma \vdash A : \text{Type} \quad \Gamma \vdash B : \text{Type} \quad \Gamma \vdash t : A}{\Gamma \vdash t : B} \quad \text{Conversion} \quad A \equiv_{\beta\mathcal{R}} B $$

$$ \frac{\Gamma \vdash A : \text{Kind} \quad \Gamma \vdash B : \text{Kind} \quad \Gamma \vdash t : A}{\Gamma \vdash t : B} \quad \text{Conversion2} \quad A \equiv_{\beta\mathcal{R}} B $$

Notice that we can also extend the $\lambda\Pi^-$-calculus with rewrite rules. In this case, we introduce conversion rules, using the congruence defined by the system $\mathcal{R}$ alone.

*Example 1.* Consider the context $\Sigma = [P : \text{Type}, Q : \text{Type}]$ and the rewrite system $\mathcal{R}$ formed with the rule $P \to (Q \Rightarrow Q)$. The term $\lambda f : P \lambda x : Q (f x)$ is well-typed in the $\lambda\Pi$-calculus modulo $\mathcal{R}$.
### 3 The Pure Type Systems

There are several ways to extend the functional interpretation of proofs to simple type theory. The first is to use the fact that simple type theory can be expressed in Deduction modulo with rewrite rules only [8]. Thus, the proofs of simple type theory can be expressed in the $\lambda\Pi$-calculus modulo, and even in the $\lambda\Pi^-$-calculus modulo. The second is to extend the $\lambda\Pi$-calculus by adding the following typing rules, allowing for instance the construction of the type $\Pi P : Type$ ($P \Rightarrow P$).

$$ \frac{\Gamma \vdash A : \mathit{Kind} \quad \Gamma[x : A] \vdash B : \mathit{Type}}{\Gamma \vdash \Pi x : A B : \mathit{Type}} \quad \mathbf{Product3} $$

$$ \frac{\Gamma \vdash A : \mathit{Kind} \quad \Gamma[x : A] \vdash B : \mathit{Kind}}{\Gamma \vdash \Pi x : A B : \mathit{Kind}} \quad \mathbf{Product4} $$

$$ \frac{\Gamma \vdash A : \mathit{Kind} \quad \Gamma[x : A] \vdash B : \mathit{Type} \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash \lambda x : A t : \Pi x : A B} \quad \mathbf{Abstraction3} $$

$$ \frac{\Gamma \vdash A : \mathit{Kind} \quad \Gamma[x : A] \vdash B : \mathit{Kind} \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash \lambda x : A t : \Pi x : A B} \quad \mathbf{Abstraction4} $$

We obtain the *Calculus of Constructions* [4].

The rules of the simply typed $\lambda$-calculus, the $\lambda\Pi$-calculus and of the Calculus of Constructions can be presented in a schematic way as follows.

**Definition 5 (Pure type system).** A Pure Type System $[2, 15, 1] P$ is defined by a set $S$, whose elements are called sorts, a subset $A$ of $S \times S$, whose elements are called axioms and a subset $R$ of $S \times S \times S$, whose elements are called rules. The typing rules of $P$ are

$$ \boxed{\text{[ ] well-formed}} \quad \mathbf{Empty} $$

$$ \frac{\Gamma \vdash A : s}{\Gamma[x : A] \text{ well-formed}} \quad \mathbf{Declaration} \ s \in S \text{ and } x \text{ not in } \Gamma $$

$$ \frac{\Gamma \text{ well-formed}}{\Gamma \vdash s_1 : s_2} \quad \mathbf{Sort} \ \langle s_1, s_2 \rangle \in A $$

$$ \frac{\Gamma \text{ well-formed} \quad x : A \in \Gamma}{\Gamma \vdash x : A} \quad \mathbf{Variable} $$

$$ \frac{\Gamma \vdash A : s_1 \quad \Gamma[x : A] \vdash B : s_2}{\Gamma \vdash \Pi x : A B : s_3} \quad \mathbf{Product} \ \langle s_1, s_2, s_3 \rangle \in R $$

$$ \frac{\Gamma \vdash A : s_1 \quad \Gamma[x : A] \vdash B : s_2 \quad \Gamma[x : A] \vdash t : B}{\Gamma \vdash \lambda x : A t : \Pi x : A B} \quad \mathbf{Abstraction} \ \langle s_1, s_2, s_3 \rangle \in R $$

$$ \frac{\Gamma \vdash t : \Pi x : A B \quad \Gamma \vdash u : A}{\Gamma \vdash (t \ u) : (u/x)B} \quad \mathbf{Application} $$

$$ \frac{\Gamma \vdash A : s \quad \Gamma \vdash B : s \quad \Gamma \vdash t : A}{\Gamma \vdash t : B} \quad \mathbf{Conversion} \ s \in S \ A \equiv_{\beta} B $$
The simply typed λ-calculus is the system defined by the sorts Type and Kind, the axiom $\langle Type, Kind \rangle$ and the rule $\langle Type, Type, Type \rangle$. The λΠ-calculus is the system defined by the same sorts and axiom and the rules $\langle Type, Type, Type \rangle$ and $\langle Type, Kind, Kind \rangle$. The Calculus of Constructions is the system defined by the same sorts and axiom and the rules $\langle Type, Type, Type \rangle$, $\langle Type, Kind, Kind \rangle$, $\langle Kind, Type, Type \rangle$ and $\langle Kind, Kind, Kind \rangle$. Other examples of Pure Type Systems are Girard's systems F and Fω.

In all Pure Type Systems, types are preserved under reduction and the β-reduction relation is confluent. It terminates in some systems, such as the λΠ-calculus, the Calculus of Constructions, the system F and the system Fω. Uniqueness of types is lost in general, but it holds for the λΠ-calculus, the Calculus of Constructions, the system F and the system Fω, and more generally for all functional Pure Type Systems.

**Definition 6 (Functional Type System).** A type system is said to be functional if

$$ \langle s_1, s_2 \rangle \in A \text{ and } \langle s_1, s_3 \rangle \in A \text{ implies } s_2 = s_3 \\ \langle s_1, s_2, s_3 \rangle \in R \text{ and } \langle s_1, s_2, s_4 \rangle \in R \text{ implies } s_3 = s_4 $$

# 4 Embedding functional Pure Type Systems in the λΠ-calculus modulo

We have seen that the λΠ-calculus modulo and the Pure Type Systems are two extensions of the λΠ-calculus. At a first glance, they seem quite different as the latter adds more typing rules to the λΠ-calculus, while the former adds more computation rules. But they both allow to express proofs of simple type theory.

We show in this section that functional Pure Type Systems can, in fact, be embedded in the λΠ-calculus modulo with an appropriate rewrite system.

## 4.1 Definition

Consider a functional Pure Type System $P = \langle S, A, R \rangle$. We build the following context and rewrite system.

The context $\Sigma_P$ contains, for each sort $s$, two variables

$$ U_s : Type \quad \text{and} \quad \varepsilon_s : U_s \Rightarrow Type $$

for each axiom $\langle s_1, s_2 \rangle$, a variable

$$ \dot{s}_1 : U_{s_2} $$

and for each rule $\langle s_1, s_2, s_3 \rangle$, a variable

$$ \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} : \Pi X : U_{s_1} (((\varepsilon_{s_1} X) \Rightarrow U_{s_2}) \Rightarrow U_{s_3}) $$

The type $U_s$ is called the *universe* of $s$ and the symbol $\varepsilon_s$ the *decoding function* of $s$.
The rewrite rules are

$$ \varepsilon_{s_2}(\dot{s}_1) \rightarrow U_{s_1} $$

in the empty context and with the type Type, and

$$ \varepsilon_{s_3}(\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} X Y) \rightarrow \Pi x : (\varepsilon_{s_1} X) (\varepsilon_{s_2} (Y x)) $$

in the context $X : U_{s_1}$, $Y : (\varepsilon_{s_1} X) \Rightarrow U_{s_2}$ and with the type Type.

These rules are called the *universe-reduction rules*, we write $\equiv_P$ for the equivalence relation generated by these rules and the rule $\beta$ and we call the $\lambda\Pi_P$-calculus the $\lambda\Pi$-calculus modulo these rewrite rules and the rule $\beta$. To ease notations, in the $\lambda\Pi_P$-calculus, we do not recall the context $\Sigma_P$ in each sequent and write $\Gamma \vdash t : T$ for $\Sigma_P\Gamma \vdash t : T$, and we note $\equiv$ for $\equiv_P$ when there is no ambiguity.

**Example 2.** The embedding of the Calculus of Constructions is defined by the context

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\dot{Type} : U_{Kind} & U_{Type} : Type & U_{Kind} : Type \\
\varepsilon_{Type} : U_{Type} \Rightarrow Type & \varepsilon_{Kind} : U_{Kind} \Rightarrow Type & \\
\dot{\Pi}_{\langle Type,Type,Type \rangle} : \Pi X : U_{Type} (((\varepsilon_{Type} X) \Rightarrow U_{Type}) \Rightarrow U_{Type}) & & \\
\dot{\Pi}_{\langle Type,Kind,Kind \rangle} : \Pi X : U_{Type} (((\varepsilon_{Type} X) \Rightarrow U_{Kind}) \Rightarrow U_{Kind}) & & \\
\dot{\Pi}_{\langle Kind,Type,Type \rangle} : \Pi X : U_{Kind} (((\varepsilon_{Kind} X) \Rightarrow U_{Type}) \Rightarrow U_{Type}) & & \\
\dot{\Pi}_{\langle Kind,Kind,Kind \rangle} : \Pi X : U_{Kind} (((\varepsilon_{Kind} X) \Rightarrow U_{Kind}) \Rightarrow U_{Kind}) & &
\end{array}
$$

and the rules

$$
\begin{array}{l}
\varepsilon_{Kind}(\dot{Type}) \rightarrow U_{Type} \\
\varepsilon_{Type}(\dot{\Pi}_{\langle Type,Type,Type \rangle} X Y) \rightarrow \Pi x : (\varepsilon_{Type} X) (\varepsilon_{Type} (Y x)) \\
\varepsilon_{Kind}(\dot{\Pi}_{\langle Type,Kind,Kind \rangle} X Y) \rightarrow \Pi x : (\varepsilon_{Type} X) (\varepsilon_{Kind} (Y x)) \\
\varepsilon_{Type}(\dot{\Pi}_{\langle Kind,Type,Type \rangle} X Y) \rightarrow \Pi x : (\varepsilon_{Kind} X) (\varepsilon_{Type} (Y x)) \\
\varepsilon_{Kind}(\dot{\Pi}_{\langle Kind,Kind,Kind \rangle} X Y) \rightarrow \Pi x : (\varepsilon_{Kind} X) (\varepsilon_{Kind} (Y x))
\end{array}
$$

**Definition 7 (Translation).** Let $\Gamma$ be a context in a functional Pure Type System $P$ and $t$ a term well-typed in $\Gamma$, we defined the translation $|t|$ of $t$ in $\Gamma$, that is a term in $\lambda\Pi_P$, as follows

$$ - |x| = x, $$

$$ - |s| = \dot{s}, $$

$$ - |\Pi x : A B| = \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} |A| (\lambda x : (\varepsilon_{s_1} |A|) |B|), \text{ where } s_1 \text{ is the type of } A, \\ s_2 \text{ is the type of } B \text{ and } s_3 \text{ the type of } \Pi x : A B, $$

$$ - |\lambda x : A t| = \lambda x : (\varepsilon_s |A|) |t|, $$

$$ - |t u| = |t| |u|. $$
**Definition 8 (Translation as a type).** Consider a term A of type s for some sort s. The translation of A as a type is

$$ \|A\| = \varepsilon_s |A|. $$

Note that if A is a well-typed sort s' then

$$ \|s'\| = \varepsilon_s \dot{s}' \equiv_P U_{s'}. $$

We extend this definition to non well-typed sorts, such as the sort Kind in the Calculus of Constructions, by

$$ \|s'\| = U_{s'}. $$

The translation of a well formed context is defined by

$$ \|[ ]\| = \llbracket \rrbracket \quad \text{and} \quad \|\Gamma[x : A]\| = \|\Gamma\|[x : \|A\|] $$

## 4.2 Soundness

**Proposition 1.** 1. $|(u/x)t| = (|u|/x)|t|$, $\|(u/x)t\| = (|u|/x)\|t\|$.

2. If $t \to_{\beta} u$ then $|t| \to_{\beta} |u|$.

*Proof.* 1. By induction on t.

2. Because a $\beta$-redex is translated as a $\beta$-redex.

**Proposition 2.** $\|\Pi x : A B\| \equiv_P \Pi x : \|A\| \|B\|$

*Proof.* Let $s_1$ be the type of A, $s_2$ that of B and $s_3$ that of $\Pi x : A B$. We have $\|\Pi x : A B\| = \varepsilon_{s_3} |\Pi x : A B| = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1,s_2,s_3 \rangle} |A| (\lambda x : (\varepsilon_{s_1} |A|) |B|)) \equiv_P \Pi x : (\varepsilon_{s_1} |A|) (\varepsilon_{s_2} ((\lambda x : (\varepsilon_{s_1} |A|) |B|) x)) \equiv_P \Pi x : (\varepsilon_{s_1} |A|) (\varepsilon_{s_2} |B|) = \Pi x : \|A\| \|B\|$.

**Example 3.** In the Calculus of Constructions, the translation as a type of $\Pi X : Type (X \Rightarrow X)$ is $\Pi X : U_{Type} ((\varepsilon_{Type} X) \Rightarrow (\varepsilon_{Type} X))$. The translation as a term of $\lambda X : Type \lambda x : X x$ is the term $\lambda X : U_{Type} \lambda x : (\varepsilon_{Type} X) x$. Notice that the former is the type of the latter. The generalization of this remark is the following proposition.

**Proposition 3 (Soundness).**

$$ \text{If } \Gamma \vdash t : B \text{ in } P \text{ then } \|\Gamma\| \vdash |t| : \|B\| \text{ in } \lambda\Pi_P. $$

*Proof.* By induction on t.

- If $t$ is a variable, this is trivial.

- If $t = s_1$ then $B = s_2$ (where $\langle s_1, s_2 \rangle$ is an axiom), we have $\dot{s}_1 : U_{s_2} = \|s_2\|$.

- If $t = \Pi x : C D$, let $s_1$ be the type of C, $s_2$ that of D and $s_3$ that of t. By induction hypothesis, we have

$$ \|\Gamma\| \vdash |C| : U_{s_1} \quad \text{and} \quad \|\Gamma\|, x : \|C\| \vdash |D| : U_{s_2} $$
i.e.

$$ \|\Gamma\|, x : (\varepsilon_{s_1} | C) \vdash |D| : U_{s_2} $$

Thus

$$ \|\Gamma\| \vdash (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} |C| \lambda x : (\varepsilon_{s_1} |C|) |D|) : U_{s_3} $$

i.e.

$$ \|\Gamma\| \vdash |\Pi x : C D| : \|s_3\| $$

– If $t = \lambda x : C u$, then we have

$$ \Gamma, x : C \vdash u : D $$

and $B = \Pi x : C D$. By induction hypothesis, we have

$$ \|\Gamma\|, x : \|C\| \vdash |u| : \|D\| $$

i.e.

$$ \|\Gamma\|, x : (\varepsilon_{s_1} | C) \vdash |u| : \|D\| \quad \text{then} \quad \|\Gamma\| \vdash \lambda x : (\varepsilon_{s_1} | C) |u| : \Pi x : \|C\| \|D\| $$

i.e.

$$ \|\Gamma\| \vdash |t| : \|\Pi x : C D\| $$

– If $t = u v$, then we have

$$ \Gamma \vdash u : \Pi x : C D, \quad \Gamma \vdash v : C $$

and $B = (v/x)D$. By induction hypothesis, we get

$$ \|\Gamma\| \vdash |u| : \|\Pi x : C D\| = \Pi x : \|C\| \|D\| \quad \text{and} \quad \|\Gamma\| \vdash |v| : \|C\| $$

Thus

$$ \|\Gamma\| \vdash |t| : (|v|/x) \|D\| = \|(v/x)D\| $$

## 4.3 Termination

**Proposition 4.** If $\lambda\Pi_P$ terminates then $P$ terminates.

*Proof.* Let $t_1$ be a well-typed term in $P$ and $t_1, t_2, ...$ be a reduction sequence of $t_1$ in $P$. By Proposition 3, the term $|t_1|$ is well-typed in $\lambda\Pi_P$ and, by Proposition 1, $|t_1|, |t_2|, ...$ is a reduction sequence of $|t_1|$ in $\lambda\Pi_P$. Hence it is finite.

## 4.4 Confluence

We prove in this section that for any functional Pure Type System $P$, the system $\lambda\Pi_P$ is confluent. Like that of pure $\lambda$-calculus, the reduction relation of $\lambda\Pi_P$ is not strongly confluent: the term $M = (\lambda x (x x)) ((\lambda y y) 0)$ has two one-step reducts: $N_1 = (\lambda x (x x)) 0$ and $N_2 = ((\lambda y y) 0) ((\lambda y y) 0)$ and these two terms have no common one-step reduct. Thus, we introduce another reduction relation ($\dashv\dashv$) that can reduce, in one step, none to all the $\beta R$-reduces that appears in a term, that is strongly confluent and such that $\dashv\dashv^* = \dashv^*$. Then, from the confluence of the relation $\dashv\dashv^*$, we shall deduce that of the relation $\dashv$.
**Definition 9 (Parallel reduction).** The parallel reduction ($\dashv\dashv$) in $\lambda\Pi_P$, is the smallest relation on terms that verifies:

$$ \begin{array}{l@{\qquad}l} \overline{M \dashv M} & (\alpha) \qquad \overline{\varepsilon_{s_2} \dot{s}_1 \dashv U_{s_1}} & (\beta) \quad \langle s_1, s_2 \rangle \in \mathcal{A} \\ \frac{A \dashv A' \quad M \dashv M'}{\lambda x : A M \dashv \lambda x : A' M'} & (\gamma) \qquad \frac{A \dashv A' \quad B \dashv B'}{\Pi x : A B \dashv \Pi x : A' B'} & (\delta) \\ \frac{M \dashv M' \quad N \dashv N'}{M N \dashv M' N'} & (\theta_1) \qquad \frac{M \dashv M' \quad N \dashv N'}{(\lambda x : A M) N \dashv (N'/x) M'} & (\theta_2) \end{array} $$

$$ \frac{\begin{array}{c} A \dashv A' \quad B \dashv B' \\ \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B) \dashv \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A' B') \end{array}}{\varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B) \dashv \Pi x : (\varepsilon_{s_1} A') (\varepsilon_{s_2}(B' x))} \quad (\eta_1) \quad \langle s_1, s_2, s_3 \rangle \in \mathcal{R} \\ \frac{\begin{array}{c} A \dashv A' \quad B \dashv B' \\ \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B) \dashv \Pi x : (\varepsilon_{s_1} A') (\varepsilon_{s_2}(B' x)) \end{array}}{\varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B) \dashv \Pi x : (\varepsilon_{s_1} A') (\varepsilon_{s_2}(B' x))} \quad (\eta_2) \quad \langle s_1, s_2, s_3 \rangle \in \mathcal{R} $$

**Proposition 5.** For all terms $M, M', N, N'$ of $\lambda\Pi_P$, if $M \dashv M'$ and $N \dashv N'$, then $(N/x)M \dashv (N'/x)M'$.

*Proof.* By induction on M.

- if $M$ is a variable,

★ if $M = x$, then $M' = M = x$ (because $M \dashv M'$ and the only rule we can apply is $(\alpha)$).

Therefore, $(N/x)M = N \dashv N' = (N'/x)M'$.

★ if $M = y \neq x$, then, by the rule $(\alpha)$, $(N/x)M = y \dashv y = (N'/x)M'$ (and we conclude by the same way for $M = \text{Type}$ and $M = \text{Kind}$).

- if there exists terms $A$ and $B$ such that $M = \lambda y : A B$, then there exists terms $A'$ and $B'$ such that $M' = \lambda y : A' B'$ with $A \dashv A'$ and $B \dashv B'$ (because the only rules we can apply to an abstraction are $(\alpha)$ and $(\gamma)$). By induction hypothesis, we have $(N/x)A \dashv (N'/x)A'$ and $(N/x)B \dashv (N'/x)B'$. Therefore, by $(\gamma)$,

$$ (N/x)M = \lambda y : ((N/x)A) (N/x)B \dashv \lambda y : ((N'/x)A') (N'/x)B' = (N'/x)M' $$

- if there exists terms $A$ and $B$ such that $M = \Pi y : A B$, then there exists terms $A'$ and $B'$ such that $M' = \Pi y : A' B'$ with $A \dashv A'$ and $B \dashv B'$ (because the only rules we can apply to an abstraction are $(\alpha)$ and $(\delta)$). By induction hypothesis, we have $(N/x)A \dashv (N'/x)A'$ and $(N/x)B \dashv (N'/x)B'$. Therefore, by $(\delta)$,

$$ (N/x)M = \Pi y : ((N/x)A) (N/x)B \dashv \Pi y : ((N'/x)A') (N'/x)B' = (N'/x)M' $$

- if there exists terms $P$ and $Q$ such that $M = P Q$, if the last rule of the derivation of $M \dashv M'$ is:

(α) then $M' = M = P Q$.

We have $P \dashv P$ and $Q \dashv Q$, then, by induction hypothesis, $(N/x)P \dashv (N'/x)P$ and $(N/x)Q \dashv (N'/x)Q$.

Therefore, by $(\theta_1)$,

$$ (N/x)M = (N/x)P (N/x)Q \dashv (N'/x)P (N'/x)Q = (N'/x)M' $$
(β) then there exists a rule $\langle s_1, s_2 \rangle$ such that $M = \varepsilon_{s_2} \dot{s}_1$ and $M' = U_{s_1}$.
Therefore, by (β), $(N/x)M = \varepsilon_{s_2} \dot{s}_1 \dashv\dashv U_{s_1} = (N'/x)M'$

(θ₁) then there exists terms P' and Q' such that $M' = P' Q'$ with $P \dashv\dashv P'$ and $Q \dashv\dashv Q'$. By induction hypothesis, we have $(N/x)P \dashv\dashv (N'/x)P'$ and $(N/x)Q \dashv\dashv (N'/x)Q'$. Therefore, by $(\theta_1)$, $(N/x)M = (N/x)P (N/x)Q \dashv\dashv (N'/x)P' (N'/x)Q' = (N'/x)M'$

(θ₂) then there exists terms A, B, B', Q' such that $P = \lambda y : A B$ and $M' = (Q'/y)B'$ with $B \dashv\dashv B'$ and $Q \dashv\dashv Q'$.

By induction hypothesis, we have $(N/x)B \dashv\dashv (N'/x)B'$ and $(N/x)Q \dashv\dashv (N'/x)Q'$. Therefore, by $(\theta_2)$,

$$ (N/x)M = (\lambda y : (N/x)A (N/x)B) (N/x)Q \dashv\dashv ((N'/x)Q'/y) (N'/x)B' \\ = (N'/x)((Q'/y)B') = (N'/x)M' $$

(η₁) then there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms A, A', B, B' such that $M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B)$ and $M' = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A' B')$, with $A \dashv\dashv A'$ and $B \dashv\dashv B'$.

By induction hypothesis, we have $(N/x)A \dashv\dashv (N'/x)A'$ and $(N/x)B \dashv\dashv (N'/x)B'$. Therefore, by $(\eta_1)$,

$$ (N/x)M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} (N/x)A (N/x)B) \dashv\dashv \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} (N'/x)A' (N'/x)B') \\ = (N'/x)M' $$

(η₂) then there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms A, A', B, B' such that $M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B)$ and $M' = \Pi y : (\varepsilon_{s_1} A') (\varepsilon_{s_2} (B' y))$, with $A \dashv\dashv A'$ and $B \dashv\dashv B'$.

By induction hypothesis, we have $(N/x)A \dashv\dashv (N'/x)A'$ and $(N/x)B \dashv\dashv (N'/x)B'$. Therefore, by $(\eta_2)$,

$$ (N/x)M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} (N/x)A (N/x)B) \dashv\dashv \Pi y : (\varepsilon_{s_1} (N'/x)A') (\varepsilon_{s_2} ((N'/x)B' y)) \\ = (N'/x)M' $$

Then, following [6], we associate, to each term $t$ of $\lambda\Pi_P$, a term $t^\dagger$, obtained by reducing in parallel all its $\beta R$-reduces.

**Definition 10.** Let $t$ be a term of $\lambda\Pi_P$. We define, by induction on the structure of $t$, the term $t^\dagger$ as follows:

$$ - x^\dagger = x, \quad Type^\dagger = Type, \quad Kind^\dagger = Kind $$

$$ - (\lambda x : A M)^\dagger = \lambda x : A^\dagger M^\dagger, \quad (\Pi x : A B)^\dagger = \Pi x : A^\dagger B^\dagger $$

$$ - ((\lambda x : A M) N)^\dagger = (N^\dagger/x) M^\dagger $$

$$ - (\varepsilon_{s_2} \dot{s}_1)^\dagger = U_{s_1}, \quad \text{if } \langle s_1, s_2 \rangle \in \mathcal{A}, $$

$$ - (\varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B))^\dagger = \Pi x : (\varepsilon_{s_1} A^\dagger) (\varepsilon_{s_2} (B^\dagger x)), \quad \text{if } \langle s_1, s_2, s_3 \rangle \in \mathcal{R}, $$

$$ - (M N)^\dagger = M^\dagger N^\dagger, \quad \text{otherwise.} $$

**Proposition 6.** If $M$ is a term of $\lambda\Pi_P$, then $M \dashv\dashv M^\dagger$

*Proof.* By induction on $M$.

- $x^\dagger = x$, $Type^\dagger = Type$, and $Kind^\dagger = Kind$, then by the rule $(\alpha)$, we have $x \dashv\dashv x^\dagger$, $Type \dashv\dashv Type^\dagger$ and $Kind \dashv\dashv Kind^\dagger$

- If we suppose, by induction hypothesis, $A \dashv\dashv A^\dagger$ and $N \dashv\dashv N^\dagger$, then, by the rule $(\gamma)$, $\lambda x : A N \dashv\dashv \lambda x : A^\dagger N^\dagger = (\lambda x : A N)^\dagger$
- If $A \dashrightarrow A^{\dagger}$ and $B \dashrightarrow B^{\dagger}$, then by the rule $(\delta)$,
$\Pi x : A B \dashrightarrow \Pi x : A^{\dagger} B^{\dagger} = (\Pi x : A B)^{\dagger}$

- If M is an application then we consider four cases.

★ If there exists an axiom $\langle s_1, s_2 \rangle$ such that $M = \varepsilon_{s_2} \dot{s}_1$, then, by the rule $(\beta)$, we have $\varepsilon_{s_2} \dot{s}_1 \dashrightarrow U_{s_1} = (\varepsilon_{s_2} \dot{s}_1)^{\dagger}$.

★ If there exists terms A, N and P such that $M = (\lambda x : A N) P$, and if we suppose, by induction hypothesis that $N \dashrightarrow N^{\dagger}$ and $P \dashrightarrow P^{\dagger}$, then by the rule $(\theta_2)$, we have $(\lambda x : A N) P \dashrightarrow (P^{\dagger}/x) N^{\dagger} = ((\lambda x : A N) P)^{\dagger}$.

★ If there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms A and B such that
$M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B)$, and if we suppose, by induction hypothesis
that $A \dashrightarrow A^{\dagger}$ and $B \dashrightarrow B^{\dagger}$, then by the rule $(\eta_2)$, we have
$\varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B) \dashrightarrow \Pi x : (\varepsilon_{s_1} A^{\dagger}) (\varepsilon_{s_2} (B^{\dagger} x)) = (\varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B))^{\dagger}$.

★ Otherwise, if there exists terms N and P such that $M = N P$, and if we suppose, by induction hypothesis, that $N \dashrightarrow N^{\dagger}$ and $P \dashrightarrow P^{\dagger}$, then by the rule $(\theta_1)$ we have $N P \dashrightarrow N^{\dagger} P^{\dagger} = (N P)^{\dagger}$.

**Proposition 7.** For all terms $M$ and $M'$ of $\lambda\Pi_P$, if $M \dashrightarrow M'$ then $M' \dashrightarrow M^{\dagger}$

*Proof.* By induction on the last rule of the derivation of $M \dashrightarrow M'$.
If the last rule is:

(α) then $M' = M$. By Proposition 6 we have $M \dashrightarrow M^{\dagger}$

(β) then there exists a rule $\langle s_1, s_2 \rangle$ such that $M = \varepsilon_{s_2} \dot{s}_1$ and $M' = U_{s_1}$. Therefore $M' \dashrightarrow U_{s_1} = M^{\dagger}$ by the rule (α).

(γ) then there exists terms A, $A'$, P and $P'$ such that $M = \lambda x : A P$ and $M' = \lambda x : A' P'$ with $A \dashrightarrow A'$ and $P \dashrightarrow P'$. By induction hypothesis, we have $A' \dashrightarrow A^{\dagger}$ and $P' \dashrightarrow P^{\dagger}$, then, by the rule (γ),
$M' = \lambda x : A' P' \dashrightarrow \lambda x : A^{\dagger} P^{\dagger} = M^{\dagger}$

(δ) then there exists terms A, $A'$, B and $B'$ such that $M = \Pi x : A B$ and $M' = \Pi x : A' B'$ with $A \dashrightarrow A'$ and $B \dashrightarrow B'$. By induction hypothesis, we have $A' \dashrightarrow A^{\dagger}$ and $B' \dashrightarrow B^{\dagger}$, then, by the rule (δ),
$M' = \Pi x : A' B' \dashrightarrow \Pi x : A^{\dagger} B^{\dagger} = M^{\dagger}$

$(\theta_1)$ then there exists terms $P, P', Q$ and $Q'$ such that $M = P Q$ and $M' = P' Q'$ with $P \dashrightarrow P'$ and $Q \dashrightarrow Q'$.

★ If there exists terms A and B such that $P = \lambda x : A B$, then there exists terms $A'$ and $B'$ such that $P' = \lambda x : A' B'$ with $A \dashrightarrow A'$ and $B \dashrightarrow B'$ (because the only rules we can apply to an abstraction are $(\alpha)$ and $(\gamma)$). Therefore, by induction hypothesis, $B' \dashrightarrow B^{\dagger}$ and $Q' \dashrightarrow Q^{\dagger}$.
And, by $(\theta_2)$,
$M' = P' Q' = (\lambda x : A' B') Q' \dashrightarrow (Q^{\dagger}/x) B^{\dagger} = ((\lambda x : A B) Q)^{\dagger} = M^{\dagger}$

★ If there exists a axiom $\langle s_1, s_2 \rangle$ such that $P = \varepsilon_{s_2}$ and $Q = \dot{s}_1$, then $P' = P$ and $Q' = Q$ (because the only rules we can apply to $(\varepsilon_{s_2} \dot{s}_1)$ are $(\alpha)$, $(\beta)$ and $(\theta_1$ with $(\alpha)$ on both premises)).
And, by $(\beta)$, $M' = (\varepsilon_{s_2} \dot{s}_1) \dashrightarrow U_{s_1} = M^{\dagger}$
★ If there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms $A, B$, such that $P = \varepsilon_{s_3}$ and $Q = \dot{H}_{\langle s_1, s_2, s_3 \rangle} A B$, then $P' = P = \varepsilon_{s_3}$ (because the only rule we can apply is $(\alpha)$), and there exists terms $A'$ and $B'$ such that $Q' = \dot{H}_{\langle s_1, s_2, s_3 \rangle} A' B'$ with $A \dashrightarrow A'$ and $B \dashrightarrow B'$ (because the only rule we can apply is $(\theta_1)$).

Therefore, by induction hypothesis, $A' \dashrightarrow A^\dagger$ and $B' \dashrightarrow B^\dagger$.

And, by $(\eta_2)$,

$$M' = \varepsilon_{s_3} (\dot{H}_{\langle s_1, s_2, s_3 \rangle} A' B') \dashrightarrow \Pi x : (\varepsilon_{s_1} A^\dagger)(\varepsilon_{s_2} (B^\dagger x)) = M^\dagger$$

★ Otherwise, $(PQ)^\dagger = P^\dagger Q^\dagger$. We have, by induction hypothesis, $P' \dashrightarrow P^\dagger$ and $Q' \dashrightarrow Q^\dagger$. Therefore, by $(\theta_1)$, $M' = P' Q' \dashrightarrow P^\dagger Q^\dagger = M^\dagger$.

(θ₂) then there exists terms $A, B, B', Q, Q'$ such that $M = (\lambda x : A B) Q$ and $M' = (Q'/x)B'$ with $B \dashrightarrow B'$ and $Q \dashrightarrow Q'$.

By induction hypothesis, we have $B' \dashrightarrow B^\dagger$ and $Q' \dashrightarrow Q^\dagger$.

Therefore, by Proposition 5, $M' = (Q'/x)B' \dashrightarrow (Q^\dagger/x)B^\dagger = M^\dagger$

(η₁) then there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms $A, B$ such that
$M = \varepsilon_{s_3} (\dot{H}_{\langle s_1, s_2, s_3 \rangle} A B)$ and $M' = \varepsilon_{s_3} (\dot{H}_{\langle s_1, s_2, s_3 \rangle} A' B')$
with $A \dashrightarrow A'$ and $B \dashrightarrow B'$.

By induction hypothesis, we have $A' \dashrightarrow A^\dagger$ and $B' \dashrightarrow B^\dagger$.

Therefore, by $(\eta_2)$,

$$M' = \varepsilon_{s_3} (\dot{H}_{\langle s_1, s_2, s_3 \rangle} A' B') \dashrightarrow \Pi x : (\varepsilon_{s_1} A^\dagger)(\varepsilon_{s_2} (B^\dagger x)) = M^\dagger.$$

(η₂) then there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms $A, B$ such that
$M = \varepsilon_{s_3} (\dot{H}_{\langle s_1, s_2, s_3 \rangle} A B)$ and $M' = \Pi x : (\varepsilon_{s_1} A') (\varepsilon_{s_2} (B'x))$
with $A \dashrightarrow A'$ and $B \dashrightarrow B'$.

By induction hypothesis, we have $A' \dashrightarrow A^\dagger$ and $B' \dashrightarrow B^\dagger$.

Therefore, by $(\alpha)$, $(\delta)$ and $(\eta_1)$,

$$M' = \Pi x : (\varepsilon_{s_1} A') (\varepsilon_{s_2} (B'x)) \dashrightarrow \Pi x : (\varepsilon_{s_1} A^\dagger) (\varepsilon_{s_2} (B^\dagger x)) = M^\dagger.$$

**Proposition 8.** The relation $\dashrightarrow$ is strongly confluent in $\lambda\Pi_P$, i.e. for all $M$, $M'$ and $M''$, if $M \dashrightarrow M'$ and $M \dashrightarrow M''$ then there exists a term $N$ such that $M' \dashrightarrow N$ and $M'' \dashrightarrow N$.

*Proof.* By Proposition 7, $M' \dashrightarrow M^\dagger$ and $M'' \dashrightarrow M^\dagger$.

**Proposition 9.** For all terms $M$ and $M'$ of $\lambda\Pi_P$,

1. if $M \rightarrow M'$ then $M \dashrightarrow M'$

2. if $M \dashrightarrow M'$ then $M \rightarrow^* M'$

3. $M \dashrightarrow^* M'$ if and only if $M \rightarrow^* M'$ (i.e. $\dashrightarrow^* = \rightarrow^*$).

*Proof.*

1. If $M \rightarrow M'$, then $M \rightarrow_{\beta} M'$ or $M \rightarrow_{\mathcal{R}} M'$

★ If $M \rightarrow_{\beta} M'$ then $M \dashrightarrow M'$, by $(\theta_2)$ and $(\alpha)$

★ If $M \rightarrow_{\mathcal{R}} M'$ then $M \dashrightarrow M'$, by $(\beta)$, or $(\eta_2)$ and $(\alpha)$

2. By induction on the last rule of the derivation of $M \dashrightarrow M'$.

If the last rule is:

(α) then $M' = M$, and we have $M \rightarrow^* M$.
(β) then there exists a rule $\langle s_1, s_2 \rangle$ such that $M = \varepsilon_{s_2} \dot{s}_1$ and $M' = U_{s_1}$, and
we have $\varepsilon_{s_2} \dot{s}_1 \to_R U_{s_1}$, therefore $M \to^* M'$.

(γ) then there exists terms $A, A', P$ and $P'$ such that $M = \lambda x : A P$,
$M' = \lambda x : A' P'$ with $A \dashv\vdash A'$ and $P \dashv\vdash P'$.
By induction hypothesis, we have $A \to^* A'$ and $P \to^* P'$,
therefore $M = \lambda x : A P \to^* \lambda x : A' P' = M'$.

(δ) then there exists terms $A, A', B$ and $B'$ such that $M = \Pi x : A B$,
$M' = \Pi x : A' B'$ with $A \dashv\vdash A'$ and $B \dashv\vdash B'$.
By induction hypothesis, we have $A \to^* A'$ and $B \to^* B'$,
therefore $M = \Pi x : A B \to^* \Pi x : A' B' = M'$.

(θ₁) then there exists terms $P, P', Q$ and $Q'$ such that $M = P Q$ and
$M' = P' Q'$ with $P \dashv\vdash P'$ and $Q \dashv\vdash Q'$.
By induction hypothesis, we have $P \to^* P'$ and $Q \to^* Q'$,
therefore $M = P Q \to^* P' Q' = M'$

(θ₂) then there exists terms $A, B, B', Q, Q'$ such that $M = (\lambda x : A B) Q$
and $M' = (Q'/x)B'$ with $B \dashv\vdash B'$ and $Q \dashv\vdash Q'$.
By induction hypothesis, we have $B \to^* B'$ and $Q \to^* Q'$,
therefore $M = (\lambda x : A B) Q \to^* (\lambda x : A B') Q' \to_\beta (Q'/x)B' = M'$.

(η₁) then there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms $A, B$ such that
$M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B)$ and $M' = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A' B')$
with $A \dashv\vdash A'$ and $B \dashv\vdash B'$.
By induction hypothesis, we have $A \to^* A'$ and $B \to^* B'$,
therefore $M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B) \to^* \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A' B') = M'$.

(η₂) then there exists a rule $\langle s_1, s_2, s_3 \rangle$ and terms $A, B$ such that
$M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B)$ and $M' = \Pi x : (\varepsilon_{s_1} A') (\varepsilon_{s_2} (B'x))$
with $A \dashv\vdash A'$ and $B \dashv\vdash B'$.
By induction hypothesis, we have $A \to^* A'$ and $B \to^* B'$, therefore
$M = \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A B) \to^* \varepsilon_{s_3} (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} A' B')$
$\to_R \Pi x : (\varepsilon_{s_1} A') (\varepsilon_{s_2} (B'x)) = M'$.

3. By induction on the number of reductions in $M \to^* M'$ and the first point, for one way. And by induction on the length of the derivation of $M \dashv\vdash M'$ and the second point for the other way.

**Proposition 10.** The relation $\to$ is confluent in $\lambda\Pi_P$, i.e. for all $M, M'$ and $M'', if $M \to^* M'$ and $M \to^* M''$ then there exists a term $N$ such that $M' \to^* N$ and $M'' \to^* N$.

*Proof.* From Proposition 8 the relation $\dashv\vdash$ is strongly confluent, hence it is confluent. Hence, by Proposition 9 the relation $\to$ is confluent.

# 5 Conservativity

Let $P$ be a functional Pure Type System. We could attempt to prove that if the type $\|A\|$ is inhabited in $\lambda\Pi_P$, then $A$ is inhabited in $P$, and more precisely
that if $\Gamma$ is a context and $A$ a term in $P$ and $t$ a term in $\lambda\Pi_P$, such that
$\|\Gamma\| \vdash t : \|A\|$, then there exists a term $u$ of $P$ such that $|u| = t$ and $\Gamma \vdash u : A$.
Unfortunately this property does not hold in general as shown by the following
counterexamples.

*Example 4.* If *P* is the simply-typed lambda-calculus, then the polymorphic identity is not well-typed in *P*, in particular:

nat : Type $\nvdash$ (($\lambda X : Type \ \lambda x : X \ x$) nat) : (nat $\Rightarrow$ nat)
however, in $\lambda\Pi$, we have

nat : $\|Type\| \vdash ((\lambda X : \|Type\| \ \lambda x : \|X\| \ x) |nat|) : \|nat \Rightarrow nat\|$.

*Example 5.* If $\langle s_1, s_2, s_3 \rangle \in R$, $\Sigma_P \vdash \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} : \|\Pi X : s_1 : ((X \Rightarrow s_2) \Rightarrow s_3)\|$ but the term $\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle}$ is not the translation of any term of P.

Therefore, we shall prove a slightly weaker property: that if the type $\|A\|$ is inhabited by a normal term in $\lambda\Pi_P$, then $A$ is inhabited in $P$. Notice that this restriction vanishes if $\lambda\Pi_P$ is terminating.

We shall prove, in a first step, that if $\|\Gamma\| \vdash t : \|A\|$, and $t$ is a weak $\eta$-long normal term then there exists a term in $u$ such that such that $|u| = t$ and $\Gamma \vdash u : A$. Then we shall get rid of this restriction on weak $\eta$-long forms.

**Definition 11.** A term $t$ of $\lambda\Pi_P$ is a weak $\eta$-long term if and only if each occurrence of $\dot{\Pi}_{\langle s_1,s_2,s_3 \rangle}$ in $t$, is in a subterm of the form $(\dot{\Pi}_{\langle s_1,s_2,s_3 \rangle} t_1 t_2)$ (i.e. each occurrence of $\dot{\Pi}_{\langle s_1,s_2,s_3 \rangle}$ is $\eta$-expanded).

**Definition 12 (Back translation).** We suppose that $P$ contains at least one sort: $s_0$. Then we define a translation from $\lambda\Pi_P$ to $P$ as follows:

$$ - x^* = x, \quad s^* = s_0 \quad \dot{s}^* = s, \quad U_s^* = s, $$

$$ - (\Pi x : A B)^* = \Pi x : A^* B^*, $$

$$ - (\lambda x : A t)^* = \lambda x : A^* t^*, $$

$$ - (\dot{\Pi}_{\langle s_1,s_2,s_3 \rangle} A B)^* = \Pi x : A^* (B^* x), $$

$$ - (\epsilon_s u)^* = u^*, $$

$$ - (t u)^* = t^* u^* \text{ otherwise.} $$

**Proposition 11.** The back translation $(.)^*$ is a right inverse of $|\cdot|$ and $\|\cdot\|$ i.e. for all $t$ such that $|t|$ (resp. $\|t\|$) is well defined, $|t|^* = t$ (resp. $\|t\|^* = t$).

*Proof.* By induction on the structure of $t$.

**Proposition 12.** For all $t$, $u$ terms and $x$ variable of $\lambda\Pi_P$,

$$ 1. ((u/x)t)^* = (u^*/x)t^* $$

$$ 2. \text{ If } t \rightarrow u \text{ then } t^* \rightarrow_{\beta} u^* \text{ in } P. $$

*Proof.* 1. By induction on $t$.

$$ 2. \text{ If } t \rightarrow_{\beta} u \text{ then } t^* \rightarrow_{\beta} u^*, \text{ and if } t \rightarrow_{\mathbb{R}} u, \text{ then } t^* = u^*. $$
**Proposition 13.** For all terms A, B of P and C, D of $\lambda\Pi_P$ (such that $\|A\|$ and $\|B\|$ are well defined),

1. If $A \equiv_{\beta} B$, then $\|A\| \equiv \|B\|$.

2. If $C \equiv D$, then $C^* \equiv_{\beta} D^*$.

3. If $\|A\| \equiv \|B\|$, then $A \equiv_{\beta} B$.

*Proof.* 1. By induction on the length of the path of $\beta$-reductions and $\beta$-expansions between A and B, and by Proposition 1.

2. By the same reasoning as for the first point, using Proposition 12.

3. By the first and second points and Proposition 11.

**Proposition 14 (Conservativity).** If there exists a context $\Gamma$, a term $A$ of $P$, and a term $t$, in weak $\eta$-long normal form, of $\lambda\Pi_P$, such that $\|\Gamma\| \vdash t : \|A\|$, Then there exists a term $u$ of $P$ such that $|u| \equiv t$ and $\Gamma \vdash u : A$.

*Proof.* By induction on $t$.

* If $t$ is a well-typed product or sort, then it cannot be typed by a translated type (by confluence of $\lambda\Pi_P$).

* If $t = \lambda x : B t'$. The term $t$ is well typed, thus there exists a term $C$ of $\lambda\Pi_P$, such that $\|\Gamma\| \vdash t : \Pi x : B C (\alpha_0)$.

Therefore $\|A\| \equiv \Pi x : B C (\alpha_1)$, and $A \equiv \|A\|^* \equiv (\Pi x : B C)^* = \Pi x : B^* C^* (\alpha_2)$.

$\|A\|$ is well defined, and $A$ cannot be a sort by $(\alpha_2)$ and confluence of $\lambda\Pi_P$, then $A$ is well-typed.

Therefore, by $(\alpha_2)$, confluence of $\lambda\Pi_P$ and subject-reduction of $\rightarrow_{\beta}$, there exists terms $B^\sharp$ and $C^\sharp$ and sorts $s_{B^\sharp}$, $s_{C^\sharp}$, $s_3$ of $P$, such that both $A$ and $\Pi x : B^* C^*$ reduce to $\Pi x : B^\sharp C^\sharp (\beta)$, with $\Gamma \vdash B^\sharp : s_{B^\sharp}$, and $\Gamma, B^\sharp : s_{B^\sharp} \vdash C^\sharp : s_{C^\sharp}$ where $\langle s_{B^\sharp}, s_{C^\sharp}, s_3 \rangle$ is a rule of $P$.

In particular, $\|B^\sharp\|$, $\|C^\sharp\|$ and $\|\Pi x : B^\sharp C^\sharp\|$ are well defined.

Moreover, $A \equiv \Pi x : B^\sharp C^\sharp$ by $(\beta)$, then, by Propositions 13 and 2, $\|A\| \equiv \|\Pi x : B^\sharp C^\sharp\| \equiv \Pi x : \|B^\sharp\| \|C^\sharp\|$.

Therefore $\Pi x : B C \equiv \Pi x : \|B^\sharp\| \|C^\sharp\|$ by $(\alpha_1)$, and by confluence of $\lambda\Pi_P$, we have $B \equiv \|B^\sharp\| (\gamma_0)$.

Then, by $(\alpha_0)$, $\|\Gamma\| \vdash t : \Pi x : \|B^\sharp\| \|C^\sharp\|$ and $\|\Gamma\|$, $x : \|B^\sharp\| \vdash t' : \|C^\sharp\|$.

The term $\lambda x : B t'$ is in weak $\eta$-long normal form, thus $t'$ is also in weak $\eta$-long normal form, and, by induction hypothesis, there exists a term $u'$ of $P$, such that $|u'| \equiv t' (\gamma_1)$ and $\Gamma, x : B^\sharp \vdash u' : C^\sharp (\gamma_2)$.

Let $u = \lambda x : B^\sharp u'$.

By $(\gamma_2)$, we have $\Gamma \vdash u : \Pi x : B^\sharp C^\sharp$, and $\Gamma \vdash u : A$ by $(\beta)$.

And $|u| = |\lambda x : B^\sharp u'| = \lambda x : \|B^\sharp\| |u'| \equiv \lambda x : B t' = t$ by $(\gamma_0)$ and $(\gamma_2)$.

* If $t$ is an application or a variable, as it is normal, it has the form $x t_1 ... t_n$ for some variable $x$ and terms $t_1, ..., t_n$. We have $\|\Gamma\| \vdash x t_1 ... t_n : \|A\|$ ($\alpha_0$). $\negrightarrow$ If $x$ is a variable of the context $\Sigma_P$,

* If $x = s_1$ (where $\langle s_1, s_2 \rangle$ is an axiom of $P$), then $n = 0$ (because $t$ is well typed) and $\|A\| = U_{s_2}$.

We have $\vdash s_1 : s_2$ in $P$, therefore $\Gamma \vdash s_1 : s_2$.
* If $x = U_s$ (where $s$ is a sort of $P$), then $n = 0$ and $\|A\| \equiv \text{Type}$. That's an absurdity by confluence of $\lambda\Pi_P$.

* If $x = \varepsilon_s$ (where $s$ is a sort of $P$), then, as $t$ is well typed $n \le 1$.

★ If $n = 1$, then $\|\Gamma\| \vdash t_1 : U_s$, and $\|A\| \equiv \text{Type}$ (absurdity).

★ If $n = 0$, then $\|A\| \equiv U_s \Rightarrow \text{Type}$, thus by Propositions 13 and 2,

$$ U_s \Rightarrow \text{Type} \equiv \|(U_s \Rightarrow \text{Type})^*\| = \|s \Rightarrow s_0\| \equiv \|s\| \Rightarrow \|s_0\|. $$
Therefore $\text{Type} \equiv \|s_0\|$ (absurdity).

* If $x = \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle}$ (where $\langle s_1, s_2, s_3 \rangle$ is a rule of $P$), then as $t$ is well-typed and in weak $\eta$-long form, $n = 2$. We have $\|A\| \equiv U_{s_3}$ thus $A \equiv s_3$ by Proposition 13.

And $\|\Gamma\| \vdash t_1 : U_{s_1}$ i.e. $\|\Gamma\| \vdash t_1 : \|s_1\|$.

And $\|\Gamma\|, t_1 : U_{s_1} \vdash t_2 : ((\varepsilon_{s_1} t_1) \Rightarrow U_{s_2})$ ($\alpha_1$)

$t_1$ is also in weak $\eta$-long normal form, then, by induction hypothesis, there exists a term $u_1$ of $P$ such that:

$$ |u_1| \equiv t_1 \quad \text{and} \quad \Gamma \vdash u_1 : s_1 \quad (\beta_1) $$

Then, by $(\alpha_1)$, $\|\Gamma\|, t_1 : \|s_1\| \vdash t_2 : \|u_1 \Rightarrow s_2\|$.

In particular, $\|\Gamma\|, t_1 : \|s_1\| \vdash t_2 : \|u_1\| \Rightarrow \|s_2\|$.

However $t_2$ is also in weak $\eta$-long normal form, then there exists a term $t'_2$ (in weak $\eta$-long normal form) of $\lambda\Pi_P$ such that

$$ t_2 = \lambda x : \|u_1\| \quad t'_2 \quad \text{and} \quad \|\Gamma\|, x : \|u_1\| \vdash t'_2 : \|s_2\| $$

By induction hypothesis, there exists a term $u'_2$ of $P$, such that

$$ |u'_2| \equiv t'_2 \quad \text{and} \quad \Gamma, x : u_1 \vdash u'_2 : s_2 \quad (\beta_2) $$

Then we choose $u = \Pi x : u_1 u'_2$ that verifies $\Gamma \vdash u : s_3$, by $(\beta_1)$, $(\beta_2)$, and the fact that $\langle s_1, s_2, s_3 \rangle$ is a rule of $P$. And, finally,

$$ |u| = \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} |u_1| \quad (\lambda x : (\varepsilon_{s_1} |u_1|) |u'_2| \equiv \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} t_1 t_2 = t $$

If $x$ is a variable of the context $\Gamma$,

For $k \in \{0, \dots, n\}$, let $(H_k)$ be the statement:

There exists a term $T_k$ of $P$, such that $\|\Gamma\| \vdash x t_1 \dots t_k : \|T_k\|$.

We first prove $(H_0), \dots, (H_n)$ by induction.

★ $k = 0 : x$ is a variable of the context $\Gamma$, then there exists a well typed term or a sort $T$ in $P$ such that $\Gamma$ contains $x : T$. Therefore $\|\Gamma\|$ contains $x : \|T\|$.

★ $0 \le k \le n - 1$ : We suppose $(H_k)$.

$x t_1 \dots t_{k+1}$ is well typed in $\Gamma$, then there exists terms $D$ and $E$ of $\lambda\Pi_P$ such that:

$$ \|\Gamma\| \vdash t_{k+1} : D \quad (\delta_1) , \quad \|\Gamma\| \vdash x t_1 \dots t_k : \Pi y : D E \quad (\delta_2), \text{ and} $$

$$ \|\Gamma\| \vdash x t_1 \dots t_{k+1} : (t_{k+1}/y)E \quad (\delta_3). $$

However, by $(H_k)$, there exists $T_k$, such that $\|\Gamma\| \vdash x t_1 \dots t_k : \|T_k\|$, therefore $\|T_k\| \equiv \Pi y : D E (\delta_4)$, by $(\delta_2)$, and $T_k \equiv \Pi y : D^* E^* (\delta_5)$, by Propositions 11 and 13.

$\|T_k\|$ is well defined and $T_k$ can't be a sort by $(\delta_5)$ then $T_k$ is well typed. Then, by $(\delta_5)$, confluence of $\lambda\Pi_P$ and subject-reduction of $\rightarrow\beta$, there exists terms $D^\sharp$ and $E^\sharp$ and sorts $s_{D^\sharp}, s_{E^\sharp}, s_3$ of $P$, such that both $T_k$ and $\Pi x : D^* E^*$ reduce to $\Pi x : D^\sharp E^\sharp (\delta_6)$, with
$\Gamma \vdash D^\sharp : s_{D^\sharp}$, and $\Gamma, D^\sharp : s_{D^\sharp} \vdash E^\sharp : s_{E^\sharp}$ where $\langle s_{D^\sharp}, s_{E^\sharp}, s_3 \rangle$ is a
rule of $P$.

In particular, $\|D^\sharp\|$, $\|E^\sharp\|$ and $\|\Pi x : D^\sharp E^\sharp\|$ are well defined.

Moreover, $T_k \equiv \Pi x : D^\sharp E^\sharp$ by $(\delta_6)$, then, by Propositions 13 and 2,
$\|T_k\| \equiv \|\Pi x : D^\sharp E^\sharp\| \equiv \Pi x : \|D^\sharp\| \|E^\sharp\|$.

In particular, $E \equiv \|E^\sharp\|$, by $(\delta_4)$ and confluence of $\lambda\Pi_P$.

Moreover, $t_{k+1}$ is in weak $\eta$-long form, then by induction hypothesis,
there exists a term $u_{k+1}$ of $P$ such that $|u_{k+1}| \equiv t_{k+1}$.

Finally, $(t_{k+1}/y)E \equiv (|u_{k+1}|/y)E \equiv (|u_{k+1}|/y)\|E^\sharp\| \equiv \|(u_{k+1}/y)E^\sharp\|.$
And we conclude, by $(\delta_3)$ and the conversion rule of $\lambda\Pi_P$.

Then, if $n=0$, we take $u=x$ and $\Gamma$ contains $x:T$ with $\|T\| \equiv \|A\|$.

And, if $n > 0$, then, by $(\alpha_0)$, there exists terms $B$ and $C$ of $\lambda\Pi_P$ such
that $\|\Gamma\| \vdash t_n : B(\theta_1)$ and $\|\Gamma\| \vdash x t_1 \dots t_{n-1} : \Pi y : B C(\theta_2)$ with
$\|A\| \equiv (t_n/y)C(\theta_3)$.

By $(H_{n-1})$, there exists $T_{n-1}$, such that $\|\Gamma\| \vdash x t_1 \dots t_{n-1} : \|T_{n-1}\|$,
therefore $\|T_{n-1}\| \equiv \Pi y : B C$ by $(\theta_2)$, and $T_{n-1} \equiv \Pi y : B^* C^*(\theta_4)$.

$\|T_{n-1}\|$ is well defined, and $T_{n-1}$ cannot be a sort by $(\theta_4)$, then $T_{n-1}$ is
well-typed.

Therefore, by $(\theta_2)$, confluence of $\lambda\Pi_P$ and subject-reduction of $\to_\beta$,
there exists terms $B^\sharp$ and $C^\sharp$ and sorts $s_{B^\sharp}, s_{C^\sharp}, s_3$ of $P$, such that both
$T_{n-1}$ and $\Pi x : B^* C^*$ reduce to $\Pi x : B^\sharp C^\sharp (\mu_0)$, with $\Gamma \vdash B^\sharp : s_{B^\sharp}$,
and $\Gamma, B^\sharp : s_{B^\sharp} \vdash C^\sharp : s_{C^\sharp}$ where $\langle s_{B^\sharp}, s_{C^\sharp}, s_3 \rangle$ is a rule of $P$.

In particular, $\|B^\sharp\|$, $\|C^\sharp\|$ and $\|\Pi x : B^\sharp C^\sharp\|$ are well defined.

Moreover, $T_{n-1} \equiv \Pi x : B^\sharp C^\sharp$ by $(\mu_0)$, then, by Propositions 13 and 2,
$\|T_{n-1}\| \equiv \|\Pi x : B^\sharp C^\sharp\| \equiv \Pi x : \|B^\sharp\| \|C^\sharp\|$.

Therefore $\Pi x : B C \equiv \Pi x : \|B^\sharp\| \|C^\sharp\|$, and by confluence of $\lambda\Pi_P$, we
have $B \equiv \|B^\sharp\| (\gamma_0)$.

Thus, $\|\Gamma\| \vdash t_n : \|B^\sharp\|$ and $\|\Gamma\| \vdash x t_1 \dots t_{n-1} : \|\Pi y : B^\sharp C^\sharp\|$.

$t_n$ and $x t_1 \dots t_{n-1}$ are both in weak $\eta$-long normal form, then, by
induction hypothesis, there exists terms $w_1$ and $w_2$ of $P$ such that:

$|w_1| \equiv x t_1 \dots t_{n-1}$ and $\Gamma \vdash w_1 : \Pi y : B^\sharp C^\sharp$

$|w_2| \equiv t_n$ and $\Gamma \vdash w_2 : B^\sharp$

Let $u = w_1 w_2$, we have:

$|u| = |w_1| |w_2| \equiv x t_1 \dots t_{n-1} t_n$ and $\Gamma \vdash u : (w_2/y)C^\sharp$.

However, by $(\theta_3)$, Proposition 13 and the fact that $C^* \equiv C^\sharp$, we have:
$A \equiv (t_n^*/y)C^* \equiv (w_2/y)C^* \equiv (w_2/y)C^\sharp$, and, finally, $\Gamma \vdash u : A$.

Finally, we get rid of the weak $\eta$-long form restriction with the following
Propositions.

**Proposition 15.** For all terms $A$, $B$ of $\lambda\Pi_P$, and for all well typed term or sort $C$ of $P$,

1. If $A \to B$ then $A^* \to^* B$

2. If $A \equiv B$ then $A^* \equiv B$

3. If $A$ is in weak $\eta$-long form, then $A \xrightarrow{\beta}^* A$, in particular $A \equiv A$
4. $||C|| \equiv ||C||$

5. If $A \equiv ||C||$ then $A'' \equiv A$

*Proof.* 1. If $A \to_{\beta} B$, then $A'' \to_{\beta} B''$ (by induction on $A$).
If $A \to_{\mathcal{R}} B$,

- for all axiom $\langle s_1, s_2 \rangle$, $(\varepsilon_{s_2}(\dot{s}_1))'' = \varepsilon_{s_2}(\dot{s}_1) \to_{\mathcal{R}} U_{s_1} = (U_{s_1})''$.

- for all rule $\langle s_1, s_2, s_3 \rangle$, $(\varepsilon_{s_3}(\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} C D))'' =$
$\varepsilon_{s_3}((\lambda x : U_{s_1} \lambda y : ((\varepsilon_{s_1} x) \Rightarrow U_{s_2}) (\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} x y))C'' D'')$
$\to_{\beta}^2 \varepsilon_{s_3}(\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} C'' D'') \to_{\mathcal{R}} \Pi x : (\varepsilon_{s_1} C'') (\varepsilon_{s_2} (D'' x))$
$= \Pi x : (\varepsilon_{s_1} C'') (\varepsilon_{s_2} (D x))''$

2. By induction on the number of derivations and expansions from $A$ to $B$.

3. By induction on $A$, remarking that $(\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} t_1 t_2)'' \to_{\beta}^2 \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} t_1'' t_2''$.

4. A translated term $||C||$ is in weak $\eta$-long form.

5. If $A \equiv ||C||$ then $A'' \equiv ||C||'' \equiv ||C||$, by the second and fourth points.

**Proposition 16.** Let $t$ be a normal term of $\lambda\Pi_P$,

$$ \text{if } \|\Gamma\| \vdash t : \|A\| \text{ then } \|\Gamma\| \vdash t'' : \|A\| $$

*Proof.* By induction on $t$.

* If $t$ is a well-typed product or sort, then it cannot be typed by a translated type (by confluence of $\lambda\Pi_P$).

* If $t = \lambda x : B u$, then there exists a term $C$ of $\lambda\Pi_P$, such that
$||A|| \equiv \Pi x : B C (\alpha)$, with $\Gamma, x : B \vdash u : C$.

By $(\alpha)$, we have $B \equiv ||B^*|| (\beta)$ and $C \equiv ||C^*||$. Thus $\Gamma, x : ||B^*|| \vdash u : ||C^*||$. Then, by induction hypothesis, we have $\Gamma, x : ||B^*|| \vdash u'' : ||C^*||$, therefore $\Gamma \vdash \lambda x : ||B^*|| u'' : \Pi x : ||B^*|| ||C^*|| \equiv ||A||$ thus $\Gamma \vdash \lambda x : B u'' : ||A||$, by $(\beta)$. Finally, by $(\beta)$ and the Proposition 15.5, $\lambda x : B u'' \equiv \lambda x : B'' u''$, therefore, by subject reduction, $\Gamma \vdash t'' = \lambda x : B'' u'' : ||A||$

* If $t$ is an application or a variable, as it is normal, it has the form $x t_1 ... t_n$ for some variable $x$ and terms $t_1, ..., t_n$. We have $\|\Gamma\| \vdash x t_1 ... t_n : ||A||$ ($\alpha_0$).
  $\neg\neg$ If $x$ is a variable of the context $\Sigma_P$,

* If $x = \dot{s}_1$ (where $\langle s_1, s_2 \rangle$ is an axiom of $P$), then $n = 0$ (because $t$ is well typed) and we have $(\dot{s}_1)'' = \dot{s}_1$.

* If $x = U_s$ (where $s$ is a sort of $P$), then $n = 0$ and $||A|| \equiv \text{Type}$. That's an absurdity by confluence of $\lambda\Pi_P$.

* If $x = \varepsilon_s$ (where $s$ is a sort of $P$), then, as $t$ is well-typed $n \le 1$.

★ If $n = 1$, then $\|\Gamma\| \vdash t_1 : U_s$, and $\|A\| \equiv \text{Type}$ (absurdity).

★ If $n = 0$, we have $(\varepsilon_s)'' = \varepsilon_s$

* If $x = \dot{\Pi}_{\langle s_1, s_2, s_3 \rangle}$ (where $\langle s_1, s_2, s_3 \rangle$ is a rule of $P$), then as $t$ is well-typed, $n \le 2$. Moreover, $\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle}$, $(\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} t_1)$, and $(\dot{\Pi}_{\langle s_1, s_2, s_3 \rangle} t_1 t_2)$ have the same types than their weak $\eta$-long forms.

$\neg\neg$ If $x$ is a variable of the context $\Gamma$,

* If $n = 0$, we have $x'' = x$.
* If $n > 0$, then there exists terms $B$ and $C$ of $\lambda\Pi_P$ such that
  $$ \|\Gamma\| \vdash t_n : B \text{ (}\alpha_1\text{)} \text{ and } \|\Gamma\| \vdash x t_1 \dots t_{n-1} : \Pi y : B C \text{ (}\alpha_2\text{)} \text{ with} $$
  $$ \|A\| \equiv (t_n/y)C \text{ (}\alpha_3\text{)} . \text{ As in the proof of Proposition 14, we can type} $$
  $$ x t_1 \dots t_{n-1} \text{ by a translated type, then } \Pi y : B C \equiv \Pi y : \|B^*\| \|C^*\| . $$
  In particular, $B \equiv \|B^*\|$ and $C \equiv \|C^*\|$.
  Thus, $\|\Gamma\| \vdash t_n : \|B^*\|$ and $\|\Gamma\| \vdash x t_1 \dots t_{n-1} : \|\Pi y : B^* C^*\|$.
  By induction hypothesis, we have $\|\Gamma\| \vdash t_n'' : \|B^*\|$ and
  $$ \|\Gamma\| \vdash x t_1'' \dots t_{n-1}'' : \Pi y : \|B^*\| \|C^*\| . \text{ Finally, by (}\alpha_3\text{)} and Proposition 15.5, } $$
  $$ \|\Gamma\| \vdash t'' = x t_1'' \dots t_n'' : (t_n''/y)C \equiv \|A\|. $$

**Theorem 1.** Let $P$ be a functional Pure Type System, such that $\lambda\Pi_P$ is terminating. The type $\|A\|$ is inhabited by a closed term in $\lambda\Pi_P$ if and only if the type $A$ is inhabited by a closed term in $P$.

*Proof.* If $A$ has a closed inhabitant in $P$, then by Proposition 3, $\|A\|$ has a closed inhabitant in $\lambda\Pi_P$. Conversely, if $\|A\|$ has a closed inhabitant then, by termination of $\lambda\Pi_P$ and Proposition 16, it has a closed inhabitant in weak $\eta$-long normal form and by Proposition 14, $A$ has a closed inhabitant in $P$.

**Remark 1.** This conservativity property we have proved is similar to that of the Curry-de Bruijn-Howard correspondence. If the type $A^\circ$ is inhabited in $\lambda\Pi$-calculus, then the proposition $A$ is provable in minimal predicate logic, but not all terms of type $A^\circ$ correspond to proofs of $A$. For instance, if $A$ is the proposition $(\forall x P(x)) \Rightarrow P(c)$, then the normal term $\lambda\alpha : (\Pi x : \iota (P x)) (\alpha c)$ corresponds to a proof of $A$ but the term $\lambda\alpha : (\Pi x : \iota (P x)) (\alpha ((\lambda y : \iota y) c))$ does not.

**Remark 2.** There are two ways to express proofs of simple type theory in the $\lambda\Pi$-calculus modulo. We can either use directly the fact that simple type theory can be expressed in Deduction modulo [8] or first express the proofs of simple type theory in the Calculus of Constructions and then embed the Calculus of Constructions in the $\lambda\Pi$-calculus modulo.

These two solutions have some similarities, in particular if we write $o$ the symbol $U_{Type}$. But they have also some differences: the function $\lambda x \, x$ of simple type theory is translated as the symbol $I$ — or as the term $\lambda 1$ — in the first case, using a symbol $I$ — or the symbols $\lambda$ and $1$ — specially introduced in the context to express this particular theory, while it is expressed as $\lambda x \, x$ using the symbol $\lambda$ of the $\lambda\Pi$-calculus modulo in the second.

More generally in the second case, we exploit the similarities of the $\lambda\Pi$-calculus modulo and simple type theory — the fact that they both allow to express functions — to simplify the expression while the first method is completely generic and uses no particularity of simple type theory. This explains why this first expression requires only the $\lambda\Pi^-$-calculus modulo, while the second requires the conversion rule to contain $\beta$-conversion.
References

1. H. Barendregt, Lambda calculi with types, *Handbook of Logic in Computer Science*, S. Abramsky, D. Gabbay, and T. Maibaum (eds.), Oxford University Press, 1992, pp. 117-309.

2. S. Berardi, Towards a mathematical analysis of the Coquand-Huet Calculus of Constructions and the other systems in Barendregt's cube, *manuscript*, 1988.

3. F. Blanqui, Definitions by rewriting in the Calculus of Constructions. *Mathematical Structures in Computer Science*, 15, 1, 2005, pp. 37-92.

4. T. Coquand and G. Huet, The Calculus of Constructions, *Information and Com-putation*, 76, 1988, pp. 95-120.

5. D. Cousineau, *Un plongement conservatif des Pure Type Systems dans le lambda Pi modulo*, Master Parisien de Recherche en Informatique, 2006.

6. D. Dougherty, S. Ghilezan, P. Lescanne and S. Likavec, Strong normalization of the dual classical sequent calculus, *LPAR-2005*

7. G. Dowek, Th. Hardin, and C. Kirchner, Theorem proving modulo, *Journal of Automated Reasoning*, 31, 2003, pp. 33-72.

8. G. Dowek, Th. Hardin, and C. Kirchner, HOL-lambda-sigma: an intentional first-order expression of higher-order logic, *Mathematical Structures in Computer Science*, 11, 2001, pp. 1-25.

9. G. Dowek and B. Werner, Proof normalization modulo, *The Journal of Symbolic Logic*, 68, 4, 2003, pp. 1289-1316.

10. J.Y. Girard, Interprétation Fonctionnelle et Élimination des Coupures dans l'Arithmétique d'Ordre Supérieur, *Thèse de Doctorat*, Université Paris VII, 1972.

11. R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, *Journal of the ACM*, 40, 1, 1993, pp. 143-184.

12. P. Martin-Löf, Intuitionistic Type Theory, *Bibliopolis*, 1984.

13. B. Nordström, K. Petersson, and J.M. Smith, Martin-Löf's type theory. *Handbook of Logic in Computer Science*, S. Abramsky, D. Gabbay, and T. Maibaum (eds.), Clarendon Press, 2000, pp. 1-37.

14. E. Palmgren, On universes in type theory, *Twenty five years of constructive type theory*, Oxford Logic Guides, 36, Oxford University Press, 1998, pp. 191-204.

15. J. Terlouw, Een nadere bewijstheoretische analyse van GSTT's, *manuscript*, 1989.