# An algebraic interpretation of the lambda beta kappa-calculus and a labelled lambda-calculus

Jean-Jacques Levy

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

## To cite this version:

Jean-Jacques Levy. An algebraic interpretation of the lambda beta kappa-calculus and a labelled lambda-calculus. [Research Report] IRIA-RR-103, IRIA. 1975, pp.27. hal-04716090

HAL Id: hal-04716090

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

Submitted on 1 Oct 2024

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
RIA
laboria

laboratoire de recherche
en informatique
et automatique

An algebraic interpretation
of the λ β κ-calculus
and a labelled λ-calculus

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

J.J. Levy

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
78150 - Le Chesnay
Tél. 954.90.20

Rapport de Recherche n·103

Février 1975.
AN ALGEBRAIC INTERPRETATION OF THE $\lambda\beta K$-CALCULUS
AND A LABELLED $\lambda$-CALCULUS

J.J. Levy

**Résumé:** Scott [10,11] a proposé de nombreux modèles pour le λ-calcul. Dans ces interprétations, la relation d'interconvertibilité est étendue en identifiant principalement les termes non solvables (c'est à dire les expressions M telles que, pour tous arguments $N_1, N_2, ..., N_k$, l'expression $MN_1N_2...N_k$ n'a pas de forme normale). Cette extension est consistente comme Barendregt [1] et Wadsworth [13] l'ont montré. La plupart des modèles de Scott se comporte bien si l'on assimile les λ-expressions à des programmes; plus précisément, toute expression y est égale à la limite de ses approximations (voir Wadsworth [13]). Nous partirons de ce principe en définissant la valeur de toute expression par son ensemble d'approximations et nous montrerons que notre interprétation définit une congruence sur l'ensemble des λ-expressions. Pour ce faire, nous montrerons une conjecture énoncée par Welch [14] sur la complétude des réductions de l'intérieur vers l'extérieur en introduisant un λ-calcul étiqueté qui a l'air de se révéler comme un outil intéressant. Des travaux similaires ont été réalisés par Welch [15] et Hyland [4]. La définition de notre interprétation est analogue à celles de Nivat [9] et Vuillemin [12] utilisées pour les systèmes de fonctions définies récursivement. Enfin, le lecteur est prié de se référer à [5], où la plupart des résultats existent déjà.

**Introduction** : A wide range of λ-calculus models has been proposed by Scott[10,11]. In these interpretations, the interconvertibility relation among λ-expressions is extended by mainly equating the unsolvable terms ( i.e. expressions M such that, for any arguments $N_1, N_2, ..., N_k$, the expression $MN_1N_2...N_k$ has no normal form ). This extension has been shown consistent by Barendregt [1] and Wadsworth [13]. Wadsworth [13] showed the adequacy of most of Scott's models from a computational point of view ; more precisely, each expression is equal to the limit of its approximations in these models. We will try to go in the reverse direction, in the
first part of this paper, and to define the value of an expression from its set of approximations. Then we prove that, as usual, our interpretation defines (using Milner's words [7]) a congruence on the language of λ-expressions. For this, we follow Welch [14] who stated a conjecture about the completeness in the reducibility sense, of "inside-out reductions". This conjecture is proved in the second part of this paper by introducing a "labelled λ-calculus", which the author believes to be a useful tool for some λ-calculus problems. The results in this paper are related to the ones in Hyland [4] and Welch [15]. The definition of our interpretation is very similar to the one of Nivat [9] and Vuillemin [12] used for systems of recursively defined functions. Most results appeared in the author's thesis [5].
**Syntax** : We consider the set $\Lambda$ of $\lambda$-expressions, built from an infinite alphabet $V$ of variables, which is the minimal set containing :

(1) $x$ ( variable )

(2) ($\lambda x M$) ( abstraction )

(3) ($M N$) ( application )

where $x$ is in $V$ and $M, N$ are already in $\Lambda$. And we will use the standard abbreviations where :

$MNN_1N_2...N_k$ stands for $(...((MN)N_1)N_2)...N_k)$
$(\lambda x_1 x_2...x_m M)$ " " $(\lambda x_1 (\lambda x_2... (\lambda x_m M)...))$

and $M, N, N_i$ are expressions in $\Lambda$, $x_i$ are variables. We shall also omit the outermost parenthesis of an expression. The usual notions of free and bound variables are assumed defined and we note $M[x\setminus N]$ for the substitution of $N$ for the free occurrences of $x$ in $M$. We consider only two rules of conversion : the $\alpha$ and $\beta$ rules. If $M$ derives from $M$ by an $\alpha$-conversion, we write $M \xrightarrow{\alpha} N$. Similarly we have $M \xrightarrow{\beta} N$, and a reduction ( possibly of length zero ) using only $\alpha$-conversion from $M$ to $N$ is written $M \xrightarrow{\alpha}^* N$. Hence we note $M \xrightarrow{\beta}^* N$ and $M \xrightarrow{\alpha, \beta} N$ for $\beta$-reduction or any sequence of $\alpha$ and $\beta$ conversions from $M$ to $N$. We often forget $\alpha$-conversions and $M \to N$ or $M \xrightarrow{\alpha}^* N$ are understood as $M \xrightarrow{\beta} N$ or $M \xrightarrow{\alpha, \beta} N$. Equality must also be considered as equality modulo some $\alpha$-conversions. We will try to use the usual terminology ( residuals, standard, reductions ... ) defined in [2,3]. We also make use of the context notation ( See [8,13] ).

Let us first remark that $\Lambda$ can also be considered as the smallest set containing :

(i) $\lambda x.M$ ( abstraction )

(ii) $xM_1M_2...M_n$ ( head normal form )

(iii) $(\lambda x.M)NM_1M_2...M_n$

if $x$ is a variable and $M, N, M_i$ are expressions of $\Lambda$. More generally, a head normal form is any expression of the form $\lambda x_1 x_2...x_m (xM_1M_2...M_n)$ where $m, n \ge 0$ (See [13]). Others expressions are of the form $\lambda x_1 x_2...x_m (\lambda x.M)NM_1M_2...M_n$ and have a head redex $(\lambda x.M)N$. If $M \xrightarrow{\alpha}^* N$ and $N$ is an abstraction ( respectively a head normal form ) we say that $M$ has an abstraction form ( respectively a head normal form ).

**Proposition 1** : If $M$ has an abstraction form, then $M$ has a minimal abstraction form $\lambda x.N_0$, i.e. we have $M \xrightarrow{\alpha}^* \lambda x.N_0$ and, for any $\lambda x.N$ such that $M \xrightarrow{\alpha}^* \lambda x.N$, we have $\lambda x.N_0 \xrightarrow{\alpha}^* \lambda x.N$.

**Proof** : $M$ can be only of form (i) or (iii). In the first case, we have $M = \lambda x.N_0$. Otherwise for any, $\lambda x.N$ such that $M \xrightarrow{\alpha}^* \lambda x.N$, by the standardization theorem, there is a standard reduction :

$$M = M_0 \xrightarrow{R_1} M_1 \xrightarrow{R_2} M_2 \xrightarrow{R_3} \dots \xrightarrow{R_n} M_n = \lambda x.N$$
from M to $\lambda x.N$. Let $M_k$ be the first $M_i$ which is an abstraction. Then, since the reduction is standard, the redexes $R_j$ contracted between $M_{j-1}$ and $M_j$ are the head redexes of $M_{j-1}$ for $1 \le j \le k$. So each standard reduction from M to some $\lambda x.N$ has a common initial part :

$$ M_0 \underset{M_1}{\overset{R_1}{\to}} M_1 \underset{M_2}{\overset{R_2}{\to}} M_2 \underset{M_k}{\overset{R_k}{\to}} \dots \underset{M_k}{\overset{R_k}{\to}} M_k \quad \square $$

**Proposition 2** : If M has a head normal form, then M has a minimal one.

The proof is very similar to the preceding one. In both cases, the minimal form is obtained by contracting head redexes until an expression of the desired form is reached.

**Approximations** : We still follow Wadsworth [13] and define the direct approximation $\phi(M)$ of an expression M by :

$$ \left\{ \begin{array}{l} \phi(\lambda x.M) = \lambda x.\phi(M) \\ \phi(xM_1M_2\dots M_n) = x(\phi(M_1))(\phi(M_2))\dots(\phi(M_n)) \\ \phi(\lambda x.M)NM_1M_2\dots M_n) = \Omega \end{array} \right. $$

where $\Omega$ is an extra constant. Basically, $\phi(M)$ is obtained from M by replacing all ( outermost ) redexes of M by $\Omega$ and substituting $\Omega M$ by $\Omega$ until normal form. If $\Omega$ is understood as "undefined", $\phi(M)$ is the information we have from M without contracting its redexes. There is a slight modification from the Wadsworth's definition, because we do not want to identify $\Omega$ and $\lambda x.\Omega$.

We define $N$ as $N = \phi(\Lambda)$. Obviously, $N$ is the set of expressions in $\omega-\beta$ normal forms. More precisely $N$ is the minimal set containing :

$$ \left\{ \begin{array}{l} \Omega \\ \lambda x.a \\ xa_1a_2\dots a_n \end{array} \right. $$

if $x$ is a variable and $a, a_i$ are already in $N$. By considering $\Omega$ as a minimal element in $N$ and extending by monotony, we get the following partial order $<$ in $N$ :

$$ \left\{ \begin{array}{ll} \Omega < a & \\ \lambda x.a < \lambda x.b & \text{if } a < b \\ xa_1a_2\dots a_n < xb_1b_2\dots b_n & \text{if } a_i < b_i \text{ for } 1 \le i \le n \end{array} \right. $$

where $a, b, a_i$ are expressions of $N$, $x$ is a variable and $n \ge 0$. Here, we must take care of $\alpha$-conversion and the order $<$ is, in fact, an order between equivalence classes defined on $N$ by the $\alpha$-interconvertibility. So, if $a \underset{\alpha}{\overset{*}{\to}} a'$ and $b \underset{\alpha}{\overset{*}{\to}} b'$, we have $a < b$ iff $a' < b'$. Moreover, we notice that $a<b$ iff there are $M, N$ in $\Lambda$ such that $\phi(M) = a, \phi(N) = b$ and $M \not\equiv N$.
**Proposition 3** : The set N is a semi-lattice where every directed subset (*) is a lattice. More precisely :

1) N has a minimal element Ω.

2) for any pair a,b of elements in N, there exists a greatest lower bound a⊓b. ( meet operation )

3) for any pair a,b of elements in N which are dominated by a common upper bound, there exists a least upper bound a⊔b. ( join operation )

The proof is trivial, and obviously we can give the inductive definitions of a⊔b and a⊓b ( up to some α-conversions as for the definition of < above ) :

$$ egin{cases} (\lambda x.a)\sqcap(\lambda x.b) = \lambda x.(a\sqcap b) \\ (xa_1a_2...a_n)\sqcap(xb_1b_2...b_n) = x(a_1\sqcap b_1)(a_2\sqcap b_2)...(a_n\sqcap b_n) \\ a\sqcap b = \Omega \text{ otherwise} \end{cases} $$

and

$$ egin{cases} \Omega\sqcup a = a\sqcup\Omega = a \\ (\lambda x.a)\sqcup(\lambda x.b) = \lambda x.(a\sqcup b) \\ (xa_1a_2...a_n)\sqcup(xb_1b_2...b_n) = x(a_1\sqcup b_1)(a_2\sqcup b_2)...(a_n\sqcup b_n) \\ a\sqcup b \text{ is not defined otherwise} \end{cases} $$

where x is a variable and $a,b,a_i,b_i$ are expressions of N and $n \ge 0$. The set N is also complete for the $\sqcap$ operation, i.e. each subset X of N has a greatest lower bound $\sqcap X$ in N. Moreover, the order < is well-founded in N and we have no infinite strictly decreasing chains in N.

To any expression M, Wadsworth [13] associates a set of approximations A(M), which is the set of direct approximations of all expressions reducible from M :

$$ A(M) = \{\phi(N) \mid M \stackrel{*}{\to} N \} $$

We briefly review some descriptive properties.

**Proposition 4** : The set A(M) of approximations of any λ-expansion M is a sublattice of N ( with the same meet and join operations than in N )

**Proof** : We only need to show that $\sqcap$ and $\sqcup$ are closed in A(M). Suppose a,b are in A(M).

(*) If $(D,<)$ is a partial order structure, a directed subset X of D is such that for any a,b in X, there is c in X such that $a<c$, $b<c$. ( Notion similar to ascending chains if D is denumerable ). See Scott [10 ].
1) $a \sqsubseteq b$ is in $A(M)$ by induction on the size $||a\sqsubseteq b||$ of $a\sqsubseteq b$. There are three cases:

1.1. If $a\sqsubseteq b = \Omega$, then $a\not\sqsubseteq \Omega$ and $b\not\sqsubseteq \Omega$ is impossible, because of propositions 1 and 2. Therefore, $a=\Omega$ or $b=\Omega$ which implies $\phi(M)=\Omega$, and then $a\sqsubseteq b$ is in $A(M)$.

1.2. If $a\sqsubseteq b = \lambda x.c_1$, then $a = \lambda x.a_1$ and $b = \lambda x.b_1$. Hence, M has an abstraction form and, by proposition 1, a minimal one $\lambda x.M_0$. As $a_1$ and $b_1$ are in $A(M_0)$, we know by induction that $a_1\sqsubseteq b_1$ is in $A(M_0)$. Thus, $\lambda x.c_1 = \lambda x.(a_1\sqsubseteq b_1)$ is in $A(\lambda x.M_0)$, and $a\sqsubseteq b$ is in $A(M)$.

1.3. If $a\sqsubseteq b = xc_1c_2...c_n$, we have the same proof and we use proposition 2.

2) The Church-Rosser theorem shows the existence of $c$ such that $a<c$ and $b<c$. Hence, $a\sqsubseteq b$ is defined and a similar proof, based on an induction on the size $||a\sqsubseteq b||$, shows that $a\sqsubseteq b$ is in $A(M)$. $\square$

**Proposition 5** : For any $a$ in $A(M)$, there is a minimal $\lambda$-expression $N_a$ such that :

$$i) M \stackrel{*}{\to} N_a$$

$$ii) \phi(N_a) = a$$

$$iii) \text{ for any } N \text{ such that } M \stackrel{*}{\to} N \text{ and } a<\phi(N), \text{ then } N_a \stackrel{*}{\to} N$$

**Proof** : by induction on the size of a

$$1) a = \Omega. \text{ Then } \phi(M) = \Omega = a \text{ and } N_a = M$$

2) $a = \lambda x.a_1$. Then if $M \stackrel{*}{\to} N$ and $a<\phi(N)$, we have $N = \lambda x.N_1$, $\phi(N) = \lambda x.\phi(N_1)$ and $a_1<\phi(N_1)$. By proposition 1, there is a minimum abstraction form $\lambda x.M_0$ of M. Hence $M_0 \stackrel{*}{\to} N_1$ and by induction there is $N_{a_1}$ minimum for $a_1$ and reducible from $M_0$. Hence, if $N_a = \lambda x.N_{a_1}$, we have :

$$M \stackrel{*}{\to} \lambda x.M_0 \stackrel{*}{\to} N_a = \lambda x.N_{a_1} \stackrel{*}{\to} \lambda x.N_1 = N.$$

$$\text{and } \phi(N_a) = \lambda x.\phi(N_{a_1}) = \lambda x.a_1 = a.$$

3) $a = x_{a_1}a_2...a_n$. Same proof but we need now proposition 2. $\square$

Hence, generalizing propositions 1 and 2, we have a minimal expression $N_a$ for any approximation $a$. We reach it by head reductions ( leftmost outermost reductions ) until a head normal form ( if necessary ) and repeating this process on arguments of the head normal form ( when necessary ). We notice also that if $a,b$ are in some $A(M)$, then $a<b$ iff for any $N'$, such that $M \stackrel{*}{\to} N'$ and
$\phi(N') = b$, there is $N$ such that $M \stackrel{*}{\to} N$ and $\phi(N) = a$ and $N \stackrel{*}{\to} N'$.

**The interpretation domain** : In the set $\Lambda$, some $\lambda$-expressions have a finite set of approximations ; we call them expressions of finite information. The other expressions have an infinite information and, in order to be able to speak of their value, we will complete the set $N$ of $\omega\to\beta$ normal forms, by adding infinite points.
Let $\bar{N}$ be the set of all directed subsets of $N$:

$$ \bar{N} = \{ S \mid S \text{ directed, } S \subseteq N \} $$

We can extend the relation $\subset$ to $\bar{N}$ by defining for $S$ and $S'$ in $\bar{N}$ :

$$ S \subseteq S' \quad \text{iff} \quad \forall a \in S. \exists b \in S'. \ a < b $$

In order to keep an ordering, we define a quotient set :

$$ \hat{N} = \bar{N} / \equiv $$

where :

$$ S \equiv S' \quad \text{iff} \quad S \subseteq S' \subseteq S $$

Hence, if we note by $[S]$ the equivalence class of $S$ in $\hat{N}$, we have in $\hat{N}$ :

$$ [S] \subseteq [S'] \quad \text{iff} \quad S \subseteq S' $$

**Proposition 6** : The set $\hat{N}$ is a semi-lattice where every directed subset is a lattice. More precisely :

1) $\hat{N}$ has a minimal element $[\{\Omega\}]$

2) any pair of elements $[S],[S']$ in $\hat{N}$ has a greatest lower bound $[S] \sqcap [S']$

3) any pair of elements $[S],[S']$ in $\hat{N}$, which is dominated by a common upper bound, has a least upper bound $[S] \sqcap [S']$.

The proof is obvious and the definitions of $\sqcap$ and $\sqcup$ in $\hat{N}$ are

given by :

$$ [S] \sqcap [S'] = [\{ a \sqcap b \mid a \in S, b \in S' \}] $$

$$ [S] \sqcup [S'] = [\{ a \sqcup b \mid a \in S, b \in S' \}] $$

But $\hat{N}$ has a richer structure. Using Scott's terminology ( see for instance [10] ), we have :

**Proposition 7** : The domain $\hat{N}$ is :

1) complete for directed subsets of $\hat{N}$,

2) continuous,

3) algebraic since $\hat{N}$ admits a denumerable basis of isolated elements $[\{a\}]$ where $a \in N$.
This means that every directed subset $X$ of $\hat{N}$ has a least upper bound $\sqcup X$ and that each element of $\hat{N}$ is the least upper bound of the finite information points $[{a}]$ ( where $a \in N$ ) which are below it. The proof follows from the construction of $\hat{N}$ and we skip it. The method we use for the completion of $\hat{N}$ is equivalent to the one of Vuillemin [12].

**Interpretation of $\lambda$-expressions** : We associate to any expression $M$ an element in $\hat{N}$ by the following equation :

$$J(M) = [A(M)]$$

and we can thus induce a partial preorder on $\Lambda$ defined by : $M \subseteq M'$ iff $J(M) \subseteq J(M')$. By the definition of $\hat{N}$, we have :

$$M \subseteq M' \text{ iff } \forall N \text{ s.t. } M \xrightarrow{*} N \text{ } \exists N' \text{ s.t. } M' \xrightarrow{*} N' \text{ and } \phi(N) < \phi(N')$$

We write $M \equiv M'$ for $M \subseteq M' \subseteq M$ and we expect the usual properties for our interpretation $J$. Moreover, if $X$ is a directed subset of $\lambda$-expressions, $\sqcup X$ means $\sqcup J(X)$.

**Theorem 1** : The $\beta$-rule of conversion is valid in $J$, i.e. if $M \xrightarrow{*} M'$ then $M \equiv M'$.

**Proof** : Since $M \xrightarrow{*} M'$, we have $A(M') \subseteq A(M)$ and then $M' \subseteq M$. Now, suppose $M \xrightarrow{*} N$ ; then as $M \xrightarrow{*} M'$, we know, by the Church-Rosser theorem, the existence of an $N'$ such that $M \xrightarrow{*} N'$ and $M' \to N'$, and hence $\phi(N) < \phi(N')$. So we have $M \subseteq M'$. $\square$

Let the set $\Lambda$ be now extended by allowing the constant $\Omega$ whenever a free variable is possible. So $\Lambda$ is now the set of $\lambda$-$\Omega$ expressions and we consider not only $\beta$-reductions but also an $\omega$-rule of conversion defined by replacing any subexpression of the form $\Omega M$ by $\Omega$. We note this kind of reduction $N \xrightarrow{\omega} N'$. Let $C[\quad]$ denote any context ( see [8] ), i.e a $\lambda$-$\Omega$ expression with one subexpression missing, and $C[M]$ be the corresponding expression where $M$ stands at the place of the previously missing subexpression.

**Proposition 8** : $C[\Omega] \subseteq C[M]$ for any context $M$ and any expression $M$.

**Proof** : The set of expressions reducible from $C[\Omega]$ is isomorphic to a subset of the one reducible from $C[M]$. Moreover, $\phi(N[x\wedge\Omega]) < \phi(N[x\wedge M])$ for any $\lambda$-$\Omega$ expressions $M,N$. Hence, $C[\Omega] \subseteq C[M]$ by definition of $\subseteq$. $\square$

**Theorem 2** : The $\omega$-rule of conversion is valid in $J$, i.e. if $M \xrightarrow{\omega} M'$ then $M \equiv M'$.
**Proof**: By the above proposition, we already know that $M' \subseteq M$. Now, suppose $M \stackrel{*}{\to} N$, we can show easily ( by an induction on the pair $\langle \ell, \ell' \rangle$ if $\ell$ and $\ell'$ are the length of the reductions $M \stackrel{*}{\to} N$ and $M \stackrel{*}{\to} M'$ ) the existence of $N'$ such that $N \stackrel{*}{\to} N'$ and $M' \stackrel{*}{\to} N'$. Hence $\phi(N) = \phi(N')$ and then $M \subseteq M'$. $\square$

We turn now to the main point of this paper, i.e. we show that, for any context $C[ ]$, we have $C[M] \subseteq C[M']$ if $M \subseteq M'$. So, using the definition of $\subseteq$, we need to show that if $C[M] \stackrel{*}{\to} N$, then there is an $N'$ such that $C[M'] \stackrel{*}{\to} N'$ and $\phi(N) < \phi(N')$. But all we know is that, for any approximation of $M$, we can have a better one for $M'$. Therefore, in order to compare $C[M]$ and $C[M']$, we try to point out the approximation of $M$ needed by any reduction from $C[M]$ to some $N$. That is the Welch' conjecture about inside-out reductions ([14]), which we prove later. Using the Welch's notations, let $C[M] \stackrel{\#}{\supseteq} N$ designate any reduction :

$$C[M] = M_0 \underset{\sim}{\overset{R_1}{\to}} M_1 \underset{\sim}{\overset{R_2}{\to}} M_2 \underset{\sim}{\overset{R_3}{\to}} \dots \underset{\sim}{\overset{R_n}{\to}} M_n = N$$

where, for all $i$ ($1 \le i \le n$), the redex $R_i$ contracted between $M_{i-1}$ and $M_i$ is not a residual of a redex internal to the subexpression $M$ in $M_0$. Similarly, if $F$ is a set of redexes of $M_0$, we write $M_0 \stackrel{\#}{\supseteq} F M_n$ if none of the $R_i$ is a residual of a redex of $F$. Hence, if $F$ is the set of all redexes of $M$, we have $C[M] \stackrel{\#}{\supseteq} N$ iff $C[M] \stackrel{\#}{\supseteq} N$. Moreover, let $M[F\setminus\Omega]$ denote the substitution in $M$ of all redexes of $F$ by the constant $\Omega$. Now, we can state what we want. ( The proof is postponed until the next section.)

**Proposition 9**: For any context $C[ ]$ and any expression $M$, if $C[M] \stackrel{*}{\to} N$, then there are expressions $M'$ and $N'$, such that $M \stackrel{*}{\to} M'$, $N \stackrel{*}{\to} N'$ and $C[M'] \stackrel{\#}{\supseteq} N'$.

**Lemma 1**: Given a set of redexes $F$ in an expression $M$, if $M \stackrel{*}{\to} M'$ and iff $F'$ is the set of the residuals of the redexes of $F$ in $M'$, then $M[F\setminus\Omega] \stackrel{*}{\to} M'[F'\setminus\Omega]$.

**Proof**: by induction on the length of the reduction from $M$ to $M'$, which is of the form $M \stackrel{R}{\to} M_1 \underset{F_1}{\stackrel{*}{\to}} M'$, where the redex $R$, first contracted, is not one of the redexes of $F$ and $F_1$ is the set of residuals of the redexes of $F$ in $M_1$. Then, depending on the relative position of $R$ and $F$, we obviously have $M[F\setminus\Omega] \stackrel{*}{\to} M_1[F_1\setminus\Omega]$. $\square$
**Lemma 2** : If a,b are in the set N of ω-β normal forms and such that a<b, then C[a] ⊆ C[b] for any context C[ ].

**Proof** : Corollary of proposition 8, since, if a<b, then a matches b except for some Ω's. □

**Lemma 3** : For any context C[ ] and expression M :

$$C[M] \equiv \sqcup \{ C[a] \mid a \in A(M) \}$$

**Proof** : Let X = {C[a] | a ∈ A(M)}. By-lemma 2, as A(M) is a directed set, X also is directed and ⋀X exists, since N is complete for directed subsets.

First, if a is in A(M), there is an expression N such that M$^{*}$$\to$ N and a = $\phi(N)$. So, we have, by proposition 8, C[a] ⊆ C[N] since a matches N except in some Ω's. But, as M$^{*}$$\to$ N, we have too C[M] $\stackrel{*}{\to}$ C[N] and C[M] ≡ C[N] by theorem 1. Hence, we get C[a] ⊆ C[M] for any a in A(M). Therefore C[M] is an upper bound of X and ⋀X ⊆ C[M]

Conversely, if C[M] $\stackrel{*}{\to}$ N, there are M' and N' such that M$^{*}$$\to$ M', N $\stackrel{*}{\to}$ N' and C[M'] $\stackrel{\star}{\to}$ N' (by proposition 9). Let F be the set of all redexes of M'; we have C[M'] $\stackrel{\star}{\to}$ N'. By lemma 1, if F' is the set of the residuals of the redexes of F in N', we have C[M'] [F$\setminus$Ω] $\stackrel{\star}{\to}$ N' [F'$\setminus$Ω]. Moreover, C[M'] [F$\setminus$Ω] $\stackrel{\star}{\to}$ C[$\phi(M')$] and since ω and β-conversions are valid, we get :

$$\phi(N) < \phi(N') = \phi(N' [F' \setminus \Omega]) \subseteq N' [F' \setminus \Omega] \equiv C[M'] [F' \setminus \Omega] \equiv C[\phi(M')]$$

And then, for any N such that C[M] $\stackrel{*}{\to}$ N, there is an M' such that M$^{*}$$\to$ M' and $\phi(N) \subseteq C[\phi(M')]$. Since C[M] ≡ ⋀ { a | a ∈ A(C[M]) }, we have C[M] ⊆ ⋀X. □

**Theorem 3** : If M ⊆ M', then C[M] ⊆ C[M'] for any context C[ ].

**Proof** : Since M ⊆ M', for any a in A(M), there is a b in A(M') such that a<b. Hence, by lemma 2, C[a] ⊆ C[b]. Since N is complete, we get :

$$\sqcup \{ C[a] \mid a \in A(M) \} \subseteq \sqcup \{ C[b] \mid b \in A(M') \} \\ \text{and, by lemma 3, } C[M] \subseteq C[M'] . \quad \square$$
**Inside-out reductions** : In order to show proposition 9, we follow Welch [14] and define an inside-out reduction as any reduction :

$$M = M_0 \underset{M_1}{\overset{R_1}{\rightleftharpoons}} M_1 \underset{M_2}{\overset{R_2}{\rightleftharpoons}} M_2 \underset{M_3}{\overset{R_3}{\rightleftharpoons}} \dots \underset{M_n}{\overset{R}{\rightleftharpoons}} M_n = M'$$

where, for all $i,j$ such that $i<j$ and $1 \le i \le n-1$, $2 \le j \le n$, the redex $R_j$ (contracted between $M_{j-1}$ and $M_j$) is not a residual of a redex internal to $R_i$ in $M_{i-1}$. Let $M \xrightarrow{i.o.} M'$ be a notation for any such inside-out reduction from $M$ to $M'$. Welch conjectured the completeness of inside-out reductions, i.e. if $M \stackrel{*}{\to} N$, then there exists $N'$ such that $N \stackrel{*}{\to} N'$ and $M \xrightarrow{i.o.} M'$. So, as pointed out by Welch :

**Proposition 10** : If inside-out reductions are complete, then proposition 9 is true.

**Proof** : Let $C[M] \stackrel{*}{\to} N_1$, there is $N$ such that $N_1 \stackrel{*}{\to} N$ and $C[M] \xrightarrow{i.o.} N$, as inside-out reductions are complete. Let us prove, by induction on the size of the context $C[ ]$, that if $C[M] \xrightarrow{i.o.} N$, there is an $M'$ such that $M \to M'$ and $C[M'] \xrightarrow[M]{*} N$.

1) If $C[ ] = [ ]$, then $C[M] = M$ and $M' = C[M'] = N$.

2) If $C[ ] = \lambda x.C_1[ ]$, the induction works easily.

3) If $C[ ] = M_1C_1[ ]$, as the reduction $C[M] \xrightarrow{i.o.} N$ is inside-out, we have $M_1 \xrightarrow{i.o.} M'_1$, $C_1[M] \xrightarrow{i.o.} N'$ and $M'_1N' \xrightarrow[N]{*} N$. Hence, by induction there is $M'$ such that $M \stackrel{*}{\to} M'$ and $C_1[M'] \xrightarrow[M]{*} N'$. Thus $M \stackrel{*}{\to} M'$ and $C[M'] = M_1C_1[M'] \xrightarrow[M]{*} N$.

4) If $C[ ] = C_1[ ] M_1$, we have the same proof. $\square$

**A labelled $\lambda$-calculus** : The problem is now to keep track of the redexes contracted in some reduction $M \stackrel{*}{\to} N$ in order to be able to reorder them in an inside-out way, and to show the inside-out completeness. We do this by introducing a new set of $\lambda$-expressions ($\Lambda'$) defined on a set of labels $L$ as follows. Let $L_0 = \{a,b,c \dots \}$ be an infinite set of letters. We consider the set $L$ of all strings of characters formed on $L_0$, with any level of overlining and underlining. So expressions of $L$ are :

$$ \left\{ \begin{array}{ll} a & \text{if } a \in L_0 \\ \alpha\beta & \text{if } \alpha,\beta \in L \\ \bar{\alpha} & \text{" "} \\ \alpha & \text{" "} \end{array} \right. $$
and expressions of $\Lambda'$ are :

$$ \left\{ \begin{array}{llll} x^{\alpha} & \text{if} & \alpha \in L & \text{and } x \in V \\ (\lambda x.M)^{\alpha} & \text{if} & \text{"} & \text{and } M,N \in \Lambda' \\ (MN)^{\alpha} & \text{if} & \text{"} & \text{"} \end{array} \right. $$

Thus, the labelled $\lambda$-expressions are like usual $\lambda$-expressions except that every subexpression has an arbitrary label. This $\lambda$-calculus is a generalization of the one of Wadsworth [13] since, instead of considering integers as exponents, we have strings of characters. For any label $\alpha$ and expression $M$ of $\Lambda'$, we define $\alpha.M$ as :

$$ \left\{ \begin{array}{l} \alpha.x^{\beta} = x^{\alpha\beta} \\ \alpha.(\lambda x.M)^{\beta} = (\lambda x.M)^{\alpha\beta} \\ \alpha.(MN)^{\beta} = (MN)^{\alpha\beta} \end{array} \right. $$

and the substitution operation is defined by :

$$ \left\{ \begin{array}{lcl} x^{\alpha}[x\backslash N] & = & \alpha \circ N \\ y^{\alpha}[x\backslash N] & = & y^{\alpha} \\ (\lambda y.M)^{\alpha}[x\backslash N] & = & (\lambda y.M[x\backslash N])^{\alpha} \\ (MM')^{\alpha}[x\backslash N] & = & (M[x\backslash N] M'[x\backslash N])^{\alpha} \end{array} \right. $$

where we forget the difficulties due to $\alpha$-conversion. Then the $\beta$-rule is defined ( by monotony ) from :

$$ (( \lambda x.M )^{\alpha} N )^{\beta} \rightarrow \beta \bar{\alpha}.M[x\backslash \alpha.N] $$

( We do not care for the precedences between the $\circ$ and substitution operators because they commute ). Furthermore we will allow this reduction iff some predicate $P(\alpha,\beta)$ is verified. So, for instance, using a graph notation for $\lambda$-expressions ( see Morris [8] where nodes $\lambda$ and $\gamma$ corresponds to abstraction and application ), we have figure 1 if we suppose $P(\alpha,\beta)$ always true. In fact, we can restrict our attention to $\lambda$-expressions labelled by a set $L'$ of labels defined as containing :

$$ \left\{ \begin{array}{llll} a & \text{if} & a \in L_0 \\ \bar{\alpha\beta\gamma} & \text{if} & \alpha, \beta, \gamma \in L' \\ \alpha\underline{\beta\gamma} & \text{if} & \text{"} & \text{"} \end{array} \right. $$
<figure><img src="image_4.png" /><figcaption>Figure 1: Reductions from $((\lambda x.(\lambda y.(y^f_zg)^e)d_x^h)^c)^b(\lambda u.(u^k_u e)^j)^i a$</figcaption></figure>

and it is clear that expressions labelled by $L'$ keep their labels in $L'$ after some $\beta$-reductions. We remark too that other $\lambda$-calculus languages are obtainable from this one by some homomorphism : for instance Wadsworth's typed $\lambda$-calculus and Morris' definition of descendants. Let the height $h(\alpha)$ of a label $\alpha$ of $L$ be defined by :

$$ egin{cases} h(\alpha) = 0 & \text{if } \alpha \in L_0 \\ h(\alpha\beta) = \left[ h(\alpha), h(\beta) \right] & \text{if } \alpha, \beta \in L \\ h(\bar{\alpha}) = h(\bar{\alpha}) = 1 + h(\alpha) & \text{if } \alpha \in L. \end{cases} $$

and let the degree of a redex be the label of its abstraction part. Hence, $\text{degree}((\lambda x.M)^{\alpha_N})^{\beta}) = \alpha$.

**Proposition 1'** : The residuals of a redex $R$ have the same degree as $R$.

**Proof** : Suppose $M \xrightarrow{R} N$ and $R$ is a redex, in $M$, of the form $R = ((\lambda x.P)^{\alpha} Q)^{\beta}$. If $S = ((\lambda y.T)^{\gamma} U)^{\delta}$ is another redex of $M$, we show by cases that residual(s) of $S$ in $N$ have the same degree $\gamma$ than $S$ in $M$.
1) If R and S are 2 disjoint expressions, it is obvious.

2) If S is in R, then S is in P or Q and the contraction of R may have only an effect on the external label δ of S.

3) If R is in S, then R is in T or U and the contraction of R has no effect on the degree α of S. □

**Proposition 2'** : If $P(\alpha,\beta)$ implies $P(\alpha,\gamma\beta)$ for any labels $\alpha,\beta,\gamma$ of $L$, then the $\beta$-rule of the labelled calculus is Church-Rosser.

**Proposition 3'** : If

1) $P(\alpha,\beta)$ implies $P(\alpha,\gamma\beta)$ for any labels $\alpha,\beta,\gamma$ of $L$

2) the set $\{ h(\alpha) \mid P(\alpha,\beta) \text{ is true} \}$ is bounded
then any labelled $\lambda$-expression strongly normalizes ( i.e. any reduction in
this labelled calculus has a finite length ).

The proofs of these propositions are given in the appendix,
by the usual techniques. We go back to the inside-out completeness and we
will use letters as M,N to designate expressions of Λ and U,V for labelled
λ-expressions of Λ'.

**Theorem 4** : If $M \xrightarrow{\star} N$, then there is an expression N' such that $M \xrightarrow[i.o.]{} N'$ and $N \xrightarrow{\star} N'$.

**Proof** : Let U be the labelled λ-expression obtained from M by labelling all the subexpressions of M with a different letter of $L_0$. We can associate to the reduction $M \xrightarrow{\star} N$, an isomorphic labelled reduction $U \xrightarrow{\star} V$. More precisely, this reduction can be written :

$$U = U_0 \xrightarrow{R_1} U_1 \xrightarrow{R_2} U_2 \xrightarrow{R_3} \dots \xrightarrow{R_n} U_n = V$$

Let us now consider the predicate $P(\alpha,\beta)$ defined on labels
by :

$P(\alpha,\beta)$ is true iff $\alpha$ = degree $(R_i)$ for some $i$ ($1 \le i \le n$)

The two assumptions of proposition 3' are verified and, hence, U strongly normalizes. Let V' be the normal form of V, then $V \xrightarrow{\star} V'$, because the Church-Rosser assumption is true and for instance, any innermost reduction reaches the normal form V'. Let

$$U = V_0 \xrightarrow{S_1} V_1 \xrightarrow{S_2} V_2 \xrightarrow{S_3} \dots \xrightarrow{S_m} V_m = V'$$
be such an innermost reduction. ( We then have, for all i, degree ($S_i$) = degree ($R_j$) for some j between 1 and n ). We claim that this reduction is inside-out. Suppose $i<j$ for some i,j between 1 and m and suppose $S_j$ is a residual of a redex $S_j'$ internal to $S_i$ in $V_{i-1}$. By proposition 1', we have degree ($S_j'$) = degree ($S_j$) and then, as the predicate P is true for $S_j$, P is also true for $S_j'$. The reduction from U to V' is thus not an innermost reduction and we have a contradiction. Let $N'$ be the $\lambda$-expression obtained by erasing the labels of V'. As an isomorphic reduction of $\Lambda$ corresponds to any labelled reduction, we have $N \stackrel{*}{\to} N'$ and $M \xrightarrow[i.o.]{*} N'$. $\square$

In fact, with the same method, we have, if $M \stackrel{*}{\to} M'$ and $M \stackrel{*}{\to} M'',$ the existence of an $N$ such that $M' \xrightarrow[i.o.]{*} N$ and $M'' \xrightarrow[i.o.]{*} N$.

**Conclusion:** The interpretation $<I, \hat{N}>$, although strongly inspired by Scott's theory of computation, is purely algebraic. Here, we do not have a definition of application as in Scott [10, 11] or Welch [15]. But with the help of the labelled calculus, any expression can be considered as the limit of expressions having a normal form. If we think of $\lambda$-expressions as programs, the interpretation $<I, \hat{N}>$ seems to be the minimal one to consider. Thus we expect that $<I, \hat{N}>$ is some kind of free interpretation. This is proved by Welch for "continuous semantics", i.e. roughly speaking for interpretations where the Wadsworth theorem is true. Welch did it for his model but his interpretation seems to be equivalent to the one we used here. Hyland [4], who independently considered also the same interpretation, proved that there is an extensional equivalence relation corresponding to equality in I. Furthermore, he showed for any $\lambda$-expressions $M, M'$ that $M \subseteqq \bar{M}'$ iff $M \subseteqq \bar{M}'$ where $\bar{M}'$ is Scott's model [11]. Another question is to take into account extensionality and build an algebraic interpretation where the $\eta$-rule is valid. This is done by Hyland [4]. Finally, the labelled $\lambda$-calculus seems interesting in itself [6], since we can capture the history of any reduction in the labels.

**Acknowledgements:** to D.Park and P.Welch without whom I would not have thought of the inside-out reductions; to G.Plotkin, D. van Daalen and R. de Vrijer without whom I could not have done the appendix; to G.Kahn and G.Huet for their constant help.
Appendix 1: The Church-Rosser property in the labelled calculus (by the Tait-Martin Löf method)

Let C(M) be defined by:

$$
\left\{
\begin{array}{l}
C(x^\alpha) = x^\alpha \\
C((\lambda x.M)^\alpha) = (\lambda x.C(M))^\alpha \\
C(((\lambda x.M)^\alpha)N)^\beta) = \bar{\beta\alpha}.C(M)[x\underline{\alpha}.C(N)] \quad \text{if } P(\alpha,\beta) \\
C((MN)^\alpha) = (C(M)C(N))^\alpha \quad \text{otherwise}
\end{array}
\right.
$$

Let $M \to M'$ denote a parallel step of reduction and be defined by the following
inference rules and axiom:

$$
\begin{array}{l @{\quad} l @{\quad} l @{\quad} c @{\quad} l}
\text{-I-} & x^{\alpha} & \rightarrow & x^{\alpha} & \\
\text{-II-} & M & \rightarrow & M' & \\
& (\lambda x.M)^{\alpha} & \rightarrow & (\lambda x.M')^{\alpha} & \\
\text{-III-} & M & \rightarrow & M', N & \rightarrow & N' & \\
& (MN)^{\alpha} & \rightarrow & (M'N')^{\alpha} & \\
\text{-IV-} & M & \rightarrow & M', N & \rightarrow & N' & \\
& ((\lambda x.M)^{\alpha}N)^{\beta} & \rightarrow & \bar{\beta\alpha}.M' & [x\underline{\alpha}.N'] & \\
\end{array}
\quad \text{if } P(\alpha,\beta)
$$

Moreover, we suppose $P(\alpha,\beta)$ implies $P(\alpha,\gamma\beta)$ for any labels $\alpha,\beta,\gamma$.

First, we notice that the associativity of concatenation implies:

$\alpha.(\beta.M) = \alpha\beta.M$

**Lemma 1:** $\alpha.(M[x\setminus N]) = (\alpha.M)[x\setminus N]$

Proof: by cases on M. The only problem is when $M = x^\beta$. Then the associativity of concatenation gives the answer. $\square$

**Lemma 2:** If $x \neq y$ and $x$ is not free in $N'$, then:

$$
M[x\setminus N][y\setminus N'] = M[y\setminus N'][x\setminus N[y\setminus N']]
$$

Proof: by induction on the size of M. The only problem is when $M = x^\alpha$. Then we apply lemma 1. $\square$

**Lemma 3:** If $M \to M'$, then $\alpha.M \to \alpha.M'$

Proof: by cases on the rule or axiom used for $M \to M'$. The only inte-
resting case is when:

$$
M = ((\lambda x.M_1)^\gamma M_2)^\beta \rightarrow M' = \beta \bar{\gamma}.M'_1[x \setminus \underline{\gamma}.M'_2]
$$

with $M_1 \to M'_1$, $M_2 \to M'_2$ and $P(\gamma, \beta)$. Then:

$$
\alpha.M = ((\lambda x.M_1)^\gamma M_2)^{\alpha\beta} \quad \text{and} \quad \alpha.M' = \alpha.(\beta\bar{\gamma}.M'_1[x\underline{\gamma}.M'_2])
$$
As $P(\gamma, \beta)$ implies $P(\gamma, \alpha\beta)$, we have by rule IV:

$$ \alpha.M = ((\lambda x.M_1)^{\gamma} M_2)^{\alpha\beta} \rightarrow \alpha\beta\overline{\gamma}.M_1'[x\underline{\gamma}.M_2'] $$

and by the associativity of concatenation $\alpha.M \rightarrow \alpha.M'$ . □

**Lemma 4:** If $M \rightarrow M'$ and $N \rightarrow N'$, then $M[x\N] \rightarrow M'[x\N']$

**Proof:** by induction on the size of M.

1) M is a variable:

a) $M = x^\alpha = M'$. Then we use lemma 3.

b) $M = y^\alpha = M'$. Then obvious by axiom I.

2) M is not a variable and we have several cases according to the rule used for $M \rightarrow M'$. The only interesting one is when:

$$ M = ((\lambda y.M_1)^{\alpha} M_2)^{\beta} \rightarrow M' = \beta\overline{\alpha}.M_1'[y\underline{\alpha}.M_2'] $$

with $M_1 \rightarrow M_1'$, $M_2 \rightarrow M_2'$ and $P(\alpha, \beta)$. Then, ignoring $\alpha$-conversions, we have:

$$ M[x\N] = ((\lambda y.M_1[x\N])^{\alpha} M_2[x\N])^{\beta} $$

$$ \begin{aligned} M'[x\N'] &= (\beta\overline{\alpha}.M_1'[y\underline{\alpha}.M_2'])[x\N'] \\ &= \beta\overline{\alpha}.(M_1'[y\underline{\alpha}.M_2'])[x\N']) \end{aligned} \quad \text{(by lemma 1)} $$

$$ = \beta\overline{\alpha}.(M_1'[x\N'])[y\underline{\alpha}.(M_2')(x\N')] \quad \text{(by lemma 2)} $$

$$ = \beta\overline{\alpha}.(M_1'[x\N'])[y\underline{\alpha}.(M_2'[x\N'])]) \quad \text{(by lemma 1)} $$

By induction, we know that $M_1[x\N] \rightarrow M_1'[x\N']$ and $M_2[x\N] \rightarrow M_2'[x\N']$, and using rule IV, we have $M[x\N] \rightarrow M'[x\N']$. □

**Lemma 5:** If $M \rightarrow M'$, then $M' \rightarrow C(M)$.

**Proof:** by induction on the size of M. There are two interesting cases:

1) When:

$$ M = ((\lambda x.M_1)^{\alpha} M_2)^{\beta} \rightarrow M' = (M_3'M_2')^{\beta} $$

with $(\lambda x.M_1)^\alpha \rightarrow M_3'$, $M_2 \rightarrow M_2'$ and $P(\alpha, \beta)$. Then it is clear that $M_3' = (\lambda x.M_1')^\alpha$ and $M_1 \rightarrow M_1'$. Hence we have by induction $M_1' \rightarrow C(M_1)$ and $M_2' \rightarrow C(M_2)$. Then, using rule IV:

$$ M' = ((\lambda x.M_1')^{\alpha} M_2')^{\beta} \rightarrow \beta\overline{\alpha}.C(M_1)[x\underline{\alpha}.C(M_2)] = C(M) $$

2) When:

$$ M = ((\lambda x.M_1)^{\alpha} M_2)^{\beta} \rightarrow M' = \beta\overline{\alpha}.M_1'[x\underline{\alpha}.M_2'] $$

with $M_1 \rightarrow M_1'$, $M_2 \rightarrow M_2'$ and $P(\alpha, \beta)$. Then we have by induction $M_1' \rightarrow C(M_1)$ and $M_2' \rightarrow C(M_2)$. Hence, by lemma 3: $\underline{\alpha}.M_2' \rightarrow \underline{\alpha}.C(M_2)$, and by lemma 4 and 3:

$$ M' \rightarrow \beta\overline{\alpha}.C(M_1)[x\underline{\alpha}.C(M_2)] = C(M) \quad \square $$

**Lemma 6:** If $M \rightarrow M'$ and $M \rightarrow M''$, then there is an $N$ such that $M' \rightarrow N$ and $M'' \rightarrow N$. □
**Proof:** We take $N = C(M)$ and use lemma 5. □

**Proposition:** If $M \to M'$ and $M \to M'',$ then there is an $N$ such that $M' \to N$ and $M'' \to N$. □

**Proof:** by induction on the sum of length of the reductions $M \to M'$ and $M \to M''$. □

**Appendix 2:** Strong normalization in the labelled λ-calculus by a method due to D. van Daalen. We suppose:

(1) $P(\alpha, \beta)$ implies $P(\alpha, \gamma\beta)$

(2) $\{h(\alpha) | P(\alpha, \beta) \text{ is true}\}$ is bounded

Hence, we have the Church-Rosser property. Let write $\tau(N)$ for the external label of $N$. So $\tau(x^\alpha) = \tau((\lambda x.M)^\alpha) = \tau((MN)^\alpha) = \alpha$ and we call $SN$ the set of strongly normalizable labelled λ-expressions.

**Lemma 1:** If $(...((MN_1)^{\beta_1} N_2)^{\beta_2} ... N_n)^{\beta_n} \stackrel{*}{\to} (\lambda x.N)^\alpha$, then we have $h(\tau(M)) \le h(\alpha)$.

**Proof:** by induction on $n$. If $n=0$, this is clearly true. Otherwise, we must have:

$$(...((MN_1)^{\beta_1} N_2)^{\beta_2} ... N_{n-1})^{\beta_{n-1}} \stackrel{*}{\to} (\lambda y.P)^{\gamma}$$

and:

$$((\lambda y.P)^{\gamma} N_n)^{\beta_n} \to \beta_n \bar{\gamma} . P[y \setminus \underline{\gamma} . N_n] \stackrel{*}{\to} (\lambda x.N)^{\alpha}$$

Hence, we get $h(\tau(M)) \le h(\gamma)$ by induction. We also have:

$$h(\gamma) < h(\bar{\gamma}) \le h(\tau(\beta_n \bar{\gamma} . P[y \setminus \underline{\gamma} . N_n])) \le h(\alpha) \quad . \square$$

**Lemma 2:** If $M[x\N] \stackrel{*}{\to} (\lambda y.P)^\alpha$, we only have two cases:

1) $M \stackrel{*}{\to} (\lambda y.M')^\alpha$ and $M'[x\N] \stackrel{*}{\to} P$

or

2) $M \stackrel{*}{\to} M' = (...((x^{\beta_1} M_1)^{\beta_2} M_2)^{\beta_3} ... M_n)^{\beta_n}$ and $M'[x\N] \stackrel{*}{\to} (\lambda y.P)^\alpha$

**Proof:** application of propositions 1 and 2. □

**Lemma 3:** If $M, N$ are in $SN$, then $M[x\N]$ is in $SN$.

**Proof:** Let $m$ be the upper bound of the set $\{h(\alpha) | P(\alpha, \beta) \text{ is true}\}$, which exists by assumption (2), and $\text{prof}(M)$ be the maximal length of reductions starting from $M$ in $SN$. We do an induction on the triple:

$$<h(\tau(N)) - m, \text{prof}(M), ||M||>$$
where $||M||$ is the size of $M$.
The only interesting case is when:

$$M = (M_1 M_2)^\alpha \quad \text{and} \quad M_1[x\N] \stackrel{*}{\to} (\lambda y.P_1)^{\alpha_1}$$

We know by induction that $M_1[x\N]$ and $M_2[x\N]$ are in $SN$, but we wonder if $((\lambda y.P_1)^{\alpha_1} M_2[x\N])^\alpha$ is in $SN$, i.e. if $M' = \overline{\alpha \alpha_1} \cdot P_1[y\overline{\alpha_1} \cdot M_2[x\N]]$ is in $SN$. Then lemma 2 tells us there are two subcases:

1) $M_1 \stackrel{*}{\to} (\lambda y.M_1')^{\alpha_1}$ and $M_1'[x\N] \stackrel{*}{\to} P_1$. Then by lemmas 2,3,4 of the Church-Rosser proof, we get:

$$\begin{align*}
\overline{\alpha \alpha_1} \cdot M_1'[y\overline{\alpha_1} \cdot M_2][x\N] &= \overline{\alpha \alpha_1} \cdot M_1'[x\N][y\overline{\alpha_1} \cdot M_2[x\N]] \\
&\stackrel{*}{\to} \overline{\alpha \alpha_1} \cdot P_1[y\overline{\alpha_1} \cdot M_2[x\N]] = M'
\end{align*}$$

But $M = (M_1 M_2)^\alpha \stackrel{*}{\to} ((\lambda y.M_1')^{\alpha_1} M_2)^\alpha \to \overline{\alpha \alpha_1} \cdot M_1'[x\overline{\alpha_1} \cdot M_2]$. Hence:

$$\text{prof}(\overline{\alpha \alpha_1} \cdot M_1'[x\overline{\alpha_1} \cdot M_2]) < \text{prof}(M)$$

and by induction $M'$ is in $SN$.

2) $M_1 \stackrel{*}{\to} Q_1 = (\dots ((x^{\beta_1} N_1)^{\beta_1} N_2)^{\beta_2} \dots N_n)^{\beta_n}$ and $Q_1[x\N] \stackrel{*}{\to} (\lambda y.P_1)^{\alpha_1}$. As $M_1[x\N]$ is in $SN$ and $M_1[x\N] \stackrel{*}{\to} Q_1[x\N]$, we have $P_1$ in $SN$. Moreover:

$$Q_1[x\N] = (\dots (((\beta.N)N_1')^{\beta_1} N_2')^{\beta_2} \dots N_n')^{\beta_n}$$

where $N_i' = N_i[x\N]$ for all $i$. Hence, using lemma 1:

$$h(\tau(N)) \le h(\tau(\beta.N)) \le h(\alpha_1) < h(\overline{\alpha_1}) \le h(\overline{\alpha_1} \cdot M_2[x\N])$$

and by induction $M'$ is in $SN$.

**Proposition:** If $P$ verifies assumptions (1) and (2), every expression $M$ strongly normalizes.

**Proof:** by induction on the size of $M$ and application of lemma 3.

## References:

[1] Barendregt H.P., "Some extensional term models for combinatory logics and lambda-calculi", PhD thesis, Utrecht (1971)

[2] Church A., "The calculi of lambda conversion", Annals of Math. Studies, n°6, Princeton (1941)

[3] Curry H.B., Feys R., "Combinatory logic", Vol 1, North Holland (1958)

[4] Hyland M., to appear in the Rome conference (1975)

[5] Lévy J-J., "Réductions sures dans le lambda calcul", 3° cycle, Univ of Paris 7, (1974)

[6] Lévy J-J., "Réductions sures et optimales dans le lambda calcul", to appear
[7] Milner R., "Processes; A model of computing agents", Univ. of Edinburgh, Internal report (1973)

[8] Morris J.H., "Lambda calculus models of programming languages", PhD thesis, MIT, Cambridge (1968)

[9] Nivat M., "Sur l'interprétation des shémas de programmes monadiques", Rapport IRIA-LABORIA (1972)

[10] Scott D., "Continuous lattices", Technical monograph, PRG-7, Oxford (1971)

[11] Scott D., "Data types as lattices", to appear in Springer Lectures Notes

[12] Vuillemin J., "Syntaxe, sémantique et axiomatique d'un langage de programmation simple", Thèse d'état, Univ. Paris 7 (1974)

[13] Wadsworth C.P., "Semantics and pragmatics of the lambda calculus", PhD thesis, Oxford (1971)

[14] Welch P., "Another problem of lambda calculus", Univ. of Kent, Private communication (1973)

[15] Welch P., to appear in the Rome conference (1975)
## Appendice 3 :

Nous allons faire un rappel, aussi bref que possible, des notions élémentaires du λ-calcul que nous utilisons.

### Définition des λ-expressions :

Soit un alphabet $V = \{ x, y, z \}$, contenant un nombre dénombrable de lettres notées encore $v_1, v_2, v_3, \dots$ et un ensemble $S = \{ ( , ) , \lambda \}$ de symboles particuliers. Le langage $\Lambda$ des λ-expressions est le sous-ensemble minimal de $(S+V)^*$, contenant :

$$ (1) \quad x \qquad \text{si} \qquad x \in V $$

$$ (2) \quad ( \varepsilon \varepsilon' ) \qquad \text{si} \qquad \varepsilon, \varepsilon' \in V $$

$$ (3) \quad ( \lambda x \varepsilon ) \qquad \text{si} \qquad \varepsilon \in \Lambda $$

Une expression de la forme (1) est dite être une *variable*, une de la forme (2) une *application* et une de la forme (3) une *abstraction*.

### Abréviations :

Nous utiliserons couramment un certain nombre d'abréviations (voir Church [2]) destinées à restreindre l'utilisation abusive des parenthèses.

**Règle 1 :** L'omission des parenthèses () dans $(\varepsilon\varepsilon')$ est autorisée, quand on peut le faire sans ambiguïté, $(\varepsilon\varepsilon')$ pouvant être l'expression complète considérée ou simplement une sous-expression. Pour restaurer de telles parenthèses omises, la règle à suivre est l'association vers la gauche, par exemple :

$f \times y$ est une abréviation de $((fx) \ y)$

$f(\times y)$

$f \times y \times z$

$f(\times y) \ z$

$f(\lambda x \times y)$
**Règle 2** : Nous ajoutons à S un nouveau symbole "." et toute sous-formule de la forme :

λx ( εε' ) pourra être notée λx.εε'
λx ( λyε ) " " λx.λyε
λxy " " λx.y

**Règle 3** : Nous supprimons autant que possible les λ, c'est à dire :

( λxy.εε' ) signifie ( λx.λy.εε' ) ou ( λx(λy(εε'))
( λxyz.εε' ) " ( λx.λy.λz.εε' ) ou ( λx(λy(λz (εε')))

etc ...

**Règle 4** : Nous permettons l'omission des parenthèses les plus externes dans ( λx.ε ), ou dans ( λx.εε' ), ou dans ( λxy.εε' ), ou dans ( λxyz.εε' ), etc... quand ces expressions constituent l'expression entière ( et non une sous-expression ).

**Contexte** : Un contexte est une λ-expression, dans laquelle une sous-expression n'existe pas. Un contexte est donc une λ-expression avec un trou. Autrement dit, un contexte C [] est :

(1) []

(2) ( ε C'[] ) si ε ∈ Λ et C'[] est un contexte

(3) ( C'[] ε ) " " " "

(4) ( λx C'[] ) si x ∈ V et C'[] est un contexte

Nous utiliserons pour les contextes les mêmes abréviations que pour les λ-expressions et par exemple :

λxy.[ ]yx signifiera ( λx ( λy(( [ ]y)x )))

Posons C [] = λxy.[ ]yx. Par C [ε], si ε est une λ-expression quel-
conque, nous désignons l'expression obtenue en insérant ε entre les sym-
boles [] du contexte désigné par C [], et en supprimant les caractères []
ou en les remplaçant par ( ) selon que la syntaxe des λ-expressions l'exige
ou non. Par exemple :

C [z] = λxy.zyx

C [λx.x] = λxy.( λx.x )yx
## Variables libres - Variables liées :

Une même variable x peut avoir plusieurs occurrences dans une expression $\epsilon$. Pour une occurrence donnée de x dans $\epsilon$, considérons le contexte $C$ [] formé par l'expression $\epsilon$ dans laquelle nous remplaçons cette occurrence de x par []. Nous avons donc $\epsilon = C[x]$ et nous dirons que cette occurrence de x est une occurrence liée de x dans $\epsilon$, s'il existe deux contextes $C'$ [] et $C''$ [] tels que : $C[] = C'[\lambda x.C'']$. Toute occurrence de x qui n'est pas une occurrence liée est appelée occurrence libre de x dans $\epsilon$.

Une variable qui a des occurrences liées est une *variable liée*. Une variable qui a des occurrences libres est une *variable libre*. Remarquons que dans une même expression une variable peut être à la fois libre et liée. De plus les variables liées d'une expression sont celles qui suivent immédiatement un $\lambda$ dans cette expression. Les ensembles VARLIB ($\epsilon$) et VARLIE ($\epsilon$), des variables libres et liées d'une $\lambda$-expression $\epsilon$, sont exactement définis récursivement de la manière suivante :

$$ 
\left\{
\begin{array}{l}
\text{VARLIE } (x) = \emptyset \\
\text{VARLIE } (\epsilon\epsilon') = \text{VARLIE } (\epsilon) \cup \text{VARLIE } (\epsilon') \\
\text{VARLIE } (\lambda x.\epsilon) = \text{VARLIE } (\epsilon) \cup \{x\}
\end{array}
\right.
$$

$$ 
\left\{
\begin{array}{l}
\text{VARLIB } (x) = \{x\} \\
\text{VARLIB } (\epsilon\epsilon') = \text{VARLIB } (\epsilon) \cup \text{VARLIB } (\epsilon') \\
\text{VARLIB } (\lambda x.\epsilon) = \text{VARLIB } (\epsilon) \cup \{x\}
\end{array}
\right.
$$

## Substitution :

Pour deux expressions M et N, et une variable x, la substitution de x par N dans M, notée $M[x\N]$, est définie par :

$$ 
\begin{array}{lcl}
x[x\N] & = & N \\
y[x\N] & = & y \quad (x \neq y) \\
(\epsilon\epsilon') [x\N] & = & (\epsilon[x\N] \epsilon' [x\N]) \\
(\lambda x.\epsilon) [x\N] & = & \lambda x.\epsilon \\
(\lambda y.\epsilon) [x\N] & = & \lambda z.\epsilon[y\z] [x\N] \quad (x \neq y) \quad \text{où } z
\end{array}
$$

est la variable définie par :

1) si $x \notin$ VARLIB ($\epsilon$) ou $y \notin$ VARLIB (N), $z = y$
2) sinon z est la première variable dans la liste $v_1, v_2, \dots$
telle que : z ≠ VARLIB (ε) ∪ VARLIB (N)

Autrement dit, M[x\N] est l'expression obtenue en substituant toutes les occurrences libres de x dans M par l'expression N.

**Conversions :**

**α - conversion** : toute sous-expression de la forme $λx.ε$ peut être remplacée par $λy.ε$ [x\y] si y ≠ VARLIB (ε).

**β - conversion** : toute sous-expression de la forme ($λx.M)N$ peut être remplacée par M[x\N]

**η - conversion** : toute sous-expression de la forme $λx.Mx$ peut être remplacée par M si x ≠ VARLIB (M)

Toute sous-expression de la forme $λx.ε$, ($λx.M)N$, $λx.Mx$ (si x ≠ VARLIB(M)) est appelée un *radical*. Nous avons donc des α-radicaux, β-radicaux, η-radicaux.

Par la suite, nous ne considérerons que α et β conversions. Intuitivement, α-conversion veut dire renommage des variables muettes que sont les variables liées et β-conversion signifie l'application d'une abstraction à un argument.

**Notations :**

1) $ε \to ε'$ signifie que ε donne ε' par application d'une règle de conversion à un radical R de ε.

2) $ε \xrightarrow{R} ε'$ a le même sens que précédemment mais parmet de préciser le radical R sur lequel la conversion a eu lieu (Dans une même expression, il peut y avoir, bien sûr, plusieurs radicaux).

3) $ε \to_α ε'$ ou $ε \to_{β} ε'$ précise le type de la conversion effectuée.

4) $ε \to^* ε'$ signifie que ε' s'obtient de ε par un nombre (éventuellement nul) de conversions. Nous dirons encore qu'il y a une *réduction* de ε à ε' ou que ε' est *dérivable de ε*.
Nous combinons ces notations pour obtenir :

$\epsilon \xrightarrow{R} \epsilon'$, $\epsilon \xrightarrow{R} \epsilon'$, $\epsilon \xrightarrow{*} \epsilon'$, $\epsilon \xrightarrow{*} \epsilon'$, $\epsilon \xrightarrow{\alpha, \beta} \epsilon'$ dont les sens sont immédiats.

Si $\epsilon \xrightarrow{R} \epsilon'$, nous dirons encore que $\epsilon'$ s'obtient de $\epsilon$ par contraction du radical R de $\epsilon$, le contracté de R dans $\epsilon'$ étant la sous-expression correspondant à R dans $\epsilon'$.

**Convention** : Nous ignorons autant que possible par la suite les $\alpha$-conversions et chaque fois que nous parlerons de conversions ou réductions nous voudrons dire $\beta$-conversions ou $\beta$-réductions.

**Forme normale** :

Une expression qui ne contient aucun $\beta$-radical est en forme normale. Une expression $\epsilon$ a une forme normale s'il existe une expression $\eta$ en forme normale telle que : $\epsilon \xrightarrow{*} \eta$

**Descendants** :

Supposons $\epsilon \xrightarrow{R} \epsilon'$ avec $R = (\lambda x.M)N$ et considérons un autre radical de $\epsilon$, $S = (\lambda y.P)Q$. Les descendants ("résidual") de $S$ dans $\epsilon'$ sont définis de la manière suivante :

1) Si $R$ et $S$ sont deux expressions qui ne se recouvrent pas, la réduction de $\epsilon$ à $\epsilon'$ ne touche pas à $S$. Et dans $\epsilon'$ on retrouve la même expression $(\lambda y.P)Q$ qui est le descendant (unique) de $S$ dans $\epsilon'$.

2) Si $S$ contient strictement $R$ :

a) $P$ contient $R$. Dans $\epsilon'$, après contraction de $R$, nous retrouvons une sous-expression $P'$ correspondant à $P$. Et $(\lambda x.P')Q$ se transforme en $(\lambda x.P')Q$, descendant (unique) de $S$ dans $\epsilon'$.

b) $Q$ contient $R$. Après contraction de $R$, $Q$ se transforme en $Q'$, sous-expression de $\epsilon'$, et $(\lambda x.P)Q$ se transforme en $(\lambda x.P)Q'$, descendant (unique) de $S$ dans $\epsilon'$.

3) Si $S = R$, $S$ n'a aucun descendant dans $\epsilon'$.
4) Si R contient strictement S :

a) M contient S. Dans $\epsilon'$, ($\lambda x.M)N$ a été remplacé par $M[x\N]$ et les occurrences libres de x dans S, sous-expression de M, ont été remplacées par N pour donner une sous-expression (($\lambda y.P)Q[x\N]$), sous-expression de $M[x\N]$, descendant (unique) de S dans $\epsilon'$.

b) N contient S. Dans $\epsilon'$, ($\lambda x.M)N$ a été remplacé par $M[x\N]$ sous-expression de N, se retrouve autant de fois (éventuellement nul) que N remplace x dans $M[x\N]$. Toutes ces occurrences de S, dans $M[x\N]$ et donc dans $\epsilon'$, sont les descendants de S dans $\epsilon'$.

Si $\epsilon \xrightarrow{R} \epsilon'$, nous appelerons *père* d'un radical S dans $\epsilon'$, le radical de $\epsilon$ dont S est un descendant. Si $\epsilon \xrightarrow{\star} \epsilon'$, les descendants d'un radical S de $\epsilon$, dans $\epsilon'$, sont obtenus par fermeture de la définition précédente de descendant. Si $\epsilon \xrightarrow{\star} \epsilon'$, l'ancêtre dans $\epsilon$ d'un radical S de $\epsilon'$ est le radical de $\epsilon$ dont S est un descendant.
Remarquons que père et ancêtre ne sont pas toujours définis.

Nous dirons que dans une expression $\epsilon$, une sous-expression R est à gauche d'une autre sous-expression S de $\epsilon$ si :

1) R et S sont deux sous-expressions disjointes et R est à gauche de S;

2) R contient S.

Remarquons que dans ces deux cas le bord à gauche de la sous-expression R est à gauche de celui de S.

Remarquons aussi que si R et S sont deux radicaux et si R est à gauche de S et si $\epsilon \xrightarrow{S} \epsilon'$, R n'a qu'un seul descendant dans $\epsilon'$.

**Théorème de Church-Rosser**

Théorème : Si $\epsilon \xrightarrow{\star} \epsilon'$ et $\epsilon \xrightarrow{\star} \epsilon''$ il existe $\eta$ tel que : $\epsilon' \xrightarrow{\star} \eta$ et $\epsilon'' \xrightarrow{\star} \eta$.

Une démonstration de ce théorème figure dans [2] de Curry [3] le montre dans les hypotèses encore plus générales. Nous n'utiliserons par la suite que cette formulation restreinte, qui ne fait intervenir que $\alpha$ et $\beta$ conversions.

**Corollaire immédiat** : Si $\epsilon$ a une forme normale, cette forme normale est unique à des $\alpha$-conversions près.
**Théorème de standardisation :**

**Définition** : On dit qu'une réduction $\epsilon = \epsilon_0 \underset{R_1}{\stackrel{R_2}{\rightarrow}} \epsilon_1 \underset{R_n}{\stackrel{R_{n-1}}{\rightarrow}} \dots \underset{R_n}{\stackrel{R_n}{\rightarrow}} \epsilon_n$ est une (β-) réduction standard si, pour tout $i$ ($1 \le i \le n-1$), le contracté de $R_i$ dans $\epsilon_i$ est à gauche de $R_{i+1}$. De $\epsilon_0$ à $\epsilon_n$, grossièrement parlant, on contracte les radicaux de la gauche vers la droite, en fait surtout de l'extérieur vers l'intérieur.

**Théorème de standardisation** : Si $\epsilon \stackrel{*}{\rightarrow} \epsilon'$, il existe une réduction standard de $\epsilon$ à $\epsilon'$.

Une démonstration existe dans Curry [3].

**Corollaire immédiat** ; Si $\epsilon$ a une forme normale, la réduction normale ( consistant à contracter systématiquement le radical le plus à gauche ) atteint la forme normale.