# Remarks on isomorphisms of simple inductive types

David Chemouil, Sergei Soloviev

► To cite this version:

David Chemouil, Sergei Soloviev. Remarks on isomorphisms of simple inductive types. Mathematics, Logic and Computation 2003 (Satellite Event of ICALP 2003), Jun 2003, Eindhoven, Netherlands. pp.106-124, 10.1016/S1571-0661(04)80760-6. hal-00783654

HAL Id: hal-00783654

https://hal.science/hal-00783654

Submitted on 18 May 2015

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_1.png" /></figure>
# Remarks on Isomorphisms of Simple Inductive Types

David Chemouil, Sergei Soloviev <fnref n="1" />,<fnref n="2" />

IRIT, Université Paul Sabatier
118, route de Narbonne
31062 Toulouse, France

## Abstract

We study isomorphisms of types in the system of simply-typed λ-calculus with inductive types and recursion operators. It is shown that in some cases (multiproducts, copies of types), it is possible to add new reductions in such a way that strong normalisation and confluence of the calculus are preserved, and the isomorphisms may be regarded as intensional w.r.t. a stronger equality relation.

# 1 Introduction

## 1.1 Presentation

This work is part of a larger project where we are exploring the possibilities of extensions preserving strong normalisation and confluence of standard reduction systems by new reductions of the form $f' (f t) \to t$ where $f'$ is in some sense an inverse of $f$.

The way this notion of invertibility may be understood is one of the questions we are investigating. A possibility would be to take the invertibility w.r.t extensional equality of functions between inductive types.

Here, we shall consider the simply-typed λ-calculus, equipped with inductive types (*i.e* recursive types satisfying a condition of strict positivity) and structural recursion schemes on these types.

In this short paper, we will focus on two particular cases where the usefulness of this extension seems obvious. Namely, we shall study some isomorphisms of products (defined as inductive types) and the notion of *copy* of a type

<footnote n="1">¹ E-mails: chemouil@irit.fr, soloviev@irit.fr</footnote>

<footnote n="2">² Work partly funded by Project ISOT (STIC 21) from Department STIC of CNRS.
*This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science*
URL: www.elsevier.nl/locate/entcs</footnote>
## 1.2 Isomorphisms of Types

Let us first recall a few facts and definitions about isomorphisms of types.

**Definition 1.1** Consider a typed λ-calculus, equipped with an equivalence relation ~ on terms, a term $id_A : A \to A$ for any type A and a composition operator ◦ (with suitable typing) verifying the following conditions, for any function $f : A \to B$:

$$f \circ id_A \sim f \qquad id_B \circ f \sim f$$

Then, two types A and B are said to be *isomorphic* (written $A \cong B$) if there exist two λ-terms $f : A \to B$ and $g : B \to A$ such that

$$f \circ g \sim id_B \qquad g \circ f \sim id_A$$

In this case, $g$ is often written $f^{-1}$ and called the *inverse* of $f$.

Until now, isomorphisms of types have mostly been studied in various first- or second-order λ-calculi, where ~ is usually generated by βη-conversion <fnref n="3" />, $id_A \cong \lambda x : A \cdot x$ and ◦ $\cong \lambda g : B \to C \cdot \lambda f : A \to B \cdot \lambda x : A \cdot g (f x)$ (for any types A, B, and C). As an example, we have the following result:

**Proposition 1.2 ([21]; [9,11])** All isomorphisms holding in $\lambda^1\beta\eta_{\to, \times, 1}$, the first-order simply-typed λ-calculus with binary products and unit type (or, equivalently, in cartesian closed categories), are obtainable by finite compositions of the following “base” of seven isomorphisms:

$$\begin{align*}
& A \times B \cong B \times A && A \times (B \times C) \cong (A \times B) \times C \\
& (A \times B) \to C \cong A \to (B \to C) && A \to (B \times C) \cong (A \to B) \times (A \to C) \\
& A \times 1 \cong A && A \to 1 \cong 1 && 1 \to A \cong A
\end{align*}$$

## 1.3 Isomorphisms of Inductive Types

Now, it is our view that, as long as inductive types are concerned, *intensional isomorphisms*, in ordinary sense, lack expressivity. To view this problem in a larger context, one needs a notion of *extensionality*.

**Definition 1.3** Two types A and B are *extensionally isomorphic* (written $A \cong B$) if there exists two λ-terms $f : A \to B$ and $g : B \to A$ such that

$$\forall x : A \cdot g (f x) \sim x \quad \text{and} \quad \forall y : B \cdot f (g y) \sim y.$$

(Note that $\cong$ and $\cong$ are both equivalence relations.)

<footnote n="3">³ It was shown in [10] that with β-conversion solely, the only invertible term is the identity.</footnote>
Obviously, we have $A \cong B \Rightarrow A \cong B$, but the converse is usually not true. One way to achieve this kind of isomorphisms would be to add extensional reduction rules to the calculi, such as $\eta$ rules, surjective pairing, etc. However, many calculi don't come equipped with extensional reduction rules, for various reasons (decidability, confluence, etc); though some positive results do exist, e.g [17,14,16]. Hence, in this paper, we will mainly be interested with $\beta$-reduction only (where $\iota$-reduction is the rule associated to structural recursion over inductive types).

Of course, extensional isomorphisms are *provable* by induction, but they are not *computable*, i.e., one doesn't have (for example)

$$ \lambda x : A \cdot f^{-1} (f x) \to_{\beta\iota} \lambda x : A \cdot x. $$

Without appealing to full extensionality, we think that, if $f$ and $f^{-1}$ are mutually invertible extensional isomorphisms, it is worth considering the addition of new reduction rules (call them $\sigma$-reductions, following [6]) as follows:

$$ f (f^{-1} x) \to_{\sigma} x \quad \text{and} \quad f^{-1} (f x) \to_{\sigma} x. $$

## 1.4 *Outline of the paper*

In Sect. 2, we quickly give essential definitions of a simply-typed $\lambda$-calculus with inductive types.

Then, in Sect. 3, we quickly present a small lemma ("Deferment Lemma") that is of interest in the next section.

In Sect. 4, we illustrate the addition of rewrite rules on $n$-ary products. We show that, for products, strong normalisation and confluence are preserved for a rewrite rule corresponding to commutativity, while it is not the case for associativity, unless we also add surjective pairing.

Finally, in Sect. 5, we study the notion of *isomorphic copy* of a type, and how a rewrite rule corresponding to it may or not be added to the calculus.

# 2 Simply-Typed $\lambda$-Calculus with Inductive Types

We define the simply-typed $\lambda$-calculus with inductive types, which may be seen as an extension of Gödel's system $\mathcal{T}$. Some references on $\lambda$-calculus and inductive types may be found in [4,20,5,23,19,8]. Furthermore, most of our notations and results concerning rewrite systems are taken from [1]. For a given reduction $\to_R$, we write $\to_R^+$ for its transitive closure, and $\to_R^*$ for its reflexive-transitive closure.

## 2.1 *Types*

Throughout this paper, we consider an infinite set $S = \{\alpha, \beta, \dots\}$ of type variables. We also consider an infinite set of variables $V$ (with $V \cap S = \emptyset$),
and an infinite set $\mathcal{C}$ of inductive-type constructors (or introduction operators), with $\mathcal{C} \cap \mathcal{S} = \mathcal{C} \cap \mathcal{V} = \emptyset$.

Moreover, as usual in this sort of presentation, we consider all terms and types up to $\alpha$-conversion, i.e the names of bound variables are irrelevant.

**Note 1** In the following, the sign $\equiv$ will denote syntactic equality, and definitions will be introduced in the calculus with the sign $\cong$. Furthermore, we will use the common notation let $x = e_1$ in $e_2$ for $e_2[e_1/x]$.

**Definition 2.1** The set of pre-types is generated by the following grammar rules:

$$ 
\begin{align*}
\text{Ty} &::= \alpha \mid (\text{Ty} \to \text{Ty}) \mid \text{Ind}(\alpha)[\text{CS}] \\
\text{CS} &::= \text{CL} \mid \varepsilon \\
\text{CL} &::= c : \text{Ty} \mid c : \text{Ty} ; \text{CL}
\end{align*}
$$

with $c \in \mathcal{C}$ (as usual, $\varepsilon$ denotes the empty word). Of course, we require that any constructor belong to only one inductive type.

**Note 2** We consider that $\to$ is right associative, hence $\tau_1 \to (\tau_2 \to \tau_3)$ will be subsequently written $\tau_1 \to \tau_2 \to \tau_3$.

An inductive type with $n$ constructors $c_1, \dots, c_n$ in $\mathcal{C}$, each of arity $k_i$ (with $1 \le i \le n$), is then of the form

$$ \text{Ind}(\alpha)[c_1 : \sigma_1^1 \to \dots \to \sigma_1^{k_1} \to \alpha; \dots; c_n : \sigma_n^1 \to \dots \to \sigma_n^{k_n} \to \alpha], $$

where the part between brackets is bound by $\text{Ind}(\alpha)$. Moreover, every $\sigma_i \equiv \sigma_i^1 \to \dots \to \sigma_i^{k_i} \to \alpha$ must verify certain conditions, as explained below.

**Definition 2.2** A strictly positive operator $\tau$ over a type variable $\alpha$ (written $\tau \text{ spos } \alpha$) is inductively defined by the following rules:

$$ \frac{\alpha \notin \text{FV}(\tau_1)}{\alpha \text{ spos } \alpha} \qquad \frac{\tau_2 \text{ spos } \alpha}{\tau_1 \to \tau_2 \text{ spos } \alpha} $$

**Definition 2.3** An (inductive) schema $\tau$ over a type variable $\alpha$ (written $\tau \text{ sch } \alpha$) is inductively defined by the following rules:

$$ \frac{\alpha \notin \text{FV}(\tau_1)}{\alpha \text{ sch } \alpha} \qquad \frac{\tau_2 \text{ sch } \alpha}{\tau_1 \to \tau_2 \text{ sch } \alpha} \qquad \frac{\tau_1 \text{ spos } \alpha}{\tau_1 \to \tau_2 \text{ sch } \alpha} $$

Intuitively, a schema $\sigma$ is of the form $\sigma^1 \to \dots \to \sigma^k \to \alpha$, where every $\sigma^j$ is itself:

* either a type not containing $\alpha$ (we call this $\sigma^j$ a non-recursive operator);

* or a type of the form $\sigma^j \equiv \nu_1 \to \dots \to \nu_m \to \alpha$ (we call this $\sigma^j$ a strictly positive operator), where $\alpha$ does not appear in any $\nu_\ell$.
**Note 3** Given a schema $\sigma \equiv \sigma^1 \to \dots \to \sigma^k \to \alpha$, we will denote by $SP_\alpha(\sigma)$ the set of indices $j$ (with $1 \le j \le k$) such that $\sigma^j$ is a strictly positive operator over $\alpha$, i.e $SP_\alpha(\sigma) = \{j \mid 1 \le j \le k \land \sigma^j \text{ spos } \alpha\}$. This set will be useful because it corresponds to arguments (of a given constructor) on which a recursive call may be carried out.

**Definition 2.4** A type $\tau$ (written $\tau : \star$) is inductively defined by the following rules:

$$ \frac{\alpha \in \mathcal{S}}{\alpha : \star} \qquad \frac{\tau_1 : \star \quad \tau_2 : \star}{\tau_1 \to \tau_2 : \star} \qquad \frac{c_i \in \mathcal{C}}{\text{Ind}(\alpha)[c_1 : \sigma_1; \dots; c_n : \sigma_n] : \star} \qquad \frac{\sigma_i : \star \quad \sigma_i \text{ sch } \alpha}{(1 \le i \le n)} $$

**Example 2.5** With these rules, it is possible to define the types of natural numbers, of Brouwer's ordinals and of lists of natural numbers (normally, these inductive types should have different constructor names, we used some common names for the sake of readability):

$$ \begin{align*} \text{Nat} &\cong \text{Ind}(\alpha)[0 : \alpha | S : \alpha \to \alpha] \\ \text{Ord} &\cong \text{Ind}(\alpha)[0 : \alpha | S : \alpha \to \alpha | L : (\text{Nat} \to \alpha) \to \alpha] \\ \text{ListNat} &\cong \text{Ind}(\alpha)[\text{nil} : \alpha | \text{cons} : \text{Nat} \to \alpha \to \alpha]. \end{align*} $$

Note that any inductive type $\tau$ generates a *recursor* (or *structural-recursion operator*) $\mathcal{R}_{\tau,\kappa}$ to any type $\kappa$. This will be further explained in the next section concerned with terms of the language.

## 2.2 Terms

We will now define the terms of our calculus.

**Definition 2.6** The set of *terms* is generated by the following grammar rule:

$$ M ::= c \mid x \mid (\lambda x : \tau \cdot M) \mid (M M) \mid \mathcal{R}_{\tau, \kappa}, $$

where $x \in \mathcal{V}$, $c \in \mathcal{C}$ and $\tau$ and $\kappa$ are types.

**Note 4** Application is left-associative, hence $(\dots(M_1 M_2) \dots) M_n$ can be written $M_1 \dots M_n$. In the same way, abstraction is right-associative, hence $(\lambda x_1 : \tau_1 \cdot (\lambda x_2 : \tau_2 \cdot M))$ can be written $\lambda x_1 : \tau_1 \cdot \lambda x_2 : \tau_2 \cdot M$

We now define a syntactic operation that will be useful to assert typing rules for terms.

**Definition 2.7** Let $\tau$ be an inductive type, $\sigma \equiv \sigma^1 \to \dots \to \sigma^k \to \alpha$ a schema over $\alpha$ in $\tau$, and $\kappa$ a type. Let $\{j_p\}_{p=1,\ell} = SP_\alpha(\sigma)$. Then, we define

$$ \Upsilon_\tau(\sigma, \kappa) \equiv \sigma^1[\tau/\alpha] \to \dots \to \sigma^k[\tau/\alpha] \to \sigma^{j_1}[\kappa/\alpha] \to \dots \sigma^{j_\ell}[\kappa/\alpha] \to \kappa. $$
**Definition 2.8** We now present the typing rules for the calculus:

$$ \frac{\tau \equiv \text{Ind}(\alpha)[\dots; c : \sigma; \dots]}{\Gamma, x : \alpha \vdash x : \alpha} \quad \tau : \star \quad (\text{CONSTR}) $$

$$ \frac{\Gamma, x : \tau_1 \vdash M : \tau_2}{(\lambda x : \tau_1 \cdot M) : \tau_1 \to \tau_2} (\lambda) \qquad \frac{\Gamma \vdash M : \tau_1 \to \tau_2 \qquad \Gamma \vdash N : \tau_1}{\Gamma \vdash (M N) : \tau_2} (\text{APP}) $$

$$ \frac{\tau \equiv \text{Ind}(\alpha)[c_1 : \sigma_1; \dots; c_n : \sigma_n] \quad \Gamma \vdash M_i : \Upsilon_{\tau}(\sigma_i, \kappa) \quad (1 \le i \le n)}{\Gamma \vdash (\mathcal{R}_{\tau, \kappa} M_1 \dots M_n) : \tau \to \kappa} (\text{ELIM}) $$

## 2.3 Reduction

**Definition 2.9** We define the usual $\beta$-reduction rule as follows:

$$ (\lambda x : \tau \cdot M) N \longrightarrow_{\beta} M[N/x] . $$

Now, we define the $\iota$-reduction. However, to do so, we first need to make a technical definition which will be helpful.

**Definition 2.10** Let $\nu \equiv \nu_1 \to \dots \to \nu_m \to \alpha$ be a strictly positive operator over $\alpha$. Then, we define

$$ \Xi(R, N, \nu) \equiv \lambda z_1 : \nu_1 \dots \lambda z_m : \nu_m \cdot R (N z_1 \dots z_m) . $$

Of course, in the special case where $m = 0$, we have $\Xi(R, N, \nu) \equiv R N$.

**Definition 2.11** Now, let $\sigma \equiv \sigma^1 \to \dots \to \sigma^k \to \alpha$ be a schema over $\alpha$, and let $\{j_p\}_{p=1,\ell} = \text{SP}_\alpha(\sigma)$. Then, we define $\iota$-reduction by

$$ \mathcal{R}_{\tau, \kappa} M_1 \dots M_n (c_i N_1 \dots N_{k_i}) \longrightarrow_{\iota} M_i N_1 \dots N_{k_i} N'_{j_1} \dots N'_{j_\ell}, $$

where $N'_{j_p} \equiv \Xi(\mathcal{R}_{\tau, \kappa} M_1 \dots M_n, N_{j_p}, \sigma_{j_p})$, for all $1 \le p \le \ell$.

Examples of rules for some basic inductive types are given in Figure 1 on the following page.

**Proposition 2.12** For the simply-typed $\lambda$-calculus with inductive types, $\beta\iota$-reduction is strongly normalising and confluent.

See for example [8].

# 3 A Deferment Lemma

There are many lemmas concerning with strong normalisability of a relation $\to_{RS}$ when $\to_R$ and $\to_S$ are strongly normalising. Though the lemma we
<figure><img src="image_2.png" /><figcaption>Fig. 1. Recursion rules for some basic inductive types</figcaption></figure>

consider below is close to many results in the folklore, we could not find its
exact formulation in the literature.

Note also that this lemma is not equivalent to the so-called Postponement
Lemma for $\eta$-contractions in pure $\lambda$-calculus, see e.g [3] p. 386.

**Definition 3.1** Let $\rightarrow_R$ and $\rightarrow_S$ be two reductions. Then, $\rightarrow_S$ is deferable w.r.t $\rightarrow_R$ if, for all terms $t$ and $u$ such that $t \rightarrow_S \rightarrow_R u$, there is a derivation $t \rightarrow_R \rightarrow_{RS}^*$ u.

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

**Lemma 3.2 (Deferment Lemma)** Let $\rightarrow_R$ and $\rightarrow_S$ be two strongly normalising relations. Then, if $\rightarrow_S$ is deferable w.r.t $\rightarrow_R$, $\rightarrow_{RS}$ is strongly normalising.

**Proof.** Let $\rightarrow_R$ and $\rightarrow_S$ be two strongly normalising relations, such that $\rightarrow_S$ is deferable w.r.t $\rightarrow_R$. Let us suppose that $\rightarrow_{RS}$ is not strongly normalising, and show that it leads to a contradiction.

If $\rightarrow_{RS}$ is not strongly normalising, then $\rightarrow_{RS}^*$ consists of an infinite alternation of $\rightarrow_R^*$ and $\rightarrow_S^*$. Then, one can inductively "lift" $\rightarrow_R$-reductions by deferring every $\rightarrow_S$-reduction followed by an $\rightarrow_R$-reduction, thus building an infinite derivation of $\rightarrow_R$ steps. This contradicts the fact that $\rightarrow_R$ is strongly normalising. $\square$

In fact, we can prove a slightly more powerful lemma whose premises occur
however less in practice.
**Definition 3.3** Let $\rightarrow_R$ and $\rightarrow_S$ be two reductions. Then, $\rightarrow_S$ is 0-deferable w.r.t. $\rightarrow_R$ if, for all terms $t$ and $u$ such that $t \rightarrow_S u$, there is a derivation $t \rightarrow_R \rightarrow_{RS}^* u$.

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

**Lemma 3.4 (0-Deferment Lemma)** Let $\rightarrow_R$ and $\rightarrow_S$ be two strongly normalising relations. Then, if $\rightarrow_S$ is 0-deferable w.r.t. $\rightarrow_R$, $\rightarrow_{RS}$ is strongly normalising.

**Proof.** Immediate, because 0-deferment implies deferment. $\square$

**Remark 3.5** Since the submission of this paper, we found some references about what we call Deferment Lemma (cf. [2,15] and most notably [13]). While we shall keep calling this property “deferment” in the current paper, we intend to use the preferable term “adjournement” afterwards, following Delia Kesner (private communication).

# 4 Multiproducts

Let us define a schema of inductive types representing $n$-ary products:

$$ \Pi_n A_1 \dots A_n \cong \mathrm{Ind}(\alpha)[\langle\cdot\rangle_n : A_1 \to \dots \to A_n \to \alpha], $$

with recursion operator $(\|\cdot\|)_n$ defined by

$$ \begin{align*} (\|\cdot\|)_n : (A_1 \to \dots \to A_n \to B) &\to (\Pi_n A_1 \dots A_n \to B) \\ (\|f\|)_n \langle a_1 \dots a_n \rangle_n &\to \iota f a_1 \dots a_n . \end{align*} $$

The projections $p_k^n$ are defined as $(\|\lambda x_1 : A_1 \dots \lambda x_n : A_n \cdot x_k\|)_n$.

**Remark 4.1** One may note that the product of morphisms $f_i : C \to A_i$ (with $1 \le i \le n$) is definable, without the elimination operator, by

$$ \mathrm{prod}_n f_1 \dots f_n \cong \lambda z : C \cdot \langle f_1 z, \dots, f_n z \rangle_n . $$

However, many familiar properties of product and projections do not hold intensionally. For example, we have $\langle p_1^2 x, p_2^2 x \rangle_2 \neq_{\beta_i} x$ for $x : \Pi_2 A B$. In fact, this property, usually known as *surjective pairing*, stipulates that the product is unique.

## 4.1 Commutativity of Products

Now, let $\varrho$ be a permutation of $\{1, \dots, n\}$. The permutation of $\Pi_n A_1 \dots A_n$ induced by $\varrho$ is denoted $\bar{\varrho}$, and defined as $(\|\lambda x_1 : A_1 \dots \lambda x_n : A_n \cdot x_{\varrho(1)}, \dots, x_{\varrho(n)}\|)_n$.
**Proposition 4.2** For any term $t : \Pi_n A_1 \dots A_n$ and permutations $\varrho$ and $\omega$ defined on $\{1, \dots, n\}$, the equality $\overline{\varrho \circ \omega} t =_{\beta t} \overline{\varrho} (\overline{\omega} t)$ is provable.

Still, while we can prove this proposition by induction, it is important to note that the equality is not computable for an arbitrary $t$, but just when $t \equiv \langle t_1, \dots, t_n \rangle_n$ for some $n$ (cf. Sect. 1.3 on page 3). Note also that for mutually inverse permutations $\varrho$ and $\varrho^{-1}$, $\overline{\varrho}$ and $\overline{\varrho^{-1}}$ are mutually inverse extensional isomorphisms.

Now, for given mutually inverse permutations $\varrho$ and $\varrho^{-1}$, let us add the following rewrite rules to the system of $\beta t$-reductions:

$$ \overline{\varrho} (\overline{\varrho^{-1}} x) \to_{\sigma} x \qquad \overline{\varrho^{-1}} (\overline{\varrho} x) \to_{\sigma} x . $$

(Note that $\overline{\varrho}$ and $\overline{\varrho^{-1}}$ are concrete, i.e constant, terms of the calculus.)

**Remark 4.3** To lighten the notation, let us write $\pi$ and $\pi'$ for $\overline{\varrho}$ and $\overline{\varrho^{-1}}$. We will also make use of diagrams, as is usually done for this kind of proof.

**Lemma 4.4** $\sigma$-reduction is strongly normalising.

**Proof.** Take the length of terms as an ordering. $\square$

**Theorem 4.5** $\beta t \sigma$-reduction is strongly normalising.

**Proof.** We show that $\sigma$-reduction is deferable w.r.t $\beta$-reduction (case i) and w.r.t $\iota$-reduction (case ii).

(i) For $\beta$-reduction. The crucial case is when the $\sigma$-redex occurs inside a $\beta$-redex.

i.1. As a first possibility, we may have $t \equiv t'[(\lambda x : A \cdot p[\pi (\pi' s)]) q]$. Note that $\pi$ and $\pi'$ do not contain variables.

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

i.2. We may also have $t \equiv t'[(\lambda x : A \cdot p)(q[\pi (\pi' s)])]$, in which case the term $p$ may contain many (or zero) occurrences of $x$, which requires
to carry as many $\sigma$-reductions.

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

(ii) For $\iota$-reduction.

ii.1. The crucial case occurs when a $\iota$-redex may interact with $\pi$ and $\pi'$, hence we must have $t \equiv t'[\pi (\pi' \langle s_1, \dots, s_n \rangle_n)]$. But then, it is immediate to see that $t \xrightarrow{\sigma} t'[\langle s_1, \dots, s_n \rangle_n]$ can also be performed by the derivation: $t'[\pi (\pi' \langle s_1, \dots, s_n \rangle_n)] \xrightarrow{\iota} t'[\pi (\pi' \langle s_1, \dots, s_n \rangle_n)]$. This is a trivial case of 0-deferment.

ii.2. In other cases, the $\iota$-redex doesn't interfere with $\sigma$-reduction, therefore deferment is obviously possible. $\square$

**Theorem 4.6** *$\beta\iota\sigma$-reduction is confluent.*

**Proof.** First, as $\beta\iota\sigma$-reduction is strongly normalising, it is enough to show local confluence (by Newman's Lemma), i.e for all terms $t, w, w'$ such that $t \to_{\beta\iota\sigma} w$ and $t \to_{\beta\iota\sigma} w'$, there exists a term $u$ such that $w \to_{\beta\iota\sigma} u$ and $w' \to_{\beta\iota\sigma} u$.

By Lemma 2.12, $\beta\iota$-reduction is confluent. For $\sigma$-reductions alone, by Newman's Lemma it is enough to show local confluence. The critical pairs induced by $\sigma$-reduction are joinable; hence by the Critical Pair Theorem, $\sigma$-reduction is locally confluent. Therefore, for $\beta\iota\sigma$-reductions there are only two extra cases to be considered depending on whether one carries a $\beta$- or $\iota$-reduction (combined with $\sigma$-) as a first step.

(i) If it is a $\iota$-reduction, then $t \equiv t'[\pi (\pi' s)]$, and there are 4 possible cases: the $\iota$-redex is in $s$, the $\iota$-redex has no intersection with $\pi (\pi' s)$, the $\iota$-redex contains $\pi (\pi' s)$, or the $\iota$-redex is in $\pi (\pi' s)$ and intersects with $\pi$ or $\pi'$.

i.1. We have $t \equiv t'[\pi (\pi' (s'[r]))]$, $r$ being a $\iota$-redex. Then, if $t$ $\iota$-reduces to $t'[\pi (\pi' s'[r'])]$ and $\sigma$-reduces to $t'[s'[r]]$, it is possible to “close” the fork by $t'[\pi (\pi' s'[r'])] \xrightarrow{\sigma} t'[s'[r]]$ and $t'[\pi (\pi' s'[r'])] \xrightarrow{\iota} t'[s'[r]]$.

i.2. Once more, the order is indifferent.

i.3. One has $t' \equiv t''[r[\pi (\pi' s)]]$. The upper-left $\iota$-reduction cannot affect $\pi (\pi' s)$ since this part doesn't begin with an introduction operator. (In general, the lower-left reduction would possibly be $\to_{\sigma}^*$ since the number of $\sigma$-redexes may change when $\iota$-reduction is applied, but it
is not the case for products.)

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

i.4. In fact, the $\iota$-redex should coincide with $(\pi' s)$, since $(\pi' s)$ doesn't begin with an introduction operator, so it cannot be $\pi$ $(\pi' s)$ (here, we use the concrete definition of $\pi$ and $\pi'$). Thus, $s$ must be of the form $\langle s_1, \dots, s_n \rangle_n$. But, for all elements of this form, we have $\pi (\pi' \langle s_1, \dots, s_n \rangle_n) \to_{\iota} \beta_{\iota}^+ \langle s_1, \dots, s_n \rangle_n$, hence local confluence holds trivially in this case.

(ii) For $\beta$-reduction, cases ii.1 and ii.2 are similar to cases i.1 and i.2, thus treated as above.

ii.3 If $t \equiv t'[(\lambda x : A \cdot p[\pi (\pi' s)]) q]$, and $t \to_{\beta} t'[(p[\pi (\pi' s)])[q/x]]$ and $t \to_{\sigma} t'[(\lambda x : A \cdot p[s]) q]$, closing the “fork” is straightforward by observing that both terms $\sigma$- and $\beta$-reduce respectively in one step to $t'[(p[s])[q/x]]$. (Note that this situation appears because $\pi$ and $\pi'$ are closed terms.)

ii.4 In the last case, where $t \equiv t'[(\lambda x : A \cdot p)(q[\pi (\pi' s)])]$, the number of occurrences of $x$ in $p$ may influence the number of $\sigma$-reductions to perform to close the diagram. Thus, if $t \to_{\beta} t'[p[q[\pi (\pi' s)]/x]]$ and $t \to_{\sigma} t'[(\lambda x : A \cdot p)(q[s])]$, we may need a sequence of reductions $t'[p[q[\pi (\pi' s)]/x]] \to_{\sigma} t'[p[q[s]/x]]$ while a one-step $\beta$-reduction only would be necessary on the other term: $t'[(\lambda x : A \cdot p)(q[s])] \to_{\beta} t'[p[q[s]/x]]$.

□

## 4.2 Associativity of Products

As just seen, products enjoy the commutativity property. However, the associativity does not hold in general, i.e, it is not the case that, for example, $\Pi_2 (\Pi_2 A B) C \cong \Pi_2 A (\Pi_2 B C)$. This is so because there is an occurence of $\Pi_2 A B$ (or $\Pi_2 B C$) inside another $\Pi_2$. Thus, the “isomorphisms” $g$ and $g'$ would be defined in the following way:

$$ g : \Pi_2 (\Pi_2 A B) C \to \Pi_2 A (\Pi_2 B C) \\ \cong (\lambda p : \Pi_2 A B \cdot \lambda c : C \cdot (p_1^2 p, \langle p_2^2 p, c \rangle_2)_{\langle 2 \rangle}) $$
and

$$ g' : \Pi_2 A (\Pi_2 B C) \to \Pi_2 (\Pi_2 A B) C \\ \cong (\langle \lambda a : A \cdot \lambda q : \Pi_2 B C \cdot \langle \langle a, p_1^2 q \rangle_2, p_2^2 q \rangle_2 \rangle) . $$

Then, for a term $\langle p, c \rangle_2$, with $p : \Pi_2 A B$ and $c : C$, one has:

$$ g' (g \langle p, c \rangle_2) \to_{\iota} \to_{\beta} g' \langle p_1^2 p, \langle p_2^2 p, c \rangle_2 \rangle_2 \\ \to_{\iota} \to_{\beta} \langle \langle p_1^2 p, p_2^2 p \rangle_2, c \rangle_2 \neq_{\beta \iota} \langle p, c \rangle_2 $$

because of the lack of surjective pairing. It is interesting to note that, even with extensionality on canonical elements, the isomorphism establishing associativity of binary product does not hold.

### 4.3 Retractions

Now, let us consider some correspondances between $n$-products for different $n$, for example $\Pi_3 A B C$ and $\Pi_2 (\Pi_2 A B) C$. Define

$$ f : \Pi_2 (\Pi_2 A B) C \to \Pi_3 A B C \\ \cong (\langle \lambda y : \Pi_2 A B \cdot \lambda z : C \cdot \langle p_1^2 y, p_2^2 y, z \rangle_3 \rangle)_2 $$

and

$$ f' : \Pi_3 A B C \to \Pi_2 (\Pi_2 A B) C \\ \cong (\langle \lambda x : A \cdot \lambda y : B \cdot \lambda z : C \cdot \langle \langle x, y \rangle_2, z \rangle_2 \rangle)_3 . $$

For $\langle t, u, v \rangle_3 : \Pi_3 A B C$, we have:

$$ f (f' \langle t, u, v \rangle_3) \to_{\iota} \to_{\beta} f \langle \langle t, u \rangle_2, v \rangle_2 \to_{\iota} \to_{\beta} \langle t, u, v \rangle_3 . $$

However, for $\langle y, z \rangle_2 : \Pi_2 (\Pi_2 A B) C$, we have:

$$ f' (f \langle y, z \rangle_2) \to_{\iota} \to_{\beta} f' \langle p_1^2 y, p_2^2 y, z \rangle_3 \\ \to_{\iota} \to_{\beta} \langle \langle p_1^2 y, p_2^2 y \rangle_2, z \rangle_2 \neq_{\beta \iota} \langle y, z \rangle_2 , $$

once again because the type $\Pi_2 A B$ doesn't enjoy surjective pairing. This means that even in an extensional sense (on canonical elements), $f$ is only a *retraction*, and not an isomorphism. Of course, the same situation will appear if we consider the product of $n$ elements expressed with $\Pi_n$, and using a superposition of $\Pi_k$ for $k < n$. While we will not consider deeply the case of retractions in this paper, we think they deserve attention for further studies: this example suggests that $\Pi_3$ might be considered as the “canonical” representation of triples, for being the retract of all representations of triples. One may note that this observation demonstrates the usefulness of adding new reductions gradually. The correspondence between products of different
arity described above would remain hidden if surjective pairing was already present.

## 4.4 Surjective Pairing

Let us add the rule $\langle p_1^2 x, p_2^2 x \rangle_2 \to_{SP} x$ (if $x$ is of product type) to the system with $\beta$-reductions. We will now show that the Deferment Lemma may also be applied to prove strong normalisation of a system of $\beta$SP-reductions.

Consider a SP-reduction followed by some $\beta$- or $\iota$-reduction.

$$t[\langle p_1^2 s, p_2^2 s \rangle_2] \to_{SP} t[s] \to_{\iota} t^*[s^*].$$

If $s$ does not have the form $\langle s_1, s_2 \rangle_2$ or it does but the reduction does not use this occurrence of $\langle \cdot, \cdot \rangle_2$ then deferment is obviously possible.

Suppose the reduction that follows SP is $\iota$, then $t$ should be a term of the form $t[\langle p_1^2 s, p_2^2 s \rangle_2] \equiv t'[\langle \iota f \rangle_2 \langle p_1^2 s, p_2^2 s \rangle_2]$ where $s : \Pi_2 A B, s_1 : A, s_2 : B, f : A \to B \to C$ and we have

$$t'[\langle \iota f \rangle_2 \langle p_1^2 s, p_2^2 s \rangle_2] \to_{SP} t'[\langle \iota f \rangle_2 \langle s_1, s_2 \rangle_2] \to_{\iota} t'[f s_1 s_2].$$

This can be replaced by

$$t'[\langle \iota f \rangle_2 \langle p_1^2 s, p_2^2 s \rangle_2] \to_{\iota} t'[f(p_1^2 s)(p_2^2 s)] \to_{\iota} t'[f(s_1(p_2^2 s))] \to_{\iota} t'[f(s_1 s_2)]$$

(a trivial case of deferment). It is easy to see that local confluence will hold as well.

# 5 Isomorphic Copies of (Non-)Algebraic Types

The notion of the copy of a type is a very important one, and occurs quite often in many developments. For example, such operations are frequently used in tree-processing programs such as compilers. In this section, we study how isomorphisms may be used to devise an extended notion of copy, namely the *isomorphic copy* (for want of a better name).

Let us consider two extensionally isomorphic types $A$ and $B$ with isomorphisms $f : A \to B$ and $f^{-1} : B \to A$, and a type

$$C \equiv \mathrm{Ind}(\alpha)[c_1 : \sigma_1^1 \to \dots \to \sigma_1^{k_1} \to \alpha; \dots; c_n : \sigma_n^1 \to \dots \to \sigma_n^{k_n} \to \alpha],$$

possibly containing occurrences of $A$. An *isomorphic copy* $C'$ of $C$ differs by names of introduction operators, e.g $c'_1, \dots, c'_n$, and by the fact that each "atomic" occurrence of $A$ in $C$ is replaced by an occurrence of $B$ in $C'$ (that is to say: $A$ will be replaced by $B$ only if it occurs either as a non-recursive operator, or as the premise —i.e., the type of an argument— of a strictly positive operator).
The reader who prefers a less abstract setting may suppose the isomorphisms between A and B belong to the class studied in section 4. It can be also intensional isomorphism, e.g., permutation of premises of a functional type.

The definitions below also may be modified in such a way that only some selected occurrences of A are considered.

Now, let us define a function icopy : $C \to C'$ which converts canonical objects from one type to the other. Formally, icopy is of the form $\mathcal{R}_{C,C'} M_1 \dots M_n$. For every constructor $c_i : \sigma_i^1 \to \dots \to \sigma_i^{k_i} \to C$, let $\{j_p\}_{p=1,\ell} = \text{SP}_\alpha(\sigma)$ and let us denote every strictly positive operator $\sigma_i^{j_p}$ by $\nu_{i,j,1} \to \dots \nu_{i,j,p_{i,j}} \to \alpha$. Then, we have

$$M_i \equiv \lambda x_1 : \sigma_i^1 [C/\alpha] \dots \lambda x_{k_i} : \sigma_i^{k_i} [C/\alpha].$$

$$\lambda w_{j_1} : \sigma_i^{j_1} [C'/\alpha] \dots \lambda w_{j_\ell} : \sigma_i^{j_\ell} [C'/\alpha] \cdot c_i' \delta_1 \dots \delta_{k_i}$$

where

$$\delta_m \equiv \begin{cases} (a) \quad \lambda z_1 : \nu_{i,m,1}^\prime \dots \lambda z_p : \nu_{i,m,p_{i,m}}^\prime \cdot w_m z_1^\prime \dots z_p^\prime & \text{if } m \in j_1, \dots, j_\ell; \\ (b) \quad f x_m & \text{if } \sigma_i^m \equiv A; \\ (c) \quad x_m & \text{otherwise;} \end{cases}$$

and, for $1 \le r \le p_{i,m}$:

* $\nu_{i,m,r}^\prime \equiv B$ and $z_r^\prime \equiv f^{-1} z_r$ if $\nu_r \equiv A$;

* $\nu_{i,m,r}^\prime \equiv \nu_{i,m,r}$ and $z_r^\prime \equiv z_r$ otherwise.

The function icopy$^{-1}$ : $C' \to C$ is defined similarly.

We may now consider the behaviour of icopy and icopy$^{-1}$ w.r.t introduction operators, assuming that the new $\sigma$-reductions icopy$^{-1}$ (icopy $x$) $\to_\sigma x$ and $f^{-1}(f x) \to_\sigma x$ are added. The main observation is that

$$\text{icopy}^{-1}(\text{icopy}(c_i t_1 \dots t_{k_i})) \to_{\beta_l} c_i t'_1 \dots t'_{k_i}$$

where $t'_j$:

* is $t_j$ in case (c);

* is $f^{-1}(f t_j)$ in case (b);

* and is of the form $\lambda z_1 : \nu_{i,j,1} \dots \lambda z_p : \nu_{i,i,p_{i,j}} \cdot \text{icopy}^{-1}(\text{icopy}(t_j z_1' \dots z_p'))$ where $z_r' \equiv f^{-1}(f z_r)$ if $\nu_r \equiv A$, $z_r' \equiv z_r$ otherwise, in case (a).

Now, suppose we have a term of the form $q[\text{icopy}^{-1}(\text{icopy}(c_i t_1 \dots t_{k_i}))]$.
Then, by one single $\sigma$-reduction, we have

$$q[\text{icopy}^{-1} (\text{icopy} (c_i t_1 \dots t_{k_i}))] \to_{\sigma} q[c_i t_1 \dots t_{k_i}] .$$

But we may try to defer this $\sigma$-reduction. First, we have

$$q[\text{icopy}^{-1} (\text{icopy} (c_i t_1 \dots t_{k_i}))] \to_{\beta_i} q[c_i t'_1 \dots t'_{k_i}] .$$

Now, the deferment will depend on which cases the $t'_j$ are in. In case (c), we have $t'_j \equiv t_j$, so no more reduction is to be done to close the diagram. If case (b) happens, some $\sigma$-reductions will be needed:

$$q[c_i t'_1 \dots t'_{k_i}] \to_{\sigma} q[c_i t_1 \dots t_{k_i}] .$$

Finally, if case (a) happens, carrying some $\sigma$-reductions may lead to an un-closed diagram:

$$q[c_i t'_1 \dots t'_{k_i}] \to_{\sigma} q[c_i t''_1 \dots t''_{k_i}],$$

where $t''_j$ may begin by some abstractions. This situation will not happen only in the specific case, similar in result to case (b), where $\sigma_i^j$ is a strictly positive operator over $\alpha$ of null arity, i.e $\sigma_i^j \equiv \alpha$. For example, this is the case for the 'S' constructor of ordinals. In the general case however (i.e with $\sigma_i^j$ being a strictly positive operator over $\alpha$ of non-null arity), the only way to close the diagram seems to add further $\eta$-expansions in the following way:

$$q[c_i t_1 \dots t_{k_i}] \to_{\eta} q[c_i t''_1 \dots t''_{k_i}] .$$

As an example, we have, for the 'L' constructor of ordinals the following reduction graph:

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

As a conclusion, if we only meet cases (c) and (b), and case (a) with only null-arity strictly positive operators, it is always possible to (0-)defer $\sigma$-reductions in the calculus. Thus $\beta_i\sigma$-reduction is strongly normalising for "algebraic" types. Confluence follows easily, with a similar proof as for Theorem 4.6 on page 10.

As we briefly discussed above, our "strategy" is to add new reductions one by one. Thus, even the result for algebraic types only opens a large field of
applications for icopy, generated by isomorphisms of parameters introduced previously.

The difficult case is when “non-algebraic” types occur. Recently we obtained a proof for this case and the system with $\eta$-expansion.

**Definition 5.1** We define $\eta$-expansion as follows:

$$ M \to_{\eta} \lambda x : A \cdot M x \quad \text{if} \quad \left\{ \begin{array}{l} M \text{ is of function type } A \to B \\ M \text{ is neither an abstraction nor applied.} \end{array} \right. $$

In detailed form the proof is too long to be presented here and we shall only give an outline.

The main observation used in this proof is that if the terms $t_1, ..., t_{k_i}$ above are in $\eta$-expanded form then

$$ q[c_i t_1 \dots t_{k_i}] \stackrel{\beta}{\leftrightarrow} q[c_i t_1'' \dots t_{k_i}'']. $$

E.g., the diagram for 'L' constructor may be closed differently:

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

Since we consider the system with $\eta$-expansions, we need a proof that the system with $\beta\iota$ and $\eta$-expansions is strongly normalising and confluent (we currently have a sketch of this proof).

To prove strong normalisation of the system extended not only by $\eta$ but by $\sigma$-reductions related to icopy we assume that there is an infinite reduction sequence including $\sigma$ reductions.

To use the observation above we need a lemma that shows that this reduction sequence will remain infinite if we insert appropriate $\eta$-expansions (to make the terms $t$ in case (a) $\eta$-expanded).

After that, using a modification of deferment (to take into account the condition that the terms $t$ are $\eta$-expanded) we show that it would be possible to obtain an infinite sequence consisting of $\beta\eta\iota$ only and this contradiction shows that the system with $\sigma$ is SN.

The proof is completed by verification of confluence.
# Acknowledgement

We would like to thank Roberto Di Cosmo for helpful discussions, and Freiric Barral for his help and proofreading.

# 6 Conclusion

The systems based on intensional equality (e.g., many proof assistants) often puzzle mathematically-oriented users because some familiar functional equalities (such as equalities related to commutativity and associativity of product) are no more viewed as computational and their use may require additional and heavy proof development. The arguments in favor of the equality based only on $\beta$-reduction (or even $\beta\eta$) may look nice from the foundational point of view but, pragmatically speaking, there is no harm if an extension of a reduction system doesn't destroy properties such as strong normalisation and confluence.

In this short paper, we studied two cases that seem of interest: extensions of reduction systems related to products and also to "isomorphic" copies of a type.

As for products, using the Deferment Lemma, we were able to prove that adding a rewriting rule corresponding to commutativity of products keeps the calculus strongly normalising and confluent. The same lemma also enabled us to show that adding surjective pairing to the system of $\beta$-reductions does not break normalisation and confluence properties.

Secondly the notion of *isomorphic copy*, is useful for a clean distinction between the multiple uses of the type itself and of its copies. E.g., in proof assistants, the type of Even numbers is often defined as a copy of type Nat together with an appropriate coercion Even $\rightarrow$ Nat. Combining this coercion with the isomorphism copy defined above, we may obtain representations of classes of numbers modulo $2^n$. Furthermore, isomorphic copies of non-algebraic types may require a notion of $\eta$-expansion, and hence to show that $\beta\eta\iota\sigma$-reduction is strongly normalising and confluent.

There are several recent works where normalisation in extended reduction systems is considered (e.g., [22] or [7,8]). This makes the perspective seem quite optimistic.

The calculus we considered here (the simply-typed $\lambda$-calculus with inductive types) is a compromise between the richness provided by inductive constructions and the relative simplicity of simply-typed systems. In the case of dependent types, one will meet more difficulties because new reductions will influence type-equality as well.

The subject needs more investigation but appropriate methods (e.g., a modification of H. Goguen's Typed Operational Semantics, see [18]) will prob-
ably lead to useful results of the same type as presented here.

## References

[1] Baader, F. and T. Nipkow, “Term Rewriting and All That,” Cambridge University Press, New York, 1998.

[2] Bachmair, L. and N. Dershowitz, *Commutation, transformation, and termination*, in: J. H. Siekmann, editor, *Proceedings of the Eighth International Conference on Automated Deduction (Oxford, England)*, Lecture Notes in Computer Science **230** (1986), pp. 5–20.

[3] Barendregt, H. P., “The Lambda Calculus - Its Syntax and Semantics,” North-Holland, Amsterdam, 1984.

[4] Barendregt, H. P., *Lambda calculi with types*, in: D. M. Gabbai, S. Abramsky and T. S. E. Maibaum, editors, *Handbook of Logic in Computer Science*, Oxford University Press, Oxford, 1992.

[5] Barras, B., S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, E. Gimenez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi and B. Werner, *The Coq proof assistant reference manual : Version 6.1*, Technical Report RT-0203, Inria (Institut National de Recherche en Informatique et en Automatique), France (1997).

[6] Barthe, G. and O. Pons, *Type isomorphisms and proof reuse in dependent type theory*, in: F. Honsell and M. Miculan, editors, *Proceedings 4th Int. Conf. on Found. of Software Science and Computation Structures, FoSSaCS’01, Genova, Italy, 2–6 Apr. 2001*, Lecture Notes in Computer Science **2030**, Springer-Verlag, Berlin, 2001 pp. 57–71.

[7] Blanqui, F., J.-P. Jouannaud and M. Okada, *The calculus of algebraic constructions*, in: P. Narendran and M. Rusinowitch, editors, *Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99)* (1999), pp. 301–316.

[8] Blanqui, F., J.-P. Jouannaud and M. Okada, *Inductive-data-type systems*, Theoretical Computer Science **272** (2002), pp. 41–68.

[9] Bruce, K., R. Di Cosmo and G. Longo, *Provable isomorphisms of types*, Technical Report 90-14, LIENS, École Normale Supérieure, Paris (1990).

[10] Dezani-Ciancaglini, M., *Characterization of normal forms possessing inverse in the $\lambda - \beta - \eta$-calculus*, Theoretical Computer Science **2** (1976), pp. 323–337.

[11] Di Cosmo, R., “Isomorphisms of Types: From $\lambda$-Calculus to Information Retrieval and Language Design,” *Progress in Theoretical Computer Science*, Birkhäuser, Boston, MA, 1995.

[12] Di Cosmo, R. and D. Kesner, *Combining algebraic rewriting, extensional lambda calculi, and fixpoints*, Theoretical Computer Science **169** (1996), pp. 201–220.
[13] Doornbos, H. and B. von Karger, *On the union of well-founded relations*, Logic Journal of the IGPL **6** (1998), pp. 195–201.

[14] Dowek, G., G. Huet and B. Werner, *On the definition of the eta-long normal form in type systems of the cube*, in: H. Geuvers, editor, *Informal Proceedings of the Workshop on Types for Proofs and Programs*, Nijmegen, The Netherlands, 1993.

[15] Geser, A., "Relative Termination," Ph.D. thesis, Universität Passau, Passau, Germany (1990).

[16] Geuvers, H., *The Church-Rosser property for βη-reduction in typed λ-calculi*, in: *Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science*, IEEE Computer Society Press, Santa Cruz, California, 1992, pp. 453–460.

[17] Geuvers, H., "Logics and Type Systems," Ph.D. thesis, Computer Science Institute, Katholieke Universiteit Nijmegen (1993).

[18] Goguen, H., *A typed operational semantics for type theory*, LFCS report ECS-LFCS-94-304, University of Edinburgh, Department of Computer Science (1994).

[19] Luo, Z., "Computation and Reasoning: A Type Theory for Computer Science," Number 11 in International Series of Monographs on Computer Science, Oxford University Press, 1994.

[20] Paulin-Mohring, C., *Inductive definitions in the system Coq. Rules and properties*, in: M. Bezem and J. F. Groote, editors, *Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TCLA'93*, Utrecht, The Netherlands, Lecture Notes in Computer Science **664** (1993), pp. 328–345.

[21] Soloviev, S. V., *The category of finite sets and Cartesian closed categories*, in: *Theoretical Applications of Methods of Mathematical Logic III*, Zapiski Nauchnykh Seminarov LOMI **105**, Nauka, Leningrad, 1981 pp. 174–194, english translation in *Journal of Soviet Mathematics*, 22(3) (1983), 1387–1400.

[22] Walukiewicz, D., *Termination of rewriting in the calculus of constructions*, Lecture Notes in Computer Science **1443** (1998).

[23] Werner, B., *Méta-théorie du Calcul des Constructions Inductives*, Thèse Univ. Paris VII, France (1994).