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

HAL
open science

# Minimal and optimal computations of recursive programs

Gérard Berry, Jean-Jacques Levy

► To cite this version:

Gérard Berry, Jean-Jacques Levy. Minimal and optimal computations of recursive programs. [Research Report] IRIA-RR-225, IRIA. 1977, pp.14. hal-04716446

HAL Id: hal-04716446

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

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
<figure><img src="image_3.png" /></figure>

laboria

laboratoire de recherche
en informatique
et automatique

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

MINIMAL AND OPTIMAL
COMPUTATIONS
OF RECURSIVE PROGRAMS

Gérard BERRY
Jean-Jacques LÉVY

Rapport de Recherche N° 225

Mars 1977

14+p

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20
MINIMAL AND OPTIMAL COMPUTATIONS OF RECURSIVE PROGRAMS

Gérard Berry

Ecole des Mines, Paris - IRIA/LABORIA

Jean-Jacques Lévy

IRIA/LABORIA

Résumé :

Le but de cet article est de généraliser les résultats d'optimalité des calculs des programmes récursifs obtenus par J. Vuillemin. Des résultats syntaxiques nouveaux sont d'abord obtenus en remplaçant l'étude des termes par l'étude des dérivations. Les résultats d'optimalité sont ensuite montrés dans l'interprétation symbolique, et s'appliquant à diverses classes d'interprétations plus générales que les interprétations séquentielles considérées par J. Vuillemin.

Abstract :

The purpose of this paper is to generalize J. Vuillemin's results on optimal computations of recur-
sive programs. New syntactic results are obtained by considering derivation spaces instead of term
interpretation. They apply to various classes of interpretations, which are more general than the
sequential interpretations considered by J. Vuillemin.

Ce travail a été présenté au 4th ACM-SIGACT-SIGPLAN Coll. on Principles of Programming Languages, Santa Monica, Cal. Jan. 1977, et doit être cité comme tel.

This work has been presented at a conference and should be refered as a communication to the 4th ACM-SIGACT-SIGPLAN Coll. on Principles of Programming Languages, Santa Monica, Cal. Jan. 1977.

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

Procedure call mechanisms have mainly been studied in the framework of recursive programs without assignments, for the simplicity of their operational and denotational semantics (See Scott [16], Nivat [14], Vuillemin [17]).

According to operational semantics, procedure calls act as textual rewritings; "computation rules" select at each computation step the occurrences of unknown functions to be rewritten. A computation rule is called correct if the value it computes is the one given by the denotational semantics. Correctness and efficiency of computation rules have been studied in Vuillemin [17,18], Montangero-Pacini-Turini [13], Downey-Sethi [7]. The main results are well-known: innermost evaluation (call by value) is not correct, parallel outermost or full substitution are correct. Vuillemin [17,18] gives a sufficient condition for a rule to be correct, (safety), later extended by Downey-Sethi [7] into a necessary and sufficient one (security). Vuillemin also studies a particular implementation of call-by-name, the delay rule; he shows its optimality with respect to a reasonable implementation cost, provided interpretations satisfy a sequentiality condition. This result is in fact twofold: sequentiality allows elimination of useless steps, and optimality follows by using sharing mechanisms in term implementation. The basis of all these studies is the following theorem (Vuillemin [17,18]): provided some restrictive conditions on programs are satisfied, the set of terms derivable from a given term is a lattice under the derivation ordering.

Our aim is to extend these results, for the three following reasons: first, though every program can be transformed to match Vuillemin's conditions, the transformations may affect the costs of computations: a more direct proof can be investigated. Second, a direct generalization to the λ-calculus is not straightforward, since λ-terms definitely do not form lattices. Third, the symbolic (or Herbrand) interpretation [5] is not sequential in the sense of Vuillemin, and no optimality result is known for it.

Our point of view will be purely syntactic: we reconstruct the lattice property in derivations. We study minimal computations (i.e. finite or infinite derivations) in the symbolic interpretation, and transform them into optimal ones. Eventually, we characterize interpretations to which similar results

apply. Extension towards the λ-calculus is done in [10].

The lattice property of terms breaks down in general: two very different derivations may lead to the same term by syntactical accidents, which collapse two a priori different terms. In section I, we take care of this fact by introducing an equivalence and a preorder on derivations. We give three characterizations of these relations. For the main one, we extend the classical notion of residuals [4] by defining residuals of derivations by derivations. We show that derivation classes form a lattice.

In section II, we study the "simple derivations" defined by Vuillemin with use of labels (named here complete derivations). We give two characterizations of them in the usual formalism.

Section III, is devoted to minimality and optimality results. Ordering infinite derivations as well as finite one, we construct least computations of every syntactic approximation of the infinite tree determined by the program. The associated complete derivation are optimal with respect to Vuillemin's cost. Extension to interpretations is then straightforward, as soon as they satisfy a syntactic condition. All classes of sequential interpretations considered in [2,6,11,17] do satisfy this condition. The "computation rule" we use for constructing the optimal computations is very inefficient in general, but reduces to the usual delay rules in sequential interpretations.

## PRELIMINARIES

### F-Algebras

Let $F = \{f_1, f_2, \dots, f_m\}$ be a set of function symbols; each symbol $f_i$ is given with its arity $\rho(f_i) \ge 0$. We denote by $F^K$ the set of k-ary symbols in $F$. The nullary symbols are called constants. A F-algebra is an object $I = \langle D_I, f_1^I, \dots, f_m^I \rangle$ where $D_I$ is a set and each $f_i^I$ is a mapping from $D_I^{\rho(f_i)}$ into $D_I$. A morphism of F-algebras $I$ and $I'$ is a mapping $\theta: D_I \to D_{I'}$, which preserves the operations $f_i$:

$$ \forall f_i \in F^K, \forall d \in D_I^k, \theta(f_i^I(d)) = f_i^{I'}(\theta(d)) $$
### The Free F-algebra :

Consider a denumerable set $V=\{x_1,x_2,...,x_k,...\}$ of variable symbols, and $V_k=\{x_1,x_2,...,x_k\}$. Then $V$ generates the free-algebra $M(F,V)$ It contains $V$ and is such that for any $F$-algebra $I$, every mapping $v: V \to D_I$ extends in a unique way into a morphism $(I,v): M(F,V) \to D_I$. Elements of $M(F,V)$ are called terms, and will be represented by well-formed-formulae or trees. The morphism $(I,v)$ determines the value of a term for the interpretation $I$ and the data mapping $v$.

A substitution is a mapping $\sigma: V \to M(F,V)$, extended into a morphism $\sigma: M(F,V) \to M(F, V)$. We write $\sigma: \tau/\bar{\tau}$, and for $t \in M(F,V)$, $\sigma t = [\tau/\bar{\tau}]$.

### Occurrences of symbols in terms

Let $t \in M(F,v)$ and $s \in Fv$, the set $C(s,t)$ of occurrences of $s$ in $t$ is defined by:

$$ (i) \quad t=x_i \in V \quad C(x_i, x_i) = \{\epsilon\} \\ \qquad C(s, x_i) = \emptyset \quad \text{for } s \neq x_i $$

$$ (ii) \quad t=f(\tau), f \in F^k, C(s,t)=C \cup \bigcup_{j=1}^{k} ((f,j) \cdot C(s,t_j)) $$

$$ \text{with } C = \{\epsilon\} \quad \text{if } s=f \text{ and } C=\emptyset \quad \text{otherwise} $$

**Example :**

$$ t=f(x_1, f(x_2, x_1)). \text{ Then } C(f,t) = \{\epsilon, (f,2)\} \text{ and} $$

$$ C(x_1, t) = \{(f,1), (f,2), (f,2)\}. $$

The size $||t||$ of $t$ is the number of occurrences in $t$.

**Lemma 1 :** let $t''=t[t'/x_i]$ and $c'' \in C(s,t'')$. Then either $c'=c \in C(x_i,t)$ and $c' \in C(s,t')$, or $c'' \in C(s,t)$.

**Proof :** by induction on the length of $c''$. []

### Recursive program schemes. Derivation and residuals.

Consider two disjoint sets $F=\{f_1, f_2, ..., f_m\}$, of basic function symbols, and $\phi=\{\phi_1, \phi_2, ..., \phi_N\}$, of unknown function symbols, given with the arities $\rho(f_i) \ge 0$ and $\phi_i \ge 0$. We write $M=M(F\phi, V)$ and $C(\phi, t) = \bigcup_{i=1}^N C(\phi_i, t)$. All terms implicitly belong

to $M$, and since we shall only be interested in occurrences in $C(\phi, t)$, we abbreviate $c \in C(\phi, t)$ into $c$ in $t$. Given $c, c'$ in $t$, then $c$ contains $c'$, written $c \le c'$, if $c$ is a prefix of $c'$, and $c$ and $c'$ are disjoint, written $c|c'$, if neither $c \le c'$ nor $c' \le c$. An occurrence $c$ in $t$ is outermost in $t$ if it is not contained in another $c'$ in $t$.

A recursive program scheme $\Sigma$ is a system of equations

$$ \Sigma \mid \phi_i(x_1, x_2, \dots, x_p(\phi_i)) = \tau_i \quad i = 1, 2, \dots, N \text{ and } \tau_i \in M(F\phi, V) \quad \forall \phi_i \neq \emptyset $$

we consider a fixed program scheme $\Sigma$, thus omitted in notations. Let $t \in M$ and $c \in C(\phi_i, t)$, and let $y$ be an additional variable. There exists a unique decomposition $t = t_c[\phi_i(\tau)/y]$ s.t. $t_c \in M(F\phi, V)$ and $C(y, t_c) = \{c\}$.

Then $t$ derives immediately into $\tau'$ by rewriting of $c$, written $t \stackrel{\tau'}{\to} t'$, iff $t' = t_c[\tau_i[t/\bar{\tau}]/y]$. Given $c' \in C(\phi_j, t')$, three cases are possible, by lemma 1:

(i) $c' = c \cdot c_1$ with $c_1 \in C(\phi_j, \tau_i)$. Then $c'$ is created by the derivation.

(ii) $c' \in C(\phi_j, t_c)$. Then $c'$ in $t'$ is a residual of $c'$ in $t$.

(iii) $c' = c \cdot c_1 \cdot c_2$ with $c_1 \in C(x_k, \tau_i)$ and $c_2 \in C(\phi_j, t_k)$.

Then $c'$ in $t'$ is a residual of $c(\phi_j, k) \cdot c_2$ in $t$. (See Church [4]).

**Example :** $\Sigma : \phi(x) = f(x, \phi(x))$

$$ \begin{align*} t &= f(\phi(\phi(x)), \phi(x))^{(f_1!)} f(\phi(x), \phi(\phi(x))), \phi(x)) \quad \text{with} \\ t(f_1) &= f(y, \phi(x)). \quad \text{Here } (f_1)(f_2) \text{ is created, } (f,2) \\ \text{is a residual of } (f,2), \text{ and } (f,1)(f,1) \text{ and} \\ (f,1)(f,2), (\phi,1) \text{ are residuals of } (f,1), (\phi,1) \end{align*} $$

Given $C \in C(\phi, t)$, let $C/c$ denote the set of residuals of the elements of $C$ by immediate derivation of $c$, and let $c'/c$ abbreviate $\{c'\}/c$.

A derivation $d: t \stackrel{*}{\to} t'$ is a sequence

$$ d: t \to t_1 \to t_2 \to \dots \to t_k = t'. \text{ The concatenation of } d: t \stackrel{\tau}{\to} t' \text{ and } d': t \stackrel{\tau}{\to} t'' \text{ is written } d;d' \text{ and } \emptyset \text{ denotes the empty derivation. When } t \text{ is assumed from the context, } d \text{ can be written } d=c_1;c_2;\dots;c_k. \text{ Therefore } c \text{ will denote either an occurrence or its derivation, unambiguously in each context. The notion of residual extends to derivations for } C \in C(\phi, t) \text{ by :} $$

$$ C/(c;d) = (C/c)/d, \text{ and } C/\emptyset = C. $$

If $d=c_1;c_2;\dots;c_k$, then $c \cdot d$ abbreviates $c \cdot c_1; c \cdot c_2; \dots; c \cdot c_k$.

## I. EQUIVALENCE OF DERIVATIONS MODULO PERMUTATIONS.

The preorder $t \stackrel{*}{\to} t'$ is not an ordering if Vuillemin's conditions [17] are removed, and term classes do not even form lattices; let $\Sigma: \phi(x) = x, \psi(x,y)=x$ and consider all derivations from $\phi(\psi(\phi(x),y))$. This example involves the derivations $d_1: \phi(\phi(x)) \stackrel{\Sigma}{\to} \phi(x)$ and $d_2: \phi(\phi(x))^{(\phi_1!)} \phi(x)$ which give the same result by syntactical coincidence. Using term spaces is the same as using derivations spaces quotiented by the equivalence $d \equiv d'$ if $d$ and $d'$ are of the form $t \stackrel{*}{\to} t'$. Remark now that $\epsilon/d_1=\emptyset$ and $\epsilon/d_2=\{\epsilon\}$. The example suggests to define a finer equivalence : let $d, d'$ : $t \stackrel{*}{\to} t'$ be preequivalent

if $c/d = c/d'$ for all $c$ in $t$. Then $d_1 \not\equiv d_2$. Preequivalence, as a congruence for the concatenation, defines a preorder $\leq$ by $d \leq d'$ iff $\exists d'' \text{ s.t. } d;d''=d'$. (The same definition with $\equiv$ gives the image in derivations of the preorder $\stackrel{*}{\to}$ in terms). However the equivalence generated by $\leq$ is not $=$. Take $\Sigma: \phi(x,y) = \phi(y,x), \psi(x)=f$ and $d: \phi(\psi(x), \psi(x)) \stackrel{\Sigma}{\to} \phi(\psi(x), \psi(x))$. Let $d_1=d$ and $d_2=d$. Then $d_1 \leq d_2 \leq d_1$ since $d_1;d \leq d_2$ and $d_2;d \leq d_1$, but $d_1 \neq d_2$.
is false. Therefore we define a finer equivalence on derivations.

**I.1. Definition of the equivalence :**

Let $c_1, c_2$ be in a term $t$, and consider the derivation $t \stackrel{c_1}{\to} t_1$. Then $c_2/c_1$ in $t_1$ is a set of disjoint occurrences in $t_1$, and we shall also denote by $c_2/c_1$ the set of all derivations defined by the permutations of the set $c_2/c_1$. They are easily seen to be preequivalent.

When considering such derivation sets, we extend the concatenation by $D;D' = \{d;d'|d \in D \text{ and } d' \in D'\}$ and any relation $R$ by $RD'$ iff $\forall d \in D, d' \in D', dRd'$.

The following permutation lemma is the basis of our constructions.

**I.1.1. Lemma :** If $c_1, c_2$ are in a term $t$, then
$c_1; (c_2/c_1) \cong c_2; (c_1/c_2)$.

**Proof :** let $d_1=c_1; (c_2/c_1)$ and $d_2=c_2; (c_1/c_2)$. Let $c$ be in $t$. We have $d_1 \equiv d_2$ and $c/d_1=c/d_2$ by case inspection on the relative positions of $c, c_1, c_2$. Thus $d_1 \cong d_2$. $\Box$

**I.1.2. Definition :** The equivalence of derivations modulo permutations, written $\sim$, is the least equivalence satisfying :

(i) $c_1; (c_2/c_1) \cong c_2; (c_1/c_2)$

(ii) if $d \sim d'$, then $d_1;d;d_2 \sim d_1;d';d_2$ for any $d_1,d_2$.

Notice that $\sim$ is the least congruence for concatenation which satisfies the permutation lemma, and that $\sim$ is a refinement of $\cong$, i.e. $d_1 \cong d_2$ implies $d_1 \cong d_2$. Intuitively, if $d_1 \cong d_2$, we can match $d_2$ with $d_1$ by successive uses of the permutation lemma.

**I.2. Complete derivations of a set of occurrences :**

Let $C$ be a set of occurrences in a term $t$. Following Curry & Feys [6], we are concerned with deriving all occurrences of $C$. This notion clearly makes sense when $C$ is a set of disjoint occurrences (as previously seen). But this is more difficult when there are nested occurrences in $C$.

**I.2.1. Definition :** The set $\bar{C}$ of complete derivations of $C$ is the set of finite and infinite derivations defined by $\bar{C} = \{c; (C/c) | c \in C\}$.

**I.2.2. Theorem :** All derivations in $\bar{C}$ are finite and equivalent modulo permutations.

**Proof :** If $c \in C$, let $\pi(c,C)$ be the nesting level of $c$ in $C$ (i.e. the number of prefixes of $c$ in $C$). Let $k=k(C)$ be the maximal nesting level in $C$ and $n(C)$ be the number of occurrences in $C$ at level $i$. Consider the $k$-tuple $n(C) = \langle n_k(C), n_{k-1}(C), \dots, n_1(C) \rangle$. Then one can check easily that $n(C/c) < n(C)$ for any $c$ of $C$ when $<$ is the lexicographic ordering on $N^k$. Thus all derivations in $\bar{C}$ are finite. Furthermore, suppose $d_1, d_2 \in \bar{C}$. We get $d_1 \sim d_2$ by induction on $n(C)$.

The only problem is when $d_1=c_1; d_1'$ and $d_2=c_2; d_2'$. By I.1.1, we have $C/(c_1; (c_2/c_1)) = C/(c_2; (c_1/c_2)) = C'$. Thus, if $d_3 \in \bar{C}'$, then $(c_2/c_1); d_3 \in (\bar{C}/c_1)$ and $(c_1/c_2); d_3 \in (\bar{C}/c_2)$. By induction $d_1' \sim (c_2/c_1); d_3$ and $d_2' \sim (c_1/c_2); d_3$. Hence $d_1 \sim d_2$ by I.1.1. $\Box$

This theorem is a strengthened form of Curry's Property E [6], because we replaced preequivalent by equivalent. The modification seems minor here but is crucial for what follows.

The permutation lemma extends to sets of complete derivations as follows (and this corresponds to the so-called "lemma of parallel moves in [6]):

**I.2.4. Lemma :**

If $c_1$ and $c_2$ are sets of occurrences in a term $t$, then $\bar{c}_1; \bar{c}_2/c_1 \sim \bar{c}_2; c_1/c_2$.

**Proof :** Both sets only contain complete derivations of $c_1 \cup c_2$. $\Box$

**I.2.5. Definitions :**

By theorem I.2.2, given $t$ and a set $C$ of occurrences in $t$, there exists a unique $t'$ such that any $d \in \bar{C}$ is of the form $d:t=t'$. We therefore write $t \stackrel{C}{\to} t'$ and define set derivations in the same way as derivations, but using upper-case letters :

$D = C_1; C_2; \dots; C_n$ etc... Any derivation $d = c_1; c_2; \dots; c_n$ can be considered as a singleton derivation $d = \{c_1\}; \{c_2\}; \dots; \{c_n\}$. Lower case letters will be consistently used for singleton derivations. Conversely, to any set derivation $D = C_1; C_2; \dots; C_n$ is associated the set of derivation $\bar{D} = \bar{C}_1; \bar{C}_2; \dots; \bar{C}_n$.

The equivalence relation $\sim$ can therefore be extended to set derivations by $D \sim D'$ if $\bar{D} \sim \bar{D}'$ as derivation sets. Notice that by theorem I.2.2 and lemma I.2.4, the equivalence of set derivation is also the least congruence for the concatenation satisfying $C_1; (C_2/C_1) \sim C_2; (C_1/C_2)$ for all $t$ and $C_1$ and $C_2$ in $t$.

We denote by $D(t)$ the set of set derivations starting from $t$. The length $|D|$ of $D$ is the number of nonempty sets derived in $D$.
**I.3. Residuals of derivations :**

**I.3.1. Definition :** If $D_1, D_2 \in \mathcal{D}(t)$, the derivation $D_2/D_1$ *residual of* $D_2$ *by* $D_1$ *is defined inductively* by :

(i) $\emptyset / D = \emptyset$

(ii) $(D_2; C_2)/D_1 = (D_2/D_1); (C_2/(D_1/D_2))$

This definition makes sense by induction on $|D_1|+|D_2|$, taking as hypothesis that $|D_2/D_1| \le |D_2|$ and is illustrated by diagram 1, where each elementary square is an application of I.2.4.

**I.3.2. Lemma :**

1) $D/\emptyset = D$

(2) $(D_2; D_1')/D_1 = (D_2/D_1); (D_1'(D_1/D_2))$

3) $D_2/(D_1; D_1') = (D_2/D_1)/D_1'$

*Proof* : by induction on $|D|$ for 1, by simultaneous induction on $\langle \max(|D_1'|, |D_2'|), |D_2| \rangle$ for 2 and 3. □

**I.3.3. Lemma :** If $D_1, D_2 \in \mathcal{D}(t)$, then

$D_1; (D_2/D_1) \sim D_2; (D_1/D_2).$

*Proof* : by induction on $|D_1| + |D_2|$. □

This lemma is a generalisation of the permutation lemma to derivations, but is also a strengthened form of the Church-Rosser theorem and the proof technique is exactly the one used in [6]. But the advantage of considering equivalence instead of preequivalence appears in terms of residuals of derivations. Equivalence exactly means consistency of residuals of derivations.

The equivalence ~ defined in I.1.2. can be generated using lemmas I.2.4. or I.3.3. instead of lemma 1.1.1.

**I.3.4. Lemma :** If $D_1 \sim D_2$, then $D_1/C \sim D_2/C$.

*Proof* : We have only to consider $D_1=C_1; (C_2/C_1)$ and $D_2=C_2; (C_1/C_2)$. Thus $D_1/C=(C_1/C); D_1'$ where $D_1'=(C_2/C_1)/(C/C_1)$. By lemma I.3.2., we get $D_1'=C_2/(C_1;(C/C_1))=C_2/(C;(C_1/C))$ by lemma I.3.3. Therefore $D_1'=(C_2/C); (C_1/C)$ by I.3.2. and $D_1/C=C_1'; (C_2'/C_1')$ if $C_1'=C_1/C$ and $C_2'=C_2/C$. Similarly $D_2/C=C_2'; (C_1'/C_2')$. Hence $D_1/C \sim D_2/C$ by I.3.3. □

**I.3.5. Theorem :** $D_1 \sim D_2$ iff $\forall D. D/D_1 = D/D_2$ iff $D_1/D_2 = D_2/D_1 = \emptyset$.

*Proof* : 1 => 2. By induction on $|D|$ using I.3.4. We remember that $D_1 \sim D_2$ implies $D_1 \simeq D_2$.

2 => 3. Take $D=D_1$ or $D=D_2$ and remark that $D_1/D_1=D_2/D_2=\emptyset$.

3 => 1. By induction on $|D_1|+|D_2|$ using I.3.2 and I.3.3. □

**I.3.6 Proposition :** $D_1 \sim D_2$ iff $\forall D. D_1/D \sim D_2/D$ iff $\forall D. D_1/D=D_2/D$.

*Proof* : 1 => 2. By induction on $|D|$ and lemma I.3.4.

2 => 3. Because ~ is a refinement of =.

3 => 1. Take $D=D_1$ or $D=D_2$ and apply I.3.5. □

**I.3.7. Proposition :** The equivalence ~ is left simplifiable. Formally, if $D; D_1 \sim D; D_2$, then $D_1 \sim D_2$.

*Proof* : obvious from I.3.5. since $(D; D_1)/(D; D_2)=D_1/D_2$. □

**I.4. The lattice of derivation classes :**

We now define the preorder on derivations.

**I.4.1. Definition :** $D_1 \le D_2$ iff $\exists D_s. t. D_1; D \sim D_2$

**I.4.2. Proposition :** The relation $\le$ is a preorder with ~ for associated equivalence and $D_1 \le D_2$ iff $D_1/D_2=\emptyset$.

*Proof* : $D \le D$ since $D \sim D$. Assume $D_1 \le D_2 \le D_3$. Then there are $D_1'$ and $D_2'$ s.t. $D_1; D_1' \sim D_2$ and $D_2; D_2' \sim D_3$. Hence $D_1; D_1'; D_2' \sim D_3$ and $D_1 \le D_3$. Now suppose $D_1 \le D_2$. Then $D_1; D \sim D_2$ for some $D$. Thus lemma I.3.2 and theorem I.3.5 implies $(D_1; D)/D_2=(D_1/D_2); D'=\emptyset$. Therefore $D_1/D_2=\emptyset$

Conversely, if $D_1/D_2=\emptyset$, one has $D_1; (D_2/D_1) \sim D_2$ by the permutation lemma, i.e. $D_1 \le D_2$. Now if $D_1 \le D_2 \le D_1$, we have $D_1/D_2=D_2/D_1=\emptyset$ and thus $D_1 \sim D_2$ by I.3.5. □

**I.4.3. Notation :** Let $[D]$ be the equivalence class of $D$ and $[D(t)]$ be the set $D(t)/\sim$.

**I.4.4. Theorem :** The set $[D(t)]$ with the quotient ordering $\le$ is a upper-semilattice. Two elements $[D_1]$ and $[D_2]$ have the l.u.b. $[D_1; (D_2/D_1)]=[D_2; (D_1/D_2)]$

*Proof* : One has $D_1 \le D_1; (D_2/D_1)$ and $D_2 \le D_2; (D_1/D_2)$. Furthermore, let $D_1 \le D$ and $D_2 \le D$. By I.4.2, we have $D_1/D=D_2/D=\emptyset$. Lemma I.3.2 implies $(D_1; (D_2/D_1))/D=(D_1/D); D'=D'$ where $D'=(D_2/D_1)/(D/D_1)$. But $D'=D_2/(D_1; (D/D_1))=D_2/(D; (D_1/D))=(D_2/D)/(D_1/D)$ by I.3.2, I.3.3 and I.3.5. Hence $D'=\emptyset$ and $D_1; (D_2/D_1) \le D$ by I.4.2. □

It is also shown in [3] that $[D_1]$ and $[D_2]$ have a greater lower bound.
**I.5. Standard derivations :**

Standard derivations, which work in an out-
side-in way and by convention from left to right
for disj.int occurrences, are introduced in [6].
The standardisation theorem in [6] allows any reduc-
tion to be standardised. But, although there can
be several standard derivations between two given
terms, each equivalence class contains a unique
standard derivation. This will be our improved
standardisation theorem.

**I.5.1. Definition** : For $t=s(\vec{t})$ and $d_i:t_i\to t_i'$, let
$s(\vec{d})=((s,1).d_1);((s,2).d_2);...((s,k).d_k)$ where
$k=p(s)$. The *derivation* $d$ is *standard* if $d=\epsilon;d'$ and
$d'$ is standard or if $d=s(\vec{d})$ and $d_i$ is standard for
all $i$.

**I.5.2. Notations** : The set $C$ of ... occurrences is
internal if $\epsilon \in C$. The derivation $D$ is internal if
it only derives internal sets. Let $\epsilon^n = \epsilon; \epsilon; ... \epsilon$.

**I.5.3. Lemma** : For any $C$, there are $n$ and $C'$ inter-
nal s.t. $n \ge 0$ and $C \sim \epsilon^n; C'$.

*Proof* : by theorem I.2.2, since we can consider
any outside-in complete derivation of C. $\square$

**I.5.4. Theorem** : There is a unique standard deriva-
tion in each equivalence class of $[D(t)]$.

*Proof : Existence* (this proof comes from [12]).
Consider any derivation $D: t \xrightarrow{*} t'$. With the above
lemma, we can write $D=C_1;C_2;...C_n$ where either
$C_i=\{\epsilon\}$ or $C_i$ is internal for all $i$. Let $\ell(D)$ be
maximal s.t. $D=D'; \epsilon^\ell(D); D''$ with $D''$ internal. Let
$n(D)$ be the number of internal $C_i$ preceeding some
$\epsilon$-step. Formally $n(D)$ is the number of $i$ s.t. $C_i$ is
internal and $\exists j$. $1 \le i < j \le n$ s.t. $C_j=\{\epsilon\}$. Consider the
triple $< ||t'||, n(D), \ell(D)>$. We have two cases. First-
ly $D=\epsilon^\ell(D)$; $D_2$ with $D_2$ internal. By induction on
$||t'||$, we get $D_2 \sim D_2'$ where $D_2'$ is standard and
$D \sim \epsilon^\ell(D)$; $D_2'$. Secondly $D=D_1; C; \epsilon^\ell(D)$; $D_2$ with $C$ and $D_2$
internal and $\ell(D)>0$. But $C$ cannot create $\epsilon$ and $C; \epsilon$
is a complete derivation of $Cu\{\epsilon\}$. Hence $C; \epsilon \sim \epsilon^P; C'$
with $C'$ internal by the above lemma and $p>0$ since
$\epsilon \in Cu\{\epsilon\}$. Therefore $D \sim D'$ with
$D'=D_1; \epsilon^P; C'; \epsilon^{\ell(D)-1}$; $D_2$. Then $n(D')<n(D)$ if $C'=\emptyset$ or
$\ell(D)=1$, and $n(D')=n(D)$, $\ell(D')<\ell(D)$ if $C' \ne \emptyset$ and
$\ell(D)>1$. By induction $D' \sim D$ where $D'$ is standard.

**Uniqueness.** Let $d,d':t \xrightarrow{*} t'$ be standard s.t. $d \sim d'$.
We prove $d=d'$ by induction on $<|d|+|d'|, ||t'||$.
The induction works easily when $d=s(\vec{d}), d'=s(\vec{d}')$ or
$d=\epsilon;d_1, d'=\epsilon;d_1'$. Now suppose $d=\epsilon;d_1$ and $d'=s(\vec{d}')$.
Then $s=\phi\epsilon\Phi$ and $\epsilon/d'=(\epsilon)\ne\emptyset$ which contradicts $d \sim d'$ by
theorem I.3.5. $\square$
**I.6. Labelled derivations [9, 17]** :

We use Vuillemin's labelling system [17] to
mark occurrences along derivations. Given an alpha-
bet E, let the set E* of words on E be the set of
labels. (In fact associativity is not necessary but
convenient for notations). A labelling µ of a term t
is a mapping µ:C(Φ,t)→E*. A labelling ν of the pro-
gram Σ is a N-tuple (v₁,v₂,...,vN) of labellings vᵢ
of the τᵢ. Given a labelled term (t,µ) and an ele-
mentary derivation d:t<sup>Σ</sup>t' with c∈C(Φᵢ,t), the
corresponding step of labelled derivation

d:(t,μ)\* (t',μ') is defined by ;

μ'(c')=μ(c'|) if c'∈c'|/c

μ'(c')=μ(c)vᵢ(c'|) if c creates c' and c'=c.c'|.

For example, let $t=\phi(\phi(x))$ and $\Sigma: \phi(x)=f(x,\phi(\phi(x)))$ and let us write labels as exponents of occurrences in terms. Suppose $(\Sigma, v): \phi(x)=f(x, \phi^a(\phi^b(x)))$ and $(t, \mu)=\phi^c(\phi^d(x))$. Then $(t, \mu)=f(\phi^d(x), \phi^{ca}(\phi^{cb}(\phi^d(x)))).$

**I.6.1. Notation** : We write $d \equiv d'$ if $d$ and $d'$ are of the form $d, d' : (t, \mu)^{\frac{1}{2}}(t', \mu')$.

The permutation lemma also holds for labelled
derivations.

**I.6.2. Lemma** : If $c_1, c_2$ are in $t$, then
$c_1 ; (c_2 / c_1) \equiv_{\mu} c_2 ; (c_1 / c_2)$ for all $\mu$.

Proof : by cases inspection. ☐

**I.6.3. Proposition** : If $d_1 \sim d_2$, then $d_1 \equiv_{\mu} d_2$ for all $\mu$.

Proof : obvious from I.6.2. ☐

**I.6.4. Definition** : A labelling $\mu$ of a term $t$ is *consistent* if the labels $\mu(c)$ and $\mu(c')$ are incompatible for any pair $c$ and $c'$ of nested occurrences in $t$. A labelling $\nu$ of $\Sigma$ is consistent if all the $\nu_i$ are consistent.

With our notations, if $\mu$ is consistent and $c<c'$ then $\mu(c) \lor \mu(c')$. We remark that $\alpha|\beta$ implies $\alpha\gamma|\beta\delta$ and $\gamma\alpha|\delta\beta$ for any $\gamma$ and $\delta$. The consistency of labels is a technical condition used to connect labelled terms and the equivalence ~.

**I.6.5. Lemma** : If $\mu, \nu$ are consistent and if $(t, \mu)^{\frac{1}{2}}(t', \mu')$, then $\nu'$ is consistent.

Proof : by cases inspection on one step of
labelled derivation. []

**I.6.6. Proposition** : If $\mu, \nu$ are consistent, then for any $d$ there is one and only one $d'$ standard s.t. $d \equiv_{\mu} d'$.

**Proof** : By I.5.4, for any $d$, there is $d'$ standard s.t. $d \equiv_{\mu} d'$. Hence $d \equiv_{\mu} d'$ by I.6.3. Now suppose that $d$ and $d'$ are standard s.t. $d \equiv_{\mu} d'$. More precisely, let $d, d' : (t, \mu)^{\frac{1}{2}}(t', \mu')$. We prove $d=d'$ by induction on $<d|+|d'|, ||t||>$. If $d=s(d')$, $d'=s(d')$ or $d=\varepsilon;d_1$, $d'=\varepsilon;d'_1$, the induction works easily by using I.6.5.

Assume now that $d=\varepsilon;d_1$ and $d'=s(d')$. We have $s=\phi\in\Phi$ and $t=\phi(t)$, $t'=\phi(t')$. Along $d'$, we get $\mu'(\varepsilon)=\mu(\varepsilon)$. But $d:(\phi(t),\mu)^{\frac{1}{2}}(\tau[t/\tilde{x}],\mu_1)^{\frac{1}{2}}(t',\mu')$. Consider any $c_1$ in $\tau[t/\tilde{x}]$. Either $c_1\in\varepsilon/\varepsilon$ with $c$ internal to some $t_i$ and $\mu_1(c_1)=\mu(c)|_{\mu(\varepsilon)}$ by the consistency hypothesis. Either $c_1$ is created by $\varepsilon$ and $\mu(\varepsilon)<\mu(c_1)$. Therefore there is no $c$ in $\tau[t/\tilde{x}]$ s.t. $\mu_1(c)\le\mu(\varepsilon)$. Hence no occurrence in $t'$ can have $\mu(\varepsilon)$ for label, which contradicts $\mu(\varepsilon)=\mu'(\varepsilon)$. []

**I.6.7 Theorem** : $D_1 \sim D_2$ iff $D_1 \equiv_{\mu} D_2$ for all $\mu$, iff $D_1 \equiv_{\mu} D_2$ for some consistent $\mu, \nu$.

Proof : 1 => 2 by I.6.3, 2 => 3 by instantiation,

3 => 1 by I.5.4 and I.6.5. []

<figure><img src="image_6.png" /><figcaption>Diagram 1.</figcaption></figure>

**II. FAMILY OF OCCURRENCES AND f-COMPLETE DERIVATIONS**

**II.1: Family of occurrences :**

In order to compute in an "optimal" way, we
must share duplicated objects (see [13,17]). Sha-
ring residuals along derivations is certainly
necessary, but not sufficient, as shown by the
following example.

Let $\Sigma: \phi_1(x)=f(x,x), \phi_2(x)=g(\phi_2(x))$. Let $d:t=\phi_1(\phi_2(x))^\xi f(\phi_2(x),\phi_2(x))^c f(g(\phi_2(x)),g(\phi_2(x)))=t'$ where $C=\{(f,1),(f,2)\}$. The two occurrences $c_1=(f,1)(g,1)$ and $c_2=(f,2)(g,1)$ in $t'$ are not residuals of the same object along $d$. But it is easy
to see that they have to be shared. This can be
expressed in two ways. The first alternative, used
by Vuillemin [17], is to share them because they
have the same label in any labelling of d. Intuiti-
vely, residuals of shared occurrences are shared,
but also occurrences which are created in the same
way by shared occurrences. The second way, used here,
does not involve labels. There is a permutation d'
of d, namely

d':t=φ₁(φ₂(x))§ φ₁(g(φ₂(x)))§f(g(φ₂(x)),g(φ₂(x))=t'
s.t. c'=(φ₁,1). Then c₁,c₂ are indeed residuals of a
unique occurrence c=(φ₁,1)(g,1) in φ₁(g(φ₂(x))),
and therefore can be shared in d. The two approaches
will be shown equivalent. Thus the behaviour of
labels will be explained within the usual formalism.

II.1.1 : **Notation** : From now on, any pair derivation-occurrence written (D,c) is an abbreviation for D:t+t' and c in t'. We also consider pairs (D,C) when C is a set of occurrences in t'.

II.1.2. Definitions : We consider the relations $\le$ and $\sim$ (read "has for residual" and "belong to the same family as") over pairs (D,c) defined as follows :

$(D_1, c_1) \le (D_2, c_2)$ if $\exists$ D s.t. $(D_1;D) \sim D_2$ and $c_2 \in c_1/D$.

$(D_1, c_1) \sim (D_2, c_2)$ if $(D_1, c_1) \le (D_2, c_2)$

or $(D_2, c_2) \le (D_1, c_1)$ or $\exists (D,c) \text{ s.t. } (D_1, c_1) \sim (D,c) \sim (D_2, c_2)$

Hence the second relation is the symmetric and transitive closure of the first one. It is straightforward to check that $\le$ is a preorder and $\sim$ is an equivalence. Let us remark that, though we use the same symbols for different relations, the context will always avoid any confusion.

II.1.3 : **Proposition** : The two above relations are compatible with the equivalence of derivations w.r.t. permutations. Namely, if $D_1 \sim D'_1$ and $D_2 \sim D'_2$, we have
$(D_1, c_1) \le (D_2, c_2)$ iff $(D'_1, c_1) \le (D'_2, c_2)$ and
$(D_1, c_1) \sim (D_2, c_2)$ iff $(D'_1, c_1) \sim (D'_2, c_2)$.

Proof : obvious since $(D'_1;D) \sim D'_2$ when $D_1 \sim D'_1$, $D_2 \sim D'_2$ and $(D_1;D) \sim D_2$. $\square$

II.1.4 : **Proposition** :

1) $(D_1, c_1) \le (D_2, c_2)$ iff $D_1 \le D_2$ and $c_2 \in c_1 / (D_2 / D_1)$,

2) If $D_1 \sim D_2$ and if $(D_i, c_i) \le (D, c)$ for $i=1,2$, then
$c_1=c_2$,

3) If $(D_1, c_1) \le (D_2, c_2)$ and $D_1 \le D \le D_2$, then there is
a unique c s.t. $(D_1, c_1) \le (D, c) \le (D_2, c_2)$,

4) If $(D_i, c_i) \le (D, c)$ for $i=1,2$, then there are a unique $c'$, and some $D'$ s.t. $D' \sim 1$. u.b.($[D_1]$, $[D_2]$) and $(D_i, c_i) \le (D', c') \le (D, c)$.

Proof : obvious once we remark that $D_1 \sim D_2$ implies $c/D_1=c/D_2$ and that we have by definition $c_1=c_2$ if $c \in c_1/D$ and $c \in c_2/D$. $\square$

Consider again the above example. Let $d_1=(\epsilon;(f,1))$, $d_2=(\epsilon;(f,2))$ and $d_3=(\phi_1,1)$. Suppose $c_1,c_2,c$ have the same values as above. We have $(d_1,c_1) \sim (d_2,c_2) \sim (d_3,c)$, but $(d_3,c)$ seems more representative inside its family, because $d_3$ does nothing but "creating" c and all the elementary steps of $d_3$ are contained in the derivations $d_1$ and $d_2$.

II.1.5. **Definition** : The derivation *d* generates (d,c) if $d=\emptyset$ or $d=d_1;c_1$ with $d_1$ generating $(d_1,c_1)$ and $c_1$ creating c.

II.1.6. **Notation** : If $c_1;d'=d;c$, let $\bar{g}(d,c)=c_1$.

II.1.7. **Proposition** : If *d* generates (d,c), then there are $d_1$ and $c_1$ s.t. $d=\bar{g}(d,c) \cdot d_1$ and $c=\bar{g}(d,c)c_1$.

Proof : obvious by induction on $|d|$. $\square$

II.1.8. Notation : If *d* generates (d,c) and $\bar{g}(d,c) \in c' / d'$, then let $(d,c) \setminus d' = (c' \cdot d_1, c' c_1)$ where $d=\bar{g}(d,c) \cdot d_1$ and $c=\bar{g}(d,c)c_1$.

This notation makes sense by II.1.7.

II.1.9. **Definition** : For any pair (d,c), the canonical representative of (d,c), written (d,c)$_o$, is defined by :

$(\emptyset, c)_o = (\emptyset, c)$

$$
\overline{((c';d),c)_o} = (d,c)_o \setminus c' \text{ if } c' \text{ does not create } \underline{g((d,c)_o)}
$$

$$
((c';d),c)_o = ((c';d_o),c_o) \text{ if } (d_o,c_o) = (d,c)_o \text{ and } c' \text{ creates } \bar{g}((d,c)_o)
$$

This definition means that we extract from *d*
the only steps concerned by the creation of *c*. We
first prove that the canonical representative
definition is consistent with the equivalence of
reductions modulo permutations.

II.1.10. **Lemma** : $((c_1;(c_2/c_1)),c)_o = ((c_2;(c_1/c_2)),c)_o$ for any $c_1, c_2, c$.

Proof : by cases inspection. $\square$

II.1.11. Lemma : If $\overline{g((d_2,c)_o)} = c_1$, if $(d_1,c_1)_o = (d'_1,c'_1)$ and if $(d_2,c)_o = (c_1 \cdot d'_2, c_1 c')$, then $((d_1;d_2),c)_o = ((d'_1;(c'_1 \cdot d'_2)),c'_1 c'_1)$.

Proof : by induction on $|d_1| + |d_2|$. $\square$

II.1.12. **Proposition** : If $d_1 \sim d_2$, then $(d_1, c)_o = (d_2, c)_o$.

Proof : by induction on the definition of I.1.2 using the two above lemmas. $\square$

We now connect families of occurrences and canonical representatives in two steps. We first prove $(d,c)_o \sim (d,c)$. In fact we shall have a stronger property which is not necessary for our theorem. Then we show that $(d_1,c_1) \sim (d_2,c_2)$ implies $(d_1,c_1)_o = (d_2,c_2)_o$.
**II.1.13. Definition**: If $D: t^*t'$ and $c$ is in $t$, then $c$ and $D$ are disjoint iff $D=(C_1; C_2; \dots C_n)$ and $c, C_i$ are disjoint for any $i$ s.t. $1 \le i \le n$. Thus $c/D=\{c\}$.

**II.1.14. Lemma**: If $c, D$ are disjoint and $c_1 \in c/D_1$, then $c_1$ and $D/D_1$ are disjoint. Moreover $c_1/(D/D_1) = \{c_1\}$ and $c_1 \in c/(D_1/D)$.

*Proof*: by induction on $|D|$. The only problem is when $D=C$. By hypothesis, we have $c$ and $c'$ disjoint for any $c'$ in $C$. As residuals of disjoint occurrences are still disjoint, one has $c_1$ and $C/D_1$ disjoint too. Thus $c_1/(C/D_1) = \{c_1\}$, i.e. $c_1 \in c/(D_1;(C/D_1))$. But since $D_1;(C/D_1) \sim C;(D_1/C)$ and since residuals are consistent with respect to permutations, we have $c_1 \in c/(C;(D_1/C))$, i.e. $c_1 \in c/(D_1/C)$. $\square$

**II.1.15. Lemmas** :

1) If $((d_1;d_2),c_2)_o = (d_1,c_1)$, then $c_2 \in c_1/d_2$

2) If $c_2 \in c_1/d_2$, then $((d_1;d_2),c_2)_o = (d_1,c_1)_o$

3) If $(d_2,c_2)_o = (d_o,c_o)$, then

$$((d_1;d_2),c_2)_o = ((d_1;d_o),c_o)_o$$

*Proof*: by induction on $|d_1| + |d_2|$. $\square$

**II.1.16. Proposition**: For any $(D,c)$, there is $(D_1,c_1)$ s.t. $(D,c) \subseteq (D_1,c_1)$ and $(D_o,c_o) \subseteq (D_1,c_1)$.

*Proof*: Consider any $d$ in $D$. Then $(D,c)_o = (d,c)_o$ by II.1.12. Use an induction on $|d|$. If $d=\emptyset$, then $(d,c)_o = (d,c) \subseteq (d,c)$. Now suppose $d=c'$; $d'$. By induction there is $(D'_1,c'_1)$ s.t. $(d',c'_o) \subseteq (D'_1,c'_1)$ and $(d',c) \subseteq (D'_1,c'_1)$. Let $(d_o,c_o) = (d,c)_o$ and $(d'_o,c'_o) = (d',c)_o$. Let $c_2 = \overline{g}(d_o,c_o)$ and $c'_2 = \overline{g}(d'_o,c'_o)$.

We have two cases. First, if $c'$ creates $c'_2$, then $d_o=c'$; $d'_o$ and $c_o=c'_o$. Therefore, if $D_1=c'$; $D'_1$ and $c_1=c'_1$, we have $(d_o,c_o) \subseteq (D_1,c_1)$ and $(d,c) \subseteq (D_1,c_1)$. Secondly $c'$ does not create $c'_2$. Then $(d_o,c_o) = (d'_o,c'_o) \setminus c'$, i.e. $d'_o=c'_2 \cdot d''_o$, $c'_o=c'_2 \cdot c''_o$ and $d_o=c_2 \cdot d''_o$, $c_o=c_2 \cdot c''_o$ where $c'_2 \in c_2/c'$. Hence, as $c_2/c'$ is a set of disjoint occurrences, the derivations $c''_2 \cdot d''_o$ are disjoint for all $c''_2$ in $c_2/c'$. But these derivations form $d_o/c'$. Therefore $d'_o \subseteq d_o/c'$. Moreover $c'_o$ and $d_3=(d_o/c')/d'_o$ are disjoint. Hence $c'_o \in c'_o/d_3$. But by the permutation lemma, we have $c'_o \cdot d'_o; d_3 \sim d_o; (c'/d_o)$. By II.1.12, we get $((c';d'_o;d_3),c'_o)_o = ((d_o;(c'/d_o)),c'_o)_o$. By II.1.15, one has $((c';d'_o;d_3),c'_o)_o = (d_o,c_o)$ and $c'_o \in c_o/(c'/d_o)$. Let $d'_1 \in D'_1/d'_o$. Since $(d'_o,c'_o) \subseteq (D'_1,c'_1)$, we have $c'_1 \in c'_o/d'_1$ by II.1.14 and therefore $c'_1 \in c'_o/(d'_1/d_3)$ by II.1.14 since $c'_o$ and $d_3$ are disjoint. Moreover by

II.1.14 we get $c'_1 \in c'_o/(d_3/d'_1)$. In short if $c_1=c'_1$ and $D_1=c'$; $D'_1/(d_3/d'_1)$, then $(d,c) \subseteq (D_1,c_1)$ and $(d_o,c_o) \subseteq (D_1,c_1)$. $\square$

**II.1.17. Theorem**: $(D_1,c_1) \sim (D_2,c_2)$ iff $(D_1,c_1)_o = (D_2,c_2)_o$.

*Proof*: The previous proposition implies $(D,c)_o \sim (D,c)$. Hence if $(D_1,c_1)_o = (D_2,c_2)_o$, then $(D_1,c_1) \sim (D_2,c_2)$. Conversely, suppose $(D_1,c_1) \subseteq (D_2,c_2)$ By definition, there is $D$ s.t. $(D_1;D) \sim D_2$ and $c_2 \in c_1/D$. Hence $(D_1,c_1)_o = ((D_1;D),c_2)_o$ by lemma II.1.15 and $((D_1;D),c_2)_o = (D_2,c_2)_o$ by proposition II.1.12. Now when $(D_1,c_1) \sim (D_2,c_2)$, we have by transitivity $(D_1,c_1)_o = (D_2,c_2)_o$. $\square$

Therefore two occurrences belongs to a same family iff they are generated in a same way.

**II.1.18. Proposition**: Let $(D,c)_o = (d_o,c_o)$. Then $d_o \subseteq D$ iff $(d_o,c_o) \subseteq (D,c)$.

*Proof*: corollary of II.1.4 (1st clause) and II.1.16, II.1.4 (4th clause). $\square$

We now show the connection between families and labels.

**II.1.19. Definition**: Given any term $t$, the labelling $\mu$ is elementary if $\mu:C(\phi,t) \to E$ i.e. the range of $\mu$ is the set of letters $E$.

**II.1.20. Lemma**: For any label $\alpha$, if $\mu$ and $\nu$ are injective elementary labellings, there is at most one $(d,c)$ s.t. $d:(t,\mu)\frac{\star}{\alpha}(t',\mu')$, $d$ generates $(d,c)$ and $\mu'(c)=\alpha$.

*Proof*: by induction on the length of $\alpha$. $\square$

**II.1.21. Theorem**: Let $D_i=(t,\mu)\frac{\star}{i}(t_i,\mu_i)$ for $i=1,2$. Then $(D_1,c_1) \sim (D_2,c_2)$ iff $\mu_1(c_1)=\mu_2(c_2)$ when $\mu,\nu$ are injective elementary iff $\mu_1(c_1)=\mu_2(c_2)$ for all $\mu$.

*Proof*: First $(D_1,c_1) \sim (D_2,c_2)$ implies $\mu_1(c_1)=\mu_2(c_2)$ by the definitions. The converse follows from II.1.20 and II.1.17. $\square$

**II.2. Complete derivations** :

**II.2.1. Definition**: The set $C$ of occurrences is f-complete with respect to $D$, in short $(D,C)$ is f-complete, iff $C=\{c'|(D,c') \sim (D,c)\}$ when $c \in C$.

**II.2.2. Definition**: $(D,C)$ is $d$-complete if $C$ is maximal s.t. there are $D'$, $D''$, $c$ with $D \sim D'$; $D''$ and $C=c/D''$.

**II.2.3. Definition**: $(D,C)$ is $\ell$-complete if $C=\{c'|\mu'(c')=\mu'(c)\}$ when $c \in C$ and $D:(t,\mu)\frac{\star}{\ell}(t',\mu')$.

**II.2.4. Definition**: The derivation $D$ is $f$-complete (respectively $d$ and $\ell$-complete) if $D=\emptyset$ or $D=D_1;C$ when $D_1$ and $(D_1,C)$ are $f$-complete (resp. $d$ and $\ell$-complete).
II.2.5 : Lemma : If D is f-complete, then
$(D,c) \stackrel{\le}{\subset} (D,c)$ for any c.

Proof : by II.1.18, it is sufficient to prove
$d_o \stackrel{\le}{\subset} D$ if $(D,c)_o = (d_o, c_o)$. We use an induction on $|D|$.
If $D=\emptyset$, then $d_o=\emptyset \le D$. Otherwise $D=D_1;C_1$ with $D_1$ and
$(D_1,C_1)$ f-complete. If $c \in C_1/C_1$, then
$(D,c)_o = (D_1,c_1)_o$ and by induction $d_o \stackrel{\le}{\subset} D_1 \le D$. Else,
there is only one $c_1$ in $C_1$ which creates c. Let
$(d'_o, c'_o) = (D_1, c_1)_o$. One has $d_o = d'_o; c'_o$ by II.1.11,15.
But, as $(D_1, C_1)$ is f-complete, we get
$(D_1, c_1)_o = (D_1, c_2)_o$ for all $c_2$ in $C_1$ by II.1.17. By
induction $d'_o \stackrel{\le}{\subset} D_1$. Hence $C_1 = c'_o / (D_1/d'_o)$ by II.1.18
and II.1.4. So $d_o \le D$. $\square$

II.2.6 : Proposition : D is f-complete iff D is d-complete iff D is l-complete when the initial labellings are injective and elementary.

Proof : obvious with the above lemma and theorem II.1.21. $\square$

II.2.7. Notation : We write $t^* \supseteq t'$ for an f-complete derivation from t to t'. We call $FD(t)$ the set of f-complete derivation starting at t.

II.2.8 : Proposition : The set $[FD(t)] = FD(t)/$
with the $\le$ ordering is a sublattice of $[D(t)]$
with the same 1.u.b. operation.

Proof : Let us remark that if $(d_o, c_o) = (D_2, c_2)_o$
and $d_o \le D_1 \le D_2$, then there is $c_1$ s.t.
$(d_o, c_o) \le (D_1, c_1) \le (D_2, c_2)$ by II.1.4 and II.1.18.
Suppose now that $D_1, D_2$ are f-complete, then it
is obvious by induction on $|D_2|$ that $D_1; (D_2/D_1)$
is f-complete for any $D_2$ with use of II.2.5. $\square$

II.2.9. Definition : For any $d$ in $\mathcal{P}(t)$, we
consider the f-complete derivation $\overline{d}$ associated
to $d$ defined by :

$\overline{d} = \emptyset$

$\overline{d}; c=\overline{d}; c \text{ where } C=\{c' \mid (d,c) \sim (\overline{d}, c')\}$

This definition does not work nicely with
permutations, but we will use it for the dis-
cussion about the cost of derivations. It is
straightforward to check that $\overline{d}$ is f-complete,
that $d \le \overline{d}$ and that $D = \overline{d}$ for any $d \in D$ when $D$
is f-complete.

III. LEAST AND OPTIMAL COMPUTATIONS

III.1. Semantics of recursive programs.

We define the operational semantics in comple-
te F-algebras as in [14,17]. The equivalence of this
semantics with denotational or algebraic semantics
is shown in [14].

III.1.1. Definitions : ordered sets : let (D, c, 1) be an ordered set of least element 1. When they exists, least upper bounds (1, u, b.) and greatest lower bounds (g, 1, b.) are denoted αuα' and αna'. A set Δ ⊂ D is directed if ∀α, α' ∈ Δ, ∃α" ∈ Δ s.t. αca" and α'ca", and is an ideal if it is directed and satisfies $\forall \alpha \in \Delta, \forall \alpha' \in D, \alpha'ca$ implies α' ∈ Δ. An ordered set D is complete if every directed set Δ ⊂ D has a 1, u, b. uΔ. A mapping h : D → D' is monotonic if αca' implies h(α) ⊑ h(α'), continuous if D and D' are complete and h(uΔ) = uh(Δ) for every directed set Δ ⊂ D. Given an ordered set D, a completion $D^∞$ of D is a complete set containing D, up to morphism, and such that for any complete D', every monotonic mapping h : D → D' extends in a unique way into a continuous mapping $h^∞ : D^∞ → D'$. All completions of D are equal up to unique isomorphism. As an example, the completion by ideals is the set $D^∞$ of nonempty ideals of D, ordered by inclusion. It contains α ∈ D represented by I(α) = {α' ∈ D | α'caα}, and has {1} for least element. Every mapping h : D → D' extends by $h^∞(J) = \{h(α), α ∈ J\}$. The completion of (D, ≤) is denoted ($D^∞$, ≤).

III.1.2. Definitions : ordered and complete F-alge-
bras [14].

An ordered (complete) F-algebra is a F-alge-
bra I where $D_I$ is ordered, has least element $\perp$ and
the mappings $f^I$ are monotonic (continuous). A mor-
phism of ordered (complete) F-algebras is a mor-
phism of F-algebras which is also monotonic (conti-
nuous). Let $\Omega$ be a new constant symbol, let
$M_{\Omega}(F, V) = M(Fu\Omega, V)$, also written $M_{\Omega}$. Let $\llcorner$ be the
the least ordering on $M_{\Omega}$ s.t. $\Omega \llcorner a$ for all $a$, and
$a \llcorner \vec{a}'$ implies $f(a) \llcorner f(\vec{a}')$ for all $f, a, \vec{a}'$. For exam-
ple, $f(\Omega, g(\Omega, \Omega)) \llcorner f(x, g(\Omega, y))$ holds. Then $M_{\Omega}$ is the
free ordered F-algebra generated by $V$, and its com-
pletion by ideals $\llcorner M_{\Omega}^\infty, \llcorner \Omega, f_i^\infty \rrcorner$ is the free complete
F-algebra generated by $V$.

For any ordered (complete) F-algebra I, every
data mapping $v: V \to D_I$ extends in a unique way into a
morphism $(I, v): M_{\Omega} \to I$. Intuitively, $\Omega$ is the syntac-
tic undefined, and $M_{\Omega}$ contains infinite terms re-
presented by all their finite approximations. The
morphism $(I, v)$ gives the value of any term under
the interpretation I of the function symbols and
the data mapping $v$.

III.1.3. Definitions : Operational semantics : to
any $t \in M(Fu\Phi, V)$, we associate its syntactic value
$S(t) \in M_{\Omega}$ :

$$
(i) S(x_i) = x_i
$$

$$
(ii) S(f(\vec{t})) = f(S(\vec{t})) \text{ for all } f \in F
$$

$$
(iii) S(\phi(\vec{t})) = \Omega \quad \text{for all } \phi \in \Phi
$$

Call program a triple $\langle \Sigma, I, v \rangle$ where $\Sigma$ is a
scheme on $\mathbb{F}, \Phi, V$, the interpretation I is a complete
F-algebra, and $v$ is a data mapping. Then $t \stackrel{*}{\to} t'$ implies $S(t) < S(t')$ by induction on $|t|$, and the set $\{S(t')|t \stackrel{*}{\to} t'\}$ is directed in $M_{\Omega}^{\infty}$; its l.u.b. in $M_{\Omega}^{\infty}$ is called $\Sigma(t)$, the infinite term determined by the program. The value $P(t)$ computed by $P$ on $t$ is

$P(t)=(I,v)\tau(t)=u((I,v)(S(t'))|t \stackrel{*}{\to} t').$ Remark that
$\tau(t)=P_s(t)$ where $\Gamma_s=<\Sigma, M_{\Omega}^{\infty}(F,v), v_0>$, with $v_0:x_i \to x_i$.
For $d:t \stackrel{*}{\to} t'$, we denote $S([d])=S(d)=S(t')$ and
$(I,v)[d]=[I,v]d=(I,v)\tau'$.

### III.2. Infinite derivations. Computations.

**III.2.1. Definitions** : Let $D^{\infty}(t)$ be the set of finite and infinite derivations from $t$. For $\delta \in D^{\infty}(t)$, let $\delta_k$ denote the $k$ first steps of $\delta$, and let $S(\delta)=u_k\{S(\delta_k)\}$ and $(I,v)\delta=u_k(I,v)\delta_k$. Define $\delta \leq_k \delta'$ to hold iff $\forall k \geq 0, \exists k' \geq 0$ s.t. $\delta_k \leq \delta'_{k'}$, and let $\sim_{\infty}$ be the associated equivalence. Let $[D^{\infty}(t)] = \mathbb{N}^{\infty}(t)/\sim_{\infty}$, let $[\delta]$ be the class of $\delta$. Clearly, $\delta \leq_{\infty} \delta'$ implies $S(\delta) < S(\delta')$, and the notations $S([\delta])$ and $(I,v)[\delta]$ make sense.

**III.2.2. Proposition** : The structure $\langle D^{\infty}(t), \leq_{\infty} \rangle$ is a completion of $\langle \mathcal{D}(t), \leq \rangle$, and is a complete lattice.

*Proof:* Notice that $[D^{\infty}(t)]$ contains $[\mathcal{D}(t)]$ and that the relation $\leq_{\infty}$ restricts to $\le$ on $[\mathcal{D}(t)]$. Moreover, every $[\delta]$ is the limit of the directed set $\{[\delta_k]|k \ge 0\} \subset [\mathcal{D}(t)]$. This completes the proof of the first part. Using the completion by ideals, it is easy to see that a completion of an upper-semi-lattice is a complete lattice. $\sqcap$

We can therefore abbreviate $\leq_{\infty}$ and $\sim_{\infty}$ by $\le$ and $\sim$.

**III.2.3. Definition** : Let the full derivations $K_i(t)$ be defined by $K_0(t)=\emptyset; t^* \to t=\emptyset$ and $K_{i+1}(t): t \stackrel{*}{\to} t_{i+1}$ s.t. $K_{i+1}(t) = K_i(t); C(\phi, t_i)$. Let $K(t)$ be the infinite full derivation.

**III.2.4. Proposition** : $[K(t)] = \bigcup [D^{\infty}(t)]$
*proof* : by induction on $|d|$, show that $[d] \le [K_d](t)$.
$\sqcap$

**III.2.5. Definition** : Let $P$ be a program and $t$ an initial term. A computation of $P$ on $t$ is a derivation $\delta \in D^{\infty}(t)$. It is a computation of $\alpha \in D_I$ iff $(I,v)\delta \supseteq \alpha$. A computation is correct if it computes $P(t)$ syntactically, and correct if it computes $\tau(t)$ in $M_{\Omega}^{\infty}$: $S(\delta)=\Sigma(t)$. A computation $\delta \in D^{\infty}(t)$ is least for $\alpha \in D_T$ if $(I,v)\delta \supseteq \alpha$ and $(I,v)\delta' \supseteq \alpha$ implies $\delta' \supseteq \delta$ for every $\delta' \in \mathbb{N}^{\infty}(t)$.

Every syntactically correct derivation is correct. The full derivation is correct by III.2.4.

### III.3 Least Computations in $M_{\Omega}^{\infty}$.

We restrict our attention to the symbolic interpretation $M_{\Omega}^{\infty}$, and construct a least computation of every $A \prec \tau(t)$.

**III.3.1. Definition** : A derivation $d \in D(t)$ is outermost iff every occurrence derived in $d$ is outermost in the corresponding term.

**III.3.2. Lemma** : If $\Sigma(t) \not\equiv \Omega$, then there exists a least $n \ge 0$ such that $S(\epsilon^n) \not\equiv \Omega$. Every standard or outermost $d \in D(t)$ such that $S(d) \not\equiv \Omega$ begins with $\epsilon^n$. Moreover $\Sigma(t) \not\equiv \Omega$ is decidable.

*Proof* : If $\Sigma(t) \not\equiv \Omega$, there exists $d \in D(t)$ standard such that $S(d) \not\equiv \Omega$. If $t=f(\vec{t})$, then $n=0$. If $t=\phi(\vec{t})$, every standard or outermost derivation must begin with $\epsilon$, and the result follows by induction on $|d|$. If $N$ denotes the cardinality of $\phi$, then $\Sigma(t) \not\equiv \Omega$ is equivalent to $S(\epsilon^N) \not\equiv \Omega$, which is decidable (see [18]). $\sqcap$

**III.3.3. Definition** : Let $t \in M$ and $a \in M_{\Omega}^{\infty}$ satisfy $a \prec \Sigma(t)$. There exists a derivation $d_a(t)$ which is least for $a$, standard, and outermost.

*Proof* : by induction on $||a||$. For $a=\Omega$, then $d_a(t)=\emptyset$. For $a=f(\vec{a})$, by lemma III.3.2, every standard $d$ such that $S(d) \not\equiv \Omega$ is of the form $\epsilon^n;d'$ where $\epsilon^n:t \stackrel{*}{\to} f(\vec{t})$ and $d'=f(d_1', d_2', \dots, d_k')$ for some $d_1' \in D(t_i)$. Then by induction, $d_a(t)=\epsilon^n; f(d_a(\vec{t}))$ where $d_a(\vec{t}) = d_{a_1}(t_1); \dots; d_{a_k}(t_k)$ satisfies the conditions. $\sqcap$

We now extend this result to infinite derivations. Notice that $\delta \ge d$ holds iff $\exists \delta'$ s.t. $\delta \sim d; \delta'$.

**III.3.4. Notations** : Let $t \in M$ and $A \in M_{\Omega}^{\infty}$ such that $A \prec \Sigma(t)$. Let $S=\{a_n|n \ge 1\} \subset M_{\Omega}^{\infty}$ be an increasing chain of limit $A$. Let $\delta_S(t)=d_{a_1}(t_0); d_{a_2}(t_1); \dots; d_{a_k}(t_{k-1})$; ... where $t_0=t$ and $d_{a_i}(t_{i-1}): t_{i-1} \stackrel{*}{\to} t_i$ is constructed as in III.3.3. Let $\delta_S^k(t)=d_{a_1}^k(t_0); d_{a_2}^k(t_1); \dots; d_{a_k}^k(t_{k-1})$.

**III.3.5. Theorem** : If $S$ is a chain of limit $A$, then $\delta_S(t)$ is least for $A$ and also for any $A$'s t.

$A \prec A' \prec S(\delta_S(t))$.

*Proof* : Let $\delta$ such that $S(\delta) > A'$, and assume by induction $\delta \ge \delta_S^k(t)$. Then $\delta \sim \delta_S^k(t); \delta'$ for some $\delta'$. Since $S(\delta') > A'$, there exists some $d' \le \delta'$ such that $S(d') > a_{k+1}$; Then $\delta' \ge d' \ge d$ ($t_k$) implies $\delta \ge \delta_S^k(t)$; $d$ ($t_k$) = $\delta_S^k(t)$. $\sqcap$

Notice that a least syntactically correct derivation can be constructed from the chain $S(K_i(t))$.

### III.4 Optimal computations in $M_{\Omega}^{\infty}$.

From now on, we denote by $\overline{d} \in D(t)$ a $f$-complete derivation, and by $\delta \in F^{\infty}(t)$ a finite or infinite $f$-complete derivation (Definitions II.2.4 and III.2.9 trivially extends to infinite derivations).

The cost of a derivation $d \in D(t)$ is its length $|d|$. But, as noticed before, a simple sharing technique applied to $f$-complete derivations allows to derive all occurrences in a complete step at cost 1: let $\Sigma: \phi(x) = f(x, \phi(x))$

<figure><img src="image_7.png" /></figure>
The cost of a $f$-complete derivation $\bar{d}$ is then the number $|\bar{d}|$ of nonempty set derived. This notion of cost does not extend to infinite derivation; we shall use a finer way of comparing derivations.

**III.4.1. Definition** : Given $t \in \mathbb{M}$ and $d \in \mathcal{D}(t)$, the family of $F(d,c)$ is the equivalence class of $(d',c')$ such that $d' \in \mathcal{D}(t)$ and $(d,c) \sim (d',c')$. For $d=c_1; c_2; \cdots; c_k$, let $d_i=c_1; c_2; \cdots; c_i$ and define $F(d) = \{F(d_i, c_{i+1}) | 0 \le i < k\}$. Let $F(\delta) = u_i F(\delta_i)$, and let $F(\bar{d})$ and $F(\bar{\delta})$ be similarly defined.

**III.4.2. Lemma** : Let $\bar{d}=d_1; c_1; d_2; c_2; d_3 \in \mathcal{FD}(t)$. Then $F(d_1, c_1) \neq F(d_2, c_2)$.

*Proof* : Obvious from II.2.5 and II.1.18. □

Therefore $|\bar{d}|$ is the cardinality of $F(\bar{d})$, and $F(\bar{d}) \subset F(\bar{d}')$ implies $|\bar{d}| \le |\bar{d}'|$. We can compare infinite derivation by $F(\bar{\delta}) \subset F(\bar{\delta}')$ for cost $(\bar{\delta}) \le \text{cost}(\bar{\delta}')$.

**III.4.3. Definition** : Let $t \in \mathbb{M}$ and $A \in \mathbb{M}_{\Omega}^{\infty}$ such that $A \subset \Sigma(t)$. Then $\bar{\delta} \in \mathcal{FD}^{\infty}(t)$ is optimal for $A$ if it computes $A$ and satisfies $F(\bar{\delta}) \subset F(\bar{\delta}')$ for any $\bar{\delta}' \in \mathcal{FD}^{\infty}(t)$ which computes $A$.

We now transform minimality results into optimality results.

**III.4.4. Definitions** : A derivation $\bar{\delta} \in \mathcal{FD}^{\infty}(t)$ is outermost if each set derived in $\bar{\delta}$ contains an outermost occurrence in the corresponding term.

**III.4.5. Lemma** : Let $c$ be outermost, assume $\bar{d}' \supsetneq D$; $c$. Then $F(D, c) \in F(\bar{d}')$

*Proof* : We have $c/(\bar{d}'/D) = \emptyset$. Then $\bar{d}'$ is of the form $D'$; $c'; D'$$ with $c \in D/(D/D')$, otherwise $c/(\bar{d}'/D) = \{c\}$. Therefore $F(D, c) = F(D', c) \in F(\bar{d}')$. □

**III.4.6. Lemma** : Let $d \in \mathcal{D}(t)$, $\bar{d}' \in \mathcal{FD}(t)$ with $d$ outermost. Then $\bar{d}' > d$ implies $F(\bar{d}') > F(d)$.

*Proof* : Induction on $|d|$ and lemma III.4.5. □

**III.4.7. Lemma** : Let $d \in \mathcal{D}(t)$ outermost. Then $\bar{d}$ is outermost and $F(\bar{d}) = F(d)$.

*Proof* : Induction on $|d|$. Let $d=d'$; $c$ and $\bar{d}=\bar{d'}$; $c$. If $c/(\bar{d}'/d')=\emptyset$, then $c=\emptyset$ by III.4.5 and III.4.2. Otherwise $c/(\bar{d}'/d')=\{c\}$ and $c \in D$ is outermost. So $\bar{d}$ is outermost. Now $F(\bar{d}) \subset F(d)$ and $F(d) \subset F(\bar{d})$ follow by II.2.9 and III.4.6. □

**III.4.8. Proposition** : Let $\bar{d}, \bar{d}' \in \mathcal{FD}(t)$ with $\bar{d}$ outermost. Then $\bar{d} \le \bar{d}'$ holds iff $F(\bar{d}) \subset F(\bar{d}')$.

*Proof* : Induction on $|\bar{d}|$. Let $\bar{d}=\bar{d}_1; c$ with $c \in D$ outermost. If $\bar{d} \le \bar{d}'$, then $F(\bar{d}_1, c) \in F(\bar{d}')$ by III.4.5 and $F(\bar{d}) \subset F(\bar{d}')$ holds by induction. If $F(d) \subset F(\bar{d})$, we get $c/(\bar{d}'/\bar{d})=\emptyset$ by III.4.5 and III.4.2, and $\bar{d} \le \bar{d}'$ by induction and I.4.2. □

**III.4.9. Proposition** : Let $\bar{\delta} \in \mathcal{D}^{\infty}(t)$ and $\bar{\delta}' \in \mathcal{FD}^{\infty}(t)$ with $\bar{\delta}$ outermost. Then $\bar{\delta} \le \bar{\delta}'$ implies $\bar{\delta} \le \bar{\delta}'$ and $F(\bar{\delta}) \subset F(\bar{\delta}')$.

*Proof* : By definition of $\le$, III.4.6, III.4.7 and III.4.8. □

**III.4.10. Theorem** : Let $t \in \mathbb{M}$ and $A \in \mathbb{M}_{\Omega}^{\infty}$ such that $A \subset \Sigma(t)$. Let $S=\{a_n | n \ge 1\}$ be a chain of limit $A$, let $A' \in \mathbb{M}_{\Omega}^{\infty}$ be such that $A \subset A' \subset S(\bar{\delta}_S(t))$. Then $\bar{\delta}_S(t)$ is least for $A$ and $A'$ in $\mathcal{FD}^{\infty}$, and is optimal for $A$ and $A'$.

*Proof* : If $S(\bar{\delta}) \supset A'$, then $S(\bar{\delta}) \supset A$ and $\bar{\delta} \ge \delta_S(t)$ by III.3.5. But $\delta_S(t)$ is outermost. Hence $\bar{\delta} \ge \delta_S(t)$ and $F(\bar{\delta}) > F(\bar{\delta}_S(t))$ follow by III.4.9. □

As before, notice that an optimal syntactical-ly correct derivation is constructible from $S(K_i(t))$.

**III.5. Least and optimal computations in interpretations.**

Our results in $\mathbb{M}_{\Omega}^{\infty}$ extend to interpretations, provided the following condition is satisfied.

**III.5.1. Definition** : An interpretation $I$ is projective if for every $v:V \to D_I$ there exists a mapping $c_{I,v}:D_I \times \mathbb{M}_{\Omega}^{\infty} \to \mathbb{M}_{\Omega}^{\infty}$ such that $c_{I,v}(\alpha, T)=g.1.b.\{T' \subset T | (I, v)T' \supset \alpha\}$ for $\alpha \in (I, v)T$. Therefore computing $\alpha$ exactly means computing $c_{I,v}(\alpha, \Sigma(t))$ in $\mathbb{M}_{\Omega}^{\infty}$. Define optimal for $\alpha$ as in III.4.3.

**III.5.2. Theorem** : Let $I$ projective and $v:V \to D_I$. Let $\alpha \in P(t)$, let $S$ be any chain in $\mathbb{M}_{\Omega}^{\infty}$ of limit $c_{I,v}(\alpha, \Sigma(t))$, let $\alpha', \alpha''$ s.t. $\alpha \subset \alpha'$ $c_{I,v}(\alpha, \Sigma(t))$ and $\alpha \subset \alpha'' c_{I,v}(\alpha, \Sigma(t))$. Then $\delta_S(t)$ is least for $\alpha$ and $\alpha'$ in $\mathcal{D}^{\infty}(t)$, and $\bar{\delta}_S(t)$ is least and optimal for $\alpha$ and $\alpha''$ in $\mathcal{FD}^{\infty}(t)$.

*Proof* : From III.3.5 and III.4.10, using $c_{I,v}(\alpha', \Sigma(t)) \subset S(\bar{\delta}_S(t))$ and $c_{I,v}(\alpha'', \Sigma(t)) \subset S(\bar{\delta}_S(t))$ which trivially follow from the definition of $c_{I,v}$.□

Notice that when $(I, v)$ is algebraic (see [5]), the projectivity condition can be restricted to hold only on finite terms.

**Example** : Non-projective interpretations typically contain "parallel functions" as the "parallel or" : $I \text{ or } tt=tt \text{ or } I=tt$ and $c_{I,v}(tt, tt \text{ or } tt)$ does not exist. We give without proofs the following examples of projective interpretations.

- Stable interpretations [1, 2] :

Write $\vec{\alpha} \uparrow \vec{\alpha}'$ if $\exists \vec{\alpha}''$ s.t. $\vec{\alpha} \subset \vec{\alpha}''$ and $\vec{\alpha}' \uparrow \vec{\alpha}''$. Assuming continuous g. l. h. exist in $D_J$, then $I$ is stable if every $f^I$ satisfies

$$ \forall \vec{\alpha}, \vec{\alpha}', \vec{\alpha} \uparrow \vec{\alpha}' \Rightarrow f^I(\vec{\alpha} \uparrow \vec{\alpha}') = f^I(\vec{\alpha}) \lor f^I(\vec{\alpha}') $$

Notice that $\mathbb{M}_{\Omega}^{\infty}$ is stable.

- Sequential interpretations : several non-equivalent definitions exist :

- Vuillemin [17] : $\forall f^I, \forall \vec{\alpha}, \exists i \text{ s.t. } \vec{\alpha}' \supset \vec{\alpha}$ and $\alpha_i' = \alpha_i$ implies $f(\vec{\alpha}') = f(\vec{\alpha})$.

No algebraicity condition is needed on $D_I$. Here $\mathbb{M}_{\Omega}^{\infty}$ is not sequential.
- Kahn-Plotkin [8] : These interpretations are stable, and then projective. Here $M_{\Omega}^{\infty}$ is sequential.

### III.6. Progressively optimal computations and computation rules.

The theorem III.5.2. does not suggest a practical way of performing optimal computations : we do not want to first compute in trees and then adapt this computation in pointer structures.

Moreover we are not only interested in the result of an infinite computation, but also in the intermediate results it produces (see [17]). Call information step of $\delta$ any $i \ge 0$ such that $(I, v)\delta_i \stackrel{\delta}{\rightleftharpoons} (I, v)\delta_{i-1}$. (With a $\llcorner$ iff a $\llcorner$ b and a $\not\llcorner$ b).

**III.6.1. Definition:** A computation $\bar{\delta}$ is progressively optimal if $\bar{\delta}_i$ is optimal for $(I, v)\delta_i$ at each information step $i$.

We give without proof a result in [3]. Define the covering relation $\llcorner$ in $M_{\Omega}^{\infty}$ by a $\llcorner$ a' if $a=a'$ implies $a''=a'$. Then a' is obtained from a by replacing an $\Omega$ by some $f(\bar{\delta})$. Construct now $t_i$ and $\bar{D}$ in the following way, by a slight extension of II.2.9 :

(i) $t_o=t$, $\bar{D}_o=\emptyset$

(ii) $\bar{D}_{i+1} = \bar{D}_i \cup \{d_i : t_i \stackrel{*}{\to} t_{i+1}\}$ for some $a_i$ such that $c_{I_i} \{(I, v)t_i, t_{i+1}\} \subset a_i \subset c_{I_{i+1}}(P(t), (t))$ if such an $a_i$ exists, $\bar{D}_{i+1} = \bar{D}_i$ otherwise.

**III.6.2. Theorem:** The computation $\bar{D}$ is progressively optimal.

The covering $a_i$ is used to designate some occurrence of $\phi_i$ in $t_i$ to be substituted. The construction of $\bar{D}$ can be done directly in pointer structures.

Let $c(T)=c_{I_i, v}((I, v)T, T)$. It is possible to "construct" a progressively optimal correct computation (which is also optimal) in the following way: starting from $t_i$, perform full derivations to reach $t'$ such that $(t_i^v)t'^v(I, v)t_i$, then choose a suitable $a_i$ such that $c(t_i) \subset a_i \subset c(t')$, and apply (ii) to reach $t_{i+1}$. Notice that optimal computations may be finite, which is undecidable in general (but not in $M_{\Omega}^{\infty}$). In this case, our "rule" loops performing full substitutions from some $t_j$.

Notice also that this "rule" is of no practical interest : we first perform full derivations, and then a posteriori select the useful steps. What we really need is a way of selecting $a_i \supset c(t_i)$ only from $c(t_i)$. This is the purpose of the sequentiality definitions : Vuillemin's $\bar{a}$ definition implies $\forall a \in M_{\Omega}^{\infty}, \exists a' \supset a$ st. $\forall a \in M_{\Omega}^{\infty}, \exists a', (I, v)A_p(I, v)a \Rightarrow \exists a'$ where $a'$ can be constructed only from $a$.

In this case, our "rule" reduces to Vuillemin's "delay rule". Notice that when optimal computations, are finite, the delay rule loops producing useless steps instead of looping in searching for the next

step. In fact, in such sequential interpretations, the computed values form a chain, and a stronger optimality result holds : if $\delta$ is progressively optimal, then for any $\bar{d}$ there exists $i \ge 0$ such that $(I, v)\delta_i \stackrel{\bar{d}}{\rightleftharpoons} (I, v)\bar{d}$ and $F(\delta_i) \subset F(\bar{d})$. (see [17]). Such an optimality can not be expected if non comparable values can be computed, as it is the case in $M_{\Omega}^{\infty}$, in stable interpretations or in Kahn-Plotkin sequential interpretations.

## CONCLUSION

Under some "fair" conditions, optimal computations of recursive programs have been studied at a purely syntactical level. Then by considering minimal derivations, we left the Herbrand universe and dealt with the following problem : how to relate the $\le$ ordering on derivations to the cost of derivations ? This has been done here with use of outermost derivations which derive only "crucial" occurrences. Intuitively, any "true" permutations of an outermost reduction could have worked, i.e. permutations which only use the permutation lemma when $c_1/c_2 \ne \emptyset$ and $c_2/c_1 \ne \emptyset$. These derivations are very similar to the safe computations in [16] when we consider a covering approximation step, although the safe derivations are defined in some more semantical way. The security conditions in [7] are directly related to our $\le$ ordering since secure derivations are dominating the "safe parallel outermost" derivation. Progressively optimal derivations seem interesting when values of derivations can be infinite objects as in [8] where cutoutines are evaluated with a delay rule mechanism. Finally, nearly all propositions and theorems in this paper are also true in the $\lambda$-calculus. This indicates that an axiomatized approach could be taken (see [15]) although it seems to the authors that such an approach could not bring simplifications.

## REFERENCES

[1] G. Berry, *Bottom-up Computations of Recursive Programs*. R.A.I.R.O. Informatique Théorique, Vol 10, n°3, Mars 1976, pp.47-82.

[2] G. Berry and B. Courcelle, *Program Equivalence and Canonical Forms in Stable Discrete Interpretations*. Automata Languages and Programming, 3rd Coll, 1976, Edinburgh University Press, U.K. p.168-188.

[3] G. Berry, *Calculs Minimaux et Optimaux des Programmes Récursifs*, to appear.

[4] A.Church, *The calculi of Lambda Conversions*, Annals of Math. Studies, n°6, Princeton, 1941

[5] B. Courcelle and M. Nivat, *Algebraic Families of Interpretations*, 17th FOCS, Houston, 1976.
[6] H.B.Curry and R.Feys, *Combinatory logic*, Vol 1, North-Holland, 1958

[7] P.J.Downey and P.Sethi, *Correct Computation Rules for Recursive Languages*, 16th Annual Symposium on Foundations of Computer Science, Berkeley, Oct. 1975.

[8] G.Kahn and G.Plotkin, *Concrete Data Types*, To appear, University of Edinburgh, A.I.Dept.

[8b] G.Kahn and D.McQueen, *Coroutines and Networks of Parallel Processes*, To appear as IRIA-LABOPITA report.

[9] J-J.Lévy, *An algebraic interpretation of the λβK-calculus and a labelled λ-calculus*, Proc. of the Symposium on λ-calculus and Computer Science Theory, Roma, Italy, March 1975.

[10] J-J.Lévy, *Réductions sûres et optimales dans le λ-calcul*, To appear.

[11] R.Milner, *Fully Abstract Models of Typed λ-calcul*, To appear in Theoretical Computer Science.

[12] G.Mitschke, *The Standardisation Theorem for λ-calculus*, Swansea 1975.

[13] C.Montanero, G.Pacini and F.Turini, *Graph Representation and Computation Rules for Typeless Recursive Program Schemes*, Proc. 2nd Colloq. Automata, Languages and Programming, Saarbrücken (1974), Lect. Notes in Comp. Sc. 14.

[14] M.Nivat, *On the Interpretation of Recursive Program Schemes*, Symposia Mathematica, Vol. XV, Instituto Nazionale di Alta Matematica, Italy, 1975, P. 255-281.

[15] B.Rosen, *Tree Manipulation Systems and Church-Rosser Theorems*, JACM Vol 20 n°1, 1973.

[16] D.Scott, *Cutline of a Mathematical Theory of Computation*, P.R.G.mono.N°2, Oxford 1970.

[17] J.Vuillemin, *Proof Techniques for Recursive Programs*, Ph.D. Comp.Sc.Dept, Stanford (1973)

[18] J.Vuillemin, *Syntaxe, Sémantique et Axiomatique d'un langage de Programmation Simple*, Thèse d'état, Univ. Paris VI, 1974