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

HAL
open science

# Correct and optimal implementations of recursion in a simple programming language

Jean Vuillemin

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

## To cite this version:

Jean Vuillemin. Correct and optimal implementations of recursion in a simple programming language.

[Research Report] IRIA-RR-024, IRIA. 1973, pp.24. hal-04715976

HAL Id: hal-04715976

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

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

Distributed under a Creative Commons Attribution 4.0 International License
RIA
laboria

laboratoire de recherche
en informatique
et automatique

Correct and
optimal implementations
of recursion in a simple
programming language

jean Vuillemin

Institut de Recherche
d'Informatique
et d'Automatique

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

Rapport de Recherche n° 24
juillet 1973
# CORRECT AND OPTIMAL IMPLEMENTATIONS OF RECURSION IN A SIMPLE PROGRAMMING LANGUAGE *

J. Vuillemin

## ABSTRACT

The object of this paper is to study the mechanism of recursion in a simple, LISP-like programming language, where the only mean of iteration is through recursion. The theory of computation developed in Scott [6] provides the framework of our study. We show how the implementations of recursion which deserve to be called «correct» can be characterized semantically, and demonstrate a general criterion for the correctness of an implementation. We then describe an implementation of recursion which is both correct and optimal in a general class of sequential languages, and therefore constitutes an attractive alternative to both «call-by-name» and «call-by-value».

## RÉSUMÉ

Le but de ce papier est l'étude systématique du mécanisme de récursion dans un langage de programmation simple.

Les résultats principaux sont une caractérisation des implantations qui sont correctes et de celles qui sont optimales.

<footnote>* Part of this research was supported by the Department of Computer Science at Stanford University and Stanford Artificial Intelligence Project.</footnote>
# INTRODUCTION

It is more or less the programmer's intuition that, unless side-effects take place, the result of a recursive routine, if any, will not depend on whether its parameters have been declared as name or value parameters. It would also seem natural that "call-by-value" be more efficient than "call-by-name", since it avoids many redundant computations of arguments. As pointed out by Morris [4] and Cadiou [1], this is not always the case, and there are recursive routines which never terminate when using "call-by-value" and yield their result quite rapidly with "call-by-name".

The purpose of this paper is to study the functions computed by various implementations of recursion. Unlike Cadiou [1] who studied the functions computed by "call-by-value", we devote our energy to characterizing implementations equivalent to "call-by-name", which deserve the name of correct implementation because they terminate whenever it is possible to do so. We then describe a correct implementation of recursion, the delay rule which is optimal in that it computes its result faster than any other rule for any argument.

## Some minimal background in Scott's theory of computation

A *data-type* is the semantic interpretation of the domain on which a computation is performed. Abstractly, a data-type is a set partially ordered by the relation $\sqsubseteq$ in which any chain $x_0 \sqsubseteq \dots \sqsubseteq x_n \sqsubseteq x_{n+1} \dots$ has a least-upper bound or limit $\sqcup_{n>0} x_n$ such that $x_n \sqsubseteq \sqcup_{n>0} x_n$ for any $n$ and $x_n \sqsubseteq x$ for any $n$ implies $\sqcup_{n>0} x_n \sqsubseteq x$.

The relation $x \sqsubseteq y$ means that $x$ is an approximation to $y$, and a data-type $\mathcal{D}$ has a least element $UU_\mathcal{D}$ such that $UU_\mathcal{D} \sqsubseteq x$ for any $x \in \mathcal{D}$, which represents a complete absence of information. For example, the data-type $\mathbb{N}$ of natural numbers can be represented by $0, 1, 2, \dots$ where $\omega$ is an abbreviation for $UU_\mathbb{N}$.

In this case, $x \sqsubseteq y$ means either that $x$ is *undefined*, i-e, is the result of some non-terminating procedure, or that $x$ and $y$ are the same integer.

The data-type $[\mathcal{D} \to \mathcal{D}]$ of partial functions over some data-type $\mathcal{D}$ can be ordered by:

$f \sqsubseteq g$ in $\mathcal{D} \to \mathcal{D}$ whenever $f(x) \sqsubseteq g(x)$ in $\mathcal{D}$ for all $x \in \mathcal{D}$. In $[N \to N]$, let us define the function *one* as *one* ($x) \equiv 1$ for any natural number $x$ and *one* ($\omega$) $\equiv \omega$. (Here, $x \equiv y$ means $x \sqsubseteq y$ and $y \sqsubseteq x$).

This function can also be defined as the limit of a chain of partial functions:

$$ \text{one} \equiv \sqcup_{i \ge 0} [\lambda x. \text{ if } x < i \text{ then } 1 \text{ else } \omega]. $$

If we now consider programs as functions mapping data-types into data-types, *computable functions* ought to be monotone and continuous, i-e, $x \sqsubseteq y$ implies $f(x) \sqsubseteq f(y)$ and $x \equiv \sqcup_{i \ge 0} x_i$ implies $f(\sqcup_{i \ge 0} x_i) \equiv \sqcup_{i \ge 0} f(x_i)$. (See Scott [6] for motivation). For functions of several arguments,

continuity and monotonicity is meant componentwise.
One can then formulate Kleene's first recursion theorem as follows :

**Theorem :** Any continuous function $\lambda x.f(x)$ over a data-type $\mathfrak{D}$ has a least-fixed-point $x_f$ and
$$x_f \equiv \bigsqcup_{n>0} f^n(\mathfrak{U}x_{\mathfrak{D}}).$$

*Proof:* Here $f^n(\mathfrak{U}U)$ means $f(f(...(f(\mathfrak{U}U)...))$ (n times) and, by monotonicity of $f$, the sequence $\mathfrak{U}U \equiv f(\mathfrak{U}U) \equiv \dots \equiv f^n(\mathfrak{U}U) \equiv \dots$ is indeed a chain. By continuity $f(x_f) \equiv f(\bigsqcup_{n>0} f^n(\mathfrak{U}U)) \equiv \bigsqcup_{n>0} f^{n+1}(\mathfrak{U}U) \equiv x_f$ and $x_f$ is indeed a fixed-point of $f$. Let $y$ be an arbitrary fixed-point of $f$, $i-e, y \equiv f(y)$. It is easy to prove by induction that $f^n(\mathfrak{U}U) \equiv y$ for any $n$. The conclusion $x_f \equiv \bigsqcup_{n>0} f^n(\mathfrak{U}U) \equiv y$ follows by definition of limits, and $x_f$ is indeed minimal.

# 1. COMPUTATIONS OF RECURSIVELY DEFINED FUNCTIONS

Before defining a computation rule, we must describe two programming languages, *lang S* and *lang P*. Although those two languages were chosen for their extreme simplicity, their use of recursion is a general as any, and the results of this paper provide some insight into semantics and implementation of more complex programming languages.

*Lang S* permits only *sequential* computations, and corresponds precisely to a certain "typed" subset of Algol or LISP.

*Lang P* requires some parallel operations, and thus departs from more classical programming languages, although we could undoubtedly write an interpreter for *lang P* in any of those classical languages.

## 1.1. Description of lang S and lang P

### Syntax

Both languages have the same syntax :

*<program>* :: = $F(x_1,...,x_n) \Leftarrow <term>$  
*<term>* :: = $A_1|A_2|...$  
$|x_1|...|x_n|$  
$|G_1(<term l>,...,<term p_l>)|$  
$...$  
$|G_k(<term l>,...,<term p_k>)|$.

We limited ourselves to a single recursive equation, the extension of the results in this paper to systems of mutually recursive equations being straightforward.
Here, $A_1, A_2, ..., G_1, ..., G_k$ denote fixed constants and functions respectively. It is convenient to use a more standard syntax, e.g., $F(X) \Leftarrow IF X = 0 THEN 1 ELSE X:F(X-1)$ instead of

$F(X) \Leftarrow G_1 (P_1(X, A_0), A_1, G_2(X, F(G_3(X))))$.

The meaning of a program will be a continuous mapping in $[\mathcal{D}_1 x...x \mathcal{D}_n \to \mathcal{D}]$ where each $\mathcal{D}_i$ and $\mathcal{D}$ are some data-types; for simplicity, the $\mathcal{D}_i$'s will be identical to $\mathcal{D}$ unless explicitly specified.

The meaning of a `<term>` is a (continuous) functional $\lambda f. \lambda x_1, ..., x_n \mathcal{S} (<term>)$ where the semantic function $\mathcal{S}$ is defined inductively as follows:

(i) $\mathcal{S}(A_1) \equiv a_1$ where $a_i \in \mathcal{D}$

(ii) $\mathcal{S}(X) \equiv x_i$

(iii) $\mathcal{S}(G_k (<term 1>, ..., <term $p_k$>) \equiv g_k (\mathcal{S}(<term 1>), ..., \mathcal{S}(<term $p_k$>))$ where $g_k$ is some continuous function in $[\mathcal{D}^{p_k} \to \mathcal{D}]$.

## Semantics of Terms in lang S

The semantics of lang S is defined in precisely the same way, the difference lying in restrictions on the interpretation of base functions. In lang S, we require functions to be sequential, i.e., roughly that their arguments can be computed in sequence. We shall give later a precise definition of this notion. For expository purposes, however, we shall limit ourselves for the moment to studying a particular sequential language.

The data-types on which our particular lang S is computing are discrete, i.e., they look like:

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

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

In what follows, we use $\omega$ instead of $u_\omega$ and $\Omega$ in place of $u_\Omega \to \mathcal{D}$ in order to help the eye avoid type confusions. Among the base functions, we point out a particular one, denoted `IF-THEN-ELSE` whose interpretation is the usual conditional, i.e., `if u1 then x else y` $\equiv \omega$, `if tt then x else y` $\equiv x$ and `if ff then x else y` $\equiv$ `.`

All other base functions are required to be strict, i.e., $g_i(..., \omega, ...)$ $\equiv \omega$ : they are undefined as soon as at least one of their arguments becomes undefined. They are meant to correspond to the "hardware" functions : add, addone, test-for-equality, ...

It will be shown that all functions definable in lang S are sequential. The symmetric OR defined by the table:

<table><thead><tr><th>x OR y</th><th>uu</th><th>tt</th><th>ff</th></tr></thead><tbody><tr><th>uu</th><td>uu</td><td>tt</td><td>uu</td></tr><tr><th>tt</th><td>tt</td><td>tt</td><td>tt</td></tr><tr><th>ff</th><td>uu</td><td>tt</td><td>ff</td></tr></tbody></table>
or the symmetric multiply * where $O*x \equiv x*O \equiv O$ are not sequential, and are therefore *not definable* in lang S, nor in Algol for that matter.

## Semantics of Programs in both lang S and lang P

The functional $\tau \equiv \lambda f.\lambda x_1, ..., x_n \mathcal{S}^f (<term>)$ as defined in lang S or lang P can be shown to be continuous. It must therefore have a least fixed-point $f_\tau$ and it would be nice to define the meaning $\eta$ of the corresponding program as $\eta (<program>) \equiv f_\tau$.

This is unfortunately not true for all implementations of recursion, and our goal will be to characterize the implementations for which the computed function is equal to this least fixed-point.

## 1.2. Conventions and Notations

The reader has already noticed that syntactic entities are denoted by upper case letters, while the associated semantic objects are represented by the corresponding lower-case letters. We shall keep this convention throughout this paper. For example, if $T$ is $IF X = O THEN 1 ELSE X.F.(X-1)$, then $\tau \equiv \lambda f.\lambda x \mathit{if} x = O \mathit{then} 1 \mathit{else} x.f(x-1)$, where $=$ in this last expression means the equality function over the natural numbers, $O$ the number $0$, etc.

From now on, we use upper case letters other than $A, X, F$ and $G$ to denote (syntactic) terms. If $T$ and $S$ are terms, we denote by $T\{S/X_1\}$ the result of replacing all occurrences of the letter $X_1$ by the term $S$ in $T$. By $T\{P/F\}$, we mean the term obtained by replacing in $T$ all subterms of the form $F(A_1, ..., A_n)$ by $P\{A_1/X_1, ..., A_n/X_n\}$, for example,

$$ \text{if } T = G_1(F(X_1, F(X_1, X_2)), X) \text{ and } P = G(F(X_2, X_1)), $$

$$ \text{then } T\{P/F\} = G_1(G(F(G(F(X_2, X_1)), X_1)), X_1). $$

Whenever we only wish to substitute $P$ for some occurrences of $F$ in $T$, we rename, say $F_1$, the occurrences that we shall substitute and $F_2$ the others. The result of the substitutions is then $T\{P/F_1, F/F_2\}$. The same kind of notation also applies to semantic terms.

We use $F(\bar{x})$ and $f(\bar{x})$ as abbreviations for $F(X_1, ..., X_n)$ and $f(x_1, ..., x_n)$ respectively.

Also, it will be convenient to only consider programs $F(\bar{x}) \Leftarrow P$, where $P$ is of the form $G(P_1, ..., P_p)$ with the additional restriction that each of the letters $F, X_1, ..., X_n$ occurs at least once in $P$.

That is, $P$ is required not to ignore any of its program variables, to depend upon $F$ (i.e., to be recursive) and not to be of the uninteresting form $F(X) \Leftarrow F(A_1, ..., A_n)$. The main results of this paper generalize without this restriction, but the proofs are made longer by an addition of special cases.

## 1.3. Computation Rule

A computation rule $\mathcal{E}$ is an algorithm for selecting some occurrences of the letter $F$ in each term.
For any such rule and input $\bar{D}$, we construct the computation sequence $T_0, T_1, \dots, T_n, \dots$ of the term $T$ by the program $F(\bar{X}) \Leftarrow P$ as follows: $T_0 = T\{\bar{D}/\bar{X}\}$ and $T_{i+1}$ is the result of substituting $P$ for the $F$'s chosen by $\mathcal{C}$ in $T_i$. For example, if $P = \text{IF } X < 2 \text{ THEN } X \text{ ELSE } F(X-1)+F(X-2)$, the computation sequence of $F(2)$ according to "call-by-value" is:

$$ 
\begin{align*}
T_0 &= F(2) \\
T_1 &= \text{IF } 2 < 2 \text{ THEN } 2 \text{ ELSE } \underline{F}(1)+F(0) \\
T_2 &= \text{IF } 2 < 2 \text{ THEN } 2 \text{ ELSE } \left( \begin{array}{l} \text{IF } 1 < 2 \text{ THEN } 1+\underline{F}(0) \text{ ELSE } F(0)+F(-1)+F(0) \end{array} \right) \\
T_3 &= \text{IF } 2 < 2 \text{ THEN } 2 \\
    &\quad \text{ELSE } \left( \begin{array}{l} \text{IF } 1 < 2 \text{ THEN } \text{IF } 0 < 2 \text{ THEN } 1 \\ \phantom{\text{ELSE } \text{IF } 1 < 2 \text{ THEN }} 1+\underline{F}(-1)+\underline{F}(-2) \\ \phantom{\text{ELSE } \text{IF } 1 < 2 \text{ THEN }} \text{ELSE } F(0)+F(-1)+F(0) \end{array} \right) \\
T_4 &= T_5 = \dots = T_3.
\end{align*}
$$

(Here, $F(1)$ is in fact an abbreviation for $F(2-1)$, etc.).

In $T_n$, we underline the $F$'s selected by the computation rule for substitution. It is interesting to see precisely how the underlined $F$ is selected in this last example. For this purpose, we must introduce the notion of simplification. The simplification mechanism is discussed at length in Cadiou[1], and we refer the interested reader to this work. In our particular example, it is possible to define a simplification mechanism $\lambda T \text{ simpl}(T)$ such that:

$$ 
\begin{align*}
\text{simpl}(T_0) &= F(2) \\
\text{simpl}(T_1) &= F(1)+F(0) \\
\text{simpl}(T_2) &= 1+F(0) \\
\text{simpl}(T_3) &= \text{simpl}(T_4) = \dots = 1
\end{align*}
$$

(Note that now, $F(1)$ is no longer an abbreviation since $\text{simpl}(2-1) = 1$).

The rule "call-by-value" then selects the leftmost-innermost occurrence of $F$ in simplified terms. Similarly, "call-by-name" selects the "leftmost-outermost" one.

In its most general form, simplification can be an extremely powerful computation tool. For example, if our program is $F(X) \Leftarrow \text{IF } X = 0 \text{ THEN } 0 \text{ ELSE } F(X-1)$ it is perfectly all right to use $F(X) \to 0$ as a simplification rule over the natural numbers, and there is no room left for substitutions! Our purpose however is to study computations which are performed by substitutions and **not** by simplifications. We must therefore restrict the power of simplifications which we allow, and, for this purpose, we merely borrow Cadiou's notion of **standard simplifications** (see Cadiou[1] for a precise definition). Roughly, standard simplifications force us to know everything about base functions, and nothing a priori about the recursively defined function $F$, since simplifications of the type $F(\bar{D}) \to A_i$ are not permitted. In effect, we have to compute without any "built in" value of the recursively defined function, stored for example in memory from a previous computation.

We shall not study standard simplifications in $\underline{\text{lang }} P$, since this would require describing completely the data-type on which computations are performed but we will describe them in
In language S. For all constants $A_{i1}, \dots, A_{ip}$ and base function $G_p$ or predicate $P_p$, there exists a standard simplification of the type

$$G_p(A_{i1}, \dots, A_{ip}) \to A_j$$

$$P_p(A_{i1}, \dots, A_{ip}) \to \text{TRUE or FALSE.}$$

In effect, this says that the values of the base-functions over the domain are known, and these functions are total. Accordingly, the conditional admits the simplifications

$$\text{IF TRUE THEN } B \text{ ELSE } C \to B \text{ and}$$

$$\text{IF FALSE THEN } B \text{ ELSE } C \to C.$$

Those are the only standard simplifications in language S and we say that a term is simplified when all of its subterms have been simplified.

## 1.4. Computation lattice of a program

Instead of considering computation sequences for each input and computation rule, we can apprehend the set of all possible computations in one infinite diagram.

For example, the computation diagram of the term $F(F(X))$ by the program $F(X) \leftarrow G(X, F(F(X)))$ looks like.

<figure><img src="image_6.png" /><figcaption>FIGURE 1: Computation lattice of $F(F(X))$ by $F(X) \leftarrow G(X, FFX)$</figcaption></figure>

A computation rule is then an algorithm for selecting a path in such a graph for each input. This computation diagram has a very rich structure which we shall now study.

### Computation of a term according to P

We say that $B \stackrel{P}{\to} C$ or simply $B \to C$ whenever $C$ can be obtained by substituting $P$ for some occurrences of $F$ in $B$. The notation $B \stackrel{*}{\to} C$ or $B \stackrel{P}{\to} C$ means that there exists a finite sequence of terms

$D_0, D_1, \dots, D_m$ such that $D_0 = B$, $D_m = C$ and $D_i \to D_{i+1}$ for $0 \le i < m$.
## Definition

The computation diagram of T by P is the set of terms U such that $T \underset{P}{\stackrel{*}{\to}} U$, partially ordered by $\le$ where $B \le C$ whenever $B \underset{P}{\stackrel{*}{\to}} C$.

It is clear that $\le$ is reflexive and transitive. In order to prove that it is also antisymmetric, we notice that, if $B \underset{P}{\to} C$, the size $|C|$ (where size is, say the number of symbols) of the term C is strictly larger than the size of B if at least one substitution has been performed (this is due to our restriction on P). It follows that $B \stackrel{*}{\to} C$ and $C \stackrel{*}{\to} B$ implies $B = C$.

Clearly, the computation diagram of T by P has the Church-Rosser property of the $\lambda$-calculus. (This follows from the work of Rosen [5] for example). However, it also has a property which is *not* true of the $\lambda$-calculus, namely :

### Theorem 1

The computation diagram of T by P is a lattice under the ordering $\le$, and we shall name it the computation lattice of T by P.

*Proof.* In order to study the structure of the computation diagram of a term $T_0$ by a program P, we need to relate the structure of C to that of B when $B \underset{P}{\stackrel{*}{\to}} C$.

### Lemma 1

(i) $A_i \stackrel{*}{\to} C$ if and only if $C = A_i$ and $X_j \stackrel{*}{\to} C$ if and only if $C = X_j$.

(ii) $G_i(B_1, \dots, B_{p_i}) \stackrel{*}{\to} C$ if and only if $C = G_i(C_1, \dots, C_{p_i})$ and $B_i \stackrel{*}{\to} C_i$ for $1 \le i \le p_i$.

(iii) $F(B_1, \dots, B_n) \stackrel{*}{\to} C$ if and only if $C = F(C_1, \dots, C_n)$ with $B_i \stackrel{*}{\to} C_i$ for $1 \le i \le n$ or $P\{B_1/X_1, \dots, B_n/X_n\} \stackrel{*}{\to} C$.

*Proof.* Claims (i) and (ii) are easy and we only prove (iii).

If $B = F(B_1, \dots, B_n) \stackrel{*}{\to} C$ and $C$ is not of the form $F(C_1, \dots, C_n)$, there must be a point in the computation $B \stackrel{*}{\to} C$ where the outermost $F$ of $B$ is substituted, i.e., $F(B_1, \dots, B_n) \stackrel{*}{\to} F(B'_1, \dots, B'_n) \stackrel{*}{\to} P\{B''_1/X'_1, \dots, B''_n/X'_n\} \stackrel{*}{\to} C$ with $B'_i \to B''_i$ (and therefore $B_i \stackrel{*}{\to} B''_i$) for any $1 \le i \le n$.

It follows from our definitions that $B_i \stackrel{*}{\to} B''_i$ for $1 \le i \le n$ implies

$P\{B_1/X_1, \dots, B_n/X_n\} \stackrel{*}{\to} P\{B'_1/X'_1, \dots, B'_n/X'_n\}$ and consequently $P\{B_1/X_1, \dots, B_n/X_n\} \stackrel{*}{\to} C$, as claimed in (iii). In order to get the other part of the implication (iii), we simply notice that $F(B_1, \dots, B_n) \to P\{B_1/X_1, \dots, B_n/X_n\}$ by substituting $P$ for the outer $F$ in $F(B_1, \dots, B_n)$.

If $B \le C$, we can define a distance $dist(B,C)$ between B and C as follows :

(i) if $B = A_i$ or $B = X_j$ then $C = B$ and $dist(B,C) = 0$;

(ii) if $B = G_i(B_1, \dots, B_{p_i})$ then $C = G_i(C_1, \dots, C_{p_i})$ with $B_i \le C_i$ for $1 \le i \le p_i$ and $dist(B,C) = \max \{dist(B_j, C_j)\}; 1 \le j \le p_i$.
(iii) if $B = F(B_1, \dots, B_n)$ then (by Lemma 1), either $C = F(C_1, \dots, C_n)$
and $\text{dist}(B,C) = \max \{\text{dist}(B_i, C_i)\}$ or
$1 \le i \le n$
$$P\{B_1/X_1, \dots, B_n/X_n\} \le C \text{ and } \text{dist}(B,C) = 1+\text{dist}(P\{B_1/X_1, \dots, B_n/X_n\}, C).$$

It is easily seen that the distance between any two terms $B \le C$ is finite.

**Lemma 2**

If $B = F(B_1, \dots, B_n)$, $C = F(C_1, \dots, C_n)$, $B' = P\{B'/X_1, \dots, B_n'/X_n\}$
and $C' = P\{C_1/X_1, \dots, C_n/X_n\}$ then $B \le C$ implies $B' \le C'$ and $\text{dist}(B'C') \le \text{dist}(B,C)$.

**Proof.** By a straightforward induction on $||P||$, one proves that
$\text{dist}(P\{B_1/X_1, \dots, B_n/X_n\}, P\{C_1/X_1, \dots, C_n/X_n\}) \le \max \{\text{dist}(B_i, C_i)\}$, hence
$1 \le i \le n$
$\text{dist}(B', C') \le \text{dist}(B, C)$. $\square$

We now start the proof of Theorem 1 :

For any two terms $B,C$ in the computation diagram of $T$ by $P$, we must show the existence of $\min(B,C)$ and $\max(B,C)$ such that

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

and for any $D$ and $H$

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

$D \le \min(B,C)$

implies

and

$\max(B,C) \le H$

**Existence of max(B,C)**

We shall describe an algorithm for computing $\max(B,C)$ and then prove the correctness of this
algorithm : let $\sigma(B,C)$ be defined recursively as

(i) $\sigma(B, B) = B$,

(ii) $\sigma(G_i(B_1, \dots, B_{p_i}), G_i(C_1, \dots, C_{p_i})) = G_i(\sigma(B_1, C_1), \dots, \sigma(B_{p_i}, C_{p_i})),$

(iii) $\sigma(F(B_1, \dots, B_n), F(C_1, \dots, C_n)) = F(\sigma(B_1, C_1), \dots, \sigma(B_n, C_n)),$

(iv) $\sigma(F(B_1, \dots, B_n), G(C_1, \dots, C_p)) = \sigma(P\{B_1/X_1, \dots, B_n/X_n\}, G(C_1, \dots, C_p)) = \sigma(G(C_1, \dots, C_p), F(B_1, \dots, B_n)),$
(v) in all the other cases, $\sigma(B,C)$ yields an error symbol, (say a german gothic letter) which is not part of our set of letters.

We shall prove that $\sigma(B,C) = \max(B,C)$ in two parts :

**Part 1.** For any terms $T, B, C$

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

implies

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

The proof is by induction on couples $\langle \text{dist}(T,B) + \text{dist}(T,C), ||T|| \rangle$ ordered lexicographically by $<$

Assuming the result to be true for all triples $T', B', C'$ with $\langle \text{dist}(T',B') + \text{dist}(T',C'), ||T'|| \rangle < \langle \text{dist}(T,B) + \text{dist}(T,C), ||T|| \rangle$, we prove it for $T, B, C$ by a case analysis on the structure of $T$.

**Case 1.** $T = A_i$ or $T = X_j$.

By Lemma 1, $T \stackrel{*}{\rightarrow} B$ and $T \stackrel{*}{\rightarrow} C$ implies $T = B$ and $T = C$; hence $B = C = \sigma(B,C)$ and indeed $B \stackrel{*}{\rightarrow} \sigma(B,C)$ and $C \stackrel{*}{\rightarrow} \sigma(B,C)$.

**Case 2.** $T = G_i(T_1, \dots, T_{p_i})$.

By Lemma 1, $B = G_i(B_1, \dots, B_{p_i})$ and $C = G_i(C_1, \dots, C_{p_i})$, with $T_i \stackrel{*}{\rightarrow} C_i$ for $1 \le i \le p_i$. Since $\text{dist}(T_i, B_i) + \text{dist}(T_i, C_i) \le \text{dist}(T, B) + \text{dist}(T, C)$ and $||T_i|| < ||T||$ for any $1 \le i \le p_i$, the induction hypothesis tells us that $B_i \stackrel{*}{\rightarrow} \sigma(B_i, C_i)$ and $C_i \stackrel{*}{\rightarrow} \sigma(B_i, C_i)$ for each $1 \le i \le p_i$.

Regrouping everything, the conclusion $B \stackrel{*}{\rightarrow} \sigma(B,C)$ and $C \stackrel{*}{\rightarrow} \sigma(B,C)$ then follows from the definition $\sigma(C_i(B_1, \dots, B_{p_i}), G_i(C_1, \dots, C_{p_i})) = G_i(\sigma(B_1, C_1), \dots, \sigma(B_{p_i}, C_{p_i}))$.

**Case 3.** $T = F(T_1, \dots, T_n)$.

By symmetry, we only need consider the subcases :

**Case 3.1.** $B = F(B_1, \dots, B_n)$ and $C = F(C_1, \dots, C_n)$

The proof is similar to that of Case 2.

**Case 3.2.** $B = F(B_1, \dots, B_n)$ and $C = G(C_1, \dots, C_p)$.

Let $T' = \{T_1/X_1, \dots, T_n/X_n\}$ and $B' = \{B_1/X_1, \dots, B_n/X_n\}$.

By Lemma 1, we know that $T' \stackrel{*}{\rightarrow} C$ and $T_i \stackrel{*}{\rightarrow} B_i$ for $1 \le i \le n$, hence $T' \stackrel{*}{\rightarrow} B'$. By Lemma 2, we know that $\text{dist}(T', B') < \text{dist}(T, B)$. Since $\text{dist}(T', C) < \text{dist}(T, C)$, we can apply the induction hypothesis
to the terms $T', B', C'$, i.e., $B' \stackrel{*}{\rightarrow} \sigma(B',C)$ and $C \stackrel{*}{\rightarrow} \sigma(B',C)$. Since $B \rightarrow B'$ and $\sigma(B,C) = \sigma(B',C)$ by definition of $\sigma$, we have established that $B \stackrel{*}{\rightarrow} \sigma(B,C)$ and $C \stackrel{*}{\rightarrow} \sigma(B,C)$.

**Case 3.3.** $B = G(B_1, \dots, B_p)$ and $C = G(C_1, \dots, \bar{C}_p)$.

Let $T' = P\{T_1/X_1, \dots, T_n/X_n\}$. By Lemma 1, we know that $T' \stackrel{*}{\rightarrow} B$ and $T' \stackrel{*}{\rightarrow} C$. Since $\text{dist}(T',C) < \text{dist}(T,D)$ and $\text{dist}(T',C) < \text{dist}(T,C)$, we can use the induction hypothesis in order to get $B \stackrel{*}{\rightarrow} \sigma(B,C)$ and $C \stackrel{*}{\rightarrow} \sigma(B,C)$.

**Part 2.** For any terms $B, C, D$

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

The proof is by induction on $\langle \text{dist}(B,D) + \text{dist}(C,D), ||D|| \rangle$.

**Case 1.** $D = A_i$ or $D = X_j$.

Then $D = B = C = \sigma(B,C)$ and $\sigma(B,C) \stackrel{*}{\rightarrow} D$.

**Case 2.** $D = F(D_1, \dots, D_n)$ or $D = G_i(D_1, \dots, D_{p_i})$ where $G_i$ is not $G$.

The proof goes mutatis-mutandis as that of Part 1, Case 2.

**Case 3.** $D = G(D_1, \dots, D_p)$

We only need consider the cases :

**Case 3.1.** $B = G(B_1, \dots, B_p)$ and $C = G(C_1, \dots, C_p)$.

Back to Case 2.

**Case 3.2.** $B = F(B_1, \dots, B_n)$ and $C = G(C_1, \dots, C_p)$

Let $B' = P\{B_1/X_1, \dots, B_n/X_n\}$. Since $\text{dist}(B',C) < \text{dist}(B,D)$, we know by the induction hypothesis that $\sigma(B',D) = \sigma(B,C) \stackrel{*}{\rightarrow} D$.

**Case 3.3.** $B = F(B_1, \dots, B_n)$ and $C = F(C_1, \dots, C_n)$.

Let $B' = P\{B_1/X_1, \dots, B_n/X_n\}$ and $C' = P\{C_1/X_1, \dots, C_n/X_n\}$.

The induction hypothesis tells us that $\sigma(B',C') \stackrel{*}{\rightarrow} D$. One then proves by induction on $||P||$ that $\sigma(B',C') =$

$$ \sigma(P\{B_1/X_1, \dots, B_n/X_n\}, P\{C_1/X_1, \dots, C_n/X_n\}) = P\{\sigma(B_1, C_1)/X_1, \dots, \sigma(B_n, C_n)/X_n\}. $$

We conclude the proof by noticing that $\sigma(B,C) \rightarrow \sigma(B',C')$ since

$$ \sigma(B,C) = F(\sigma(B_1, C_1), \dots, \sigma(B_n, C_n)) \rightarrow P\{\sigma(B_1, C_1)/X_1, \dots, \sigma(B_n, C_n)/X_n\} = \sigma(B', C'). $$
Existence of min(B,C)

For any terms B, C in the computation diagram of T by P the set {L|L < B, L < C} of lower bounds of B and C is not empty because T ≤ B and T < C and it is finite. We know from elementary lattice theory that, if any two elements in a partially ordered set have a least-upper-bound, any non-empty finite subset also has a least-upper-bound. We then define min(B,C) as max {L|L < B, L < C} and verify easily that min has all the desired properties. ☐

Relation between the Computation Lattice and the Data-type of Continuous Functions over $\mathbb{B}$.

In order to characterize computed partial functions in terms of the semantic interpretation of a given computation lattice, we notice that

Lemma C

For any terms B, C in the computation lattice of T by P, $B \le C$ implies $b(\Omega) \leq c(\Omega)$.

Proof. The proof is straightforward by induction on $||B||$ :

If $B = A_i$ and $B = X_j$ then $B = C$ and $b(\Omega) \equiv c(\Omega)$.

If $B = G_i(B_1, \dots, B_{p_i})$, then $C = G_i(C_1, \dots, C_{p_i})$ and we know by induction that $b_j(\Omega) \le c_j(\Omega)$ for $1 \le j \le p_i$. Since $[\lambda x_1, \dots, x_{p_i} . g_i(x_1, \dots, x_{p_i})]$ is monotone with respect to any of its arguments, $b(\Omega) \equiv g_i(b_1(\Omega), \dots, b_{p_i}(\Omega)) \le g_i(c_1(\Omega), \dots, c_{p_i}(\Omega)) \equiv c(\Omega)$. Finally, if $B = F(B_1, \dots, B_n)$ then $b(\Omega) \equiv \Omega \le c(\Omega)$. ☐

In particular, to any computation sequence $T_0 \to T_1 \to \dots \to T_n \to T_{n+1} \to \dots$ according to some rule $\mathcal{E}$ and input $\bar{D}$, we associate the chain $t_0(\Omega)(\bar{d}) \sqsubseteq t_1(\Omega)(\bar{d}) \sqsubseteq \dots \sqsubseteq t_n(\Omega)(\bar{d}) \sqsubseteq t_{n+1}(\Omega)(\bar{d}) \sqsubseteq \dots$.

The corresponding computed partial function $\mathcal{E}_p$ is therefore characterized as :

$$ \mathcal{E}_p \equiv \lambda \bar{d}. \sqcup t(\Omega)(\bar{d}). \quad \underset{n \ge 0}{\le} $$

From these definitions follows an easy generalization of a theorem of Cadiou[1] :

Theorem 2

Any fixed-point of the equation $f' \equiv p(f)$ is an extension of any function computed by the program $F \leftarrow P$.

Proof. For any computation sequence $T_0, T_1, \dots, T_n, \dots$, where $T_0 = F(\bar{X})$ we can easily prove by induction that $\forall i t_i(\Omega) \sqsubseteq p^i(\Omega) \equiv p(p(\dots p(\Omega)\dots))$ (i times). Since p is continuous, $f_p \equiv \sqcup_{i \ge 0} p^i(\Omega)$, hence $t_i(\Omega) \sqsubseteq f_p$ for any i. It follows that $\mathcal{E}_p \equiv \sqcup_{i \ge 0} t_i(\Omega) \sqsubseteq f_p$ and, since $f_p \sqsubseteq f$ for any fixed-point f of p, the conclusion $\mathcal{E}_p \sqsubseteq f$ holds. ☐
## 2. CORRECT IMPLEMENTATION OF RECURSION

In this section, we try to characterize the computation rules $\mathcal{E}$ such that $\mathcal{E}_p \equiv_f \mathcal{F}_p$ for any program $F \Leftarrow P$, called *fixed-point computation rules*.

Here are some computation rules we shall consider, both in lang S and lang P :

(1) **Call by value** : substitute for the leftmost-innermost occurrence of F after simplifications.

(2) **Call by name** : substitute for the leftmost-outermost occurrence of F after simplifications.

(3) **Parallel innermost** : substitute for the occurrences of F having all of their arguments free of F's.

(4) **Parallel outermost** : substitute for all the F's which do not occur in any argument of another F.

(5) **Free argument** : substitute for all the occurrences of F having at least one of their arguments free of F's after simplifications.

(6) **Full substitution** : substitute for all the occurrences of F.

### 2.1. Incorrect computation rules

**Proposition 1.**

In lang P, the rules (1), (2) and (3) are incorrect.

**Proof.** Consider the program $F(X,Y) \Leftarrow \mathbf{IF} X = 0 \mathbf{THEN} 0 \mathbf{ELSE} F(X+1,F(X,Y)) * F(X-1,F(X,Y))$
where $*$ is the parallel multiplication function $0*x \equiv x*0 \equiv 0$. The least fixed-point over the
integers (considered as a discrete data-type) of the corresponding functional is the constant
function 0. The computation of $F(1,0)$ using (1), (2) or (3) is infinite.

**Proposition 2. (Morris [4])**

In lang S the rules (1) and (3) are incorrect.

**Proof.** Consider $F(X,Y) \Leftarrow \mathbf{IF} X = 0 \mathbf{THEN} 0 \mathbf{ELSE} F(X-1,F(X,Y))$. The corresponding least fixed-point over the non-negative integers is again the constant function 0 while the computation of $F(1,0)$ using rules (1) or (3) is infinite.

### 2.2. Safe Computation Rules

We now define the class of safe computation rules, and show that they correspond to "correct" implementations of recursion.

Let $\mathcal{E}$ be a computation rule and B an arbitrary term in the computation lattice of T by P; In order to describe the effect of $\mathcal{E}$ on B, we rename $F_1$ the occurrences of F selected for substitution by $\mathcal{E}$ in B for some input $\bar{D}$, and $F_2$ the others.
## Definition

We say that $\mathcal{B}$ is a safe computation rule if, for any term $B=\{F/F_1,F/F_2\}$ in the computation lattice of $T$ by $P$ and for any input $\bar{D}$, $b\{\Omega/f_1,f_p/f_2\}(\bar{d}) \equiv b\{\Omega/f_1,\Omega/f_2\}(\bar{d})$.

Intuitively, the computation is safe if the values of the $F$'s which are not substituted (renamed $F_2$) are insufficient : as long as more information is not obtained about the other arguments (the $F_1$'s), the information about $B$ cannot be improved.

In order to clarify this definition, let us prove the safeness of some of our computation rules.

## Proposition 3

In lang $S$, the rules (2), i.e., call-by-name and (5), i.e., free argument are safe.

*Proof.* By induction on $||C||$ where $C = \text{simp1}(B)$ : we first notice that, because of the semantic definition of lang $S$, if $F$ occurs in $C$ then $c(\Omega)(\bar{d}) \equiv \omega$ (remember that $C$ has been simplified).

Case $C = A_i$ then any rule is safe.

Case $C = G_i(C_1, \dots, C_{p_i})$. The letter $F$ occurs necessarily in $C$, otherwise we could simplify further. Since both rules select at least one $F$ on such terms, we know by our previous remark that $c\{\Omega/f_1, f_p/f_2\}(\bar{d}) \equiv \omega \equiv c\{\Omega/f_1, \Omega/f_2\}(\bar{d})$.

Case $C = F(C_1, \dots, C_n)$. The safeness of rule (2) is straightforward since the outermost $F$ is substituted. For the same reason, rule (5) is safe if at least one of the $C_i$ is constant. If none of the $C_i$'s is constant, then $c_i\{\Omega/f_1, f_p/f_2\}(\bar{d}) \equiv \omega$ for $1 \le i \le n$ and we must prove that $f_p(\omega, \dots, \omega) \equiv \omega$. This is ensured by imposing in lang $S$ that all program variables $X_1, \dots, X_n$ occur in $\text{simp1}(P)$ hence $f_p(\omega, \dots, \omega) \equiv p(f_p)(\omega, \dots, \omega) \equiv \omega$. $\square$

## Proposition 4

The rules (4), i.e., parallel outermost and (6), i.e., full substitution are safe in both lang $S$ and lang $P$.

*Proof.* By induction on $||B||$.

Case $B = A_i$. Any rule is safe.

Case $B = G_i(B_1, \dots, B_{p_i})$. By induction, $b_i\{\Omega/f_1, f_p/f_2\}(\bar{d}) \equiv b_i\{\Omega/f_1, f_p/f_2\}(\bar{d})$ for $1 \le i \le p$ in both cases, hence safeness is also satisfied on $b$.
Case B = F(B₁, ..., Bₙ). Both rules select the outermost F hence

$$b\{\Omega/f_1, f_p/f_2\}(\bar{d}) \equiv \omega \equiv b\{\Omega/f_1, \Omega/f_2\}(d). \quad \square$$

Note that the computation rules that we already recognized as incorrect are all unsafe. In order to prove that safe rules are correct, we need the following technical lemma :

**Lemma S**

If $\mathscr{E}$ is safe, then $B \xrightarrow{\mathscr{E}} C$ and $\min(B,D) = \min(C,D)$ imply $d(\Omega)(\bar{d}) \equiv b(\Omega)(\bar{d})$ for any terms B, C and D in the computation lattice of T by P, and input D.

**Proof.** Let us first determine some properties of the $\min$ of two terms :

**Lemma 3**

(i) $\min(G_i(B_1, \dots, B_{p_i}), G_i(C_1, \dots, C_{p_i})) = G_i(\min(B_1, C_1), \dots, \min(B_{p_i}, C_{p_i}))$.

(ii) $\min(P(B_1/X_1, \dots, B_n/X_n), G(C_1, \dots, C_p)) = P\{M_1/X_1, \dots, M_n/X_n\}$

where $M_1, \dots, M_n$ are such that $F(M_1, \dots, M_n) = \min(F(B_1, \dots, B_n), G(C_1, \dots, C_p))$.

**Proof.** Property (i) is easy and property (ii) follows from the fact that

$P\{M_1/X_1, \dots, M_n/X_n\} \xrightarrow{*} M' \xrightarrow{*} P\{B_1/X_1, \dots, B_n/X_n\}$ with $M_i \xrightarrow{*} B_i$ for $1 \le i \le n$ implies that

$M' = P\{M'_1/X_1, \dots, M'_n/X_n\}$ where $M'_i \xrightarrow{*} M_i$ for $1 \le i \le n$.

We now prove Lemma S : Let us rename $F_1$ the occurrences of F selected by $\mathscr{E}$ in B and $F_2$, the others. Let $M = \min(B,D) = \min(C,D)$.

We first prove by induction on $\langle \mathrm{dist}(M,B) + \mathrm{dist}(M,C), ||M|| \rangle$ that $D \le B\{F/F_1, P^m/F_2\}$ for some natural number $m$. (Here $P^m$ means $P\{P^{m-1}/F\}$ for $m > 0$ and $P^0 = F(X_1, \dots, X_n)$.)

$$\text{Case M} = A_i \text{ or } M = X_i$$

In this case, $M = B = C = D$ and we can choose $m = 0$.

$$\text{Case M} = G_i(M_1, \dots, M_{p_i})$$

By Lemma 1, $B = G_i(B_1, \dots, B_{p_i})$, $C = G_i(C_1, \dots, C_{p_i})$ and $D = G(D_1, \dots, D_{p_i})$. By Lemma 3,

$M_i = \min(B_i, D_i) = \min(C_i, D_i)$ for $1 \le i \le p$. It follows by induction that $D_i \le B_i\{F/F_1, P^m/F_2\}$.

We can then choose $m = \sup_{1 \le i \le p_i} \{m_i\}$ in order to get $D \le B\{F/F_1, P^m/F_2\}$.

$$\text{Case M} = F(M_1, \dots, M_n)$$

By definition of $\min$, we need only consider the cases :
Case B = $G(B_1, \dots, B_p)$ and D = $F(D_1, \dots, D_n)$

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

Let $M' = P\{M_1/X_1, \dots, M_n/X_n\}$ and

$D' = P\{D_1/X_1, \dots, D_n/X_n\}$. By Lemma 3 $M' = \min(B,D') = \min(C,D')$.

By Lemma 2, $\min(M',D') + \min(M',D') < \min(M,B) + \min(M,D)$ so we know by induction that

$D' \le B\{F/F_1, P^m/F_2\}$ and, a fortiori $D \le B\{F/F_1, P^m/F_2\}$ for some $m$.

Case B = $F(B_1, \dots, B_n)$ and $D = G(D_1, \dots, D_p)$

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

Since $\min(B,D) = \min(C,D)$, the term C is also of the form

$C = F(C_1, \dots, C_n)$. Let $M' = P\{M_1/X_1, \dots, M_n/X_n\}$,

$B' = P\{B_1/X_1, \dots, B_n/X_n\}$ and $C' = P\{C_1/X_1, \dots, C_n/X_n\}$. By Lemma 3,

we know that $M' = \min(B',D) = \min(C',D)$.

By Lemma 2, $\min(M',D') + \min(M',D) < \min(M,B) + \min(M,D)$, and the induction hypothesis tells us that $D \le B'\{F/F_1, P^m/F_2\}$.

Since the outermost F has not been selected by C in B then $B' \le B\{P/F_2\}$. Our last case is then treated since

$D \le B\{F/F_1, P^{m+1}/F_2\}$.

It is now easy to finish the proof of Lemma S. For any $m$, $P^m(\Omega) \subseteq f_p$ implies $b\{\Omega/f_1, P^m(\Omega)/f_2\} \subseteq b\{\Omega/f_1, f_p/f_2\}$. By choosing $m$ large enough, we know that $d(\Omega) \supseteq b\{\Omega/f_1, P^m(\Omega)/f_2\}$ and therefore $d(\Omega) \subseteq b\{\Omega/f_1, f_p/f_2\}$. Since $\mathcal{C}$ is safe, $b\{\Omega/f_1, f_p/f_2\}(\bar{d}) = b(\Omega)(\bar{d})$ and the conclusion $d(\Omega)(\bar{d}) \subseteq b(\Omega)(\bar{d})$ follows. $\square$

**Theorem 3**

Any safe rule is a fixed-point rule.

**Proof.** In the computation lattice of $T_0 = F(\bar{D})$ by P, let $T_0, T_1, \dots, T_n, \dots$ and $S_0, S_1, \dots, S_n, \dots$ (where $S_0 = T_0$) be the computation sequences corresponding to respectively some safe rule $\mathcal{C}$ and the full substitution rule. Since $s_n(\Omega) \equiv P^n(\Omega)$ then $\bigcup_{n \ge 0} s_n(\Omega) \equiv \bigcup_{n \ge 0} P^n(\Omega) \equiv f_p$. We know by Theorem I that $\mathcal{C} \subseteq P(\bar{d})$ and it is therefore sufficient to show that $\bigcup_{n \ge 0} s_n(\Omega)(\bar{d}) \supseteq \bigcup_{n \ge 0} T_n(\Omega)(\bar{d})$, in order to prove $\mathcal{C} = f_p$.

Let $S_n$ be an arbitrary term in $S_0, S_1, \dots$. Since there are only finitely many minors of $S_n$ in the computation lattice, there exists some $m$ such that $\min(T_m, S_n) = \min(T_{m+1}, S_n)$. The rule $\mathcal{C}$ being safe, it follows from Lemma S that $s_n(\Omega)(\bar{d}) \supseteq T_m(\Omega)(\bar{d})$, hence $\bigcup_{n \ge 0} s_n(\Omega)(\bar{d}) \supseteq \bigcup_{m \ge 0} T_m(\Omega)(\bar{d})$. $\square$
As a corollary, rules (2) and (5) are fixed-point in <u>lang S</u> and rules (4) and (6) are fixed-point rules in both <u>lang S</u> and <u>lang P</u>.

### 3. AN OPTIMAL IMPLEMENTATION OF RECURSION IN LANG S

Among the correct implementations of recursion, we now try to determine which ones are efficient. This proves unsuccessful in lang P, but we shall describe an implementation of recursion for lang S which turns out to be optimal.

We already know that, in lang S, "call-by-name" is a fixed-point rule, while "call-by-value" is not. However, "call-by-name" is not an efficient way of computing. For example, in the program $F(X) \Leftarrow IF X > 0 THEN X-1 ELSE F(F(X+2))$ the "call-by-name" computation of $F(0)$ would be $F(0) \to F(F(2)) \to IF F(2 > 0) \text{ then } F(2)-1 \text{ ELSE } F(F(2)+1)) \to F(2)-1 \to 0$.

What happens here is that the term $F(2)$ has been duplicated and subsequently computed twice. We shall describe a computation mechanism, called the *delay-rule*, which avoids those duplications, and prove its optimality.

#### 3.1. Never do today what you can put off until tomorrow

A natural way to keep track of duplications of terms is to assign labels to all occurrences of F in a computation sequence, so that copies of the same F will receive the same label. This can be achieved by first labelling differently all $F_s$ in $T_0$ and P; then, if F is labelled $\alpha$ in $T_n$ and is to be substituted, we label each occurrence of F after substitution by $\alpha$ followed by whatever labelling this particular occurrence had in P. For example, using the same computation as before, and the labelling $F_1(X)$ for $T_0$ and If $X>0$ THEN $X-1$ ELSE $F_2(F_3(X+2))$ for P, the previous computation can be described as :

$$F_1(0) \to F_12(F_{13}(2)) \to IF F_{13}(2) > 0 \text{ THEN } F_{13}(2)-1 \text{ ELSE } F_{122}(F_{123}(F_{13}(2)+1)) \to F_{13}(2)-1 \to 0.$$

The whole idea of the delay-rule is to modify "call-by-name" so that, whenever some occurrence of F is substituted, all the occurrences having the same label will also be substituted. Hence, the "delay-rule" selects for substitution the leftmost-outermost F in a simplified term, as well as all the other F's having the same label.

Consequently, the delay rule computation of $F(0)$ in the program above is

$$F_1(0) \to F_{12}(F_{11}(2)) \to IF F_{11}(2) > 0 \text{ THEN } F_{11}(2)-1 \text{ ELSE } F_{122}(F_{121}(F_{11}(2)+1)) \to 0.$$

At this point, it is clear that the "delay rule" is safe (proof similar to that of Proposition 1); what is not clear is that the "delay rule" should be more efficient than "call-by-name" and in fact, in our last example, it was less efficient since it took four substitutions versus three for "call-by-name" in order to obtain its result. When "call-by-name" computed $F_{11}(2)$ twice, the delay rule has been computing it three times! It is a simple exercise in data structuring however to avoid all those recomputations : instead of actually copying various occurrences of some $F_\alpha$ in a term, we simply set some pointers to a unique copy of the term $F_\alpha$. Whenever any occurrence of $F_\alpha$ is chosen for substitution, the substitution is actually performed in the unique copy of $F_\alpha$ so that <u>all</u> occurrences of $F_\alpha$ are substituted at the price of one substitution.
Going a little bit away from our particular programming language we can sketch an implementation of this idea for, say Algol. The arguments of any procedure should be stored as pointers to formal expressions, together with a tag indicating that those arguments have not yet been computed. Whenever the value of an argument is explicitly needed, (for the evaluation of a conditional or on the right-hand side of an assignment), the tag is tested. If the value of the parameter is already there, we use it; otherwise the corresponding formal expression must be computed, its value kept for further references, and the tag is to be changed. In a machine like the Burroughs B5000 (see, for example, Lonergan-King [3]), the so-called "operand call syllabe" would do very nicely: depending on a tag stored with the operand, a load operation for example would get its argument either directly or through a subroutine call. Of course, one would then have to abandon "side-effects" altogether !

Before proving the optimality of the delay rule let us compare the efficiency of various computation rules on the programs

$$
\begin{align*}
\text{Zer}(X) &\leftarrow \text{IF } X>0 \text{ THEN } X-1 \text{ ELSE } \text{Zer}(\text{Zer}(X+2)) \\
\text{Ack}(X,Y) &\leftarrow \text{IF } X=0 \text{ THEN } Y+1 \\
&\phantom{\leftarrow \text{IF }} \text{ELSE } \text{IF } Y=0 \text{ THEN } \text{Ack}(X-1,1) \\
&\phantom{\leftarrow \text{IF }} \text{ELSE } \text{Ack}(X-1,\text{Ack}(X,Y-1)) \\
\text{Ble}(X,Y) &\leftarrow \text{IF } X=0 \text{ THEN } 1 \text{ ELSE } \text{Ble}(X-1,\text{Ble}(X-Y,Y)) \\
\text{Fib}(X) &\leftarrow \text{IF } X<2 \text{ THEN } X \text{ ELSE } \text{Fib}(X-1)+\text{Fib}(X-2)
\end{align*}
$$

over the integers.

<table><thead><tr><th></th><th>Zer(-2)</th><th>Ack(2,1)</th><th>Ble(8,2)</th><th>Fib(5)</th></tr></thead><tbody><tr><td>Delay rule</td><td>7</td><td>14</td><td>9</td><td>15</td></tr><tr><td>Call by name</td><td>25</td><td>29</td><td>9</td><td>15</td></tr><tr><td>Call by value</td><td>7</td><td>14</td><td>341</td><td>15</td></tr><tr><td>Free argument</td><td>7</td><td>23</td><td>~ 4000</td><td>15</td></tr><tr><td>Full substitution*</td><td>11</td><td>23</td><td>~ 10000</td><td>15</td></tr></tbody></table>

(*Strictly speaking, we are using the full substitution only on simplified terms, otherwise the computation would always be infinite.)

The entries in this array indicate the number of substitutions required for computing the values at the top of the corresponding column, according to the rules at the left of the rows.

If he has been through those examples, the reader may feel quite disappointed because he can beat the delay-rule in almost all cases. For example, the hand-computation of Fib(5) only requires five substitutions if we are careful never to recompute an argument twice. It would be interesting to study a mechanism in which this type of computation would be possible; namely one could imagine a set of simplification rules which could be augmented dynamically, and allow some computations to be performed by simplifications of the style $F(\bar{D}) \to A$. In our scheme of things, however, this type of "built-in" values is not possible, since our only mean of computation is through substitutions, and we should blame inefficiencies on the program, not on the computation rule.
### 3.2. Optimality of the Delay rule

So far, we know that the normal rule is safe, and that it never recomputes copies of the same term. Using the same labelling as before, we say that a label $F_\alpha$ is maximal in a term if $\alpha$ is not a proper initial segment of $\beta$ for any label $F_\beta$ in the term. A term is simple if all of its labels are maximal. In other words, a term is simple if all computations of various copies of subterms have been pushed to the same point. For example, if $P = F_2(F_1(X))$ and $T_0 = G(X, F_4(F_3(X)))$ then $C(G(X, F_{14}(F_{13}(X))), F_{24}(F_{23}(F_1(X)))))$ is not simple while $F_2(G(X, F_{14}(F_{13}(X))))$ is simple.
A computation is simple if all $F'_s$ with the same labels are all treated alike in all substitutions (if one of them is to be substituted, all of them are to be substituted). All terms in a simple computation are necessarily simple. If we are to count for one a substitution of all $F'_s$ with the same labels, as justified by our previous exercise in data structuring, simple computations are more efficient than others. Namely, if we define $\text{length}(T_0 \xrightarrow{\star} A)$ as the total number of substitutions performed during the computation $T_0 \xrightarrow{\star} A$, we have

**Lemma E**

For any term $A$, there exists a simple term $\bar{A}$ with $A < \bar{A}$ such that, for any computation $T_0 \xrightarrow{\star} A$ and simple computation $T_0 \xrightarrow{\star} \bar{A}$, $\text{length}(T_0 \xrightarrow{\star} \bar{A}) < \text{length}(T_0 \xrightarrow{\star} A)$.

**Proof.** Let $r(Q)$ be the number of maximal labels and $s(Q)$ be the sum of the lengths of the maximal labels in a term $Q$, while $q$ and $p$ mean respectively the number of occurrences of $F$ in $T_0$ and $P$. It is easily proven by induction on length ($T_0 \xrightarrow{\star} Q$) that $\text{length}(T_0 \xrightarrow{\star} Q) \ge \varphi(Q,p,q)$ where $\varphi(Q,p,q) = \text{if } p=1 \text{ then } \frac{s(Q)}{q} \text{ else } \frac{r(Q)-q}{p-1}$. In a similar way, ($Q$ simple) and ($T_0 \xrightarrow{\star} Q$ simple) imply $\text{length}(T_0 \xrightarrow{\star} Q) = \varphi(Q,p,q)$.

Given any term $A$, we can "complete" it into an $\bar{A}$ by substituting $P$ for all occurrences of $F$ with non-maximal labels until there is none left. An $\bar{A}$ constructed in this way will be simple and such that $A < \bar{A}$ while $r(A) = r(\bar{A})$. It follows that, for any computation $T_0 \xrightarrow{\star} A$ and simple computation $T_0 \xrightarrow{\star} \bar{A}$, $\text{length}(T_0 \xrightarrow{\star} \bar{A}) = \varphi(\bar{A},p,q) = \varphi(A,p,q) \le \text{length}(T_0 \xrightarrow{\star} A)$. $\square$

The intuitive meaning of this lemma is very simple : nothing is to be gained by working on individual copies of the same term. At the same price, we get more information by substituting all copies of the same occurrences. In particular, all the computation rules described so far will be improved by "lumping" together occurrences of $F$ with the same labels, thus becoming simple rules. However they may still perform unnecessary substitutions unless :

**Theorem 4**

Any computation rule which is simple, safe and performs at most one substitution at each computation step is optimal.
**Proof.** Let $T_0$ be a term, $F(\bar{X}) \Leftarrow P$ a program and $\mathcal{E}$ a safe and simple computation rule performing only one substitution at a time. Let $T_0 \stackrel{*}{\Rightarrow} T_1 \Rightarrow \dots \Rightarrow T_n \Rightarrow \overline{T}_{n+1} \Rightarrow \dots$ the (simple) computation sequence of $T_0$ according to $\mathcal{E}$ for some input $\bar{D}$.

If $T$ is a term in the computation lattice of $T_0$ by $P$, let us consider an arbitrary computation $T_0 \stackrel{*}{\Rightarrow} T$, and prove that whatever approximation $t(\Omega)(\bar{d})$ of $T_0(f_p)(\bar{d})$ is computed by $T$ will be computed **faster** by $C$. For this purpose, we construct $\overline{T}$ as in Lemma E, and consider a simple computation $T_0 \stackrel{*}{\Rightarrow} \overline{T}$ (the argument in Lemma E not only proves the existence of $\overline{T}$ but also that of a simple computation $T_0 \stackrel{*}{\Rightarrow} \overline{T}$).

Let $i$ be some natural number such that $T_i \le T$ and $T_{i+1} \le \overline{T}$. Since $\mathcal{E}$ performs only one substitution at the time, this implies $T_i = \min(T_{i+1}, \overline{T}) = \min(T_i, \overline{T})$. By Lemma S, we then know that $\overline{t}(\Omega)(\bar{d}) \subseteq t_i(\Omega)(\bar{d})$. Using Lemmas E and C now, $T \le \overline{T}$ implies $t(\Omega)(\bar{d}) \subseteq \overline{t}(\Omega)(\bar{d})$ and $\text{length}(T_0 \stackrel{*}{\Rightarrow} \overline{T}) < \text{length}(T_0 \stackrel{*}{\Rightarrow} T)$. Since both $T_0 \stackrel{*}{\Rightarrow} \overline{T}$ and $T \stackrel{*}{\Rightarrow} T_i$ are simple and $T_i \le \overline{T}$, we have $\text{length}(T_0 \stackrel{*}{\Rightarrow} T_i) < \text{length}(T_0 \stackrel{*}{\Rightarrow} \overline{T})$ hence $t(\Omega)(d) \subseteq t_i(\Omega)(d)$ while $\text{length}(T_0 \stackrel{*}{\Rightarrow} T_i) < \text{length}(T_0 \Rightarrow T)$. $\square$

We shall derive two applications of this theorem.

**Corollary 1**

The delay rule is optimal in lang S.

**Proof.** The delay rule has all the properties required by Theorem 4. $\square$

**Corollary 2**

In lang S, "call by value" is optimal whenever the least fixed-point $f_p$ corresponding to the program $F(\bar{X}) \Leftarrow P$ is a strict function

**Proof.** Since "call by value" is clearly a simple rule and performs at most one substitution at each step, we only need proving that it is safe whenever $f_p$ is strict. We prove that the substitution $B \rightarrow B'$ is safe in that case by induction on $||C||$ where $C = \text{simpl}(B)$ :

Case $C = A_i$. Any rule is safe.

Case $C = G_i(C_1, \dots, C_{p_i})$. Same argument as for the safeness of "call by name".

Case $C = F(C_1, \dots, C_n)$. If $F$ does not occur in any of the $C_i$'s, then the outermost substitution is performed, which is clearly safe. Otherwise, let $C_i$ be the leftmost term in which $F$ occurs. Then, $C_i\{\Omega/f_1, f_p/f_2\}(d) \equiv \omega$ and $C\{\Omega/f_1, f_p/f_2\}(\bar{d}) \equiv f_p(..., \omega, ...)(\bar{d}) \equiv \omega \equiv C\{\Omega/f_1, \Omega/f_2\}(\bar{d})$. $\square$
### 3.3. Sequential Functions

The applications of Theorem 4 given in the previous section do not quite match with the generality of the result. In particular, the data-type on which lang S is computing has no chain of length more than two. What we shall now sketch is a theory of sequential functions, where Theorem 4 finds its full application.

The relevant notion here seems to be:

**Definition**

A function $\lambda x_1, \dots, x_n \cdot g(x_1, \dots, x_n)$ in $[\mathcal{D}_1 x \dots x \mathcal{D}_n \to \mathcal{D}]$ is sequential if, for all $x_1 \in \mathcal{D}_1, \dots, x_n \in \mathcal{D}_n$ there exists an $i \in [1, n]$ such that, for all $y_1, \dots, y_n$ such that $x_j \subseteq y_j$ for $j \in [1, n]$ and $x_i \equiv y_i$ we have $g(x_1, \dots, x_n) \equiv \varepsilon(y_1, \dots, y_n)$.

Intuitively, $g$ is sequential if, at any given moment, the value of (at least) one of its arguments is crucially needed in order to increase the value of the result. For the purpose of our theory, we need to check that sequentiality has the correct closure property, namely

**Proposition S**

Sequentiality is preserved by composition of functions and fixed-point operators.

**Proof**

- **Composition**. If $\lambda z_1, \dots, z_n g(z_1, \dots, z_n)$ and $\lambda x_1, \dots, x_n f_i(x_1, \dots, x_n)$ for $1 \le i \le n$ are sequential, then $\varphi \equiv \lambda x_1, \dots, x_n g(f_1(x_1, \dots, x_m), \dots, f_m(x_1, \dots, x_m))$ is also sequential : for any $x_1, \dots, x_m$ and $i \in [1, n]$, let $z_i \equiv f_i(x_1, \dots, x_m)$; since $g$ is sequential $z_1, \dots, z_n$ determines some $i_0 \in [1, n]$ and, $f_{i_0}$ being also sequential, $x_1, \dots, x_m$ determine some $j \in [1, m]$ which can then be used for the sequentiality of $\varphi$.

- **Fixed-point operator**. If the functions $\lambda x_1, \dots, x_n f_i(x_1, \dots, x_n)$ are sequential for any natural number $i$, the function $\varphi \equiv \lambda x_1, \dots, x_n \sqcup f_i(x_1, \dots, x_n)$ is also sequential : for any $x_1, \dots, x_n$ sequentiality of the $f_i$'s determines a sequence $j_0, j_1, \dots$ where $j_i \in [1, n]$. At least one of the $j_i$'s must occur infinitely often in this sequence, and it can be used for proving that $\varphi$ is sequential. $\square$

For example, over a discrete data-type, conditional and strict functions are sequential; hence, by Proposition S, all functions definable in lang S are sequential.

In a data-type which is a lattice, the functions, $\lambda x, y \sup(x, y)$ and $\lambda x, y \inf(x, y)$ are not sequential in general.

The set $\Sigma^\omega$ of finite or infinite words over some vocabulary $\Sigma$ becomes a data-type under the partial ordering : $x \subseteq y$ whenever $x$ is an initial segment of $y$.
In $Σ^ω$, the functions

$λx.first(x)$ (take the first letter of x),

$λx.first(x)$ (erase the first letter of x),

and $λx,y,x \otimes y$ (append the first letter of x to y) are sequential.

(The relevance of these functions and data-type to parallel programs is shown in Kahn [2].)

This is clear enough for first and rest. For $x \otimes y$, if $x \equiv \Lambda$, i.e., $x$ is the empty word, then the first argument is to be chosen for sequentiality; otherwise, $x \not\equiv \Lambda$ and any $x'$ such that $x \sqsubseteq x'$ will have the same first letter so that we can use the other argument $y$ for sequentiality.

- *Yet another programming language.* We define a new language *lang GS* similar to our previous ones except that all base functions must be sequential.

Let $\mathcal{E}$ be a computation rule, called the generalized delay rule (GDR) defined as follows:

First, using the same type of data-structuring as for the delay rule, $\mathcal{E}$ will be simple.

In any term $T$, rule $\mathcal{E}$ will select at most one $F$ (or rather set of $F$'s with the same labels), as follows:

If $T = A_i$, no $F$ is chosen.

If $T = G_i(T_1, \dots, T_{p_i})$, the $F$ will be the $F$ chosen by $\mathcal{E}$ in $T_j$ where $j$ is the index corresponding to the sequentiality of $g_i$ with the arguments $t_1(\Omega)(\bar{d}), \dots, t_{p_i}(\Omega)(\bar{d})$. Of course, this requires the choice of $j$ to be effective; also, since we want $\mathcal{E}$ to be simple, all $F$'s with the same labels occuring in other subterms are also to be substituted.

If $T = F(T_1, \dots, T_n)$ the outermost $F$ is selected by $\mathcal{E}$.

We can apply Theorem 4 again in order to prove.

### Corollary 3

*The generalized delay rule is optimal in lang GS.*

*Proof.* Since the GDR is simple and performs at most one substitution at each step, all we need to prove is that it is safe. The proof is by induction on $||B||$ where $B$ is any term in the computation lattice of $T_0 = T\{\bar{D}/\bar{X}\}$ by P.

The cases $B = A_i$ of $B = F(B_1, \dots, B_n)$ are easy.

If $B = G_i(B_1, \dots, B_{p_i})$ and $j$ is the sequentiality index of $g_i(b_1(\Omega)(d), \dots, b_{p_i}(\Omega)(\bar{d}))$, then $b_j(\Omega/f_1, f_p/f_2)(\bar{d}) = b_j(\Omega)(\bar{d})$ by induction. Since $b_k(\Omega)(\bar{d}) \sqsubseteq b_k(\Omega/f_1, f_p/f_2)(\bar{d})$, the very definition of sequentiality gives us $b\{\Omega/f_1, f_p/f_2\}(\bar{d}) = b\{\Omega/f_1, \Omega/f_2\}(\bar{d})$.

### Conclusion

The results of this chapter generalize quite nicely to a programming language where we introduce assignments, goto's and while statements. What is less clear to the author is how to perform computation in a "typeless" recursive language where procedures can be passed as arguments, say in a full LISP for example. It might also be interesting to study (or prove
the non-existence of) optimal computation rules when the simplifications allowed are less
restrictive than the ones we chose.

***Acknowledgments.*** We are grateful to Donald Knuth whose criticism on an earlier draft led to many fruitful improvements. Jean-Marie Cadiou contributed greatly to the proof of Theorem 1.

References

[1] J.M. CADIOU "Recursive Definitions of Partial Functions and Their computations", Ph. D. Thesis, Computer Science Department, Stanford University (1972).

[2] G. KAHN "A preliminary theory of parallel programs", Rapport LABORIA, IRIA, 78-Rocquencourt, France (1973).

[3] W. LONERGAN and P. KING "Design of the B5000 System", Datamation, Vol. 7, No. 5, (May 1961). 28-32.

[4] J.H. MORRIS "Lambda-Calculus Models of Programming Languages", Report MAC-TR-57, Mass. Inst. of Technology (1968).

[5] B.K. ROSEN "Tree-Manipulating Systems and Church-Rosser Theorems", J. ACM, Vol. 20, No. 1, (1973), 160-187.

[6] D. SCOTT "Outline of a Mathematical Theory of Computation", Oxford Mono. PRG-2, Oxford University (1970).