# A non-uniform finitary relational semantics of System T

Lionel Vaux

## ► To cite this version:

Lionel Vaux. A non-uniform finitary relational semantics of System T. RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), 2013, 6th Workshop on Fixed Points in Computer Science (FICS'09), 47 (1), pp.111 - 132. 10.1051/ita/2012031. hal-01264669

HAL Id: hal-01264669

https://hal.science/hal-01264669

Submitted on 2 Feb 2016

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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>
# A NON-UNIFORM FINITARY RELATIONAL SEMANTICS
OF SYSTEM T*

LIONEL VAUX<fnref n="1" />

**Abstract.** We study iteration and recursion operators in the denotational semantics of typed λ-calculi derived from the multiset relational model of linear logic. Although these operators are defined as fixpoints of typed functionals, we prove them finitary in the sense of Ehrhard's finiteness spaces.

**1991 Mathematics Subject Classification.** 03B70, 03D65, 68Q55.

## 1. INTRODUCTION

Since its inception in the late 1960's, denotational semantics has proved to be a valuable tool in the study of programming languages, by recasting the equalities between terms induced by the operational semantics into an more abstract algebraic setting. By the Curry-Howard correspondence between proofs and programs, this concept also provided important contributions to the design of logical systems. Notably, the invention of linear logic by Girard [1] followed from his introduction of coherences spaces as a refinement of Scott's continuous semantics of the λ-calculus [2], moreover taking into account the property of stability put forward by Berry [3].

The design of coherence spaces was moreover largely based on the ideas previously developed by Girard about a quantitative semantics of the λ-calculus [4]: the property that the behaviour of a program is specified by its action on finite approximants of its argument can be related with the fact that analytic functions are given by power series. This suggests interpreting types by particular topological vector spaces, and terms by analytic functions between them: Girard proposed

<footnote>*Keywords and phrases:* Higher order primitive recursion — Denotational semantics</footnote>

<footnote>* This work has been partially funded by the French ANR projet blanc "Curry Howard pour la Concurrence" CHOCO ANR-07-BLAN-0324.</footnote>

<footnote n="1">¹ Institut de Mathématiques de Luminy, CNRS UMR 6206, Marseille, France.</footnote>
such an interpretation using the notion of normal functor, a categorical analogue
of analytic functions.

Applying these ideas in a qualitative setting (i.e. forgetting about coefficients in power series) led Girard to the definition of qualitative domains [5], later refined into coherence spaces. These models, together with the so-called graph models introduced by Engeler, Plotkin and Scott [6], share the following basic idea: one may interpret types as sets, which we will call webs, possibly with some additional structure (order, coherence, etc.); and then one may interpret terms as subsets of the webs of their types, respecting the additional structure (ideals, cliques, etc.).

The properties of the interpretations of programs (continuity, stability, etc.)
are put to use in that they allow the particular morphisms associated with λ-
abstractions to be unambiguously represented by their traces, i.e. sets of (input
bits/output bit)-pairs. Notice the plural in "input bits": intuitively, a program
may need several bits of input information to produce one bit of output. Scott's
continuity roughly means that each bit of output requires only finitely many bits of
input. Berry's stability indicates that each output bit produced by a deterministic
program is characterized by a minimal set of input bits. Girard's linearity specifies
those programs which use exactly one input bit per output bit. Such webbed
models can be refined as models of linear logic, so that every morphism from A
to B becomes a linear morphism from !A to B, where !A stands for the type of
"chunks" of information (precisely those that are sufficient to obtain one output
bit).

The most simple webbed model is the relational one: types are interpreted by
sets without any additional structure, and any subset is (potentially) the interpre-
tation of a term. Linear morphisms from A to B are simply relations, i.e. subsets
of A × B. The exponential modality ! is represented by the finite multiset con-
struction, so that arbitrary morphisms from A to B are relations between finite
multisets over A and elements of B. Despite its apparent simplicity, the relational
model of the λ-calculus thus obtained has many interesting properties: for instance
it is injective on βη-classes [7], and it is closely connected with intersection types
and execution time [8].

Ehrhard introduced finiteness spaces [9] by refining this relational model. A
finiteness space is a set equipped with a finiteness structure, *i.e.* a particular set
of subsets which are said to be finitary; and the model is such that the relational
denotation of a proof in linear logic is always a finitary subset of its conclusion.
The distinctive property of finiteness spaces is that the intersection of two fini-
tary subsets of dual types is always finite. In the associated model of the simply
typed λ-calculus, this feature allowed Ehrhard to reformulate Girard’s quantita-
tive semantics in a standard algebraic setting, where morphisms interpreting typed
λ-terms are analytic functions between the topological vector spaces generated by
vectors with finitary supports. More explicitly:

* the vectors of type *A* are of the form $(v_\alpha)_{\alpha \in |A|}$ where $|A|$ is the web of the associated finiteness space;

* !A is similar to the symmetric algebra on A, in particular |!A| is the set of all finite multisets of elements of |A|;
* an analytic function from A to B is given by a power series:

$$ (f(v))_{\beta} = \sum_{\bar{\alpha} \in !A} f(\bar{\alpha}, \beta) \cdot v^{\bar{\alpha}} $$

where $v^{\bar{\alpha}}$ denotes $\prod_{i=1}^{n} v_{\alpha_i}$ when $\bar{\alpha} = [\alpha_1, \dots, \alpha_n]$;

* considering only vectors with finitary supports ensures the convergence of the previous sum, because it has only finitely many non-zero terms.

This provided the semantic foundations of Ehrhard–Regnier’s differential λ-calculus [10] and motivated the general study of a differential extension of linear logic (e.g., [11–17]).

It is worth noticing that finiteness spaces can accommodate typed λ-calculi only. In particular, we will see the relational semantics of fixpoint combiners is finitary only on empty types: this strengthens a previous remark by Ehrhard. The whole point of the finiteness construction is actually to reject infinite computations, by ensuring the intermediate sets involved in the relational interpretation of a cut are all finite. This contrasts with the purely relational model where the inclusion order defines a cpo on homsets and fixpoints are available at all types — the relational semantics even admits reflexive objects, hence models of the untyped λ-calculus [18, 19]. Despite this restrictive design, Ehrhard was able to define a finitary interpretation of tail-recursive iteration (Section 3 of [9]): this indicates that the finiteness semantics can accommodate a form of typed recursion. This interpretation, however, is not completely satisfactory: tail recursive iteration is essentially linear, thus it does not provide a type of natural numbers in the associated model of the λ-calculus.

The main result of the present paper is that finiteness spaces can actually accommodate the standard notion of primitive recursion in the λ-calculus, Gödel’s system T: we prove Fin admits a weak natural number object in the sense of [20, 21], and we more generally exhibit a finitary recursion operator for this interpretation of the type of natural numbers. This achievement is twofold:

* Before considering finiteness, we must define a recursion operator in the cartesian closed category deduced from the relational model of linear logic. As we have already stated, Ehrhard’s proposition does not match this requirement, which has nothing to do with the finiteness structure: this is essentially due to the fact that the interpretation of natural numbers is flat (in the sense of domains). In fact, a similar effect was already noted by Girard in the design of his coherence semantics of system T [22]: his solution was to propose a lazy interpretation of natural numbers, where laziness refers to the possibility of pattern matching on non normal terms. We adapt Girard’s solution to the purely relational case.

* The second aspect of our work is to establish that this relational semantics is finitary. This is far from immediate because the recursion operator is defined as the union of its finitary approximants, by a fixpoint construction: since the fixpoint operator itself is not a finitary relation, it is necessary to obtain stronger properties of these approximants to deduce finitariness.
Parigot proved by syntactic means that no term in the iterator variant of system *T* could define a valid predecessor operator, *i.e.* a formal inverse of the successor on Church natural numbers [23]. This implies in particular that the recursion operator of system *T* cannot be recovered from the sole iterator. A notable outcome of our relational interpretation of system *T* is that it provides semantic evidence of this gap in expressive power between iterator and recursor (although we did not manage to turn this evidence into a fully new proof).

The present paper takes place in a series of works, aiming to extend the quantitative semantics of the simply typed λ-calculus in vectorial finiteness spaces to functional programming with base types. This would broaden the scope of the already well developed proof theory of differential linear logic: quantitative semantics provides more precise information on cut elimination, and is thus a better guide in the design of syntax than the plain relational interpretation.

Earlier achievements in this direction include Tasson's extension of the algebraic λ-calculus [24] with a type of booleans, together with a semantic characterization of total terms which is proved to be complete on boolean functions [16]. The present work contributes an important step by defining precisely the relational framework in which a quantitative semantics of system T could be developed.

Since such quantitative approaches are known to extend the proofs-as-programs paradigm to parallel [25], non deterministic [26], concurrent [13] or even quantum [27] programming features, our hope is that recasting standard datatypes in this setting will bring interesting new ideas on how to integrate such features within functional programming languages.

## 1.1. STRUCTURE OF THE PAPER

In section 2, we briefly describe two cartesian closed categories: the category *Rel* of sets and multirelations, and the category *Fin* of finiteness spaces and finitary multirelations. In section 3, we give an explicit presentation of the relational semantics of typed λ-calculi in *Rel* and *Fin*, which we extend to system *T* in section 4. In section 5, we establish a uniformity property of iteration-definable morphisms, which does not hold for recursion in general. Finally, we discuss possible further developments of this work.

# 2. SETS, RELATIONS AND FINITENESS SPACES

## 2.1. NOTATIONS

If *A* is a set, we write #*A* for the cardinality of *A*, ℘(*A*) for the powerset of *A* and ℘<sub>*f*</sub>(*A*) for the set of all finite subsets of *A*. We identify multisets of elements of *A* with functions *A* → N. If μ is such a multiset, we write Supp(μ) for its support set {α ∈ *A*; μ(α) ≠ 0}. A finite multiset is a multiset with finite support. We write *A*<sup>1</sup> for the set of all finite multisets of elements of *A*. Whenever (α<sub>1</sub>, ..., α<sub>n</sub>) ∈ *A*<sup>n</sup>, we write $\bar{\alpha} = [\alpha_1, ..., \alpha_n]$ for the corresponding finite multiset: α ∈ *A* ↦ # {i; α<sub>i</sub> = α}. We also write # [α<sub>1</sub>, ..., α<sub>n</sub>] = *n* for the cardinality of
multisets. The empty multiset is [] and we use the additive notation for multiset union, i.e. $\mu + \mu' : \alpha \in A \mapsto \mu(\alpha) + \mu'(\alpha)$.

## 2.2. SETS AND (MULTI-)RELATIONS

Let $f \subseteq A \times B$ be a relation from $A$ to $B$. We write $f^{\perp} = \{(\beta, \alpha); (\alpha, \beta) \in f\}$. For all $a \subseteq A$, we write $f \cdot a$ for the direct image of $a$ by $f$:

$$f \cdot a = \{\beta \in B; \exists \alpha \in a, (\alpha, \beta) \in f\}.$$

We call *multirelation* from $A$ to $B$ any relation from $A^1$ to $B$. We define the category *Rel* of sets and multirelations:

* objects are sets;

* morphisms are multirelations, i.e. $\mathrm{Rel}(A, B) = \mathfrak{P}(A^1 \times B)$;

* the identity on $A$ is $\mathrm{id}_A = \{([\alpha], \alpha); \alpha \in A\}$;

* if $f \in \mathrm{Rel}(A, B)$ and $g \in \mathrm{Rel}(B, C)$ then their composite is $g \circ f = \{(\sum_{i=1}^n \bar{\alpha}_i, \gamma); \exists \bar{\beta} = [\beta_1, \dots, \beta_n] \in B^1, (\bar{\beta}, \gamma) \in g \wedge \forall i (\bar{\alpha}_i, \beta_i) \in f\}$.

This construction can be thought of as follows: $([\alpha_1, \dots, \alpha_p], \beta) \in f$ represents the instance of $f$ which produces the result $\beta$ by consuming the resources $[\alpha_1, \dots, \alpha_p]$. Then the definition of composition is quite natural: to produce $\gamma$, $g$ might consume resources $[\beta_1, \dots, \beta_n]$, each $\beta_i$ being produced by $f$, consuming $\bar{\alpha}_i$; the overall process builds $\gamma$ from $\sum_{i=1}^n \bar{\alpha}_i$.

Let us mention that *Rel* is the co-Kleisli category of the comonad $(-)^{\perp}$ in the relational model of linear logic. Beyond the motivations and general line of work exposed in our introduction, this point is however of marginal interest in the remaining of the paper. The careful reader may nonetheless refer to the addendum of [9] for a formal definition of this model of linear logic.

The category *Rel* is cartesian closed. The cartesian product is given by the disjoint union of sets $A \uplus B = (\{1\} \times A) \cup (\{2\} \times B)$, with terminal object the empty set $\emptyset$. Projections are $\{([1, \alpha]), \alpha; \alpha \in A\} \in \mathrm{Rel}(A \uplus B, A)$ and $\{([2, \beta]), \beta; \beta \in B\} \in \mathrm{Rel}(A \uplus B, B)$. If $f \in \mathrm{Rel}(C, A)$ and $g \in \mathrm{Rel}(C, B)$, pairing is given by: $\langle f, g \rangle = \{(\bar{\gamma}, (1, \alpha)); (\bar{\gamma}, \alpha) \in f\} \cup \{(\bar{\gamma}, (2, \beta)); (\bar{\gamma}, \beta) \in g\} \in \mathrm{Rel}(C, A \uplus B)$. The unique morphism from $A$ to $\emptyset$ is $\emptyset$. The adjunction for closedness is $\mathrm{Rel}(A \uplus B, C) \cong \mathrm{Rel}(A, B^1 \times C)$ which boils down to the bijection $(A \uplus B)^1 \cong A^1 \times B^1$: this is a typical feature of cartesian closed categories derived from models of linear logic by the co-Kleisli construction (see, e.g., the comprehensive survey by Melliès [28]).

Moreover, *Rel* is enriched on cpos: the inclusion of multirelations is a complete partial order.

## 2.3. FINITENESS SPACES AND FINITARY MULTIRELATIONS

The construction of finiteness spaces follows a well established pattern [29]. It is given by the following notion of orthogonality on subsets $a, a' \subseteq A$: $a \perp a'$ iff $a \cap a'$ is finite. Then one unrolls the familiar definitions associated with
biorthogonal closure. We retain only what is necessary for our exposition: for a detailed presentation, the obvious reference is [9].

Let $\mathfrak{F} \subseteq \mathfrak{P}(A)$ be any set of subsets of $A$. We define the pre-dual of $\mathfrak{F}$ in $A$ as $\mathfrak{F}^{\perp} = \{a' \subseteq A; \forall a \in \mathfrak{F}, a \perp a'\}$. We have the following immediate properties: $\mathfrak{F} \subseteq \mathfrak{F}^{\perp\perp}$ and, if $\mathfrak{G} \subseteq \mathfrak{F}$, $\mathfrak{F}^{\perp} \subseteq \mathfrak{G}^{\perp}$. By the last two, we get $\mathfrak{F}^{\perp} = \mathfrak{F}^{\perp\perp}$. Moreover, $\mathfrak{P}_f(A) = \mathfrak{P}(A)^{\perp} \subseteq \mathfrak{F}^{\perp}$. A finiteness structure on $A$ is a set $\mathfrak{F}$ of subsets of $A$ such that $\mathfrak{F}^{\perp\perp} = \mathfrak{F}$. Then a finiteness space is a dependent pair $\mathcal{A} = (|\mathcal{A}|, \mathfrak{F}(\mathcal{A}))$ where $|\mathcal{A}|$ is the underlying set, called the web of $\mathcal{A}$, and $\mathfrak{F}(\mathcal{A})$ is a finiteness structure on $|\mathcal{A}|$. We write $\mathcal{A}^{\perp}$ for the dual finiteness space: $|\mathcal{A}^{\perp}| = |\mathcal{A}|$ and $\mathfrak{F}(\mathcal{A}^{\perp}) = \mathfrak{F}(\mathcal{A})^{\perp}$. The elements of $\mathfrak{F}(\mathcal{A})$ are called the finitary subsets of $\mathcal{A}$.

For every set $A$, $(A, \mathfrak{P}_f(A))$ is a finiteness space and $(A, \mathfrak{P}_f(A))^{\perp} = (A, \mathfrak{P}(A))$. In particular, each finite set $A$ is the web of exactly one finiteness space: $(A, \mathfrak{P}_f(A)) = (A, \mathfrak{P}(A))$. We introduce the empty finiteness space $\mathcal{E} = (\emptyset, \{\emptyset\})$ and the finiteness space of flat natural numbers $\mathcal{N} = (\mathbb{N}, \mathfrak{P}_f(\mathbb{N}))$. If $\mathcal{A}$ and $\mathcal{B}$ are finiteness spaces, we define $\mathcal{A} \& \mathcal{B}$ and $\mathcal{A} \Rightarrow \mathcal{B}$ as follows:

* $|\mathcal{A} \& \mathcal{B}| = |\mathcal{A}| \uplus |\mathcal{B}|$ and $\mathfrak{F}(\mathcal{A} \& \mathcal{B}) = \{a \uplus b; a \in \mathfrak{F}(\mathcal{A}) \wedge b \in \mathfrak{F}(\mathcal{B})\}$;

* $|\mathcal{A} \Rightarrow \mathcal{B}| = |\mathcal{A}|^{\prime} \times |\mathcal{B}|$ and $f \in \mathfrak{F}(\mathcal{A} \Rightarrow \mathcal{B})$ iff $\forall a \in \mathfrak{F}(\mathcal{A}), f \cdot a^{\prime} \in \mathfrak{F}(\mathcal{B})$, and $\forall \beta \in |\mathcal{B}|$, $(f^{\perp} \cdot \{\beta\}) \perp a^{\prime}$.

For instance, setting $\mathcal{S} = \{([k], k+1); k \in \mathbb{N}\}$, we have $\mathcal{S} \in \mathfrak{F}(\mathcal{N} \Rightarrow \mathcal{N})$. It is easily seen that $\mathcal{A} \& \mathcal{B}$ is a finiteness space, but the same result for $\mathcal{A} \Rightarrow \mathcal{B}$ is quite technical [9]. We call finitary multirelations the elements of $\mathfrak{F}(\mathcal{A} \Rightarrow \mathcal{B})$.

Notice that $\mathfrak{F}(\mathcal{A} \Rightarrow \mathcal{B}) \subseteq \mathfrak{Rel}(|\mathcal{A}|, |\mathcal{B}|)$. Moreover the identity $id_{\mathcal{A}} = id_{|\mathcal{A}|}$ is always finitary from $\mathcal{A}$ to itself, and finitary multirelations compose. We write $\mathfrak{Fin}$ for the category of finiteness spaces with $\mathfrak{Fin}(\mathcal{A}, \mathcal{B}) = \mathfrak{F}(\mathcal{A} \Rightarrow \mathcal{B})$ and composition defined as in $\mathfrak{Rel}$. It is cartesian closed with terminal object $\mathcal{E}$, product $\otimes$ and $-$: the definitions of those functors on morphisms, the natural transformations, and the adjunction required for cartesian closedness are exactly the same as for $\mathfrak{Rel}$, applied to the webs of finiteness spaces and to finitary multirelations. By contrast with $\mathfrak{Rel}$, $\mathfrak{Fin}$ is not cpo-enriched: the union of finitary multirelations might not be finitary — see Section 4.2. Again, for reference, the reader may check that $\mathfrak{Fin}$ is the co-Kleisli category of the exponential comonad in the finitary relational model of linear logic, which is detailed in the Section 1 of [9].

# 3. THE MULTiset RELATIONAL SEMANTICS OF TYPED $\lambda$-CALCULI

## 3.1. TYPED $\lambda$-CALCULI

In this section, we give an explicit description of the interpretation in $\mathfrak{Rel}$ and $\mathfrak{Fin}$ of the basic constructions of typed $\lambda$-calculi with products. Type expressions are given by:

$$A, B ::= X \mid A \to B \mid A \times B \mid \top$$
<figure><img src="image_2.png" /><figcaption>FIGURE 1. Rules of typed λ-calculi with products</figcaption></figure>

where X ranges over a fixed set $\mathfrak{A}$ of atomic types. Term expressions are given by:

$$s, t ::= x \mid a \mid \lambda x s \mid s t \mid \langle s, t \rangle \mid \pi_1 s \mid \pi_2 s \mid \rangle$$

where $x$ ranges over term variables and $a$ ranges over term constants. To each variable and to each constant, we associate a type: we write $\mathfrak{C}_A$ for the collection of constants of type $A$, and we assume that every type admits a countably infinite set of variables.

A typing judgement is an expression $\Gamma \vdash s : A$ derived from the rules in Figure 1 where contexts $\Gamma$ and $\Delta$ range over lists $(x_1 : A_1, \dots, x_n : A_n)$ of typed variables. Clearly, if a term $s$ is typable, then its type is uniquely determined, say $A$, and then $\Gamma \vdash s : A$ iff $\Gamma$ contains the free variables of $s$. We denote by $s[x := t]$ the capture avoiding substitution of $t$ for $x$ in $s$.

The operational semantics of a typed λ-calculus is given by a congruence $\simeq$ on typed terms: if $s \simeq t$, then $s$ and $t$ have the same type, say $A$; we then write $\Gamma \vdash s \simeq t : A$ for any suitable $\Gamma$. In general, we will give $\simeq$ as the reflexive, symmetric and transitive closure of a contextual relation $>$ on typed terms. We define $>_0$ as the least one such that: $\pi_i \langle s_1, s_2 \rangle >_0 s_i$ and $(\lambda x s) t >_0 s[x := t]$ (with the obvious assumptions ensuring typability), and we write $\simeq_0$ for the corresponding equivalence.

Pure typed λ-calculi are those with no additional constant or conversion rule: fix a set $\mathfrak{A}$ of atomic types, and write $\Lambda_0^{\mathfrak{A}}$ for the calculus where $\mathfrak{C}_A = \emptyset$ for all $A$, and $s \simeq t$ iff $s \simeq_0 t$.

## 3.2. RELATIONAL INTERPRETATION AND FINITENESS PROPERTY

Assume a set $[[X]]$ is given for each base type $X$; then we interpret type con-
structions by $[[A \to B]] = [[A]]^! \times [[B]]$, $[[A \times B]] = [[A]] \uplus [[B]]$ and $[[\top]] = \emptyset$. Further
assume that with every constant $a \in \mathfrak{C}_A$ is associated a subset $[[a]] \subseteq [[A]]$. The
relational semantics of a derivable typing judgement

$$x_1 : A_1, \dots, x_n : A_n \vdash s : A$$

will be a relation

$$[[s]]_{x_1:A_1, \dots, x_n:A_n} \subseteq [[A_1]]^! \times \dots \times [[A_n]]^! \times [[A]].$$
<figure><img src="image_3.png" /><figcaption>FIGURE 2. Computing the elements of the relational semantics</figcaption></figure>

We first introduce the deductive system of Figure 2, which is a straightforward
adaptation of de Carvalho’s system R [18] to the simply typed case. In this system,
derivable judgements are semantic annotations of typing judgements:

$$
x_1^{\bar{\alpha}_1} : A_1, \dots, x_n^{\bar{\alpha}_n} : A_n \vdash s^{\alpha} : A
$$

stands for

$$
(\bar{\alpha}_1, \dots, \bar{\alpha}_n, \alpha) \in [s]_{x_1:A_1, \dots, x_n:A_n}.
$$

In rules $[[\text{Var}]]$ and $[[\text{Const}]]$, $\Gamma^1$ denotes an annotated context of the form $x_1^1 : A_1, \dots, x_n^1 : A_n$. In rule $[[\text{App}]]$, the sum of annotated contexts is defined pointwise:

$$
(x_1^{\bar{\alpha}_1} : A_1, \dots, x_n^{\bar{\alpha}_n} : A_n) + (x_1^{\bar{\alpha}'_1} : A_1, \dots, x_n^{\bar{\alpha}'_n} : A_n) = (x_1^{\bar{\alpha}''_1} : A_1, \dots, x_n^{\bar{\alpha}''_n} : A_n)
$$

where $\bar{\alpha}''_i = \bar{\alpha}_i + \bar{\alpha}'_i$ for all $i$. The semantics of a term is then simply obtained as
the set of its annotations:

$$
[[s]]_{x_1:A_1, \dots, x_n:A_n} = \{(\bar{\alpha}_1, \dots, \bar{\alpha}_n, \alpha); x_1^{\bar{\alpha}_1} : A_1, \dots, x_n^{\bar{\alpha}_n} : A_n \vdash s^{\alpha} : A\}.
$$

Notice there is no rule for $\langle\rangle$ in Figure 2, hence $[[\langle\rangle]]_\Gamma = \emptyset$ for all $\Gamma$.

**Theorem 3.1 (Invariance).** If $\Gamma \vdash s \cong_0 t : A$ then $[[s]]_\Gamma = [[t]]_\Gamma$.

Proof. We followed the standard interpretation of typed λ-calculi in cartesian closed categories, in the particular case of Rel. A direct proof is also easy, first proving a substitution lemma: if Γ₀, x : A[α₁, ..., αₖ], Δ₀ ⊢ sβ : B, and, for all j ∈ {1, ..., k}, Γⱼ, Δⱼ ⊢ tαⱼ : A, then ∑k j=₀ Γⱼ, ∑k j=₀ Δⱼ ⊢ s[x := t]β : B. □

The relational interpretation also defines a semantics in Fin: assume a finiteness
structure F (X) is given for each atomic type X, so that X* = ([[X]], F(X)) is a
finiteness space, and let (A → B)* = A* ⇒ B*, (A × B)* = A* & B* and ⊤* = E.
Then, further assuming that, for all a ∈ C<sub>A</sub>, [[a]] ∈ F(A*), we obtain:

**Theorem 3.2 (Finiteness).** If $x_1 : A_1, \dots, x_n : A_n \vdash s : A$ then $[[s]]_{x_1:A_1, \dots, x_n:A_n} \in \mathfrak{F}(A_1^* \Rightarrow \dots \Rightarrow A_n^* \Rightarrow A^*)$.
*Proof.* This is a straightforward consequence of the fact that the cartesian closed structure of *Fin* is given by the same morphisms as in *Rel*. A direct proof is also possible, by induction on typing derivations. □

### 3.3. ON THE RELATIONS DENOTED BY λ-TERMS

We have just shown that *Rel* and *Fin* model $\cong_0$ in pure typed λ-calculi. Be aware that if we introduce no atomic type, then the semantics is actually trivial: in $\Lambda_0^0$, all types and terms are interpreted by $\emptyset$.

By contrast, we can consider the internal language $\Lambda_{\text{Rel}}$ of *Rel* in which all relations can be described: fix $\mathfrak{A}$ as the collection of all sets (or a fixed set of sets) and $\mathfrak{C}_A = \mathfrak{P}(\llbracket A \rrbracket)$. Then let $s \cong_{\text{Rel}} t$ iff $\llbracket s \rrbracket_{\Gamma} = \llbracket t \rrbracket_{\Gamma}$, for any suitable $\Gamma$. The point in defining such a language is to enable very natural notations for relations: in general, we will identify closed terms in $\Lambda_{\text{Rel}}$ with the relations they denote in the empty context. For instance, we write $\text{id}_A = \lambda x x$ with $x$ of type $A$; and if $f \in \text{Rel}(A, B)$ and $g \in \text{Rel}(B, C)$, we have $g \circ f = \lambda x (g(f x))$. Similarly, the internal language $\Lambda_{\text{Fin}}$ of *Fin*, where $\mathfrak{A}$ is the collection of all finiteness spaces and $\mathfrak{C}_A = \mathfrak{F}(A^*)$, allows us to denote conveniently all finitary relations.

Before we address the main subject of the paper, system *T*, let's just review some easy examples of usual λ-calculus constructions that can be modelled in *Rel* and *Fin*. First, being cartesian closed categories, they are actually models of pure typed λ-calculi with extensionality, surjective pairing and terminal object: Theorem 3.1 still holds if we add the reductions $\lambda x (u x) >_0 u$, $\langle \pi_1 s, \pi_2 s \rangle >_0 s$ and $v >_0 \langle \rangle$ as soon as $x$ is not free in $u$ and $v$ has type $\top$ (although, in that case, $>_0$ is no longer confluent).

We can also extend the language with particular base types and constants. For instance, we can introduce base type *Bool* together with constants *T* and *F* of type *Bool*, and $D_A$ of type *Bool* $\to A \to A \to A$, with the additional reductions $D T s t > s$ and $D F s t > t$ (we will in general omit the type subscript of such constants and keep the obvious hypotheses on typability implicit) and fix interpretations as follows: let $\mathcal{B}$ a finiteness space with a two element web $|\mathcal{B}| = \{\texttt{t}, \texttt{ff}\}$; then let $\texttt{Bool}^* = \mathcal{B}$, $\llbracket \texttt{T} \rrbracket = \{\texttt{t}\}$, $\llbracket \texttt{F} \rrbracket = \{\texttt{ff}\}$ and $\llbracket D_A \rrbracket = \mathcal{D}_A = \{([\texttt{t}], [\alpha], []$; $\alpha \in |A^*|$} \cup \{([\texttt{ff}], []$; [\alpha], \alpha)$; $\alpha \in |A^*|$}. That these interpretations are finitary should be clear. Then one retains that $\Gamma \vdash s \cong t : A$ implies $\llbracket s \rrbracket_{\Gamma} = \llbracket t \rrbracket_{\Gamma}$. But the essential point is that this semantics is internal: in $\Lambda_{\text{Rel}}$ and $\Lambda_{\text{Fin}}$, $x : A, y : A \vdash D_A \mathcal{T} xy \cong x : A$ and $x : A, y : A \vdash D_A \mathcal{F} xy \cong y : A$. This means that booleans interact as expected with all relations of appropriate types and not just with those derived from λ-terms.

Much more structure can be revealed in *Rel* and *Fin*, with computational counterparts in $\Lambda_{\text{Rel}}$ and $\Lambda_{\text{Fin}}$. Most importantly, the semantics of the λ-calculus in *Fin* lead Ehrhard and Regnier to the definition of the differential λ-calculus in [10]. One can present this calculus in the current framework by introducing, for all types *A* and *B*, a new constant $\text{Diff}_{A,B}$ of type $(A \to B) \to A \to A \to B$ subject to a new reduction rule $(\text{Diff} \, \lambda x \, s) t > \lambda x (\frac{\partial s}{\partial x} \cdot t)$ where $\frac{\partial s}{\partial x} \cdot t$ is the linearized version of substitution defined in [10].
3.4. SYSTEM *T*

The main contribution of the present paper is to establish that Fin models Gödel’s system *T*, which can be presented in various ways. The iterator version of system *T* is the typed λ-calculus with an atomic type Nat of natural numbers, and constants O of type Nat (corresponding to zero), S of type Nat → Nat (corresponding to successor) and for every type A, I<sub>A</sub> of type Nat → (A → A) → A → A, subject to the following additional conversions: I<sub>O</sub> uv > v and I<sub>(St)</sub> uv > u (I<sub>tuv</sub>). The recursor variant is similar, but the iterator is replaced with R<sub>A</sub> of type Nat → (Nat → A → A) → A → A subject to conversions R<sub>O</sub> uv > v and R<sub>(St)</sub> uv > ut(R<sub>tuv</sub>). Yet another possible system is obtained with tail recursive iteration: take J<sub>A</sub> of type Nat → (A → A) → A → A and let J<sub>O</sub> uv > v and J<sub>(St)</sub> uv > J<sub>tu</sub> (uv).

These systems allow us to represent exactly the same functions on the set of
natural numbers, where the number *n* is denoted by *S*<sup>*n*</sup> O: this is the consequence
of a normalization theorem (see [22]). Notice in particular that, when applied to
a canonical integer, I and J coincide: I(S<sup>*n*</sup> O)uv ≃ J(S<sup>*n*</sup> O)uv ≃ u<sup>*n*</sup> v; this does
not hold for all terms of type Nat, however (consider, e.g., a variable of type Nat).
Moreover, we can define a recursor using iteration and products with the standard
encoding rec = λx λy λz π₁(Ix (λw ⟨y (π₂w) (π₁w), S(π₂w)⟩) ⟨z, O⟩), and we get
rec(S<sup>*n*</sup> O)uv ≃ R(S<sup>*n*</sup> O)uv: the idea is to reconstruct the integer argument on the
fly. But this encoding is valid only for ground terms of type Nat: rec (St) uv ≃
ut (rect uv) holds only if we suppose *t* is of the form S<sup>*n*</sup> O, or reduces to such
a term (notice we could as well use J in the definition of rec). By contrast, the
encoding of the iterator by iter = λx λy λz (Rx (λx'y) z) is extensionally valid:
iter O uv ≃ v and iter (St) uv ≃ u (iter t uv) for all t, u, v.

The fact that one direction of the encoding holds only on ground terms in-
dicate that the algorithmic properties of both systems may differ. And these
differences will appear in the semantics (see Section 5). Also, recall the dis-
cussion in our introduction: the tail recursive variant of iterator, J subject to
J(St) uv > Jtu(uv), uses its integer argument linearly. This enabled Ehrhard
to define a semantics of iteration, with Nat* = N = (N, ℘<sub>f</sub>(N)), [[O]] = O = {0}
and [[S]] = S = {[n], n + 1); n ∈ N}. Such an interpretation of natural numbers,
however, fails to provide a semantics of I or R, in Rel or Fin.

**Lemma 3.3.** *Assume [[Nat]] = |N|, [[O]] = O and [[S]] = S, and let A be any type such that [[A]] ≠ ∅. Then there is no I<sub>A</sub> ⊆ [[Nat] → (A → A) → A → A] such that, setting [[I<sub>A</sub>]] = I<sub>A</sub>, we obtain [[I O uv]]<sub>Γ</sub> = [[v]]<sub>Γ</sub> and [[I (St) uv]]<sub>Γ</sub> = [[u (I t uv)]]<sub>Γ</sub> as soon as Γ ⊢ t : Nat, Γ ⊢ u : A → A and Γ ⊢ v : A.*

*Proof.* By contradiction, assume the above equations hold. We can then derive the following in Λ<sub>Rel</sub>: λx λy (I O (λz x) y) ≃ λx λy y and, observing that ∅ ⊆ N, λx λy (I (S ∅) (λz x) y) ≃ λx λy x. Since moreover S ∅ ≃ ∅, and the semantics is monotonic for relation inclusion, we obtain: λx λy (I (S ∅) (λz x) y) ≃ λx λy (I ∅ (λz x) y) ⊆ λx λy (I O (λz x) y). We conclude that [[λx λy x]]<sub>x:A,y:A</sub> ⊆ [[λx λy y]]<sub>x:A,y:A</sub> for every type A, which obviously fails as soon as [[A]] ≠ ∅. □
# 4. A FINITARY RELATIONAL INTERPRETATION OF PRIMITIVE RECURSION

## 4.1. LAZY NATURAL NUMBERS

We say a multirelation from $A$ to $B$ is:

* linear if it contains only elements of the form $([\alpha], \beta)$;

* affine if it contains only elements of the form $([\alpha], \beta)$ or $([\emptyset], \beta)$;

* strict if it contains no element of the form $([\emptyset], \beta)$.

In the proof of Lemma 3.3, $S\emptyset = \emptyset$ holds because $S$ is linear, hence strict. This reflects the general fact that, if $s$ is a strict multirelation from $A$ to $B$ then, for all $t \in \text{Rel}(B, C)$, $([\emptyset], \gamma)$ in $t \circ s$ iff $([\emptyset], \gamma) \in t$. Such a phenomenon was also noted by Girard in his interpretation of system $T$ in coherence spaces [22]. His evidence that there was no interpretation of the iteration operator using the linear successor relied on a coherence argument. The previous lemma is stronger: it holds in any webbed model as soon as the interpretation of successor is strict.

In short, strict morphisms cannot produce anything *ex nihilo*; but the successor of any natural number should be marked as non-zero, for the iterator to distinguish between both cases. Hence the successor should not be strict: similarly to Girard's solution, we will interpret *Nat* by so-called *lazy* natural numbers. Let $\mathcal{N}_l = (|\mathcal{N}_l|, \mathfrak{P}_f(|\mathcal{N}_l|))$ be such that $|\mathcal{N}_l| = \mathbf{N} \cup \mathbf{N}^>$, where $\mathbf{N}^>$ is just a disjoint copy of $\mathbf{N}$. The elements of $\mathbf{N}^>$ are denoted by $k^>$, for $k \in \mathbf{N}: k^>$ represents a partial number, not fully determined but strictly greater than $k$. If $\nu \in |\mathcal{N}_l|$, we define $\nu^+$ as $k+1$ if $\nu = k$ and $(k+1)^> > \nu = k^>$. Then we set $S_l = \{([\emptyset], 0^>)\} \cup \{([\nu], \nu^+); \nu \in |\mathcal{N}_l|\}$, which is affine. Notice that $O \in \mathfrak{F}(\mathcal{N}_l)$ and $S_l \in \mathfrak{F}(\mathcal{N}_l \Rightarrow \mathcal{N}_l)$.

We will show that these allow us to provide an interpretation of recursion, hence iteration, in system $T$: for all finiteness space $\mathcal{A}$, there exists

$$ \mathcal{R}_{\mathcal{A}} \in \mathfrak{F}(\mathcal{N}_l \Rightarrow (\mathcal{N}_l \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}) \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}) $$

such that, in $\Lambda_{\text{Fin}}$,

$$ y : \mathcal{N}_l \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}, z : \mathcal{A} \vdash \mathcal{R} O y z \simeq z : \mathcal{A} $$

and

$$ x : \mathcal{N}_l, y : \mathcal{N}_l \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}, z : \mathcal{A} \vdash \mathcal{R} (S_l x) y z \simeq y x (\mathcal{R} x y z) : \mathcal{A}. $$

## 4.2. FIXPOINTS

For all finiteness space $\mathcal{A}$, write $\text{Rec}[\mathcal{A}] = \mathcal{N}_l \Rightarrow (\mathcal{N}_l \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}) \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}$. We want to introduce a recursion operator $\mathcal{R}_{\mathcal{A}} \in \mathfrak{F}(\text{Rec}[\mathcal{A}])$ intuitively subject to the following definition:

$$ \mathcal{R} t u v = \text{match } t \text{ with } \left\{ \begin{array}{l} O \quad \mapsto v \\ S t' \quad \mapsto u t' (\mathcal{R} t' u v) \end{array} \right. . $$
This definition is recursive, and a natural method to obtain such an operator is as the fixpoint of

$$ \mathit{Step} = \lambda\mathcal{X} \lambda x \lambda y \lambda z \left( \begin{array}{l} \text{match } x \text{ with } \left\{ \begin{array}{rcl} \mathsf{O} & \mapsto & z \\ \mathsf{S} x' & \mapsto & y x' (\mathcal{X} x' y z) \end{array} \right. \end{array} \right). $$

The cartesian closed category Rel is cpo-enriched, the order on morphisms being inclusion. Hence it has fixpoints at all types: for all set A and $f \in \mathbf{Rel}(A, A)$, the least fixpoint of f is $\bigcup_{k \ge 0} f^k \emptyset$, which is an increasing union. The least fixpoint operator is itself definable as the supremum of its approximants, $\mathcal{F}ix_A = \bigcup_{k \ge 0} \mathcal{F}ix_A^{(k)}$, where $\mathcal{F}ix_A^{(0)} = \emptyset$ and $\mathcal{F}ix_A^{(k+1)} = \lambda f (f (\mathcal{F}ix_A^{(k)} f))$. More explicitly, $\mathcal{F}ix_A^{(k+1)} = \{([([\alpha_1, \dots, \alpha_n], \alpha)] + \sum_{i=1}^n \bar{\varphi}_i, \alpha); \forall i, (\bar{\varphi}_i, \alpha_i) \in \mathcal{F}ix_A^{(k)}\}$: the reader may check that this equation holds by inspecting all the possible annotations of $\lambda f (f (a f))$ by the rules of Figure 2, where a is any constant of type $(A \to A) \to A$. Intuitively, the pair $([\alpha_1, \dots, \alpha_n], \alpha)$ corresponds to the head instance of f in $f (a f)$, while each $\bar{\varphi}_i$ holds the instances of f used by a in order to produce $\alpha_i$ in the recursive call $(a f)$.

Notice that these approximants are finitary: if $\mathcal{A}$ is a finiteness space then, for all $k$, $\mathcal{F}ix_A^{(k)} = \mathcal{F}ix_{A|\mathcal{A}}^{(k)} \in \mathfrak{F}((\mathcal{A} \Rightarrow \mathcal{A}) \Rightarrow \mathcal{A})$. The fixpoint, however, is not finitary in general: for instance $\mathcal{F}ix S_l = \mathbf{N}^> \notin \mathfrak{F}(N_l)$ hence $\mathcal{F}ix \notin \mathfrak{F}((N_l \Rightarrow N_l) \Rightarrow N_l)$. In fact $\mathcal{F}ix \in \mathfrak{F}((\mathcal{A} \Rightarrow \mathcal{A}) \Rightarrow \mathcal{A})$ only for the empty type $\mathcal{A} = \mathcal{E}$:

**Lemma 4.1.** If $|\mathcal{A}| \ne \emptyset$, then $\mathcal{F}ix \notin \mathfrak{F}((\mathcal{A} \Rightarrow \mathcal{A}) \Rightarrow \mathcal{A})$.

*Proof.* Let $\alpha \in |\mathcal{A}|$ and $f = \{([], \alpha)\} \cup \{([\alpha], \alpha)\} \in \mathfrak{P}_f(\mathcal{A} \Rightarrow \mathcal{A}) \subseteq \mathfrak{F}(\mathcal{A} \Rightarrow \mathcal{A})$. Observe that $([([], \alpha], \alpha) \in \mathcal{F}ix^{(1)}, ([([], \alpha), ([\alpha], \alpha], \alpha) \in \mathcal{F}ix^{(2)}, \text{ and more generally } ([([], \alpha)] + n ([\alpha], \alpha], \alpha) \in \mathcal{F}ix^{(n+1)}). Hence $f^1 \cap (\mathcal{F}ix^{\perp} \cdot \{\alpha\})$ is infinite although $f \in \mathfrak{F}(\mathcal{A} \Rightarrow \mathcal{A})$, which contradicts the definition of finitary multirelations. $\square$

This result indicates that the finitary semantics refuses infinite computations and will not accommodate general recursion. It is thus very natural to investigate the nature of the algorithms that can be studied in a finitary setting, hence our interest in typed recursion and system T. So we proceed in two steps: we first introduce the finitary approximants $\mathcal{R}_A^{(k)} \in \mathfrak{F}(\mathrm{Rec}[\mathcal{A}])$ by $\mathcal{R}_A^{(k)} = \mathit{Step}_A^k \emptyset$, then we prove $\mathcal{R}_A = \bigcup_{k \ge 0} \mathcal{R}_A^{(k)} \in \mathfrak{F}(\mathrm{Rec}[\mathcal{A}])$.

On a side note, recall that coherence spaces accommodate fixpoints without difficulty [22]: in particular, the coherence semantics of system T is very similar to the relational interpretation we give in the following. By contrast, the finiteness property is completely new. We will moreover show in section 5 that, despite its similarity with the coherence semantics, the relational interpretation itself brings new light on the nature of iteration and recursion, which would not be accessible in the uniform setting of coherence spaces.
### 4.3. PATTERN MATCHING ON LAZY NATURAL NUMBERS

We introduce a finitary operator *Case*, intuitively defined as:

$$ \mathit{Case}_{t} uv = \mathit{match} \ t \ with \ \left\{ \begin{array}{rcl} \mathbf{O} & \mapsto & v \\ \mathbf{S} t' & \mapsto & ut' \end{array} \right. . $$

More formally:

**Definition 4.2.** If $\bar{v} = [\nu_1, \dots, \nu_k] \in |\mathcal{N}_l|^!$, we write $\bar{v}^+ = [\nu_1^+, \dots, \nu_n^+]$. Then for all set $A$, let

$$ \mathit{Case}_A = \left\{ \begin{array}{l} \{([0], \llbracket \alpha \rrbracket, \alpha); \alpha \in A\} \\ \cup \{([0^>], \bar{v}^+, \llbracket \bar{v}, \alpha \rrbracket, \llbracket \alpha \rrbracket); \bar{v} \in |\mathcal{N}_l|^! \wedge \alpha \in A\}. \end{array} \right. $$

**Lemma 4.3.** *The operator *Case* performs pattern matching on natural numbers:*

$$ y : \mathcal{N}_l \Rightarrow A, z : A \vdash \mathit{Case} \ O y z \simeq z : A $$

and

$$ x : \mathcal{N}_l, y : \mathcal{N}_l \Rightarrow A, z : A \vdash \mathit{Case} (S_l x) y z \simeq y x : A. $$

Moreover, pattern matching is finitary:

$$ \mathit{Case}_A = \mathit{Case}_{|A|} \in \mathfrak{F} (\mathcal{N}_l \Rightarrow (\mathcal{N}_l \Rightarrow A) \Rightarrow A \Rightarrow A). $$

*Proof.* That the equations hold is by now a routine exercise. To prove that *Case* is finitary, we check the definition of $\mathfrak{F}(\Rightarrow \Rightarrow)$). For the first direction: for all $n \in \mathfrak{F}(\mathcal{N}_l)$, $\mathit{Case}_n \subseteq \{([], [\alpha], \alpha); \alpha \in |A|\} \cup \{([\bar{v}, \alpha], \llbracket \alpha \rrbracket); \bar{v}^+ \in n' \wedge \alpha \in |A|\}$; hence, setting $n' = \{\nu; \nu^+ \in n\} \in \mathfrak{F}(\mathcal{N}_l)$, we obtain $\mathit{Case}_n \subseteq (\lambda y \lambda z z) \cup (\lambda y \lambda z (y n'))$, and we conclude since the union of two finitary subsets is finitary. In the reverse direction, we prove that, for all $\gamma \in (\mathcal{N}_l \Rightarrow A) \Rightarrow A \Rightarrow A|$, setting $N' = \mathit{Case}^{\perp} \cdot \{\gamma\}$, $n' \cap N'$ is finite: this is immediate because $N'$ has at most one element (by the definition of *Case*). $\square$

### 4.4. A RELATIONAL RECURSOR

We introduce the relation $\mathcal{R}$ as the fixpoint of *Step*.

**Definition 4.4.** *Fix a set A. Let*

$$ \mathit{Step}_A = \lambda \mathcal{X} \lambda x \lambda y \lambda z (\mathit{Case}_A x (\lambda x' (y x' (\mathcal{X} x' y z)))) z $$

and, for all $k \in \mathbb{N}$, let $\mathcal{R}_A^{(k)} = \mathit{Step}_A^k \emptyset$. Then we define $\mathcal{R}_A = \bigcup_{k \ge 0} \mathcal{R}_A^{(k)}$, and fix $\llbracket \mathbb{R} \rrbracket = \mathcal{R}$.
**Lemma 4.5.** For all finiteness space $\mathcal{A}$, $Step_{\mathcal{A}} = Step_{|\mathcal{A}|} \in \mathfrak{F}(\text{Rec}[\mathcal{A}] \Rightarrow \text{Rec}[\mathcal{A}])$ and, for all $k$, $\mathcal{R}_{\mathcal{A}}^{(k)} = \mathcal{R}_{|\mathcal{A}|}^{(k)} \in \mathfrak{F}(\text{Rec}[\mathcal{A}])$. Moreover, we have: $\mathcal{R}_{\mathcal{A}}^{(0)} = \emptyset$ and

$$ \mathcal{R}_{\mathcal{A}}^{(k+1)} = \{([0], \emptyset], [\alpha], \alpha); \alpha \in |\mathcal{A}|\} \cup \{([0]^>, + \sum_{i=0}^n \bar{\nu}_i^+, [(\bar{\nu}_0, [\alpha_1, \dots, \alpha_n], \alpha)] + \sum_{i=1}^n \bar{\varphi}_i, \sum_{i=1}^n \bar{\alpha}_i, \alpha); \\ \forall i, (\bar{\nu}_i, \bar{\varphi}_i, \bar{\alpha}_i, \alpha_i) \in \mathcal{R}_{\mathcal{A}}^{(k)}\}. $$

*Proof.* The finiteness of the approximants follows from Theorem 3.2. The explicit description of $\mathcal{R}_{\mathcal{A}}^{(k)}$ is a direct application of the definition of the relational semantics. $\square$

**Theorem 4.6 (Correctness).** For all suitable $\Gamma$ and $\Delta$, $[[\mathbb{R} \circled y z]]_{\Gamma} = [[z]]_{\Gamma}$ and $[[\mathbb{R}(\mathbb{S} x) y z]]_{\Delta} = [[y x (\mathbb{R} \circled y z)]]_{\Delta}$.

*Proof.* This follows directly from Lemma 4.3 and the fact that $\mathcal{R} = Step_{\mathcal{R}}$. $\square$

## 4.5. FINITENESS

It only remains to prove $\mathcal{R}$ is finitary. Following the definition of $(- \Rightarrow -)$, we proceed in two steps: the image of a finitary subset of $N_l$ is finitary; conversely, the preimage of a singleton is “anti-finitary”.

**Definition 4.7.** If $n \in \mathfrak{F}(N_l)$, we set $\max(n) = \max\{k; k \in n \lor k^> \in n\}$, with the convention $\max(\emptyset) = 0$. Then if $\bar{\nu} \in |N_l|!$ we set $\max(\bar{\nu}) = \max(\text{Supp}(\nu))$, and if $N \subseteq n!$ for some $n \in \mathfrak{F}(N_l)$, $\max(N) = \max(\bigcup_{\bar{\nu} \in N} \text{Supp}(\bar{\nu}))$.

**Lemma 4.8.** For all $\gamma = (\bar{\nu}, \bar{\varphi}, \bar{\alpha}, \alpha) \in \mathcal{R}_{\mathcal{A}}$, $\gamma \in \mathcal{R}_{\mathcal{A}}^{(\max(\bar{\nu})+1)}$.

*Proof.* By induction on $\max(\bar{\nu})$, using Lemma 4.5. $\square$

**Lemma 4.9.** If $n \in \mathfrak{F}(N_l)$, then $\mathcal{R}_{\mathcal{A}} n \in \mathfrak{F}((N_l \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}) \Rightarrow \mathcal{A} \Rightarrow \mathcal{A})$.

*Proof.* The previous Lemma entails $\mathcal{R}_{\mathcal{A}} n = \mathcal{R}_{\mathcal{A}}^{(\max(n)+1)} n$. We conclude recalling that $\mathcal{R}_{\mathcal{A}}^{(\max(n)+1)} \in \mathfrak{F}(\text{Rec}[\mathcal{A}])$. $\square$

**Definition 4.10.** For all $\bar{\varphi} = [(\bar{\nu}_1, \bar{\alpha}_1, \alpha_1), \dots, (\bar{\nu}_k, \bar{\alpha}_k, \alpha_k)] \in |N_l \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}|!$, let $\diamond\bar{\varphi} = \sum_{j=1}^k \#\bar{\nu}_j$.

**Lemma 4.11.** If $(\bar{\nu}, \bar{\varphi}, \bar{\alpha}, \alpha) \in \mathcal{R}_{\mathcal{A}}$, then $\#\bar{\nu} = \#\bar{\alpha} + \#\bar{\varphi} + \diamond\bar{\varphi}$.

*Proof.* Using Lemma 4.5, the result is proved for all $(\bar{\nu}, \bar{\varphi}, \bar{\alpha}, \alpha) \in \mathcal{R}_{\mathcal{A}}^{(k)}$, by induction on $k$. $\square$

**Theorem 4.12 (The recursion operator is finitary).** $\mathcal{R}_{\mathcal{A}} \in \mathfrak{F}(\text{Rec}[\mathcal{A}])$.

*Proof.* By Lemma 4.9, we are left to prove that, for all $n \in \mathfrak{F}(N_l)$ and $\gamma = (\bar{\varphi}, \bar{\alpha}, \alpha) \in |(N_l \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}) \Rightarrow \mathcal{A} \Rightarrow \mathcal{A}|$, $N = n! \cap (\mathcal{R}^{\perp} \cdot \{\gamma\})$ is finite. But by Lemma 4.11,

$$ N \subseteq \{\bar{\nu} \in |N_l|!; \#\bar{\nu} = \#\bar{\alpha} + \#\bar{\varphi} + \diamond\bar{\varphi} \land \max(\bar{\nu}) \le \max(n)\} $$
which is finite.

☐

**Remark 4.13.** We keep calling $\mathcal{R}$ “the” recursion operator, but notice such an operator is not unique in *Rel* or *Fin*: let $\text{Case}'_A = \{([0,0], \emptyset, [\alpha], \alpha); \alpha \in A\} \cup \{([0^>]+\bar{\nu}^+, [[\bar{\nu},\alpha)], \emptyset, \alpha); \bar{\nu} \in |N_l'| \wedge \alpha \in A\}$, for instance; this variant of matching operator behaves exactly like *Case*, and one can reproduce our construction of the recursor based on that. This is to be related with the fact that neither *Rel* nor *Fin* admit coproducts: in other terms, there is no canonical way to implement sum types and pattern matching in these categories.

# 5. ABOUT ITERATION

## 5.1. A WEAK NATURAL NUMBER OBJECT

We have just provided a semantics of system *T* with recursor. Now let $\mathcal{I}_A = \lambda x \lambda y \lambda z (\mathcal{R}_A x (\lambda x' y) z)$ for all set *A*. By Theorem 4.12, $\mathcal{I}_A = \mathcal{I}_{|A|} \in \mathfrak{F}(\text{Iter}[A])$, where $\text{Iter}[A] = N_l \Rightarrow (A \Rightarrow A) \Rightarrow A \Rightarrow A$. Moreover, by Theorem 4.6 this defines an iteration operator and we obtain that the triple $(|N_l|, \mathcal{O}, S_l)$, resp. $(N_l, \mathcal{O}, S_l)$, is a weak natural number object [20,21] in the cartesian closed category *Rel*, resp. *Fin*. Indeed:

**Lemma 5.1.** For all $f \in \text{Fin}(A, A)$ and all $a \in \mathfrak{F}(A)$, there exists $h \in \text{Fin}(N_l, A)$ such that $h \mathcal{O} = a$ and $h \circ S_l = f \circ h$.

*Proof.* Take $h = \lambda x (\mathcal{I} x f a)$. ☐

☐

According to Remark 4.13, there is no hope of finding a strong natural number object in these categories, i.e. to require *h* to be unique in the above lemma.

We could also have introduced $\mathcal{I}$ by a construction similar to that of $\mathcal{R}$:

**Definition 5.2.** Let

$$ \mathcal{I}tStep = \{ \lambda\mathcal{X} \lambda x \lambda y \lambda z (\mathcal{Case} x (\lambda x' (y (\mathcal{X} x' y z)))) z \} \\ \in \mathfrak{F}(\text{Iter} \Rightarrow \text{Iter}) $$

and, for all $k \in \mathbb{N}$, $\mathcal{I}^{(k)} = \mathcal{I}tStep^k \emptyset \in \mathfrak{F}(\text{Iter})$.

**Lemma 5.3.** The relations $\mathcal{I}_A^{(k)}$ are given by: $\mathcal{I}_A^{(0)} = \emptyset$ and

$$ \mathcal{I}_A^{(k+1)} = \{([0], \emptyset, [\alpha], \alpha); \alpha \in |A|\} \cup \\ \left\{ ([0^>]+\sum_{i=1}^n \bar{\nu}_i^+, [[\alpha_1, \dots, \alpha_n], \alpha]) + \sum_{i=1}^n \bar{\varphi}_i, \sum_{i=1}^n \bar{\alpha}_i, \alpha); \\ \forall i, (\bar{\nu}_i, \bar{\varphi}_i, \bar{\alpha}_i, \alpha_i) \in \mathcal{I}_A^{(k)} \right\}. $$

*Proof.* Again, routine exercise. ☐

☐

**Lemma 5.4.** We have $\bigcup_{k \ge 0} \mathcal{I}_A^{(k)} = \mathcal{I}_A$.

*Proof.* Check that, for all $k$, $\mathcal{I}^{(k)} = \lambda x \lambda y \lambda z (\mathcal{R}^{(k)} x (\lambda x' y) z)$. ☐

☐
## 5.2. UNIFORMITY OF ITERATION

We now develop a semantic investigation of the gap in expressive power between iteration and recursion, which was formally established by Parigot [23].

One distinctive feature of the (pure or finitary) relational model is non-uniformity: if $a, a' \in \mathfrak{F}(\mathcal{A})$ then $a \cup a' \in \mathfrak{F}(\mathcal{A})$; and in the construction of $a'$, there is no restriction on the elements of the multisets we consider. It is very different from the setting of coherence spaces for instance. But we can show the iterator only considers uniform sets of lazy numbers, in the following sense: if $k \in \mathbb{N}$, we define $\underline{k} = S_l^k \mathcal{O} = \{l^> ; l < k\} \cup \{k\} \in \mathfrak{F}(\mathcal{N}_l)$; we say $n \subseteq |\mathcal{N}_l|$ is uniform if $n \subseteq \underline{k}$ for some $k$. Notice that, in the coherence space of lazy natural numbers used by Girard in [22] to interpret system $T$, the sets $\underline{k}$ are the finite maximal cliques: coherence is given by $k \asymp l$ iff $k = l$, $k \asymp l^>$ iff $k > l$ and $k^> \asymp l^>$ for all $k, l$. The only infinite maximal clique is $\mathbb{N}^>$ which is not finitary (recall this is the fixpoint of $S_l$). We prove $\mathcal{I}$ considers only uniform sets of lazy numbers.

Let $\mathit{Stage}_A^{(0)} = \{([0], [], [\alpha], \alpha); \alpha \in |\mathcal{A}|\}$ and, for all $k \in \mathbb{N}$,

$$ \mathit{Stage}_A^{(k+1)} = \{([0], [], [\alpha], \alpha); \alpha \in |\mathcal{A}|\} \cup \left\{ ( [0^> ] + \sum_{i=1}^n \bar{\nu}_i^+ , [[\alpha_1, \dots, \alpha_n], \alpha)] + \sum_{i=1}^n \bar{\varphi}_i, \sum_{i=1}^n \bar{\alpha}_i, \alpha); \right. \\ \left. \forall i, (\bar{\nu}_i, \bar{\varphi}_i, \bar{\alpha}_i, \alpha_i) \in \mathit{Stage}_A^{(k)} \right\}. $$

Setting $\mathit{Stage}_A^{(-1)} = \emptyset$, one can check that $\mathit{Stage}_A^{(k-1)} \subseteq \mathcal{I}_A^{(k)} \subseteq \mathit{Stage}_A^{(k)}$ for all $k$, and then $\mathcal{I}_A = \bigcup_{k \ge 0} \mathit{Stage}_A^{(k)}$.

**Lemma 5.5.** If $\mathcal{A} \neq \mathcal{E}$ then, for all $k \in \mathbb{N}$,

$$ \bigcup \{ \text{Supp}(\bar{\nu}) ; \exists(\bar{\varphi}, \bar{\alpha}, \alpha), (\bar{\nu}, \bar{\varphi}, \bar{\alpha}, \alpha) \in \mathit{Stage}_A^{(k)} \setminus \mathit{Stage}_A^{(k-1)} \} = \underline{k}. $$

*Proof.* The first inclusion ($\subseteq$) is easy by induction on $\underline{k}$. For the reverse ($\supseteq$), check that $([0^>, 1^>, \dots, (k-1)^>, k], (k-1) [[\alpha], \alpha], [\alpha], \alpha) \in \mathit{Stage}_A^{(k)} \setminus \mathit{Stage}_A^{(k-1)}$ for all $\alpha \in |\mathcal{A}|$. $\square$

As a consequence, for all $(\bar{\nu}, \bar{\varphi}, \bar{\alpha}, \alpha) \in \mathcal{I}$, $\text{Supp}(\bar{\nu})$ is uniform. Of course, no such property holds for $\mathcal{R}$, because

$$ \mathcal{R}_A^{(1)} \supseteq \{ ([0^>] + \bar{\nu}^+, [[\bar{\nu}, [], \alpha], [], \alpha); \alpha \in |\mathcal{A}| \wedge \bar{\nu} \in |\mathcal{N}_l|^! \}. $$

Actually, this non-uniformity of recursion is not related with our specific choice of the interpretation of $\mathbb{R}$. Rather, it follows from the fact that, in the equation $\mathbb{R}(\mathcal{S}t)uv \simeq ut(\mathbb{R}tuv)$, $u$ can take arbitrary arguments. Let us make this remark precise:

**Lemma 5.6.** Fix a set $\mathcal{A} \neq \emptyset$, $\alpha \in \mathcal{A}$ and let $r$ be a relation of type $|\mathcal{N}_l| \to (|\mathcal{N}_l| \to \mathcal{A} \to \mathcal{A}) \to \mathcal{A} \to \mathcal{A}$, such that $r(S_l t) uv \simeq ut(r t uv)$ for all terms $t$, $u$ and $v$ of suitable type in $\Lambda_{\text{Rel}}$. Then, for all $\bar{\nu} \in |\mathcal{N}_l|^!$, $r$ admits an element of the form $(\bar{\nu}^+ + [0^>, \dots, 0^>], \bar{\phi}, [], \alpha) \in r$.
**Proof.** Fix $\alpha \in A$ and let $f = \{(\bar{\nu}, \llbracket \alpha \rrbracket)\}$, which is a singleton relation of type $|\mathcal{N}_l| \to A \to A$. Then, if $x$ is a variable of type $|\mathcal{N}_l|$, $r(S_l x) f \emptyset \simeq f x (r x f \emptyset)$ holds in $\Lambda_{\text{Rel}}$. Now observe that, by the definition of $f$, $\llbracket f x (r x f \emptyset) \rrbracket_{x:|\mathcal{N}_l|} = \{(\bar{\nu}, \alpha)\}$. Hence $x^{\bar{\nu}} : |\mathcal{N}_l| \vdash (r(S_l x) f \emptyset)^{\alpha} : A$. By inspecting the rules of Figure 2, we necessarily have $x^{\bar{\nu}} : |\mathcal{N}_l| \vdash (r(S_l x) f)^{\llbracket \alpha \rrbracket} : A \to A$. By the same argument, we obtain $x^{\bar{\nu}} : |\mathcal{N}_l| \vdash (r(S_l x))^{(\bar{\varphi}, \llbracket \alpha \rrbracket)} : (|\mathcal{N}_l| \to A \to A) \to A \to A$ for some $\bar{\varphi} \in f^!$. Finally, there exist finite multisets $[\mu_1, \dots, \mu_k], \bar{\rho}_1, \dots, \bar{\rho}_k \in |\mathcal{N}_l|^!$ such that $x^{\bar{\nu}} : |\mathcal{N}_l| \vdash r([\mu_1, \dots, \mu_k], \bar{\varphi}, \llbracket \alpha \rrbracket) : |\mathcal{N}_l| \to (|\mathcal{N}_l| \to A \to A) \to A \to A$ and $x^{\bar{\rho}_j} : |\mathcal{N}_l| \vdash (S_l x)^{\mu_j} : |\mathcal{N}_l| \text{ for all } j$, with moreover $\sum_j \bar{\rho}_j = \bar{\nu}$. Since $(\bar{\rho}_j, \mu_j) \in S_l$ for all $j$, we conclude that $[\mu_1, \dots, \mu_k]$ is of the form $\bar{\nu}^+ + [0^>, \dots, 0^>]$. $\square$

The contrast between Lemma 5.5 and Lemma 5.6 reflects a gap in expressive power between iteration and recursion. Indeed, from Lemma 5.5, we can deduce the following result:

**Lemma 5.7.** Consider the iterator variant of system T, and fix the interpretations $\llbracket \text{Nat} \rrbracket = \mathcal{N}_l$, $\llbracket \text{O} \rrbracket = \mathcal{O}$, $\llbracket \text{S} \rrbracket = S_l$ and $\llbracket \text{I} \rrbracket = \mathcal{I}$. Fix a variable $x$ of type Nat. Let $s$ be a term such that:

(i) all occurrences of $x$ are of the form $\mathcal{l}x$;

(ii) no occurrence of $\mathcal{l}x$ is inside the argument of an application.

Then, if some judgement $\Gamma, x^{\bar{\nu}} : \text{Nat} \vdash s^{\alpha} : A$ is derivable, $\text{Supp}(\bar{\nu})$ is uniform.

**Proof.** We prove the result by induction on $s$, the only interesting case being that of an application:

* if $s = \mathcal{l}x$ then $A$ is of the form $(B \to B) \to B$, we check that $\Gamma, x^{\bar{\nu}} : \text{Nat} \vdash \mathcal{l}x^{(\bar{\phi}, \beta)} : (B \to B) \to B$ implies $(\bar{\nu}, \bar{\phi}, \alpha) \in \mathcal{I}$, and we conclude by Lemma 5.5;

* otherwise, $s = uv$ and $x$ does not occur in $v$, hence $\Gamma, x^{\bar{\nu}} : \text{Nat} \vdash s^{\alpha} : A$ implies some judgment $\Gamma_0, x^{\bar{\nu}} : \text{Nat} \vdash u^{(\gamma_1, \dots, \gamma_k), \alpha} : C \to A$ can be derived, and we conclude by induction hypothesis applied to $u$, which necessarily satisfies (i) and (ii). $\square$

**Corollary 5.8.** No term of the form $\lambda x s$, with $s$ as in the previous lemma is a valid implementation of recursion.

Notice that this already rules out the usual naïve attempt to implement recursion using only iteration and products (recall the term *rec* from section 3.4). We can moreover drop the hypothesis (ii) in Lemma 5.7 by considering the following oriented version of coherence on $|\mathcal{N}_l|$: we say $\mu$ is less defined than $\nu$ and write $\mu \prec \nu$ if there are $m < n \in \mathbb{N}$ such that $\mu = m^>$ and either $\nu = n^>$ or $\nu = n$. The coherence relation $\prec$ is the reflexive and symmetric closure of this partial order. We then obtain the following property for $\mathcal{I}$:

**Lemma 5.9.** For all $(\bar{\nu}, \bar{\varphi}, \bar{\alpha}, \alpha) \in \mathcal{I}$, $\text{Supp}(\bar{\nu})$ is *downwards closed* for $\prec$, i.e. $\mu \prec \nu \in \text{Supp}(\bar{\nu})$ implies $\mu \in \text{Supp}(\bar{\nu})$.
*Proof.* By Lemma 5.3, it is sufficient to prove this result for $\mathcal{I}^{(k)}$, for all $k \in \mathbb{N}$. First notice that any union of downwards closed subsets of $|\mathcal{N}_l|$ is downwards closed, and that if $n \subseteq |\mathcal{N}_l|$ is downwards closed then so is $\{0\} \cup \{\nu^+; \nu \in n\}$. We then conclude by a straightforward induction on $k$. $\square$

Again, such a property fails for any implementation of recursion, by Lemma 5.6. Moreover:

**Lemma 5.10.** With the same hypotheses as in Lemma 5.7, consider a term $t$ such that all occurrences of $x$ in $t$ are of the form $|x$. Then, if some judgement $\Gamma, x^{\bar{\nu}} : \text{Nat} \vdash t^{\alpha} : A$ is derivable, $\text{Supp}(\bar{\nu})$ is downwards closed for $\prec$.

*Proof.* Again, the proof is by induction on $t$, with the only interesting case being that of an application:

* if $t = |x$, we conclude directly by the previous lemma;

* otherwise, $t = uv$ and $\Gamma, x^{\bar{\nu}} : \text{Nat} \vdash t^{\alpha} : A$ implies that we can derive judgements of the form $\Gamma_0, x^{\bar{\nu}_0} : \text{Nat} \vdash u([\beta_1, \dots, \beta_k], \alpha) : B \to A$ and $\Gamma_j, x^{\bar{\nu}_j} : \text{Nat} \vdash v^{\beta_j} : B$ for $j \in \{1, \dots, k\}$ where $\bar{\nu} = \sum_{j=0}^k \bar{\nu}_j$; we conclude by induction hypothesis applied to $u$ and $v$, together with the fact that unions of downwards closed subsets are downwards closed. $\square$

**Corollary 5.11.** No term of the form $\lambda x t$, with $t$ as in the previous lemma is a valid implementation of recursion.

This concluding result is not fully satisfactory, because there remains the condition that $x$ occurs only as the first argument of $|l$. It is still unclear to us whether our semantic argument can be refined in order to avoid this hypothesis. Notice for instance that $[[|x \emptyset x|]]_{x:|\mathcal{N}_l|} = \{([0, \nu], \nu); \nu \in |\mathcal{N}_l|\}$ where $[0, \nu]$ need not be uniform nor downwards closed for $\prec$, hence those simple properties are not sufficient to discriminate between iterator-based terms and recursion operators.

On the other hand, the fact that no term in the iterator variant of system $T$ defines a recursion operator follows straightforwardly from Parigot's work on the encodings of system $T$ in higher order intuitionistic logic [23]: Parigot's results entail that no predecessor can be derived from the iterator. A predecessor is a term $p$ such that $p \mathcal{O} \simeq \mathcal{O}$ and $p(S t) \simeq t$ for all $t$ of type Nat. Such a predecessor is trivially obtained from the recursor: consider $p = \lambda x (R x (\lambda y y) \mathcal{O})$. Hence Parigot's results subsume both Corollaries 5.8 and 5.11.

Anyway, the results of this section showed how the relational interpretation of system $T$ reflected this well known computational distinction between iteration and recursion: Lemmas 5.5 and 5.10 on the one hand, and Lemma 5.6 on the other hand, provide a semantic insight into the nature of this gap, if not a new proof of it.
RELATED AND FUTURE WORK

Our success in defining a semantics of system *T* in *Fin* immediately poses the question of its generalization to other datatypes. The cpo-enriched structure of *Rel* allowed for an abstract description of datatypes [30, 31] as particular functors which are monotonic for relation inclusion. In particular, this provided the basis of a categorical account of container types [32]. In such a setting, it is natural to define recursive datatypes, such as lists or trees, as the least fixpoints of particular Scott-continuous functors. The question is then how to transport these constructions to the finitary setting.

In recent work with Tasson [33], we study two orders on finiteness spaces derived
from set inclusion: the most restrictive one, finiteness extension, was used by
Ehrhard to provide an interpretation of second order linear logic in an unpublished
preliminary version of [9]; the largest one, finiteness inclusion, is a cpo on finiteness
spaces. We study various notions of continuity for functors in finiteness spaces, and
relate them with the existence of fixpoints for these functors. A striking feature
of this development is that we are led to consider the properties of functors w.r.t.
both orders simultaneously: continuity for finiteness inclusion, and monotonicity
for finiteness extension. We prove in particular that every functor obtained by
applying a very generic construction on finiteness spaces satisfies these properties,
and admits a least fixpoint for finiteness inclusion.

We then apply this result to describe a relational semantics of functional pro-
gramming with recursive datatypes, which generalizes the results of the present
paper: the fixpoints of algebraic datatype functors define recursive datatypes with
finitary constructors, destructors and iterators. This paves the way towards a
quantitative semantics of typed recursion, according to the following roadmap:
first find a correct quantitative semantics for constructors *vs* destructors (zero and
successor *vs* pattern matching in the case of system *T*); then check that the coeffi-
cients involved in the computation of the fixpoint defining iterators remain finite.
We may first apply this strategy to system *T*. If it proves fruitful, we would then
try to generalize it to recursive algebraic datatypes.

Notice that another standard approach to the semantics of datatypes is to
consider the impredicative encoding of inductive types, e.g. in system *F*. Such
a semantics in finiteness spaces can be derived from that of second order linear
logic. This is based on a class of functors which, in particular, are monotonic
for the finiteness extension order. Notice however that this does not provide a
denotational semantics *stricto sensu*: in general, the interpretation decreases under
cut elimination. Moreover, the possibility of defining a quantitative semantics in
this setting is not clear.

REFERENCES

[1] Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1-102, 1987.

[2] Dana S. Scott. Data types as lattices. *SIAM J. Comput.*, 5(3):522-587, 1976.
[3] Gérard Berry. Stable models of typed lambda-calculi. In Giorgio Ausiello and Corrado Böhm, editors, *ICALP*, volume 62 of *Lecture Notes in Computer Science*, pages 72–89. Springer, 1978.

[4] Jean-Yves Girard. Normal functors, power series and lambda-calculus. *Annals of Pure and Applied Logic*, 37(2):129–177, 1988.

[5] Jean-Yves Girard. The system $f$ of variable types, fifteen years later. *Theor. Comput. Sci.*, 45(2):159–192, 1986.

[6] Chantal Berline. Graph models of lambda-calculus at work, and variations. *Mathematical Structures in Computer Science*, 16(2):185–221, 2006.

[7] Richard Statman. Completeness, invariance and lambda-definability. *J. Symb. Log.*, 47(1):17–26, 1982.

[8] Daniel de Carvalho. *Sémantiques de la logique linéaire et temps de calcul*. Thèse de doctorat, Université Aix-Marseille II, 2007.

[9] Thomas Ehrhard. Finiteness spaces. *Mathematical Structures in Computer Science*, 15(4):615–646, 2005.

[10] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theoretical Computer Science*, 309:1–41, 2003.

[11] Thomas Ehrhard and Laurent Regnier. Differential interaction nets. *Electr. Notes Theor. Comput. Sci.*, 123:35–74, 2005.

[12] Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine's machine and the Taylor expansion of $\lambda$-terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, *CiE*, volume 3988 of *Lecture Notes in Computer Science*, pages 186–197. Springer, 2006.

[13] Thomas Ehrhard and Olivier Laurent. Interpreting a finitary pi-calculus in differential interaction nets. *Information and Computation*, 208(6):606–633, 2010.

[14] Paolo Tranquilli. Intuitionistic differential nets and lambda-calculus. *Theor. Comput. Sci.*, 412(20):1979–1997, 2011.

[15] Lionel Vaux. Differential linear logic and polarization. In Curien [34], pages 371–385.

[16] Christine Tasson. Algebraic totality, towards completeness. In Curien [34], pages 325–340.

[17] Michele Pagani and Christine Tasson. The inverse Taylor expansion problem in linear logic. In *LICS*, 2009.

[18] Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. Technical report, 2008. Rapport de recherche INRIA n° 6638.

[19] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In *Computer Science Logic*, volume 4646 of *Lecture Notes in Computer Science*, pages 298–312. Springer Berlin, 2007.

[20] Marie-France Thibault. Pre-recursive categories. *Journal of Pure and Applied Algebra*, 24:79–93, 1982.

[21] J. Lambek and P. J. Scott. *Introduction to higher order categorical logic*. Cambridge University Press, New York, NY, USA, 1988.

[22] Jean-Yves Girard, Paul Taylor, and Yves Lafont. *Proofs and types*. CUP, Cambridge, 1989.

[23] Michel Parigot. On the representation of data in lambda-calculus. In Egon Börger, Hans Kleine Büning, and Michael M. Richter, editors, *CSL*, volume 440 of *Lecture Notes in Computer Science*, pages 309–321. Springer, 1989.

[24] Lionel Vaux. The algebraic lambda calculus. *Mathematical Structures in Computer Science*, 19(5):1029–1059, 2009.

[25] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. A relational model of a parallel and non-deterministic lambda-calculus. In Sergei N. Artëmov and Anil Nerode, editors, *LFCS*, volume 5407 of *Lecture Notes in Computer Science*, pages 107–121. Springer, 2009.

[26] Vincent Danos and Thomas Ehrhard. On probabilistic coherence spaces. Technical report, 2008.

[27] Pablo Arrighi and Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. In Andrei Voronkov, editor, *Rewriting Techniques and Applications, 19th*
*International Conference, RTA-2008*, volume 5117 of *Lecture Notes in Computer Science*, pages 17–31, Hagenberg, Austria, July 15–17, 2008. Springer.

[28] Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine, and Paul-André Melliès. *Interactive models of computation and program behaviour*, volume 27 of *Panoramas et synthèses*, pages 1–196. Société Mathématique de France, 2009.

[29] Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. *Theor. Comput. Sci.*, 294(1/2):183–231, 2003.

[30] Roland Carl Backhouse and Paul F. Hoogendijk. Generic properties of datatypes. In Roland Carl Backhouse and Jeremy Gibbons, editors, *Generic Programming*, volume 2793 of *Lecture Notes in Computer Science*, pages 97–132. Springer, 2003.

[31] Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. Polynomial relators. In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo, editors, *AMAST, Workshops in Computing*, pages 303–326. Springer, 1991.

[32] Paul Hoogendijk and Oege De Moor. Container types categorically. *J. Funct. Program.*, 10:191–225, March 2000.

[33] Christine Tasson and Lionel Vaux. Transport of finiteness structures and applications. to appear in Mathematical Structures in Computer Science, 2011.

[34] Pierre-Louis Curien, editor. *Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings*, volume 5608 of *Lecture Notes in Computer Science*. Springer, 2009.

Communicated by (The editor will be set by the publisher).

November 21, 2011.