# Le probleme du partage dans l'evaluation des λ-expressions

Jean-Jacques Levy

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

## To cite this version:

Jean-Jacques Levy. Le probleme du partage dans l'evaluation des λ-expressions. [Rapport de recherche] IRIA-RR-326, IRIA. 1978, pp.18. hal-04716542

HAL Id: hal-04716542

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

Submitted on 1 Oct 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
RIA

laboria

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20

laboratoire de recherche
en informatique
et automatique

LE PROBLÈME DU PARTAGE
DANS L'ÉVALUATION
DES λ-EXPRESSIONS

Jean-Jacques LÉVY

Rapport de Recherche N° 326

Septembre 1978
LE PROBLEME DU PARTAGE DANS L'ÉVALUATION DES λ-EXPRESSIONS

Jean-Jacques Levy*

Résumé :

Il s'agit de trouver des stratégies effectives et optimales de réductions dans le λ-calcul, c'est-à-dire d'obtenir le plus rapidement possible la forme normale d'une expression si elle existe. Les résultats de Vuillemin, Berry-Lévy obtenus pour les schémas de programmes récursifs et de Staples pour la logique combinatoire sont donc généralisés au λ-calcul. Cet article ne contient pas de démonstrations et le lecteur intéressé est renvoyé à «Réductions sûres et optimales dans le λ-calcul», J.J. Lévy, thèse, Paris VII, janvier 1978.

Abstract :

Effectives and optimal reductions strategies are defined in the λ-calculus. One wants to get the normal form of any expression in an optimal way. Results in Vuillemin, Berry-Lévy for recursive programs schemes and in Staples for the combinatory logic are thus generalized to the λ-calculus. The reader interested by proofs of the propositions contained in this paper is referred to «Réductions sûres et optimales dans le λ-calcul», J.J. Lévy, thèse, Paris, janvier 1978.

<footnote>* Cet article a été présenté au 1er Colloque AFCET-SMF de Mathématiques Appliquées tenu à l'Ecole Polytechnique, 4-8 septembre 1978, Palaiseau, France.</footnote>

<footnote>* The paper has been presented at 1er Colloque AFCET-SMF de Mathématiques Appliquées held in Ecole Polytechnique, 4-8 septembre 1978, Palaiseau, France.</footnote>
# LE PROBLEME DU PARTAGE DANS L'EVALUATION DES λ-EXPRESSIONS

Jean-Jacques LEVY*

## RESUME :

Il s'agit de trouver des stratégies effectives et optimales de réduction dans le λ-calcul, c'est à dire pour obtenir le plus rapidement possible la forme normale d'une expression si elle existe.

## 1. INTRODUCTION

Les relations entre le λ-calcul de Church[4] et les langages de programmation sont depuis longtemps établies (cf. Landin [9], Mac Carthy [12], Scott [15], Scott & Strachey [16], etc...). Nous considérerons ici le λ-calcul muni de la seule règle de β-conversion. En termes de langage de programmation, nous aurons donc un langage de programmation idéal, applicatif, sans types, muni de la seule opération d'appel de procédures. Toutefois, l'absence de types permettra aux procédures de prendre d'autres procédures en arguments (sans aucune restriction) et de donner des procédures comme résultats. D'autres formalismes auraient été possibles (le λ-calcul typé ou les schémas de programmes récursifs). Mais, des restrictions de types n'apporteraient aucune simplification pour notre problème et compliqueraient même le formalisme. Quant aux schémas de programmes récursifs (cf. Nivat [13], Vuillemin [18]), l'étude de leur évaluation partagée y est nettement plus simple et a été traitée par Vuillemin [18]. Staples[17] a également montré l'existence de réductions partagées dans le formalisme de la logique combinatoire. Mais les opérations de celle-ci ne correspondent pas simplement à des calculs sur les langages de programmation. L'étude de l'évaluation partagée dans le λ-calcul présente un double avantage : 1) c'est un langage

*IRIA-LABORIA, 78150 Rocquencourt
ge simple, 2) c'est un langage suffisamment général pour nous permettre d'adap-
ter un certain nombre de résultats dans d'autres systèmes de réécritures (cf.
Berry-Lévy [3]). La difficulté du partage dans l'évaluation des λ-expressions
provient essentiellement de l'existence de variables liées. De plus, en dépit
d'une première tentative due à Wadsworth [19], il n'existe pas à première vue
d'algorithme pour réaliser une évaluation partagée optimale. Cela exigera une
étude détaillée des mécanismes de réductions dans le λ-calcul et permettra
d'établir quelques résultats précisant ou généralisant les propriétés classi-
ques des réductions du λ-calcul. Le travail présenté ici a été développé dans
la thèse de l'auteur [11].

2. SYNTAXE DU Λ-CALCUL

2.1. Expressions

Le λ-calcul est un système de réécriture sur des expressions appelées
λ-expressions. Soient C et V des ensembles de constantes et de variables, alors
l'ensemble Λ(C,V), noté plus simplement Λ, des λ-expressions est le plus petit
ensemble contenant C et V et clos par les deux opérations suivantes :

1) Si M,N∈Λ, alors (MN)∈Λ (application)

2) Si $x \in V$ et $M \in \Lambda$, alors $(\lambda x M) \in \Lambda$ (abstraction)

On supprime habituellement un nombre excessif de parenthèses en uti-
lisant les abréviations suivantes :

$(M_1 M_2 M_3 \cdots M_n)$ pour $(\cdots ((M_1 M_2) M_3) \cdots M_n)$

$(\lambda x_1 x_2 \cdots x_n \cdot M)$ pour $(\lambda x_1 (\lambda x_2 \cdots (\lambda x_n M) \cdots))$

2.2 Occurrences

Pour désigner la sous-expression M+u d'occurrence u dans M, on utili-
sera un ensemble O(M) de mots fabriqués à partir des caractères 1,2 et λ véri-
fiant :

O(c) = O(x) = ε (mot vide) M↓ε = M

O(λxM) = {ε}∪λO(M) (λxM)↓λu = M↓u

O(MN) = {ε}∪10(M)∪20(N) (MN)↓1u = M↓u

(MN)↓2u = N↓u

Si M,N sont deux expressions et u∈O(M), alors on notera M[u←N] l'expression M où la sous-expression d'occurrence u est remplacée textuellement par N.
## 2.3 Variables et substitution

Dans toute expression $M$, on distingue deux ensembles de variables : l'ensemble VARLIB($M$) des variables libres et l'ensemble VARLIF($M$) des variables liées. Une occurrence $u$ d'une variable $x$ dans $M$ est liée ssi il existe $u_1, u_2$ et $N$ tels que $M \downarrow u = x$, $u = u_1 u_2$ et $M \downarrow u_1 = (\lambda x \cdot N)$. Sinon $u$ est une occurrence librè. L'occurrence du lieu d'une occurrence $u$ liée de $x$ dans $M$, notée LIEUR($M$, $u$), est l'occurrence $u_1$ maximale réalisant la condition précédente. En termes de programmation ALGOL, on retrouve donc les lois habituelles de portée de blocs, comme le montrent les deux exemples suivants :

1) $M = (\lambda x \cdot xx)(\lambda y \cdot yz)$. Alors les occurrences $1\lambda1$, $1\lambda2$, $2\lambda1$ sont liées et l'occurrence $2\lambda2$ est libre. Donc VARLIF($M$) = {$x,y$} et VARLIB($M$) = {$z$}.

2) $M = \lambda x \cdot (\lambda x \cdot xx)(\lambda y \cdot yx)(\lambda x \cdot xx)$. Alors les occurrences $\lambda11\lambda1$, $\lambda11\lambda2$, $\lambda12\lambda2$, $\lambda2\lambda1$ et $\lambda2\lambda2$ ont respectivement comme lieu $\lambda11, \lambda11, \epsilon, \lambda2$ et $\lambda2$.

Les règles de réécriture du $\lambda$-calcul sont définies principalement à partir d'une opération de substitution des variables libres. Cette opération est intuitivement évidente, mais légèrement compliquée par la présence des variables liées. L'expression $M[x\N]$ obtenue à partir de $M$ en substituant $x$ par $N$ est définie formellement par :

$$ 
\begin{align*}
c[x\N] &= c \\
x[x\N] &= N \\
y[x\N] &= y \quad \text{si } x \neq y \\
(\mathit{MM'})[x\N] &= (M[x\N] M'[x\N]) \\
(\lambda x \cdot M)[x\N] &= (\lambda x \cdot M) \\
(\lambda y \cdot M)[x\N] &= (\lambda z \cdot M[y\z][x\N]) \quad \text{si } x \neq y \text{ et } z \text{ est la variable telle que}
\end{align*}
$$

1) si $x \notin VARLIB(M)$ ou $y \notin VARLIB(N)$, alors $z=y$

2) sinon $z$ est la première variable de $V$ (en supposant donc $V$ énumérable) vérifiant $z \in VARLIB(M) \cup VARLIB(N)$. (On veille donc à ce qu'aucune occurrence libre d'une variable de $N$ ne devient liée dans $M[x\N]$).

## 2.4 Règles de conversion

Ecrivons $M \to N$ pour signifier que $M$ se récrit en $N$. Les règles de réécritures classiques du $\lambda$-calcul, encore appelées règles de conversion sont définies par :

(α-règle) $(\lambda x \cdot M) \to (\lambda y \cdot M[x\y])$ si $y \notin VARLIB(M)$

(β-règle) $((\lambda x \cdot M)N) \to M[x\N]$

(η-règle) $(\lambda x \cdot M_x) \to M$ si $x \in VARLIB(M)$

(δ-règle) $cM_1 M_2 \cdots M_n \to N$
La première règle signifie que les variables liées sont des variables muettes dont le nom a peu d'importance. Nous l'ignorerons donc et nous place- rons donc dans l'espace quotient engendré par la relation d'α-interconverti- bilité, l'égalité de deux expressions devant être souvent comprise comme éga- lité modulo cette règle. La β-règle représente l'application d'un argument à une procédure et est la seule règle qui nous intéresse. La η-règle est une no- tion d'extensionalité sur les fonctions et n'a pas grand sens d'un point de vue "informatique". Les δ-règles (qui peuvent être aussi nombreuses qu'il y a de constantes) servent à décrire le comportement de ces dernières. En fait, Church [4] en donne une définition plus restrictive. Nous les ignorerons ici et cela simplifiera notamment notre problème, quoique ces règles ont un sens important pour refléter le comportement des langages de programmation.

En résumé, comme nous ne nous intéressons qu'aux appels de procédures, nous ne considérerons que la β-règle. De plus, comme le comportement des const- tantes par rapport à la β-règle est identique à celui des variables libres, nous poserons C=Ø. Donc, le λ-calcul considéré ici sera un λ-calcul pur sans constantes muni de la seule β-règle.

## 2.5 Réductions

Appelons *radical* (redex en anglais) toute expression de la forme `((λx·M)N)`. Soit `RAD(M)` l'ensemble des occurrences des sous-expressions de M qui sont des radicaux. Si `ueRAD(M)`, on dit que M se réduit en N en une étape par conversion du radical d'occurrence u, noté $M \xrightarrow{u} N$, ssi $M \downarrow u = R \to S$ et $N = M[u \to S]$. On écrira aussi $M \xrightarrow{R} N$ quand l'occurrence du radical R de M est claire d'après le contexte, et $M \to N$ quand on ne se soucie pas du radical con- verti. (On a donc étendu le sens de $\to$). Une succession (éventuellement vide) $M \to M_1 \to M_2 \to \dots \to M_n = N$ de réductions élémentaires est appelée une *réduction*, que nous noterons également $M \xrightarrow{*} N$. Pour nommer une réduction, on posera

$$ \rho : M = M_0 \xrightarrow{u_1} M_1 \xrightarrow{u_2} M_2 \dots \xrightarrow{u_n} M_n = N $$

Les expressions d'origine et d'extrémité d'une réduction $\rho$ sont no- tées `ORG(\rho)` et `EXT(\rho)`. Dans notre exemple, on a `ORG(\rho)=M` et `EXT(\rho)=N`. De plus, si `EXT(\rho) = ORG(\sigma)`, la concatenation de $\rho$ et $\sigma$ est notée $(\rho;\sigma)$. Dans les lan- gages de programmation, une réduction correspond donc à des appels successifs de procédures, c'est à dire à un calcul (puisque nous ne nous intéressons qu'à ces derniers).

Une expression `M` irréductible, donc telle que `RAD(M)=Ø`, est dite *en forme normale*. Enfin, si $M \xrightarrow{*} N$ et N est en forme normale, alors on dit que M
a une forme normale.

Nous abandonnons à présent la terminologie des programmes en laissant le soin au lecteur d'associer aux mots "$\lambda$-expressions", "réductions" ou "forme normale", les mots "programme", "calcul" ou "résultat final", en étant conscient que cette analogie peut parfois offrir quelques difficultés.

### 3. EVALUATION PARTAGEE DE $\lambda$-EXPRESSIONS

Comme il peut y avoir plus d'un radical dans une même expression, plusieurs réductions sont possibles à partir de cette expression. Mais le théorème de Church-Rosser nous dit que, si une expression à une forme normale, alors celle-ci est unique. En fait, le théorème est plus fort et indique que si $M \stackrel{*}{\rightarrow} N$ et $M \stackrel{*}{\rightarrow} P$, alors il existe $Q$ tel que $N \stackrel{*}{\rightarrow} Q$ et $P \stackrel{*}{\rightarrow} Q$. Donc si on réduit une expression de manières différentes, on peut converger vers un résultat commun.

Appelons **stratégie de réduction** toute fonction $\phi$ définie pour toute expression $M$ qui n'est pas en forme normale et telle que $\phi(M) \in RAD(M)$. (Voir Barendregt [2]). Soit $\phi^*(M)$ la réduction associée, issue de $M$, telle que

$$ \phi(M) : M \xrightarrow{\phi(M)} M_1 \xrightarrow{\phi(M_1)} M_2 \xrightarrow{\phi(M_2)} \dots $$

Une **stratégie** $\phi$ sera correcte ssi, pour tout $M$ qui a une forme normale, alors $\phi^*(M)$ aboutit à cette forme normale. Une **stratégie** correcte $\phi$ sera optimale ssi, pour tout $M$ qui a une forme normale $N$, alors $|\phi^*(M)| \le |\rho|$ pour toute réduction $\rho$ telle que $ORG(\rho)=M$ et $EXT(\rho)=N$. (On représente par $|\rho|$ le nombre d'étapes de $\rho$). Autrement dit, une stratégie optimale atteint la forme normale en un nombre minimum d'étapes. Notre problème est simple : il s'agit de trouver des stratégies effectives optimales.

D'abord, il y a une réponse immédiate au problème de la correction. En effet, le théorème de standardisation de Curry & Feys [5] donne (en corol- laire) une stratégie très effective correcte : il suffit de contracter à chaque étape le radical le plus à gauche et le plus extérieur. La situation est aisément vue dans l'exemple suivant : soit $\Delta = \lambda x \cdot xx$, alors $\Delta\Delta$ n'a pas de forme normale, mais $(\lambda x \cdot y)(\Delta\Delta)$ en a une que l'on obtient immédiatement en contrac- tant le radical extérieur. Il peut être dangereux de réduire un argument avant de contracter un radical car ce dernier peut ne pas se servir de l'argument qui peut ne pas avoir de forme normale. On peut faire quelques variations sur ce thème et définir des stratégies "sures" ou "critiques" (cf. Vuillemin[18], Downey-Sethi [6], O'Donnell [14], Lévy [10]...).
réductions sur ces objets, 2) définir la notion de duplication sur la forme développée et la réduction simultanée de radicaux dupliqués.

La première approche est celle de Wadsworth [19]. Elle ne sera pas traitée ici. Elle est intéressante d'un point de vue informatique, car elle consiste à donner un évaluateur partagé optimal de $\lambda$-expressions. Wadsworth a en effet quelques difficultés, à cause des variables liées, comme le montre l'exemple suivant, en posant $I = \lambda x \cdot x$.

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

Dand $M_1$, le radical le plus à gauche et le plus extérieur est le radical $((\lambda y \cdot Iy)a)$. On voudrait donc le réduire sans dupliquer $Iy$. Résoudre ce problème n'est pas simple et reste ouvert. Wadsworth, dans ce cas, fait la duplication de $Iy$ et son algorithme n'est pas optimal. A la différence des schémas de programmes récursifs, on doit partager dans le $\lambda$-calcul des objets plus compliqués que des sous-expressions (en fait des "sous-contextes" ou des paires environnements-expressions).

Nous adopterons la seconde méthode et allons montrer que l'on peut définir des stratégies optimales sur la forme développée, à condition d'auto-riser la contraction simultanée de radicaux dupliqués.

## 4. DUPLICATIONS DE RADICAUX

Pour définir cette notion de duplication, on a besoin de dire ce que devient un radical après une réduction. C'est exactement ce que Church [4] a appelé l'ensemble des résidus d'un radical. (Cette définition avait été introduite pour démontrer Church-Rosser). Formellement, si $\rho : M \stackrel{*}{\to} N$ et si $u \in \text{RAD}(M)$, l'ensemble $u/\rho$ des résidus de $u$ par $\rho$ est un sous-ensemble de radicaux de $N$ définis par cas sur $\rho$ de la manière suivante.

1) si $|\rho|=0$, alors $u/\rho = \{u\}$

2) si $|\rho|>1$, alors $\rho = (\sigma;\tau)$ et $u/\rho = (u/\sigma)/\tau$

3) si $|\rho|=1$, alors $\rho : M \stackrel{Y}{\to} N$ et plusieurs cas se présentent selon la position de $u$ et de $v$

3a) si $u=v$, alors $u/\rho = \emptyset$
3b) si u et v sont disjoints ou si u contient strictement v, alors
$$u/\rho = \{u\}$$

3c) si u est contenu dans la partie fonction de v, c'est à dire
$$u = v1\lambda u', \text{ alors } u/\rho = \{vu'\}$$

3d) si u est contenu dans la partie argument de v, c'est à dire
$$u = v2u', \text{ alors}$$

$$u/\rho = \{vw' | \text{LIEUR}(M, v1\lambda w) = v1\}$$

En outre, admettons pour un instant définie la notion de conversion simultanée d'un ensemble de radicaux, notée $M \xrightarrow{U} N$ si $U \subset RAD(M)$. (On peut par exemple les contracter comme le fait Martin-Löt (voir [1]). L'analogue d'une réduction partagée sur la forme développée des expressions semble être de la forme

$$\rho : M = M_0 \xrightarrow{U_1} M_1 \xrightarrow{U_2} M_2 \xrightarrow{U_3} \dots$$

où, pour tout $n \ge 0$, on a $U_{n+1}$ maximum tel qu'il existe $m \le n$ et $u_m \in RAD(M_m)$ vérifiant $U_{n+1} = u_m/\rho_{m+1,n}$ (en désignant par $\rho_{m+1,n}$ le sous-segment de $\rho$ compris entre $M_m$ et $M_{m+1}$). On peut vérifier aisément qu'il existe qu'un seul tel $U_{n+1}$ contenant un $u_{n+1}$ donné de $RAD(M_n)$, pour tout $n \ge 0$, puisque, pour $u$ et $\rho$ donnés, il existe au plus un $v$ tel que $u \in v/\rho$. Cette forme de réduction est utilisée par O'Donnell [14]. Malheureusement, elle n'est pas suffisante comme le montre notre premier exemple de réductions partagées. En effet, dans

$$M = \Delta((\lambda x \cdot xa)I) \xrightarrow{U_1} M_1 = ((\lambda x \cdot xa)I)((\lambda x \cdot xa)I) \xrightarrow{U_2} M_2 = (Ia)(Ia) \xrightarrow{U_3} M_3 = aa$$

les deux radicaux de $U_2$ sont bien résidus d'un radical de $M$, mais les deux radicaux de $U_3$ ne sont pas résidus d'un même radical. Pour arriver à les relier, il faut donc une relation plus forte. Pour ce faire, il y a deux méthodes :

1) décréter que deux radicaux sont des duplications d'un même objet, non seulement si ce sont des résidus d'un même radical, mais aussi s'ils sont créés de la même manière par deux radicaux déjà reliés. Mais la création des radicaux est un phénomène horrible dans le $\lambda$-calcul. On peut toutefois s'en sortir en introduisant un $\lambda$-calcul étiqueté (voir [11]) qui n'est qu'une adaptation (non triviale) d'un formalisme étiqueté de Vuillemin [18], ou en se servant d'un douloureux formalisme de sous-contextes.

2) s'appercevoir que l'on peut permuter les deux premières étapes de la réduction précédente et que, dans la réduction

$$M = \Delta((\lambda x \cdot xa)I) \xrightarrow{U_1} M'_1 = \Delta(Ia) \xrightarrow{U_2} M_2 = (Ia)(Ia) \xrightarrow{U_3} M_3 = aa$$

ainsi obtenue, les deux radicaux de $U_3$ sont bien résidus d'un même radical.
Autrement dit, il faut étudier les duplications de radicaux modulo des permutations de réductions.

Le premier effort sera donc d'étudier les propriétés des permutations de réductions.

## 5. REDUCTIONS EQUIVALENTES PAR PERMUTATIONS

Le théorème des développements finis, démontré par Church [4] et Curry[5] pour le $\lambda I$-calcul et par Hindley [7], BBKV[2], Lévy[11] dans toute sa généralité, permet de définir très fortement la contraction simultanée de plusieurs radicaux.

Soit $U \subset RAD(M)$. Une réduction $\rho$ issue de $M$ est relative à $U$ si elle ne consiste qu'à contracter des radicaux résidus de radicaux de $U$. De plus, ce sera un développement de $U$ si $U/\rho = \emptyset$.

**Théorème :** Soit $U \subset RAD(M)$.

1) Il n'y a pas de réductions relatives à $U$ infinies

2) Si $\rho$ et $\sigma$ sont deux développements de $U$, alors $EXT(\rho) = EXT(\sigma)$

3) Si $\rho$ et $\sigma$ sont deux développements de $U$ et si $v \in RAD(M)$, alors $v/\rho = v/\sigma$.

La démonstration n'est pas si simple, car $U$ peut contenir des radicaux imbriqués. On peut donc définir sans ambiguïté la réduction $M \underset{N}{\stackrel{U}{\to}} P$ de plusieurs radicaux et la troisième partie du théorème indique que l'on peut toujours parler de résidus de manière cohérente. Un corollaire intéressant est le lemme de permutation suivant, aussi appelé lemme des déplacements parallèles.

**Lemme :** Si $U, V \subset RAD(M)$, si $\rho : M \stackrel{U}{\to} N$ et $\sigma : M \stackrel{V}{\to} P$, si $U' = U/\sigma$ et $V' = V/\rho$, et si $\rho \sqcup \sigma$ et $\sigma \sqcup \rho$ sont les deux réductions $M \underset{N}{\stackrel{U}{\to}} Q_1 \stackrel{V'}{\to} P$ et $M \stackrel{V}{\to} P \underset{Q_2}{\stackrel{U'}{\to}} Q_2$, alors

1) $EXT(\rho \sqcup \sigma) = EXT(\sigma \sqcup \rho)$

2) si $w \in RAD(M)$, alors $w/(\rho \sqcup \sigma) = w/(\sigma \sqcup \rho)$.

Le lemme s'obtient à partir du théorème en considérant trivalement $U \cup V$, et se résume sur les deux figures suivantes
<figure><img src="image_4.png" /></figure>

On en déduit aisément le théorème de Church-Rosser par le pavage suivant, qui permet également de définir les résidus $\sigma/\rho$ et $\rho/\sigma$ de deux réductions coinitiales $\sigma$ et $\rho$.

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

Posons également $\rho\parallel\sigma = (\rho;(\sigma/\rho))$ si $\rho$ et $\sigma$ sont coinitiales. Le lemme précédent devient triviallement :

**Lemme :** Si $\text{ORG}(\rho) = \text{ORG}(\sigma) = M$, alors

1) $\text{EXT}(\rho\parallel\sigma) = \text{EXT}(\sigma\parallel\rho)$ (propriété Church-Rosser)

2) Si $\text{ORG}(\tau) = M$, alors $\tau/(\rho\parallel\sigma) = \tau/(\sigma\parallel\rho)$.

La réduction d'un ensemble vide de radicaux issue de $M$ est notée $\emptyset_M$ ou plus simplement $\emptyset$. Une réduction de plusieurs telles étapes est aussi noté $\emptyset$. (En fait, il s'agit plus ou moins de la réduction vide).

**Définition :** L'équivalence de deux réductions $\rho$ et $\sigma$ par permutations
est la plus petite congruence pour la concaténation engendrée par le lemme de permutation. Autrement dit $\rho \equiv \sigma$ est défini par

1) $\rho \sqcup \sigma \equiv \sigma \sqcup \rho$

2) $\rho;\emptyset \equiv \emptyset;\rho \equiv \rho$

3) Si $\rho \equiv \sigma$ et $\sigma \equiv \tau$, alors $\rho \equiv \tau$

4) Si $\rho \equiv \sigma$, alors $(\tau;\rho;\tau') \equiv (\tau;\sigma;\tau')$

Dans le premier cas, on peut se contenter de supposer $|\rho|=|\sigma|=1$. Grâce aux propriétés de commutation précédentes, on montre aisément :

**Proposition :**

1) $\rho \equiv \sigma \text{ ssi } \rho/\sigma=\emptyset \text{ et } \sigma/\rho=\emptyset$ ($\equiv$ est donc décidable)

2) $(\tau;\rho) \equiv (\tau;\sigma)$ implique $\rho \equiv \sigma$ (simplifiabilité à gauche)

3) $\rho \equiv \sigma \text{ ssi } \forall \tau \cdot \tau/\rho=\tau/\sigma$ (cohérence des résidus),

4) $\rho \equiv \sigma$ implique $\rho/\tau \equiv \sigma/\tau$

Il est aussi naturel de considérer la relation suivante sur les réductions coinitiales.

**Définition :** $\rho \le \sigma \text{ ssi } \rho/\sigma=\emptyset$

**Proposition :**

1) $\rho \le \rho$ et si $\rho \le \sigma \le \tau$, alors $\rho \le \tau$ ($\le$ est un préordre)

2) $\rho \equiv \sigma \text{ ssi } \rho \le \sigma \le \rho$ (avec $\equiv$ comme équivalence associée)

3) $\rho \le \sigma \text{ ssi } \exists \tau \cdot (\rho;\tau) \equiv \sigma$

4) $\rho \le \rho \sqcup \sigma$ et $\sigma \le \rho \sqcup \sigma$

5) Si $\rho \le \tau$ et $\sigma \le \tau$, alors $\rho \sqcup \sigma \equiv \sigma \sqcup \rho \le \tau$

Donc, l'ensemble des réductions issues d'une même expression a une structure de *sup-demi treillis*. On retrouve le treillis de calcul de Vuillemin [18], mais la démonstration est beaucoup plus simple en termes de résidus et ne demande aucune restriction. Curry [5] dit qu'une réduction

$$ \rho : M = M_0 \xrightarrow{u_1} M_1 \xrightarrow{u_2} M_2 \cdots \xrightarrow{u_n} M_n = N $$

est *standard* ssi, pour tout i et j tels que $1 \le i < j \le n$, on n'a pas $u_j \equiv u'_j/\rho_{i,j-1}$ avec $u'_j$ plus externe ou plus à gauche que $u_i$. On peut améliorer le résultat de Curry.

**Proposition :** Pour tout $\rho$, il existe une et une seule réduction $\rho_s$ *standard* telle que $\rho \equiv \rho_s$.
On peut remarquer que plusieurs réductions standards sont possibles entre deux mêmes expressions (par exemple $I(Ix)$ et $Ix$ où $I = \lambda x \cdot x$) et que $\stackrel{*}{\to}$ n'engendre pas de structure de treillis (par exemple $I(K(Ix)y)$ où $I = \lambda x \cdot x$ et $K = \lambda xy \cdot x$).

## 6. FAMILLES DE RADICAUX

Pour signaler que $u \in \text{RAD}(\text{EXT}(\rho))$ ou $U \subset \text{RAD}(\text{EXT}(\rho))$, nous écrirons $(\rho, U)$ ou $(\rho, U)$. Ayant ainsi relativisé les radicaux par rapport aux réductions, on est en mesure de définir la relation de *duplication* recherchée.

**Définition :** $(\rho, u) \leq (\sigma, v)$ ssi $\exists \tau \cdot (\rho; \tau) \equiv \sigma$ et $\text{veu}/\tau$

**Proposition :**

1) $(\rho, u) \leq (\sigma, v)$ ssi $\rho \leq \sigma$ et $\text{veu}/(\sigma/\rho)$ ($\leq$ est décidable)

2) $\leq$ est compatible avec $\equiv$

3) $\leq$ est une relation d'ordre (modulo $\equiv$)

On peut même fermer la relation précédente par symétrie et transitivity et définir une notion de *famille de radicaux* qui partitionne tous les radicaux apparaissant dans les expressions obtenues par les réductions issues d'une même expression.

**Définition :** $(\rho, u) \sim (\sigma, v)$ ssi

1) $(\rho, u) \leq (\sigma, v)$ ou $(\sigma, v) \leq (\rho, u)$

2) ou $\exists (\tau, w)$. $(\rho, u) \sim (\tau, w) \sim (\sigma, v)$

**Proposition :**

1) $\sim$ est compatible avec $\equiv$

2) $(\emptyset, u) \sim (\sigma, v)$ ssi $(\emptyset, u) \leq (\sigma, v)$ ssi $\text{veu}/\sigma$

Le théorème des développements finis peut être généralisé, et cela éclaire la démonstration que nous avions en [10] sur les réductions de l'in Exhibit 1. Soit $\text{FAM}(\rho)$ l'ensemble des familles des radicaux contractés dans $\rho$, c'est à dire $\text{FAM}(\rho) = \{[(\rho_{i-1}, u_i)]\}$ où $\rho_i$ représente les i premières étapes de $\rho$ et $u_i$ est un des radicaux contractés à l'étape i. Alors $\rho$ est une réduction relative à X ssi $\text{FAM}(\rho) \subset X$. Et $\rho$ est un développement de X si $\rho$ est relative à X et il n'existe pas de tel que $[(\rho, u)] \notin X$.

**Théorème :** Si X est fini,
1) il n'y a pas de réductions relatives à X intinies

2) si $\rho$ et $\sigma$ sont deux développements de $X$, alors $\rho \equiv \sigma$, c'est à dire
$\mathrm{EXT}(\rho) = \mathrm{EXT}(\sigma)$ et, pour tout $\tau$ coinitial, on a $\tau/\rho = \tau/\sigma$.

A présent, nous donnons un procédé de décision pour la relation de même famille sur les radicaux. Ce procédé est malheureusement un peu technique. Intuitivement, il signifiera que deux radicaux sont dans une même famille ssi ils sont créés de la même manière.

**Définition** : Si $\mathrm{EXT}(\rho) = \mathrm{ORG}(\sigma)$, alors $\sigma$ est possible avant $\rho$ si la quantité $\mathrm{RES}^{-1}(\rho, \sigma)$ suivante est définie.

1) $\mathrm{RES}^{-1}(\rho, \sigma) = 0$ (où $\sigma$ est la réduction vide).

2) Si $|\sigma|=1$, alors $\mathrm{RES}^{-1}(\rho, (\sigma;\tau)) = (\sigma';\mathrm{RES}^{-1}(\rho/\sigma', \tau/(\sigma'/(\rho;\sigma)))))$ où si $\sigma : M \xrightarrow{U} N$, on a $\sigma' : M' \xrightarrow{U'} N'$ avec $U'$ minimum tel que $U\subset U'/\rho$.

Si $\mathrm{RES}^{-1}(\rho, \sigma)$ existe, on a aisément $\sigma \le \mathrm{RES}^{-1}(\rho, \sigma)/\rho$ et cela justifie en quelque sorte notre notation. L'extraction dans $\rho$ des étapes nécessaires pour faire la dernière étape se définit par la réduction $\mathrm{E}(\rho)$ coinitiale suivante.

**Définition** : Si $|\rho|=1$, alors

1) $\mathrm{E}(\rho) = \rho$

2) $\mathrm{E}(\rho;\sigma) = \mathrm{RES}^{-1}(\rho, \mathrm{E}(\sigma))$ si $\mathrm{E}(\sigma)$ est possible avant $\rho$

3) $\mathrm{E}(\rho;\sigma) = \rho;\mathrm{E}(\sigma)$ sinon

Enfin, notons $r$ et $r^{-1}$ les transformations duales suivantes de paires réduction-radical en réduction : $r(\rho,U) = (\rho;\tau)$ si $M = \mathrm{EXT}(\rho)$ et $\tau : M \xrightarrow{U} N$, réciproquement $r^{-1}(\rho;\tau) = (\rho;U)$. Le procédé de décision pour la relation de famille s'obtient comme suit.

**Définition** : $C(\rho,u) = r^{-1}(\mathrm{E}(r(\rho_s,\{u\})))$ où $\rho_s$ est la réduction standard telle que $\rho \equiv \rho_s$.

**Proposition** :

1) $(\rho,u) \sim (\sigma,v)$ ssi $C(\rho,u) = C(\sigma,v)$ ($\sim$ est décidable)

2) Si $C(\rho,u) = (\sigma,V)$, alors $\sigma$ est standard et $V = \{v\}$

3) $C(\rho,u) \sim (\rho,u)$ (C(ρ,u) est donc canonique dans $[(\rho,u)]$)

4) C(ρ,u) est le seul élément (σ,v) dans $[(\rho,u)]$ tel que σ est
standard et $|σ|$ minimum.

5) Si $C(\rho, u) = (\rho, u)$, alors pour tout $\sigma$ vérifiant $\rho \le \sigma$, on a $(\rho, u) \sim (\sigma, v)$ ssi $(\rho, u) \le (\sigma, v)$ ssi $v \in u/(\sigma/\rho)$.

Un autre procédé de décision est possible avec le $\lambda$-calcul étiqueté que nous avons en [11]. Alors deux radicaux sont dans une même famille ssi ils ont même étiquette. Remarquons finalement que les relations de duplication et de même famille peuvent être définies sans considerer l'équivalence des réductions par permutations, mais alors ces deux relations ne seraient pas décidables.

## 7. REDUCTIONS OPTIMALES

Le problème des réductions partagées soulevé en §4 peut à présent être aisément résolu.

**Définition** : Une réduction $\rho : M = M_0 \underset{U_1}{\overset{U_1}{\to}} M_1 \underset{U_2}{\overset{U_2}{\to}} \dots \underset{M_n}{\overset{U}{\to}} M_n = N$ est f-complète ssi, pour tout $i$ tel que $1 \le i \le n$, on a $U_i = \{u \mid (\rho_{i-1}, u) \sim (\rho_{i-1}, u_i)\}$ si $u_i \in U_i$ et $\rho_i$ représente les i premières étapes de $\rho$. De même, la réduction $\rho$ est d-complète ssi, pour tout $i$, l'ensemble $U_i$ est maximum tel qu'il existe $\sigma_i, \tau_i$ et $u_i$ vérifiant $(\sigma_i; \tau_i) \sim \rho_{i-1}$ et $U_i = u_i/\tau_i$.

**Proposition** :

1) Si $\rho$ est f-complète, alors pour $1 \le i \le |\rho|$ on a $C(\rho_{i-1}, U_i) \le (\rho_{i-1}, U_i)$ en utilisant des notations analogues aux précédentes.

2) $\rho$ est f-complète ssi $\rho$ est d-complète.

3) Si $\rho$ et $\sigma$ sont complètes, alors $\rho \unlhd \sigma$ et $\sigma \unlhd \rho$ sont complètes. Donc les réductions complètes forment un sous-treillis du treillis des réductions.

4) Si $\rho$ est complète et n'a aucune étape vide, alors $|\rho| = \text{card}(\text{FAM}(\rho))$.

Dans les réductions partagées, la contraction simultanée de deux radicaux dupliqués d'un même est une opération de coût unitaire. On peut donc supposer que l'on a une fonction de coût sur les réductions vérifiant $COUT(\rho) \ge \text{card}(\text{FAM}(\rho))$.

**Théorème** : Si $\rho$ est une réduction complète et si $\rho$ contracte au moins à chaque étape le radical le plus à gauche et le plus extérieur, on a $|\rho| \le COUT(\sigma)$ pour toute réduction $\sigma$ vérifiant $\sigma \equiv \rho$.

Le théorème de standardadisation nous indique que de telles réduc-
tions optimales mènent à la forme normale si elle existe. En outre, toutes les réductions aboutissant à la forme normale et issues d'une même expression sont trivialement équivalentes. Donc le théorème précédent montre bien l'existence de stratégies effectives optimales pour obtenir la forme normale de toute expression. On peut également généraliser ce résultat aux expressions sans forme normale en introduisant une notion d'approximation (cf. [11]).

## 8. CONCLUSION

Il ne reste plus qu'à trouver l'algorithme d'évaluation de $\lambda$-expressions correspondant à nos stratégies. C'est un problème de structures de données qui dépasse en fait le formalisme du $\lambda$-calcul et qui se pose dans tout système où des variables liées peuvent exister. En outre, on peut essayer de généraliser nos résultats à d'autres systèmes de réécritures et obtenir ainsi quelques propriétés d'interpréteurs plus réalistes de langages de programmation (cf. Huet-Lévy [8]).

## 9. REMERCIEMENTS

Je remercie particulièrement Gérard Berry. L'équivalence par permutations avait été défini par l'auteur par $\rho/\sigma = \sigma/\rho = \emptyset$. Gérard a eu l'idée de la définir en termes de permutations, ce qui est beaucoup plus intuitif. Par ailleurs, l'unicité de la réduction standard dans chaque classe de permutations a été obtenue en commun. Merci aussi à Gérard Huet pour quelques simplifications dans les notations.

## 10. REFERENCES

[1] Barendregt, H.P., "Some extensional term models for combinatory logics and $\lambda$-calculi", PhD Thesis, Utrecht, 71.

[2] Barendregt, H.P., Bergstra, J., Klop, J.W., Volken, H., "Degrees, reductions and representability in the $\lambda$-calculus", Univ. of Utrecht, Dept. of Math., Rapport n°22, Février 76.

[3] Berry, G., Lévy, J.J., "Minimal and optimal computations of recursive programs", 4th ACM-POPL Conf, Santa Monica, Janvier 76 et à paraître dans JACM.

[4] Church, A., "The calculi of $\lambda$-conversion", AMS n°6, Princeton, 41.
[5] Curry, H.B., Feys, R., "Combinatory logic", Volume 1, North-Holland, 1958.

[6] Downey, P.J., Sethi, R., "Correct computations rules for recursive languages", SIAM Journal, Vol 5, n°3, Sept. 76.

[7] Hindley, R., "The equivalence of complete reductions", Univ. of Swansea, 1975.

[8] Huet, G., Lévy, J-J., à paraître.

[9] Landin, P., "A correspondence between ALGOL 60 and Church's lambda notation", CACM, Vol. 8, n°2, n°1, 1965.

[10] Lévy, J-J., "Réductions sures dans le λ-calcul", 3e cycle, Paris 7, Juin 74 et aussi dans TCS, Vol 2, n°1, 76.

[11] Lévy, J-J., "Réductions correctes et optimales dans le λ-calcul", Thèse d'Etat, Paris 7, Janvier 78.

[12] Mac Carthy, J. et al., "LISP 1.5 Programmer's manual", MIT Press, Cambridge, 62.

[13] Nivat, M., "On the interpretation of recursive programs schemes", Symposia Mathematica, Vol XV, Instituto Nazionale di Alta Matematica, Italie, 75.

[14] O'Donnell, M., "Reductions strategies in tree replacement systems", Cornell, PhD Thesis, Sept. 76.

[15] Scott, D., "Continuous lattices", Oxford PRG-7, Computing Lab, Août 71.

[16] Scott, D., Strachey, C., "Towards a mathematical semantics for computer languages", Oxford PRG-6, 71.

[17] Staples, J., "Efficient combinatory reductions", Queensland Institute of Techn., Math. Dept., Brisbane, Australie, 74.

[18] Vuillemin, J., "Proof techniques for recursive programs", PhD Thesis, Stanford 73.

[19] Wadworth, C.P., "Semantics and pragmatics for the λ-calculus", PhD Thesis, Oxford 71.