RIA

laboria

laboratoire de recherche
en informatique
et automatique

# SÉQUENTIALITÉ DE L'ÉVALUATION FORMELLE DES λ-EXPRESSIONS

G. BERRY

Rapport de Recherche N° 304

Mai 1978

16p.

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20
# SÉQUENTIALITÉ DE L'ÉVALUATION FORMELLE DES λ-EXPRESSIONS

G. Berry*

## Résumé :

Le but de cet article est de montrer que le mécanisme d'évaluation symbolique des λ-expressions possède un caractère essentiellement séquentiel, ceci même lorsqu'on a à évaluer des expressions à l'intérieur de contextes, qui sont une façon classique de représenter des environnements dans le λ-calcul. Les résultats sont exprimés dans le modèle syntaxique de Lévy, où chaque expression a pour sémantique l'arbre infini obtenu par expansion complète de ses radicaux ; ils traduisent le théorème de standardisation à l'intérieur de ce modèle.

## Abstract :

We show that the symbolic evaluation mechanism of the λ-calculus is inherently sequential, this even when expressions are evaluated inside contexts (which classically represent environments). We express our results in Lévy's syntactic model where λ-terms are developed into infinite trees. They can be viewed as an expression of the standardisation theorem in Lévy's model.

Ce travail a été présenté au 3e Colloque International sur la Programmation, Paris, 28-30 mars 1978, DUNOD ed. et doit être cité comme tel.

This work has been presented at a conference and should be referred to as a communication to the 3rd International Colloquium on Programming, Paris, march 28-30, 1978, DUNOD ed.

* Ecole Nationale Supérieure des Mines de Paris. Sophia - Antipolis 06560 Valbonne (France)
# 1. INTRODUCTION

Le but de cet article est de mettre en évidence le caractère séquentiel du mécanisme d'évaluation formelle des λ-expressions. Nos résultats sont exprimés dans le modèle de Lévy [9,10] et peuvent être vus comme une expression du théorème de standardisation dans ce modèle (voir aussi "Activity Lemma" dans Plotkin [13]).

Pour présenter nos résultats, utilisons très informellement la notion intuitive de mécanisme d'évaluation, et précisons d'abord ce que nous entendons par mécanisme d'évaluation parallèle stable ou séquentiel. Une discussion plus complète sera donnée en [2]. On se pose le problème de calculer la valeur d'une expression M dans un modèle M pour un environnement ρ (affectation de valeurs dans M aux variables). Appelons *radical* (redex) de M toute sous-expression de la forme $(\lambda x.P)Q$, appelons *radical critique* de M un radical qu'il faudra de toute façon contracter au cours du calcul - lui ou un de ses résidus au sens de [5]-, appelons enfin $\omega(M)$ l'approximation directe de M obtenue en remplaçant tous les radicaux de M par un symbole "indéfini $\Omega$" (et en appliquant les règles $\Omega_M \to \Omega$ et $\lambda x.\Omega \to \Omega$), cf [9,10,20].

- Evaluation parallèle : il n'existe pas en général de sous-terme critique. Alors on peut avoir à évaluer "en parallèle" plusieurs sous-termes de M. Nous montrons que les modèles $D^\infty$, $P\omega$, $T^\omega$ [17,18,14] sont de ce type, car ils contiennent des fonctions analogues au "ou parallèle" de [19] qui vaut _vrai_ dès qu'un de ses arguments vaut _vrai_. Par exemple une expression de la forme $R_1 \text{ ou } R_2$ n'a pas de radical critique si $R_1$ et $R_2$ sont deux radicaux s'évaluant à _vrai_. (Notons que cette notion de parallèlisme est reliée à la notion classique de programme parallèle [6], car l'interpréteur du langage est typiquement un programme parallèle.).

- Evaluation stable : les expressions ont au moins un radical critique. Dans ce cas on peut montrer que toute approximation de la valeur de M a un calcul optimal au sens de [10], cf [2,3]. Cependant on ne peut pas déterminer un radical critique uniquement en fonction de $\omega(M)$, et il n'existe pas plus de procédé de calcul "optimal" que dans le cas parallèle. Une construction de modèles stables comparables à $D^\infty$ [17] est présentée en [3].

- Evaluation séquentielle : on peut toujours déterminer un radical critique en fonction de $\omega(M)$. C'est évidemment le cas favorable en pratique, car on peut alors espérer disposer de procédés de calcul "optimaux" analogues à la règle du retard de Vuillemin [19,20].

L'évaluation formelle (ou symbolique) des λ-expressions s'étudie commodément dans le modèle de Lévy [9,10] où l'on associe à chaque expression l'arbre infini obtenu par expansion complète de ses radicaux. Au lieu de considérer des environnements
au sens classique, il est plus commode - et plus général - de considérer des contextes. Nous montrons la séquentialité de l'évaluation d'une expression M dans un contexte $C$[] à l'aide d'un formalisme voisin de celui qu'utilisent Kahn-Plotkin en [8]. Nous montrons que la propriété de stabilité peut aussi être vue comme un raffinement de la propriété de continuité syntaxique qui fonde le modèle de Lévy [9,10].

## 2. INTERPRETATION ALGEBRIQUE DU $\lambda$-CALCUL

Le chapitre est consacré à la présentation de l'interprétation algébrique de Lévy [9,10].

### 2.1. Le $\lambda$-calcul

#### 2.1.1. Définitions : $\lambda$-expressions

On considère un ensemble $V = \{x_1, x_2, ..., x_n, ...\}$ de variables, aussi notées y, z, ..., L'ensemble $\Lambda$ des $\lambda$-expressions est le plus petit ensemble contenant :

(i) $x$ pour $x \in V$

(ii) $(\lambda x M)$ pour $x \in V$ et $M \in \Lambda$

(iii) $(MN)$ pour $M, N \in \Lambda$

On utilise les abréviations classiques $MN_1N_2...N_p$ pour $(...((MN_1)N_2)...N_p)$ et $\lambda x_1x_2...x_m$. M pour $(\lambda x_1(\lambda x_2...(\lambda x_m M)...))$. On utilise aussi des notations vectorielles : $M\vec{N}$ signifie $MN_1N_2...N_p$ pour $p \ge 0$ et $\lambda\vec{x} \cdot M$ signifie $\lambda x_1x_2...x_m$. M pour $m \ge 0$

Nous notons $M[N/x]$ le résultat de la substitution de N aux occurrences libres de $x$ dans M, et nous notons $M \to N$ la $\beta$-conversion induite par $(\lambda x.P)Q \to P[Q/x]$, où $(\lambda x.P)Q$ est appelé un *radical*. Nous notons $d:MN$ les $\beta$-dérivations, $d_1$ ; $d_2$ la concaténation de deux dérivations et $\mathbf{0}$ la dérivation vide.

#### 2.1.2. Définitions : formes normales de tête

Remarquons que $\Lambda$ est aussi le plus petit ensemble contenant :

(i) $\lambda x_1x_2...x_m \cdot xM_1M_2...M_n$ pour $m, n \ge 0$ et $M_i \in \Lambda$

(ii) $\lambda x_1x_2...x_m \cdot (\lambda y.P)QM_1M_2...M_n$ pour $m, n \ge 0$ et $P, Q, M_i \in \Lambda$

les expressions de la première forme sont dites en *forme normale de tête* ou *fnt*. On dit que $M$ a une *fnt* s'il existe $N$ en *fnt* telle que $M \not\equiv_N N$. On définit dans ce cas la dérivation $d_{\text{fnt}}(M)$ et l'expression $\text{Fnt}(M)$ par
$$
(i) \ d_{\text{fnt}}^{(M)} = 0 \text{ et } \text{Fnt}(M)=M \text{ si } M \text{ est en } \text{fnt}
$$

$$
(ii) d_{\text{fnt}}^{(M)} = d_o ; d_{\text{fnt}}^{(M_1)} \text{ et } \text{Fnt}(M) = \text{Fnt}(M_1) \text{ avec}
$$

$$
d_o : M = \lambda x . (\lambda y . P) Q \vec{M} \rightarrow M_1 = \lambda x . P [Q/y] \vec{M}
\text{si M n'est pas en fnt.}
$$

Le lemme suivant est à la base de nos résultats. Il dérive
du théorème de standardisation [10,12] :

2.1.3. **Lemme** (Lévy [10]) :

Fnt(M) est défini si et seulement si M a une fnt. Si
M ⇝ N où N est en fnt, alors Fnt(M) ⇝ N.

2.2. Le modèle algébrique

Comme en Wadsworth [20], on construit des approximations
directes de termes. Intuitivement, on utilise un symbole "indéfini
syntaxique" Ω : comme on ne sait rien à priori de la forme
syntaxique que peut prendre un radical après contraction, on
remplace tous les radicaux par Ω. On utilise ensuite les
"Ω-règles" λx.Ω → Ω et ΩM → Ω dont l'interprétation fonction-
nelle est évidente. Formellement, il est plus commode d'utiliser
la notion de forme normale de tête.

2.2.1. **Définition** : Ωβ - *formes normales*

L'ensemble $N$ des $\Omega\beta$ *formes normales* est le plus petit
ensemble contenant

(i) Ω

(ii) λx₁x₂...xₘ. xa₁a₂...aₙ pour m,n ≥ o et aᵢ ∈ N

On ordonne N par le plus petit ordre < vérifiant :

(i) Ω < a pour tout a ∈ N

(ii) λx₁x₂...xₘ. xa₁a₂...aₙ < λx₁x₂...xₘ. xb₁b₂...bₙ

$$
\text{si } a_1 < b_1, a_2 < b_2, \dots, a_n < b_n
$$

On appelle *ensemble dirigé* dans *N* tout Δ ⊂ *N* vérifiant

$$
\forall a_1, a_2 \in \Delta, \exists a_3 \in \Delta \text{ t.q. } a_1 < a_3 \text{ et } a_2 < a_3
$$

et *idéal* tout Δ dirigé vérifiant $\forall a \in \Delta, \forall b \in N, b < a \Rightarrow b \in \Delta$
La *complétion par idéaux* $\langle N^\infty, \langle \rangle$ de $\langle N, \langle \rangle$ est l'ensemble des
idéaux de $N$ ordonné par inclusion (cf. [9]).
Nous incluerons $N$ dans $N^\infty$ en associant à tout $A \in N$
l'idéal $\{b \in N \mid b < a\}$. Il est commode de représenter les
éléments de $N$ pour des arbres finis de la forme

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

les éléments de $N^\infty$, notés $A, B, \dots$ sont alors représentés par
des arbres infinis de la même forme, l'idéal $A$ étant l'ensemble
des troncatures finies de l'arbre infini associé. Il est clair que
$\langle N^\infty, \langle \rangle$ est un ordre partiel $\omega$-algébrique (cf. [9,11]).
complor

Deux éléments quelconques $A$ et $B$ de $N^\infty$ ont une borne
inférieure $A \triangleleft B$, et deux éléments $A$ et $B$ ayant un majorant
commun ont une borne supérieure notée $AvB$.

### 2.2.2. Définitions : Approximation directe et valeur syntaxique d'un terme

L'approximation directe $\omega(M) \in N$ de $M \in \Lambda$ est définie par :

$$
(i) \quad \omega(M) = \Omega \quad \text{si} \quad M \text{ n'est pas en} \quad \text{fnt}
$$

$$
(ii) \quad \omega(\lambda x_1 x_2 \dots x_m (x M_1 M_2 \dots M_n)) = \lambda x_1 x_2 \dots x_m \omega(M_1) \omega(M_2) \dots \omega(M_n)
$$

On vérifie qu'on a $\omega(M) \prec \omega(M')$ si $M \stackrel{\cdot}{\to} M'$. Alors l'ensemble $A(M) = \{\omega(M') \mid M \stackrel{\cdot}{\to} M'\}$ inclus dans $N$ est dirigé par le théorème de Church-Rosser, et il a une limite dans $N^\infty$ appelée *valeur syntaxique de M* dans $N^\infty$ et notée $val(M)$. Intuitivement, $val(M)$ est l'arbre infini obtenu par expansion complète des radicaux de $M$, où les $\Omega$ restants ne sont dûs qu'à des expressions qui n'ont pas de fnt.

On écrira $M \prec N$ ssi $val(M) \prec val(N)$, et on écrira de même $A \prec M$, $M \prec a$ etc... en se plaçant toujours dans $N^\infty$ par l'intermédiaire de $val$. On écrira enfin $M \equiv N$ pour $val(M) = val(N)$.

On voit facilement en utilisant le théorème de Church-Rosser que $val$ est préservé par $\beta$-conversion, i.e. que $M \not\equiv N$ entraîne $M \equiv N$.

### 2.3. Le théorème de continuité syntaxique.

Il reste à montrer que l'application $val : \Lambda \to N^\infty$ est une
sémantique monotone du $\lambda$-calcul, c'est-à-dire que $M \prec M'$ et
$N \prec N'$ entraînent $\lambda x.M \prec \lambda x.M'$ et $MN \prec M'N'$. Notons qu'alors
$M \equiv M'$ et $N \equiv N'$ entraînent $\lambda x.M \equiv \lambda x.M'$ et $MN \equiv M'N'$. Pour
cela on montre la continuité de l'opération de prise de contexte
que nous définissons maintenant :
### 2.3.1. Définitions : contextes

On considère un ensemble ${{[]_i \mid i \in N}}$ dont les éléments sont appelés *trous*. L'ensemble $C[ ]$ des contextes est le plus petit ensemble contenant les trous, les variables et $(\lambda x C_1[ ]) \text{ et } (C_1[ ] C_2[ ]) \text{ pour } C_1[ ], C_2[ ] \in C[ ].$

Le remplissage de $[ ]_i$ par $C'[ ]$ dans $C[ ]$ donne un nouveau contexte $C[ ][C'[ ]]_i = C_o[ ]$ défini par

(i) $C_o[ ] = C'[ ]$ si $C[ ] = [ ]_i$

(ii) $C_o[ ] = C[ ]$ si $C[ ] = x \in V$ ou $C[ ] = [ ]_j \neq [ ]_i$

(iii) $C_o[ ] = \lambda x.C_1[ ][C'[ ]]_i$ si $C[ ] = \lambda x.C_1[ ]$

(iv) $C_o[ ] = (C_1[ ][C'[ ]]_i)(C_2[ ][C'[ ]]_i)$ si $C[ ] = C_1[ ]C_2[ ]$

Nous écrirons :

$$C[ ][C[ ]] = C[ ][C_1[ ]]_1[C_2[ ]]_2\dots[C_n[ ]]_n$$

ou plus simplement :

$$C[M] = C[ ][M_1]_1[M_2]_2\dots[M_n]_n$$

si le contexte obtenu est une expression de $\Lambda$, i.e. ne contient plus de trous.

Etant donné un contexte $C[ ]$, on note $r(C[ ])$ le contexte obtenu en renommant par des entiers consécutifs les trous de $C[ ]$ de la gauche vers la droite : par exemple si

$$C[ ] = ([ ]_2(\lambda x[ ]_1))[ ]_2, \quad \text{alors}$$

$$r(C[ ]) = ([ ]_1(\lambda x[ ]_2))[ ]_3$$

Les contextes se définissent de la même manière pour $N$ et forment un ensemble $N[ ]$. Pour tout $a \in N$, il existe un seul contexte $C_a[ ] \in C[ ]$ tel que $C_a[\Omega]_1 = a$. On note alors

$$a^{\Omega}[ ] = r(C_a[ ]) \text{. Par exemple si } a = (\lambda x.\Omega)x\Omega\Omega, \text{ alors}$$

$$C_a[ ] = (\lambda x.[ ]_1)x[ ]_1[ ]_1 \text{ et } a^{\Omega}[ ] = (\lambda x.[ ]_1)x[ ]_2[ ]_3.$$

Remarquant que si $\Delta = \lambda x.xx$ alors $\Delta\Delta \equiv \Omega$, on plonge $N$ dans $\Lambda$ en représentant $a$ par $a^{\Lambda} = C_a[\Delta\Delta]_1$. On écrira $C[a]$ pour $C[a^{\Lambda}]$.

Tout contexte $C[ ] \in C[ ]$ ne contenant que les trous $[ ]_1, [ ]_2, \dots, [ ]_n$ détermine une application de $\Lambda^n$ (ou $N^n$ avec l'identification précédente) dans $N^\infty$ qui à $M \in \Lambda^n$ associe $\text{val}(C[M]) \in N^\infty$. Le théorème essentiel de continuité syntaxique de Lévy [9] s'exprime comme suit, en écrivant $\vec{a} \prec \vec{M}$ pour $a_1 \prec M_1, a_2 \prec M_2, \dots, a_n \prec M_n$.
### 2.3.2. Théorème :

Soit $C[\vec{a}] \in C[\vec{a}]$ ne contenant que $[\vec{a}]_1, [\vec{a}]_2, \dots, [\vec{a}]_n$,
soit $\vec{M} = (M_1, M_2, \dots, M_n) \in \Lambda^n$. Alors

$$ \forall \vec{b} \in \mathbb{N}, \ \vec{b} < C[\vec{M}], \ \exists \vec{a} < \vec{M} \text{ t.q. } \vec{b} < C[\vec{a}] $$

ou équivalent

$$ C[\vec{M}] = U\{C[\vec{a}] \mid \vec{a} \in \mathbb{N}^n, \vec{a} < \vec{M}\} $$

Ainsi pour calculer une approximation finie $\vec{b}$ de $C[\vec{M}]$, on n'a besoin que d'une approximation finie $\vec{a}$ de $\vec{M}$

### 2.3.3. Corollaire :

Si $\vec{M} < \vec{M}'$ alors $C[\vec{M}] < C[\vec{M}']$ pour tout $C[\vec{a}]$

En particulier $\lambda x.M < \lambda x.M'$ et $MN < M'N'$ si $M < M'$ et $N < N'$ en prenant respectivement $C[\vec{a}] = \lambda x.[\vec{a}]_1$ et $C[\vec{a}] = [\vec{a}]_1[\vec{a}]_2$.

Notons qu'on peut maintenant étendre l'opération $C[\vec{a}]$ sur $\mathbb{N}^\infty$ en posant $C[\vec{A}] = U\{C[\vec{a}] \mid \vec{a} < \vec{A}\}$. Le théorème 2.3.2. assure la cohérence de cette définition en montrant qu'on a bien $C[\vec{M}] = C[\text{val}(\vec{M})]$.

## 3. SEQUENTIALITE ET STABILITE DU $\lambda$-CALCUL

Nous nous intéressons à la relation $C[\vec{A}] = B$ dans $\mathbb{N}^\infty$ à $C[\vec{a}]$ fixé. La propriété de stabilité exprime que si l'on s'intéresse à une approximation $B' < B$, alors il existe une approximation minimum $\vec{A}'$ de $\vec{A}$ telle que $B' < C[\vec{A}']$ (dans le cas $B' = b'$ fini, le théorème 2.3.2. assure l'existence d'un $\vec{a}' < \vec{A}$ fini tel que $b' < C[\vec{a}']$, mais ne donne pas d'indication sur la structure de l'ensemble $\{\vec{a}' < \vec{A} \mid b' < C[\vec{a}']\}$. Nous montrons que cet ensemble a un minimum, ou ce qui revient au même qu'il est fermé par intersection).

La propriété de séquentialité s'intéresse à la façon d'augmenter l'argument $\vec{A}$ lorsqu'on désire augmenter l'information de sortie B. Il n'y a pas ici de phénomène de séquentialité au sens de Vuillemin [19], c'est-à-dire il n'y a pas de moyen uniforme d'augmenter $\vec{A}$ pour faire croître B : en particulier si $C[\vec{a}] = [\vec{a}]_1$, alors $B = A_1$ et on augmente B quelle que soit la façon d'augmenter $A_1$. Il existe en revanche une propriété de séquentialité au sens de Kahn-Plotkin [8] : si on s'intéresse à faire croître B en une certaine occurrence $u_1$ de $\Omega$, il existe une occurrence unique $u_2$ de $\Omega$ dans l'un des $A_i$ sur laquelle on doit faire croître $\vec{A}$. Le caractère unique de $u_2$
s'explique par le fait qu'on peut faire croître B en $u_1$
simplement en remplaçant l'occurrence $u_2$ de $\Omega$ par une variable
convenable, sans toucher aux autres occurrences de $\Omega$ dans $\hat{A}$.
(Notons que cette unicité n'est pas vérifiée pour des fonctions
bien "séquentielles" comme l'addition sur les entiers : il faut
faire croître les deux arguments $\perp$ pour faire croître $\perp + \perp$.)
La situation est illustrée sur le dessin suivant :

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

Si on veut augmenter B en $\ominus$ (resp. $\ominus_2$), il faut augmenter $A_1$ en $\ominus$ (resp. $A_2$ en $\ominus$).

**Exemples** : les indices servent à distinguer les occurrences de $\Omega$

$$
1. C[\ ] = [\ ]_2[\ ]_1, A_1 = A_2 = \Omega
$$

Alors $B = \Omega$ et il faut faire croître $A_2$. On a
$B = z\Omega \neq \Omega$ en prenant $A_2 = z$

$$
2. C[\ ] = x[\ ]_2[\ ]_1, A_1 = x\Omega_1\Omega_2, A_2 = \Omega_3
$$

Alors $B = x\Omega_a (x\Omega_b \Omega_c)$ avec les correspondances
$\Omega_a \to \Omega_3$, $\Omega_b \to \Omega_1$, $\Omega_c \to \Omega_2$

$$
3. C[\ ] = (\lambda x[\ ]_1)[\ ]_2, A_1 = \Omega, A_2 = \Omega
$$

Alors $B = \Omega$, il faut augmenter $A_1$ pour augmenter $B$, et
il suffit de prendre $A_1 = y$

3.1. Séquentialité dans le cas fini.

3.1.1. Définitions : occurrences

Nous définissons les occurrences comme des chemins dans des arbres, cf. Rosen [15]. Une occurrence est notée $u \in \mathbb{N}^*$ et est le mot vide de $\mathbb{N}^*$ et $u \downarrow A$ est le sous-terme de $A$ à l'occurrence $u$, défini par :

$$
(i) \quad \epsilon \to A = A
$$

$$
(ii) \quad \text{ku } \downarrow \lambda x.^{\to} x A_1 A_2 \dots A_n = u \downarrow A_k \quad \text{si} \quad 1 \le k \le n
$$

indéfini sinon

On appelle *occurrence de Ω* dans A tout u tel que
*u ↓ A = Ω*. On écrit $A \trianglelefteq_u B$ si $A \triangleleft B$ avec $u \downarrow A = \Omega$ et
*u ↓ B ≠ Ω*. On écrit $\hat{A} \trianglelefteq_i u \hat{B}$ si on a $A_i \trianglelefteq_u B_i$.

On écrit $u \downarrow M$ pour $u \downarrow \text{val}(M)$.
**3.1.2. Lemme :** Si $M \equiv \Omega$ alors $M[N/x] \equiv \Omega$ pour tout N.

**preuve :** On a $M[N/x] \equiv (\lambda x. M)N \equiv \mathcal{U}\{(\lambda x. a)N \mid a < M\}$ par application de 3.2.2 au contexte $(\lambda x. [\mathcal{J}])N$. Si $M \equiv \Omega$ alors
$$M[N/x] \equiv (\lambda x. \Omega)N \equiv \Omega.$$

□

**3.1.3. Proposition :**

Soit $C[\mathcal{J}] \in C[\mathcal{J}]$, soit $B \equiv C[\tilde{\Omega}]$, $B \in \mathbb{N}^{\infty}$

soit $\mathcal{U}$ une occurrence de $\Omega$ dans B. On a un et un seul des deux cas suivants :

1. $\mathcal{U} \to C[M] = \Omega$ pour tout $M \in \mathcal{A}$

2. Il existe un $i \in \mathbb{N}$ unique tel que $\mathcal{U} \to C[M] \neq \Omega$ entraine $M_i \neq \Omega$. De plus si $z$ est une variable n'apparaissant pas dans $C[\mathcal{J}]$, on a $\mathcal{U} \to C[N] \neq \Omega$ dès que $N_i = z$

**preuve :** Supposons qu'il existe $M$ tel que $\mathcal{U} \to C[M] \neq \Omega$. On opère par récurrence sur $\langle |\mathcal{U}|, |d_{\text{fnt}}(C[M])| \rangle$ où $|\mathcal{U}|$ est la longueur de $\mathcal{U}$ et $|d_{\text{fnt}}(C[M])|$ est la longueur de $d_{\text{fnt}}(C[M])$ qui existe par 2.1.3. car $C[M]$ à une fnt puisque $C[M] \neq \Omega$.

**Cas 1 :** $C[\mathcal{J}] = \lambda^{\vec{x}}. [\mathcal{J}]_i C[\mathcal{J}]$

Alors $i$ répond à la question (cas de base).

**Cas 2 :** $C[\mathcal{J}] = \lambda^{\vec{x}}. \mathcal{X} C[\mathcal{J}]$

Alors $\mathcal{U} = \mathcal{KU}'$ pour un $\mathcal{K} \in \mathbb{N}$, et $\mathcal{U}' \to C_k[\tilde{\Omega}] = \Omega$
La récurrence appliquée à $\mathcal{U}'$ et $C_k[\mathcal{J}]$ fournit $[\mathcal{J}]_i$
qui répond aussi à la question pour $C[\mathcal{J}]$

**Cas 3 :** $C[\mathcal{J}] = \lambda^{\vec{x}}. (\lambda y. C_o[\mathcal{J}]) C'_o[\mathcal{J}] C[\mathcal{J}]$

Soit alors $C''[\mathcal{J}] = \lambda^{\vec{x}}. C_o[\mathcal{J}][C'_o[\mathcal{J}]/\mathcal{Y}] C[\mathcal{J}]$ et soit $C'[\mathcal{J}] = r(C''[\mathcal{J}])$, cf. 2.3.1. Notons $q(i)$ l'ancien numéro dans $C''[\mathcal{J}]$ d'un trou $[\mathcal{J}]_i$ de $C'[\mathcal{J}]$ avant la rénumérotation par $\mathcal{R}$. Pour tout $\vec{P}$, on a $C[\vec{P}] \to C'[\vec{P}]$ où les $P'_j$ sont déterminés de la manière suivante :

- $P'_j = P_{q(j)}[C'_o[\vec{P}]/\mathcal{Y}]$ si $[\mathcal{J}]_j$ dans $C'[\mathcal{J}]$ provient de la rénumérotation d'une occurrence de $[\mathcal{J}]_{q(j)}$ de $C''[\mathcal{J}]$ qui est dans $C_o[\mathcal{J}]$ mais pas sous la
portée d'un λy dans $C_o[ ]$ (ceci à cause des problèmes de renommage des variables dans la β-conversion).

- P'j = Pq(j) sinon

Montrons que la récurrence s'applique à C'[ ] et u.

- On a $C[\vec{\Omega}] \to C'[\vec{\Omega}]$ puisque $\Omega = (\Lambda\Delta)$ est invariant par substitution. Donc $u \downarrow C'[\vec{\Omega}] = u \downarrow C[\vec{\Omega}] = \Omega$.

- Si $C[\vec{M}] \to C'[\vec{M}']$, alors $u \downarrow C'[\vec{M}'] = u \downarrow C[\vec{M}] \neq \Omega$

- On a $|d_{\text{fnt}}(C'[\vec{M}'])| < |d_{\text{fnt}}(C[\vec{M}])|$ puisque $C[\vec{M}] \to C'[\vec{M}']$ est précisément la première étape de $d_{\text{fnt}}(C[\vec{M}])$, cf. 2.1.2.

La récurrence fournit donc $[ ]_i$ pour $C'[ ]$. Montrons que $[ ]_{q(i)}$ répond à la question pour $C[ ]$.

- Si $P_{q(i)} = \Omega$, alors $C[\vec{P}] \to C'[\vec{P}]$ avec par 3.1.2 $P'_i = \Omega$. Donc $u \downarrow C[\vec{P}] = u \downarrow C'[\vec{P}] = \Omega$.

- Si z n'a pas d'occurrence dans $C[ ]$ alors il n'a pas non plus d'occurrence dans $C'[ ]$. Si $N_{q(i)} = z$ et si $C[\vec{N}] \to C'[\vec{N}']$, alors $N'_i = z$ puisque $z \neq y$. Donc $u \downarrow C[\vec{N}] = u \downarrow C[\vec{N}'] \neq \Omega$. $\square$

### 3.1.4. Corollaire :

Soit $C[ ] \in C$, soit $\vec{a} \in N$, soit $B \equiv C[\vec{a}] \in N^\infty$. Soit u une occurrence de $\Omega$ dans B. On a un et un seul des deux cas suivants :

1. $u \downarrow C[\vec{a}'] = \Omega$ pour tout $\vec{a}' > \vec{a}$

2. Il existe $i \in N$ et $u \in N^*$ uniques tels que $\vec{a} < \vec{a}'$ et $B \ll u C[\vec{a}']$ entraînent $\vec{a} \ll_i u, \vec{a}'$. De plus $u \downarrow C[\vec{a}'] \neq \Omega$ dès que $\vec{a}' > \vec{a}$ et $u' \downarrow a'_i = z$, où z n'apparaît pas dans $C[ ]$.

**preuve** : Remarquons que l'énoncé de 3.1.3 peut se reformuler en remplaçant $\vec{M}$ par $\vec{a} \in N$ et $\vec{N}$ par $\vec{b} \in N$. En effet $u \downarrow C[\vec{M}]$ pour tout $\vec{M}$ équivaut par 3.2.2 à $u \downarrow C[\vec{a}]$ pour tout $\vec{a}$. IL suffit alors de considérer le contexte $r(C[\vec{a}^\Omega[ ]])$, cf. 2.3.1

les trous de ce contexte sont en bijection avec les occurrences des $\Omega$ dans les $a_i$ apparaissant dans $C[\vec{a}]$. $\square$
### 3.2. Séquentialité et stabilité dans le cas général :

On montre d'abord une propriété de préservation de l'inter-section qui est un cas particulier de stabilité. Ecrivons $A \uparrow B$ si $A$ et $B$ ont un majorant commun, et remarquons que si $A \uparrow B$ alors on ne peut avoir simultanément $u \downarrow A \neq \Omega$, $u \downarrow B \neq \Omega$ et $u \downarrow (A \wedge B) = \Omega$.

#### 3.2.1. Lemme :

si $A \prec B$ et $A \neq B$, il existe $u$ tel que $u \downarrow A = \Omega$ et $u \downarrow B \neq \Omega$. Si $\Delta \subsetneq N^\infty$ est dirigé, alors pour tout $u$ tel que $u \downarrow (U\Delta) \neq \Omega$ il existe $B \in \Delta$ tel que $u \downarrow B \neq \Omega$.

#### 3.2.2. Lemme :

si $C[\overrightarrow{\alpha}] \in C$ et $\overrightarrow{\alpha} \in N$ et $\overrightarrow{\alpha} \in N^\infty$ avec $\overrightarrow{\alpha} \uparrow \overrightarrow{\alpha}$, alors $C[\overrightarrow{\alpha} \wedge \overrightarrow{\alpha}] = C[\overrightarrow{\alpha}] \wedge C[\overrightarrow{\alpha}]$.

**preuve :** On a $C[\overrightarrow{\alpha} \wedge \overrightarrow{\alpha}] \prec C[\overrightarrow{\alpha}] \wedge C[\overrightarrow{\alpha}]$ par 2.3.3. Supposons l'inégalité stricte. Alors par 3.2.1. il existe $u$ tel que $u \downarrow C[\overrightarrow{\alpha} \wedge \overrightarrow{\alpha}] = \Omega$ et $u \downarrow C[\overrightarrow{\alpha}] \neq \Omega$ et $u \downarrow C[\overrightarrow{\alpha}] \neq \Omega$. Donc par 3.1.3. il existe $i, u'$ tels que $u' \downarrow (a_i \wedge A_i) = \Omega$, $u' \downarrow a_i \neq \Omega$ et $u' \downarrow A_i \neq \Omega$, ce qui est impossible si $a_i \uparrow A_i$. $\square$

Nous pouvons maintenant montrer les résultats finaux.

#### 3.2.3. Théorème de séquentialité :

Soient $C[\overrightarrow{\alpha}] \in C[\overrightarrow{\alpha}]$ et $\overrightarrow{\alpha} \in N^\infty$, soit $B = C[\overrightarrow{\alpha}]$, soit $u$ tel que $u \downarrow B = \Omega$. Alors on a un et un seul des deux cas suivants

1. $u \downarrow C[\overrightarrow{\alpha}] = \Omega$ pour tout $\overrightarrow{\alpha}' > \overrightarrow{\alpha}$

2. Il existe $i \in N$ et $u' \in N^\infty$ uniques tels que $\overrightarrow{\alpha}' \prec \overrightarrow{\alpha}'$ et $B \prec_u C[\overrightarrow{\alpha}']$ entraînent $\overrightarrow{\alpha}' \prec_{i, u'} \overrightarrow{\alpha}'$. De plus $u \downarrow C[\overrightarrow{\alpha}'] \neq \Omega$ dès que $\overrightarrow{\alpha}' > \overrightarrow{\alpha}$ et $u' \downarrow A'_i = z$, où $z$ n'apparaît pas dans $C[\overrightarrow{\alpha}]$

**preuve :** Supposons qu'il existe $\overrightarrow{\alpha}' > \overrightarrow{\alpha}$ tel que $u \downarrow C[\overrightarrow{\alpha}] \neq \Omega$. Alors par 2.3.2. et 3.2.1. on a $u \downarrow C[\overrightarrow{\alpha}] \neq \Omega$ pour un $\overrightarrow{\alpha}' \prec \overrightarrow{\alpha}'$. Puisque $\overrightarrow{\alpha}' \uparrow \overrightarrow{\alpha}$ on a $C[\overrightarrow{\alpha}' \wedge \overrightarrow{\alpha}] = C[\overrightarrow{\alpha}'] \wedge C[\overrightarrow{\alpha}]$ par 3.2.2. et donc $u \downarrow C[\overrightarrow{\alpha}' \wedge \overrightarrow{\alpha}] = \Omega$. Par 3.1.4. il existe $i, u'$ tels que $\overrightarrow{\alpha}'' > \overrightarrow{\alpha}' \wedge \overrightarrow{\alpha}'$ et $u \downarrow C[\overrightarrow{\alpha}''] \neq \Omega$ entraînent $\overrightarrow{\alpha}' \wedge \overrightarrow{\alpha}'' \prec_{i, u'} \overrightarrow{\alpha}''$ pour tout $\overrightarrow{\alpha}$'. Montrons que $i, u'$ répond à la question pour $\overrightarrow{\alpha}$.

- On a en particulier $u' \downarrow a'_i \neq \Omega$, donc $u' \downarrow A'_i = \Omega$ car $u' \downarrow (a'_i \wedge A'_i) = \Omega$
### 3.3. Stabilité et séquentialité dans d'autres modèles du λ-calcul

On peut se demander si des propriétés analogues existent dans des modèles de nature plus sémantiques comme $D^\infty$, $P^\omega$ ou $T^\omega$ (cf. [17,18,14]). Notons $\rho[M]$ la sémantique de $M$ dans un environnement $\rho$ (association de valeurs aux variables libres de $M$) pour un modèle continu ($D, \mathcal{C}$). On dira que ($D, \mathcal{C}$) est un modèle stable si on a

$$ \forall C[\ ] \in C[\ ], \forall \vec{A} \in N^\infty, \forall \rho, \forall \alpha \in C \ \rho[C[\vec{A}]] \\ \exists \vec{A}' \prec \vec{A} \ \text{minimum tel que } \alpha \in C \ \rho[C[\vec{A}']]] $$

En utilisant 3.2.4., il est clair que la propriété précédente est vraie pour tout contexte si et seulement si elle l'est pour le contexte vide. Pour montrer que $D^\infty$, $P^\omega$ et $T^\omega$ ne sont pas stables, on prend $a= xyy$ et on montre que pour $\rho$ convenable l'ensemble $\{a' \prec a \mid \rho[a'] = \rho[a]\}$ a deux éléments minimaux $xy\Omega$ et $x\Omega y$ :

- Pour $D^\infty$ ou $P^\omega$, prendre $\rho[x] = \lambda\alpha\beta$. $\alpha U\beta$ et $\rho[y] \neq \bot$

- Pour $T^\omega$ prendre $\rho[x] = \lambda\prec a,b\prec a',b'\prec$. $O \in a$ ou $O \in a'$ et prendre $\rho[y] = \prec\{o\},\emptyset\prec$, (avec les notations de Ploktin [13]).

## CONCLUSION.

Nous présentons en [2,3] une construction de modèles sémantiques préservant la propriété de stabilité. La construction de modèles sémantiques préservant la propriété de séquentialité semble plus délicate, et est reliée au problème de la construction de modèles pleinement abstraits du λ-calcul typé posé par Plotkin [13] et Milner [11] (Ces modèles sont tels que deux termes ont la même sémantique si et seulement si ils sont interchangeables dans tout programme). Différentes notions sémantiques de fonctions séquentielles ont été proposées dans la littérature [8,11,16,19]. Le fait que la propriété de séquentialité que nous avons mise en évidence est exactement une propriété de séquentialité au sens de Kahn-Plotkin [8] semble suggérer que cette définition est la plus adaptée à la construction sémantique de modèles séquentiels.
- Si $\vec{B} > \vec{A}$ vérifie $u \downarrow C[\vec{B}] \neq \Omega$, alors $u' \downarrow B_i \neq \Omega$ par $\vec{B} > \vec{a}' \wedge \vec{A}$ et 3.2.1.

- Si $\vec{B} > \vec{A}$ est tel que $u' \downarrow B_i = z$, alors $u \downarrow C[\vec{B}] \neq \Omega$ par monotonicité puisque $\vec{B} > \vec{a}' \wedge \vec{A}$. $\square$

### 3.2.4. Théorème de stabilité :
Soit $C[\vec{A}] \subseteq C[\vec{A}]$, soit $\vec{A} \in \mathbb{N}^\infty$

1. Pour tout $B' \subset C[\vec{A}]$ il existe $\vec{A}' \subset \vec{A}$ minimum tel que $B \subset C[\vec{A}']$

2. Pour tout ensemble majoré $\vec{X}$ de vecteurs sur $\mathbb{N}^\infty$, on a $C[\wedge \vec{X}] = \wedge C[\vec{X}]$

3. Si $\vec{A} \uparrow \vec{B}$, alors $C[\vec{A} \wedge \vec{B}] = C[\vec{A}] \wedge C[\vec{B}]$

**preuve** : 3. est un cas particulier de 2. et 1. se déduit de 2. en prenant $\vec{A}' = \wedge \{\vec{A}'' \mid \vec{A} \mid B \subset C[\vec{A}'']\}$

Montrons donc 2. On a par monotonicité $C[\wedge \vec{X}] \subset \wedge C[\vec{X}]$. Si l'inégalité est stricte, il existe $u$ tel que $C[\wedge \vec{X}] \subset_u \wedge C[\vec{X}]$. Par le théorème de séquentialité, il existe $i, u'$ tels que $\wedge \vec{X} \subset_{i, u'} \vec{A}$ pour tout $\vec{A} \in \vec{X}$ : ceci est impossible puisque $\vec{X}$ est majoré. Donc $C[\wedge \vec{X}] = \wedge C[\vec{X}]$. $\square$

Comme indiqué dans l'introduction, le théorème de stabilité exprime que l'opération de contexte préserve l'existence des calculs optimaux au sens de [10]. Lévy [10] montre que pour tout $A \subset M$ il existe une dérivation éventuellement infinie de $M$ qui est optimale pour calculer $A$ (nous laisserons ici le mot "optimal" complètement intuitif. Voir [10] pour une définition précise). Si on considère $A \subset C[M]$, on sait qu'il existe $A' \subset M$ minimum tel que $A \subset C[A']$. Le calcul optimal de $A'$ à partir de $M$ peut donc être appelé de façon naturelle *calcul optimal de A à partir de M dans C[\dots]*. Le théorème de séquentialité indique précisément comment trouver de manière semi-effective un radical critique de $M$ dans $C[\dots]$. et ceci uniquement en fonction de $\omega(M)$. L'algorithme est précisément donné par la démonstration. Il n'est bien sûr que semi-effectif, puisqu'on ne peut pas décider si $M \equiv \Omega$, donc si $M$ a un radical critique.
BIBLIOGRAPHIE

[1] H.P. BARENDREGT, J. BERGSTRA, J.W. KLOP, H. VOLKEN, "Degrees, reductions and representability in the λ-calculus" Univ. of Utrecht, Dept. of Math, Report n° 21, Jan. 1976.

[2] G. BERRY, "Calculs minimaux et optimaux des programmes dans les interprétations stables et séquentielles". Thèse à paraître.

[3] G. BERRY, "Stable functions as a model of typed λ-calculi" A paraître.

[4] G. BERRY, J.J. LEVY, "Minimal and Optimal Computations of Recursive Programs", Proc 3e ACM-SIGACT-SIGPLAN Conference on Principles of Programming Languages, Los Angeles, Jan. 1977.

[5] A. CHURCH, "The calculi of λ-conversion", AMS n° 6, Princeton 1941.

[6] E.W. DIJKSTRA, "Guarded Commands, nondeterminacy and formal derivation of programs", Comm. ACM 18, 8 (1975).

[7] P.J. DOWNEY, R. SETHI, "Correct Computation rules for recursive languages", SIAM journal of Computing, vol. 5, n° 3, p. 378-402, (1976).

[8] G. KAHN, G.D. PLOTKIN, "Concrete data types", à paraître.

[9] J.J. LEVY, "An algebraic interpretation of the λβk-calculus and an application of a labelled λ-calculus", Theoretical Computer Science, vol 2, n° 1, p. 97-114 (1976).

[10] J.J. LEVY, "Réductions correctes et optimales dans le λ-calcul", Thèse de doctorat d'état, Université Paris VII, 1977.

[11] R. MILNER, "Fully abstract models of typed λ-calculi", Theoretical Computer Science vol 4, n° 1, p. 1-23, (1977).

[12] G. MITSCHKE, "The standardization theorem for λ-calculus", Univ. of Swansea, (1975).

[13] G.D. PLOTKIN, "LCF considered as a programming language", Colloque Construction, amélioration et vérification de programmes, Arc et Senans, 1-3 juillet 1975. (A paraître dans T.C.S.).

[14] G.D. PLOTKIN, "Tω as a universal domain", Edinburgh University, Aout 1976.
[15] B.K. ROSEN, "Tree manipulation systems and Church-Rosser-Theorems", JACM vol 20, n° 1, (1973).

[16] V. SAZONOV, "Sequentially and parallelly computable functionals", λ-calculus and Computer Science Theory, Rome, (1975), et LNCS n° 37, Springer-Verlag.

[17] D. SCOTT, "Data types as Lattices", Notes, Amsterdam, (non publié), (1972).

[18] D. SCOTT, "Data types as Lattices", SIAM Journal of Computing, vol 5, n° 3, (1976).

[19] J. VUILLEMIN, "Syntaxe, sémantique et axiomatique d'un langage de programmation simple", Thèse de doctorat d'état, Université Paris VII, (1974).

[20] C.P. WADSWORTH, "The relation between computational and denotational properties for Scott's D∞ - models of the λ-calculus", SIAM Journal of computing, vol 5, n° 3, Sept. 1976.

Remerciements : Je tiens à remercier tout particulièrement Jean-Jacques Lévy qui a directement collaboré à ce travail, effectué pour la plus grande partie à l'IRIA.