# Call by need computations in non-ambiguous linear term rewriting systems

Gérard Huet, Jean-Jacques Levy

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

## To cite this version:

Gérard Huet, Jean-Jacques Levy. Call by need computations in non-ambiguous linear term rewriting systems. [Research Report] IRIA-RR-359, IRIA. 1979, pp.57. hal-04716618

HAL Id: hal-04716618

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

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

Institut de Recherche
d'Informatique
et d'Automatique

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

laboratoire de recherche
en informatique
et automatique

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

CALL BY NEED
COMPUTATIONS
IN NON-AMBIGUOUS
LINEAR TERM
REWRITING SYSTEMS

ARCHIVES

Gérard HUET
Jean-Jacques LEVY

Rapport de Recherche N° 359

Août 1979

STP.
CALL BY NEED COMPUTATIONS IN NON-AMBIGUOUS LINEAR TERM
REWRITING SYSTEMS

Gérard Huet, Jean-Jacques Levy

IRIA/LABORIA

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

Résumé :

On étudie la structure des calculs dans les règles de réécriture de termes non superposables. A l'aide d'une étude algébrique sur la structure de treillis des dériva\^tions, on démontre un théorème de standardisation qui généralise la règle de calcul d'appel par nom dans les schémas de programmes récursifs. Mais ici cette règle ne correspond pas à une simple interprétation en préordre, et en fait n'est pas effective. Nous introduisons la notion de systèmes séquentiels, pour lesquels on peut calculer sans avoir à simuler des calculs futurs. Finalement nous définissons les systèmes fortement séquentiels, pour lesquels il existe un interpréteur séquentiel effectif. Cet interpréteur est très efficace, et étend aux arbres l'algorithme linéaire de recherche de motif dans les chaînes de caractères.

Notre travail est une première étape vers une théorie générale de la méta-compilation des langages de programmation.

Abstract :

We study the structure of computations by tree rewrite rules which do not overlap. Using a semi-lattice structure of the space of derivations, we prove a standardization theorem that generalizes the well-known call by name computation rule of recursive program schemes. However this rule, which does not correspond here to leftmost-outermost interpretation, is not effective. We introduce the notion of sequential systems, in which it is possible to compute without look-ahead. Finally we define strongly sequential systems, for which an effective sequential interpreter exists. This interpreter is very efficient, relying on an extension to trees of the linear string pattern matching algorithm.

Our work is a first attempt towards a general theory of meta-compilation of programming lan-
guages.
Introduction

We present in this paper a study of derivations which formalize the computa-
tions of expressions in programming languages. Our formalism extends recursive pro-
grams with simplifications in [16, 21, 7, 30, 25, 27, 10, 3]. It permits to provide
an operational semantics to programming languages such as NPL [5]. The derivations
we study may also be considered as proofs in certain equational theories which are
of use to study abstract data types [12, 24, 7]. Finally, our work may be used for
the design of efficient simplifications in formula manipulation systems such as
LCF [22].

The results of this paper may be sketched as follows. We consider systems of
pairs of first-order terms : Σ = {αᵢ → βᵢ | i ≤ n}. Computations consist in rewriting an
occurrence of some instance of an αᵢ into the same instance of βᵢ. We impose to
every rule αᵢ → βᵢ that variables of βᵢ occur in αᵢ and that every variable of αᵢ has
a unique occurrence in αᵢ. Furthermore, no two rules of Σ are non-trivially superpo-
sable. We believe that most computations in programming languages without parallelism
can be formalized in this setting.

Section one contains the preliminary definitions. In section two, we show
how the parallel moves lemma induces a congruence ("permutation") on derivations
issued from a given term. The usual notion of residuals of a redex is extended to
derivations, yielding a sup-semi lattice structure to the permutation classes of
derivations. This generalizes Church-Rosser results from [28, 14, 26]. In section
three we define the notion of a redex occurrence being external for a given deriva-
tion. This notion is invariant by permutation, and every non-empty derivation pos-
sesses at least one external redex occurrence. This permits us to define the notion
of a standard derivation, and we show that every derivation class contains a unique
standard derivation. We finally define the notion of a redex occurrence being
external in a given term, which yields the notion of the normal derivation issued
from a given term. When the term possesses a normal form, the normal derivation
terminates in this normal form. This may be considered as an extension to our
systems of the call by name computation rule for recursive program schemas, and
of the normal derivations in λ-calculus. However, our formalism differs in
essential ways from these two, because of the possibility of upward creation of
redexes, and our call by name rule does not correspond to a simple leftmost-outer-
most strategy of computation. The results imply that all the non-ambiguous linear
term rewriting systems are d-outer in the sense of O'Donnell [26]. The existence
of normal derivations entails the possibility of doing only needed computations in
a top-down manner. However it does not correspond to an effective computation
rule, and at this stage the only correct effective interpreters use parallel strategies such as parallel outermost.

The next problem we address is the definition of sequential interpreters for our systems. Using a sequentiality criterion derived from the semantic notion of sequentiality in concrete data types [15], we characterize an important subclass of our systems, which admit a correct sequential strategy of interpretation. Intuitively, $Σ$ is sequential iff it is possible to compute in call by need without doing some look-ahead. That is, for any term $M$ not in normal form, there exists a place in $M$ which we need to compute in order to get to the normal form of $M$ (if any), and furthermore we can determine this place without looking at the subparts of $M$ which are not computed yet. Unfortunately, it is undecidable in general whether $Σ$ is sequential or not.

We finally consider a restriction of sequential systems which allows us to define an effective sequential strategy. Intuitively, a system $Σ$ is strongly sequential if the computation effected to determine the needed positions is independent of the right hand sides of $Σ$. For a strongly sequential system $Σ$ it is possible to represent the left hand sides of $Σ$ in a trie structure which we call matching dag. The computation of the needed subpart, together with the actual pattern-matching of the left-hand sides, is driven by the matching dag. We show that this computation is linear in the size of the term we compute on, extending to trees the technique of the Knuth-Morris-Pratt string pattern matching algorithm. Our technique use a new notion of top-down tree automaton with a markers stack.

Strong sequentiality is decidable, and is verified easily in many important subcases, under which fall for instance combinatory logic, primitive recursive schemes and recursive programming languages with constructors such as NPL [5].

We believe our paper is a first attempt towards a general theory of interpreters for programming languages. More powerful languages could be dealt with, firstly by introducing block structure (i.e. $λ$-calculus), secondly by adding imperative constructs. Most of our essential concepts are adaptations to syntactic domains of denotational semantics notions. This algebraic approach permits us to state and prove our theorems in an abstract fashion, suggesting that our results can be extended to a more general theory of meta-compilation.

# 1 Preliminary definitions

We follow here the notations of Huet [14] and Berry-Lévy [3]. Let $F_n$ be a set of function symbols of arity $n$, $F = \cup\{F_n | n \ge 0\}$, $V$ be a denumerable set of variable symbols. Our expression language is the set $M(F, V)$ of first-order terms formed from $F$ and $V$, i.e. :

$$ (1) \quad V \in M(F, V) $$

$$ (ii) \quad F \in F_n \quad \& \quad \forall i \le n \quad M_i \in M(F, V) \Rightarrow F(M_1, M_2, \dots, M_n) \in M(F, V). $$
When $F$ and $V$ are fixed from the context, we shall usually denote $M(F,V)$ by $T$.

For any term $M$, we define the set of occurrences $O(M)$ as a finite subset of $N_+^*$ as follows :

(i) $\Lambda \in O(M)$ (the empty occurrence)

(ii) $u \in O(M_i) \Rightarrow i \in O(F(M_1, M_2, \dots, M_n))$ for $1 \le i \le n$

We shall also use the notation : $\bar{O}(M) = \{u \in O(M) | M/u \notin V\}$.

If $u \in O(M)$, we define the *subterm of $M$ at $u$* as the term $M/u$, and, for every $M'$, the *replacement in $M$ of $M'$ at $u$* as the term $M[u \leftrightarrow M']$, such that :

(i) $M/\Lambda = M$

(ii) $F(M_1, M_2, \dots, M_n)/iu = M_i/u$

(iii) $M[\Lambda \leftrightarrow M'] = M'$

(iv) $F(M_1, M_2, \dots, M_n) [iu \leftrightarrow M'] = F(M_1, M_2, \dots, M_i [u \leftrightarrow M'], \dots, M_n)$.

The set of occurrences $O(M)$ is partially ordered by the prefix ordering : $u \le v$ iff $\exists w \ uw=v$. In this case, we shall define $v/u$ as $w$. If $u \not\le v$ and $v \not\le u$, we say that $u$ and $v$ are *disjoint*, and write $u|v$. Finally $u \not\le v$ iff $u \le v$ and $u \not\le v$.

We call *substitution* any term morphism $\sigma$ :

$$ \sigma(F(M_1, M_2, \dots, M_n)) = F(\sigma(M_1), \sigma(M_2), \dots, \sigma(M_n)). $$

We call *term rewriting system* (abbreviated TRS) any set $\Sigma$ of pairs of terms $\alpha_i \to \beta_i$ such that $V(\beta_i) \subseteq V(\alpha_i)$, where $V(M)$ is the set of variables appearing in $M$. We denote by $red_\Sigma$ the set of left-hand sides $\alpha_i$ of $\Sigma$, which we call *redex schemes*. For any substitution $\sigma$ and $\alpha \in red_\Sigma$, $\sigma(\alpha)$ is called a *redex of $\Sigma$*. We denote by $R_\Sigma(M)$ the set of redex occurrences in the term $M$. A term $M$ such that $R_\Sigma(M)=\emptyset$ is called a *$\Sigma$-normal form*. We denote by $NF_\Sigma$ the set of terms in normal form.

From now on, we shall assume that TRS $\Sigma$ is fixed, and therefore drop the subscript $\Sigma$ except when needed.

We say that the term $M$ *reduces* to $N$ at occurrence $u$ using rule $\alpha_k \to \beta_k$ iff there exists a substitution $\sigma$ such that $M/u = \sigma(\alpha_k)$ and $N = M[u \leftrightarrow \sigma(\beta_k)]$. The pair $A = \langle M, u \rangle$ is called an *elementary derivation*, and we shall write $A : M \xrightarrow{k} N$. In this notation, $k$, $u$ or $A$ may be omitted.
A *derivation* is a sequence $A = A_1 A_2 \cdots A_n$ of elementary derivations
$A_i : M_i \to M_{i+1}$. We use AB for the concatenation of A and B, O for the empty deriva-
tion, and $|A|$ for the length of derivation A. We shall use the notation $A : M \stackrel{*}{\to} N$
to indicate that derivation A starts in M and ends in N.

Let $U = \{u_1, u_2, \dots, u_n\}$ be a set of mutually disjoint redex occurrences in
term $M$, let $M/u_i = \sigma(\alpha_i)$. We call *elementary multiderivation* the pair $A = \langle M, U \rangle$
and write $A : M \stackrel{U}{\to} N$ where

$N=M[u_i \leftarrow \sigma_i(\beta_i) | 1 \le i \le n] = M[u_1 \leftarrow \sigma_1(\beta_1)] \cdots [u_n \leftarrow \sigma_n(\beta_n)]$
(Of course the order of the $u_i$'s is irrelevant.)

We define *multiderivations* in the same way and use the same notation as for derivations. Furthermore, if we want to emphasize the system Σ we use, we can write $M_{\Sigma}^{*}N$. We denote $\mathcal{D}(M)$ the set of multiderivations issued from M, and $F(A)$ the final term reached by the (multi) derivation A. We say that A and B are *coinitial* if $A, B \in \mathcal{D}(M)$, *cofinal* if $F(A) = F(B)$. The notation AB, for the concatenation of A and B, assumes that $B \in \mathcal{D}(F(A))$. Concatenation being associative, we write ABC for $(AB)C$ or $A(BC)$. Every set $\mathcal{D}(M)$ contains an empty multiderivation which we shall denote 0, the term M being usually understood from the context. Thus we write freely $AO=OA=A$.

When considering a derivation $A : M_0 \xrightarrow{u_1} M_1 \xrightarrow{u_2} M_2 \cdots \xrightarrow{u_n} M_n$

it is convenient to denote by $A[i]$ the $i$ first steps of $A$, with $0 \le i \le n$. The rest of $A$ is denoted $A[i,n]$. Thus $A=A[i]A[i,n]$ with $M_i$ as the final term of $A[i]$. Similarly for multiderivations.

We shall study in this paper the properties of derivations in TRS's which
have two constraints :

(1) *Left linearity* : for every $\alpha$ in red , every variable of $\alpha$ occurs only once : $\alpha/u = \alpha/v \in V \Rightarrow u=v$.

(2) *Non ambiguity* : if $\alpha_i, \alpha_j \in \text{red}$ , for every $u$ in $\bar{\sigma}(\alpha_i)$ there are no $\sigma, \sigma'$ such that $\sigma(\alpha_i/u) = \sigma'(\alpha_j)$.
We also rule out the trivial TRS's which have just one rule $\alpha \to \beta$, with $\alpha \in V$. Therefore, we have $red_n V = \emptyset$ by condition (2).

Our TRS's are similar to the schematic tree replacement systems of Rosen [28] and O'Donnell [26]. Condition 2 is called the nonoverlapping condition in these papers. Note that 1 and 2 imply together that our systems are outer, in the terminology of [26]. In the terminology of Knuth-Bendix [18], there is no critical pair. The derivation relation $\to$ is confluent (has the Church-Rosser property) [14,28]. We shall study in this paper some stronger properties of derivation spaces, generalizing results in Berry-Lévy obtained for recursive equations.

## 2. The derivations space

In this section, we prove an important property of derivations in TRS's, the parallel moves lemma (see Curry & Feys [9]). This allows us to define a partial ordering on derivations, inducing a semi-lattice property on derivation spaces. This useful tool generalizes the one defined in Berry-Lévy [3], which can also be defined in the $\lambda$-calculus (Lévy [20]).

**Definitions**: If $A: M_k^u N$ is an elementary derivation and $v \in R(M)$, then we define the set of residuals of $v$ by $A$ as $v \setminus A \subset O(N)$, where :

$$ v\setminus A = \begin{cases} \emptyset & \text{if } v=u \\ \{v\} & \text{if } v|u \text{ or } v<u \\ \{uw_1v_1 | \beta_k/w_1=x\} & \text{if } v=uw_1v_1 \text{ and } \alpha_k/w=x \in V \end{cases} $$

All the relative positions of $u$ and $v$ have been considered, because of the non ambiguity condition, which together with left linearity implies $v\setminus A \subset R(N)$. If $w \in R(N)$ and $w \in v\setminus A$, then $v$ is unique. When $w \in R(N)$ and $\nexists v w \in v\setminus A$, we say that $w$ is created by $A$.

For any non elementary derivation $A$, we define $v\setminus A$ by

$$ \begin{cases} v\setminus O = \{v\} \\ v\setminus (AB) = \{w\setminus B | w \in v\setminus A\} \end{cases} $$

The residual mapping is extended to sets of redex occurrences by defining

$$ U\setminus A = U\{u\setminus A | u \in U\}. $$
Finally, if $A$ is an elementary multiderivation $A : M \xrightarrow{U} N$ with
$U = \{u_1, u_2, \dots, u_n\}$, we define $v\setminus A$ as $v\setminus (A_1A_2\dots A_n)$ where $A_i : M_i \xrightarrow{u_i} M_i, M_0=M$
and $M_n=N$. Of course $v\setminus A$ is independent of the order of the $u_i$'s. We extend $v\setminus A$ to
non elementary multiderivations, and to sets of redex occurrences, as above.

Let $A,B \in \mathcal{D}(M)$, with $|B|=1$, contracting the set $U \subset \mathcal{R}(M)$. We define the *residual*
$B \setminus A$ of $B$ by $A$ as the elementary derivation in $\mathcal{D}(F(A))$ contracting the set $U \setminus A$. We
define also $A \cup B = A(B \setminus A)$.

**Lemma 2.1** (The parallel moves lemma)

Let $A,B \in \mathcal{D}(M)$, with $|A|=|B|=1$. Then $F(AB) = F(BA)$ and, for all $u$ in $R(M)$,
we have $u(AB) = u(BA)$.

**Proof :** Similar to the proof of theorem 6.5 in [25], lemma 11 in [14], lemma 2.1.6 in [3]. $\square$

**Corollary :** (The Church-Rosser property). Since $|B\setminus A| = |A\setminus B| = 1$, lemma 2.1 shows that the multiderivation relation is strongly confluent (see [14]) and therefore that the relation $\to$ is confluent. Therefore, for every $M$, there is at most one normal form $N$ such that $M \stackrel{*}{\to} N$.

The parallel moves lemma permits us to generalize the residual relation to
arbitrary derivations, as follows.

**Definition**

Let $A,B \in \mathcal{D}(M)$, with $|B|=1$. We define $A\setminus B \in \mathcal{D}(F(B))$ by induction on $|A|$:

$$ \bullet \quad 0\setminus B=0 \qquad (1) $$

$$ \bullet \quad (A_1A_2)\setminus B = (A_1\setminus B)(A_2\setminus (B\setminus A_1)) \quad \text{with } |A_1|=1 \qquad (2) $$

Remark that $A_2\setminus (B\setminus A_1)$ is defined by induction, since $|B\setminus A_1|=1$, and that it
can be concatenated to $A_1\setminus B$, by the preceding lemma. Now, for $A,B \in \mathcal{D}(M)$ of arbitrary
lengths, we define $A\setminus B \in \mathcal{D}(F(B))$ by induction on $|B|$:

$$ \bullet \quad A\setminus 0 = A \qquad (3) $$

$$ \bullet \quad A\setminus(B_1B_2) = (A\setminus B_1)\setminus B_2 \quad \text{with } |B_1|=1 \qquad (4) $$
We also extend the notation $A\cup B = A(B\setminus A)$. It is easy to show by induction that $|A\cup B| = |A|$, that equations (1), (2), (3) and (4) are valid without length conditions, and to generalize the parallel moves lemma :

**Lemma 2.2** (The generalized parallel moves lemma)

For all $A, B \in \mathcal{D}(M)$ we have $F(A\cup B) = F(B\cup A)$ and, for all $u$ in $R(M)$ : $u\setminus(A\cup B) = u\setminus(B\cup A)$.

The last part of lemma 2.2 can be generalized to an arbitrary multiderivation coinitial with A and B, as follows.

**Lemma 2.3** (The cube lemma)

For all $A, B, C \in \mathcal{D}(M)$ we have $C\setminus(A\cup B) = C\setminus(B\cup A)$.

*Proof* : By induction on $|A| + |B| + |C|$.

If $C=0$, use (1) ; otherwise, let $C=C_1C_2$ with $|C_2|=1$.

$$ \text{We get } (A\cup B)\setminus C_1 = (A\setminus C_1)((B\setminus A)\setminus(C_1\setminus A)) \quad \text{by (2)} $$

$$ = (A\setminus C_1)(B\setminus (A\cup C_1)) \quad \text{by (4)} $$

$$ = (A\setminus C_1)(B\setminus (C_1\cup A)) \quad \text{by ind.hyp.} $$

$$ = (A\setminus C_1)((B\setminus C_1)\setminus(A\setminus C_1)) \quad \text{by (4)} $$

$$ = (A\setminus C_1)\sqcup(B\setminus C_1). $$

$$ \begin{align*} \text{Thus } C_2\setminus((A\cup B)\setminus C_1) &= C_2\setminus((A\setminus C_1)\sqcup(B\setminus C_1)) \\ &= C_2\setminus((B\setminus C_1)\sqcup(A\setminus C_1)) \quad \text{by lemma 2.2} \\ &= C_2\setminus((B\cup A)\setminus C_1) \quad \text{symetrically.} \end{align*} $$

Finally $C_1\setminus(A\cup B) = C_1\setminus(B\cup A)$ by ind. hyp., which achieves the proof, using (2). $\square$

It we now define, for $A, B \in \mathcal{D}(M)$, $A \equiv B$ iff for all $C \in \mathcal{D}(M)$ $C\setminus A = C\setminus B$, we get :

**Corollary** : $\forall A, B \in \mathcal{D}(M) \ A\cup B = B\cup A$.

We shall call relation $\equiv$ the *permutation equivalence*.
**Lemma 2.4** (Ł is associative)

$$ \forall A,B,C \in \mathcal{D}(M) \quad (A \cup B) \cup C = A \cup (B \cup C) $$

**Proof :**

$$ \begin{align*} (A \cup B) \cup C &= (A \cup B)(C \setminus (A \cup B)) \\ &= (A \cup B)(C \setminus (B \cup A)) \qquad \text{by lemma 2.3} \\ &= A(R \setminus A)((C \setminus B) \setminus (A \setminus B)) \qquad \text{by (4)} \\ &= A((B \cup C) \setminus A) \qquad \text{by (2)} \\ &= AL \cup (BL \cup C). \quad \Box \end{align*} $$

The empty multiderivation $O$ in $\mathcal{D}(M)$ should not be confused with the elementary multiderivation starting from $M$ and contracting an empty set of redex occurrences, which we shall denote $\emptyset$. In particular, $|\emptyset|=1$. However, it follows from the definition of residual that for every $A$ in $\mathcal{D}(M)$ we have $\emptyset \setminus A = \emptyset$. By an easy induction on $|A|$ we get that $A \setminus \emptyset = A$, and thus $O \equiv \emptyset$, and also that $A \setminus A = \emptyset^n$, with $n = |A|$. This and lemma 2.2 imply easily that if $A \equiv B$ then $F(A) = F(B)$.

**Lemma 2.5** ($\equiv$ is a congruence)

Let $A,B \in \mathcal{D}(M)$, with $A \equiv B$. We have :

$$ \bullet \quad \forall C \in \mathcal{D}(M) \quad A \setminus C \equiv B \setminus C \qquad (5) $$

$$ \bullet \quad \forall C \in \mathcal{D}(M) \quad AL \cup C \equiv BL \cup C \qquad (6) $$

$$ \bullet \quad \forall C \in \mathcal{D}(F(A)) \quad AC \equiv BC \qquad (7) $$

$$ \bullet \quad \forall C \quad \text{such that } F(C)=M \quad CA \equiv CB \qquad (8) $$

**Proof :** Easy consequences of the definitions. $\square$

**Corollaries** $\forall A \in \mathcal{D}(M) \quad A \setminus A \equiv O$

(9)

$$ \forall A \in \mathcal{D}(M) \quad AL \cup A \equiv A \qquad (10) $$

We now define a relation $\subseteq$ between coinitial multiderivations by :

$$ \forall A,B \in \mathcal{D}(M) \quad A \subseteq B \quad \text{iff} \quad AL \cup B \equiv B. $$

**Lattice of derivations theorem** : $<\mathcal{D}(M)/\equiv, \subseteq, \cup>$ is an upper semi-lattice.

**Proof** : Easy algebraic manipulations from the preceding lemmas. $\square$
Phrased in categorical terminology, this result means that the category whose objects are terms and whose morphisms are the equivalence classes of derivations, is a pushout.

Using all that precedes, it is easy to prove the following relations (with the appropriate conditions on initial and final terms of the following derivations).

(11) $(AB)\A\equiv\B$

(12) $(CA)\(\overline{(CB)}\)\equiv\overline{A\B}$

(13) $A\overline{\llcorner}B \text{ iff } A\B=\emptyset^m \text{ with } m=|A|$

(14) $A\equiv\B \text{ iff } A\overline{\llcorner}B\overline{\llcorner}A$

(15) $A\equiv\emptyset \text{ iff } A=\emptyset^n$ for some $n\ge 0$

(16) $A\overline{\llcorner}B \text{ iff } AC\equiv\B$ for some C

(17) $A\overline{\llcorner}B \text{ implies } A\C\overline{\llcorner}B\C$

(18) $A\overline{\llcorner}B \text{ implies } CA\overline{\llcorner}CB$

Remark that 13 and 14 show that $\overline{\llcorner}$ and $\equiv$ are easily decidable.

We could also have defined $\equiv$ as the smallest relation on $\mathcal{D}(M)$ such that $\emptyset\equiv\emptyset$ and $A\overline{\llcorner}B\overline{\llcorner}B\overline{\llcorner}A$. This justifies our terminology of permutation equivalence.

Finally, we may extend relations $\overline{\llcorner}$ and $\equiv$ to derivations by confusing the derivation

$$ M_0 \xrightarrow{u_1} M_1 \xrightarrow{u_2} M_2 \dots \xrightarrow{u_n} M_n \text{ with the multiderivation } M_0 \xrightarrow{U_1} M_1 \xrightarrow{U_2} M_2 \dots \xrightarrow{U_n} M_n $$
where $\forall i \le n \ U_i = \{u_i\}$.

### 3. Standardization, call by name, call by need

We are going to show in this paragraph that every derivation is equivalent by permutations to a certain derivation computing redexes in an outside-in manner. In analogy to what happens for recursive definitions or $\lambda$-calculus, we shall call these special derivations *standard*. However it should be remarked that, unlike in these two formalisms, the leftmost outermost derivations are usually not standard in TRS. For instance, consider

$$ \Sigma = \{F(x,A) \to B, C \to C, D \to A\} $$
The standard derivation starting from the term F(C,D) and ending in its normal form is $F(C,D) \rightarrow F(C,A) \rightarrow B$ whereas the leftmost outermost rule leads to an infinite derivation $F(C,D) \rightarrow F(C,D) \rightarrow \dots$

### 3.1 Outside-in and standard computations

Let us first give some preliminary definitions and technical lemmas.

#### Definitions

Let $u \in R(M)$, $\alpha$ the redex scheme at $u$ in $M$. We define the set $C_M(u)$ of occurrences of $M$ that are necessary to create the redex at $u$ as :

$$C_M(u) = \{v \in O(M) \mid u \leq v \text{ and } v \notin \bar{O}(\alpha)\}.$$

$$\text{We define also : } \bar{C}_M(u) = \{v \in O(M) \mid u \leq v \text{ and } v \notin C_M(u)\}.$$

$$\text{Note that } u \in C_M(u), \text{ since } \alpha \notin V, \text{ and thus } \forall v \in \bar{C}_M(u) \text{ } u < v.$$

Let $u, v \in R(M)$, with $u < v$. The non-ambiguity condition imposes $v \in \bar{C}_M(u)$. Furthermore, for any elementary $A:M \rightarrow N$ such that $v \in V$, we get $u \setminus A = \{u\}$.

**Lemma 3.1** Let $u, v \in R(M)$. If $C_M(u) \cap \bar{C}_M(v) \neq \emptyset$, then $u \in \bar{C}_M(v)$.

**Proof :** easy corollary of non-ambiguity. □

#### Definition

Let $A:M_0 \rightarrow M_1 \rightarrow M_2 \rightarrow \dots \rightarrow M_n$, and $u \in O(M_0)$.

$$\text{We say that } A \textit{ preserves } u \text{ iff } \forall i \leq n \neq v \in U_i \text{, } v < u.$$

**Lemma 3.2** Let $A \in D(M)$, preserving $v$. For every $u$ in $R(M)$ such that $u < v$ we have $u \setminus A = \{u\}$.

**Proof :** Easy induction on $|A|$. □

We can easily refine the parallel moves lemma to derivations preserving an occurrence $u$, using :
**Lemma 3.3** Let A,B∈D(M), both preserving u. Then A\B preserves u.

**Proof** : Easy induction on |A|+|B|, using the following observation. Let A₁ : P ↕ V Q. For all w∈R(P), w\A₁ does not contain any occurrence above vLw. □

**Lemma 3.4** Let A,B∈D(M), with A[B]. If B preserves u, then A preserves u too.

**Proof** : Assume A[B, B preserves u and A does not preserve u. That is, A=A₁A₂A₃ where A₁ preserves u, A₂ contracts set W such that ∃w∈W· w<u. By 3.3 B\A₁ preserves u, and by 3.2 w\(B\A₁)={w}, whence A\B≠O, contrary to hypothesis. □

We are now ready to present the important definition of an occurrence
being external for a (multi) derivation. This definition iterates the preserving
relation above, keeping track of creations upward.

**Definition** : Let A∈D(M), u in O(M). We say that u is *external* for A, and write u∈X(A), iff :

- either A preserves u

- or A = A₁A₂A₃ and there exists v<u such that :

- A₁ preserves u

- A₂ : P ↕ V Q with v∈V and u∈Cₚ(v)

- v∈X(A₃).

Note that, in the second case, v and the decomposition of A in A₁A₂A₃
are unique : A₂ is the first step in A that does not preserve u, and v is the uni-
que redex occurrence above u contracted at this step.

Let A : M₀ → M₁ → M₂ → ... → Mₙ, and u ∈ R(M₀). We say that u is an *initial redex occurrence contributing* to A, and write u ∈ R(A), iff ∃i ≤ n Uᵢ nu \ A[i-1] ≠ ∅.

Finally, we define the *external redex occurrences* of A by : E(A)=R(A)∩X(A).

We shall first extend lemmas 3.2, 3.3 and 3.4 above to X(A). For lemma 3.2,
we need an extra hypothesis : v must be below the redex scheme at u.
**Lemma 3.5** Let $A \in \mathcal{D}(M)$, $u$ in $R(M)$. If $X(A) \cap \bar{C}_M(u) \neq \emptyset$, we have $u\A = \{u\}$.

**Proof** : By induction on $|A|$. Let $v \in X(A) \cap \bar{C}_M(u)$. If A preserves $v$, use lemma 3.2. Otherwise, $A=A_1A_2A_3$ and there exists $w<v$ such that :

(a) $A_1$ preserves $v$ and therefore $u\A_1=\{u\}$ by lemma 3.2.

(b) $A_2$ : $P \twoheadrightarrow Q$ with $w \in W$ and $v \in C_p(w)$. Furthermore, by (a) $v \in \bar{C}_p(u)$, and thus $w \in \bar{C}_p(u)$, using lemma 3.1. Therefore $u\A_2=\{u\}$, and $w \in \bar{C}_Q(u)$.

(c) $w \in X(A_3)$ and therefore, using $w \in \bar{C}_Q(u)$ we get $u\A_3=\{u\}$ by induction hypothesis, and finally $u\A=\{u\}$. $\square$

We now extend lemma 3.3 as follows.

**Lemma 3.6** Let A and B coin initial, B preserving $u \in X(A)$. Then $u \in X(A \B)$.

**Proof** : By induction on $|A|$.

**Case 1** : A preserves u. Then by lemma 3.3 $A \B$ preserves u, and therefore $u \in X(A \B)$.

**Case 2** : $\exists v<u$ such that $A=A_1A_2A_3$ as in definition above. $A_1$ and B preserving u, $A_1 \B$ preserves u by lemma 3.3. Similarly, $B \A_1$ preserves u and therefore $v\B(B\A_1)=\{v\}$ by lemma 3.2. Finally $B \A_1$ preserves v (since $v<u$), $A_2$ preserves v trivially, and by lemma 3.3 $B\A_1A_2$ preserves v. $v \in X(A_3)$ implies $v \in X(A_3\B(B\A_1A_2)))$ by induction hypothesis, and therefore $A \B = (A_1 \B)(A_2\B(P\A_1))(A_3\B(B\A_1A_2)))$ is a decomposition showing $u \in X(A \B)$. $\square$

Note also that it follows from the definition of $X$ that if A preserves $v \in X(B)$, we have $u \in X(AB)$. We shall use freely this property below. We are now able to prove the extension of lemma 3.4.

**Lemma 3.7** Let A and B coin initial, with $A \lhd B$. We have $X(B) \in X(A)$.

**Proof** : Let $A \lhd B$, and $u \in X(B)$. We show $u \in X(A)$, by induction on $|A|$.

**Case 1** : A preserves u. Then $u \in X(A)$.
**Case 2** : Otherwise, B does not preserve u, by lemma 3.4. Therefore $B=B_1B_2B_3$, with $B_2:P^V_Q$, $\exists v \in V$ $v<u$, $B_1$ preserves u, $u \in C_P(v)$, and $v \in X(B_3)$. Since A does not preserve u, we have $A=A_1A_2A_3$, where $A_1$ preserve u, and $A_2:R^W_S$, such that $\exists w \in W$ $w<u$. Let $A'_1, A'_2, \dots, B'_1, B'_2, \dots$ as shown in Fig.1, which expresses the parallel moves lemma for A and B :

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

By lemma 3.3 $A'_1$ preserves u, and therefore v, $B_2$ preserves v trivially, and by lemma 3.3 again $A''_1$ preserves v. By lemma 3.6 we get $v \in X(B'_3)$. $A'_1$ preserving u, v is contracted by $B'_2$, using lemma 3.2. Similarly $B'_1$ preserves u, and therefore w is contracted in $A'_2$. Let us consider the situation in term R. There are two cases, according to the relative positions of v, $w \in R(R)$.

**Case 2.1** : $v \neq w$. Since our systems are non-ambiguous, $u \in C_R(v)$ and $w<u$ imply $v \in \bar{C}_R(w)$, and thus $w \setminus B'_2 = \{w\}$. Therefore $w \in R(S)$, and using $v \in X(B'_3)$ we get by lemma 3.5 that $w \setminus B'_3 = \{w\}$, and therefore $A_2 \setminus (B'_1B'_2B'_3) \neq \emptyset$, a contradiction with $A \subseteq B$.

**Case 2.2** : $v=w$. Since $A'_2$ and $B'_2$ preserve v, so do $A''_2$ and $B''_2$, using lemma 3.3. By lemma 3.6 we get $v \in X(B''_3)$. $B''_1B''_2$ preserving v, we have $v \in X(B''_1B''_2B''_3)$. Since $A_3 \subseteq B''_1B''_2B''_3$, we get $v \in X(A_3)$ by induction hypothesis, and $A_1A_2A_3$ is a decomposition of A showing $u \in X(A)$. □

**Corollary** : $A \equiv B$ implies $X(A) = X(B)$.

External redex occurrences are their own residual, until they are contracted :
**Lemma 3.8** : Let $A:M^*\to N$ and $u\in X(A)\cap R(M)$. We have either $u\in R(A)$ and $u\backslash A=\emptyset$, or $u\notin R(A)$ and $u\backslash A=\{u\}$.

**Proof** : straightforward from the definitions of $X(A)$ and $R(A$). $\square$

**Lemma 3.9** : If $A\equiv B$, we have $E(A)=E(B)$.

**Proof** : Let $A\equiv B$, and $u\in E(A)$. We get $u\in X(B)$ by the corollary to lemma 3.7.
Lemma 3.8 implies $u\backslash A=\emptyset$ and therefore, by the parallel moves lemma, $u\backslash B=\emptyset$.
Lemma 3.8 applied now to B gives $u\in R(B)$, and thus $u\in E(B)$. $\square$

If $u$ is preserved by $A$, then any prefix occurrence $v\le u$ is also preserved
by $A$, obviously. This property is also true of members of $X(A)$.

**Lemma 3.10** : If $u\in X(A)$, then $\forall v\le u$ $v\in X(A)$.

**Proof** : Induction on $|A|$.

**Case 1** : $A$ preserves $u$. Then $A$ preserves $v$, and $v\in X(A)$.

**Case 2** : $A=A_1A_2A_3$ with $A_2:P^W\to Q$ and $\exists w<u$ such that $w\in W$, $u\in C_p(w)$ and $w\in X(A_3)$.
Moreover $A_1$ preserves $u$, and therefore $v$.

**Case 2.1** : $v\le w$. Then $v\in X(A_3)$ by induction hypothesis and therefore, since $A_1A_2$
preserve $v$, we get $v\in X(A)$.

**Case 2.2** : $w<v\le u$. Then $v\in C_p(w)$, and therefore the decomposition $A_1A_2A_3$ shows
$v\in X(A)$. $\square$

The set $X(A)$ is therefore closed by prefix. When it contains some $u\in R(M)$,
with $A\in D(M)$, it contains also all the members of $C_M(u)$. $X(A)$ is obviously non empty
since it always contains $\Lambda$, preserved by every derivation. We shall now show that
$E(A)$ is also non empty, whenever $A\ne\emptyset^n$.

**Lemma 3.11** : If $A\ne\emptyset$ we have $E(A)\ne\emptyset$.

**Proof** : By induction on $|A|$.

If $A=0$ it is trivial. Otherwise, let $A=A_1A_2$ with $A_1:M\to N$ elementary.
If $A_2 \equiv 0$, i.e. $A_2 = \emptyset^n$, then $U \neq \emptyset$, and any member of $U$ is obviously in $E(A)$. Otherwise, let us consider $v \in E(A_2)$, which exists by induction hypothesis.

**Case 1** : There exists $u$ in $U$ such that $u \leq v$. Then $u \in X(A_2)$ by lemma 3.10 and thus $u \in X(A)$ since $A_1$ preserves $u$. Therefore $u \in E(A)$.

**Case 2** : Otherwise $v$ is preserved by $A_1$, and therefore $v \in X(A)$.

**Case 2.1** : There exists $u$ in $\bigcup M(v)$. Then by definition $u \in X(A)$, and therefore $u \in E(A)$.

**Case 2.2** : Otherwise $v \in R(A)$, and therefore $v \in E(A)$. $\square$

We are now ready to use $E(A)$ to construct an outside-in equivalent of $A$. The following definition is useful to show that this construction will always terminate.

**Definition** : We define a relation $▷$ between multiderivations as follows : $A▷B$ iff $A \neq 0$ and $B=A\u$ with $u \in E(A)$.

**Lemma 3.12** The relation $▷$ is noetherian, i.e. there is no infinite chain $A_1▷A_2▷A_3\dots$

**Proof** : Let $A : M_0 \xrightarrow{U_1} M_1 \xrightarrow{U_2} \dots \xrightarrow{U_n} M_n$. If $A \neq 0$ there is no $B$ such that $A▷B$. Otherwise, let $u \in E(A)$. According to lemma 3.8, there exists $k \leq n$ such that $u \in A[k-1] = \{u\}$ and $u \in U_k$. Therefore $(A\u)[k-1,n] = A[k-1,n]\u$ contracts the sets $U_{k-\{u\}}$, $U_{k+1}, \dots, U_n$. Thus $A\u$ is less then $A$ in the lexicographic ordering $\langle |U_n|, |U_{n-1}|, \dots, |U_1| \rangle$. $\square$

**Definition** : The derivation $A$ is said to be *outside-in* iff - either $A=0$ - or $A=A_1A_2$, where $A_1$ is the elementary derivation contracting some $u$ in $E(A)$, and $A_2$ is outside-in.

Let $A$ be any multiderivation. We construct an outside-in equivalent $B$ of $A$ as follows. If $A \neq 0$, we stop with $B=0$. Otherwise, let us pick some $u$ in $E(A)$. We define $B$ as the elementary derivation contracting $u$, followed by an outside-in equivalent of $A\u$. By noetherian induction, using lemma 3.12, the construction always terminate. By construction, $B[A]$. But, according to lemma 3.11, the construction can only stop when $A[B$, and therefore $B \in A$, which justifies our terminology.
The construction is illustrated in Fig.2.

<figure><img src="image_7.png" /><figcaption>Fig.2</figcaption></figure>

**Definition**: Let A be any derivation. We say that A is *standard* iff A is outside-in, and at every step the redex occurrence u is the *leftmost* in E(A).

Similarly to above, we define *the standard derivation B* in the class of A, and we write $B=st(A)$. Using lemma 3.9, we get easily by noetherian induction that $st(A_1)=st(A_2)$ whenever $A_1\equiv A_2$.

To conclude, we have shown :

**Standardization theorem**

Every derivation class contains a unique standard derivation.

Note that the leftmost condition is unimportant here : any choice function over sets of disjoint occurrences would guarantee the uniqueness of the standard derivation.

**Example**: Let $\Sigma = \{F(x,B) \to G(x,x), A \to B, C \to D\}$. Among the derivations starting at $F(C,A)$, all the ones that do not use the reductions marked with an X are standard in the diagram shown in Fig.3.

<figure><img src="image_8.png" /><figcaption>Fig.3</figcaption></figure>
Finally, we remark that it is possible to express standard derivations in terms of residuals, because $E(A)$ can be characterized as the set of redex occurrences of $A$ that stay outermost modulo permutations, in the following sense.

**Definition:** Let $A: M_0 \underset{M_1}{\to} M_2 \underset{M_3}{\to} \dots \underset{M_n}{\to} M_n$, $u \in R(A)$. We say that $u$ is outermost in $A$, and write $u \in \text{Out}(A)$ iff $\forall i \le n \ \forall v \in u \setminus A[i-1] \ \exists u_i \in U_i \ u_i < v$. In other words, $u \in \text{Out}(A)$ iff $u \in U_i$ for some $i \le n$, and $\forall j < i \ \exists u_j \in U_j \ u_j \le u$. Therefore $\forall j < i \ u \setminus A[j] = \{u\}$ and $u \setminus A[i] = u \setminus A = \emptyset$. Note that lemma 3.8 implies that $E(A) \subseteq \text{Out}(A)$. The converse in true for outside-in derivations.

**Lemma 3.13.** If $A$ is outside-in, we have $E(A) = \text{Out}(A)$.

**Proof:** Let $A: M_0 \underset{M_1}{\to} M_2 \underset{M_3}{\to} \dots \underset{M_n}{\to} M_n$ be an outside-in derivation and $u \in \text{Out}(A)$. By definition, $\exists i \le n \ u_i = u$ and $\forall j < i \ u_j \ne u$. Since $A$ is outside-in, we have $u \in E(A[i-1,n])$ and, $A[i-1]$ preserving $u$, we get $u \in E(A)$. The converse follows from lemma 3.8. $\square$

**Lemma 3.14.** $E(A) = \bigcap_{B \equiv A} \text{Out}(B)$.

**Proof:** Let $B \equiv A$. We have, by lemma 3.9, $E(A) = E(B) \subseteq \text{Out}(B)$, which shows $E(A) \subseteq \bigcap_{B \equiv A} \text{Out}(B)$. Conversely, take $B = \text{st}(A)$ and use the preceding lemma. $\square$

That is, $E(A)$ is the set of redex occurrences which are outermost in every permutation of $A$, or equivalently which are outermost in some outside-in equivalent of $A$.

The results obtained so far do not allow us to say "how to compute in a standard way", since $E(A)$ may depend on the whole of $A$. We are now going to relate these notions to the starting term of derivation $A$, so that we may define an outside-in computation rule, generalizing the call-by-name computation rule for recursive program schemes.

## 3.2 Normal derivations, call by name

**Definition:** We define the set of *external occurrences in term* $M$ as :
$$ X(M) = \bigcap_{A \in D(M)} X(A). $$
Similarly to above, we define the set of *external redex occurrences in* $M$ as :
$$ E(M) = R(M) \cap X(M) $$
or, equivalently, $E(M) = \bigcap_{A \in D(M)} E'(A)$

where, for A in D(M), we define $E'(A) = X(A) \cap R(M)$.
Similarly to lemma 3.14, it is easy to show that

$$E'(A) = \bigcap_{B \equiv A} Out'(R),$$

where $Out'(A) = \{u \in R(M_0) | \forall i \le n \ \forall v \in u \ \forall A[i-1] \ \nexists u_i \in U_i \ u_i < v\}$

$$\text{with } A : M_0 \xrightarrow{U_1} M_1 \xrightarrow{U_2} \dots M_{n-1} \xrightarrow{U_n} M_n.$$

We may therefore characterize alternatively $E(M)$ as the set of redex occurrences of $M$ which are outermost in every derivation issued from $M$:

$$E(M) = \bigcap_{A \in D(M)} Out'(A).$$

We shall now show that $E(M)$ is not empty, if $M$ is not a normal form. But we need first a technical lemma.

**Notation** : We write $\xrightarrow{\text{int}}$ for $\xrightarrow{\Lambda}$ (internal reduction). We say that derivation $A$ is *internal* iff it is composed of internal reductions. That is, $A$ in $D(M)$ is internal iff $M=FM_1 \cdots M_p$ and $A$ preserves $1,2,\cdots,p$ (and therefore $F(A)=FN_1 \cdots N_p$). Of course if $A$ is internal, every permutation of $A$ is internal. We say that $A$ is *external* iff it is not internal (i.e. it contracts some redex at the top level).

**Lemma 3.15** Let $A : M \xrightarrow{\ast_{\text{int}}} \Lambda \to N$. For any $B$ in $D(N)$, we have $X(AB)=X(A)$.

**Proof** : Obvious from definitions, since $\Lambda \in X(B)$. []

**Lemma 3.16** $M \in NF$ iff $E(M)=\emptyset$

**Proof** : If $M$ is a normal form, $R(M)=\emptyset$ and thus $E(M)=\emptyset$. Conversely, by induction on $M$. Assume $M \in NF$. We show $E(M) \neq \emptyset$.

**Case 1** : Every $A$ in $D(M)$ is internal. Thus $M=F(M_1, \cdots, M_p)$ and for some $k \le p$ $M_k \notin NF$. By induction hypothesis there exists $u_k$ in $E(M_k)$, and therefore $k \cdot u_k$ is in $E(M)$.

**Case 2** : There is some $A : M \xrightarrow{\Lambda} \emptyset$. Let us show that $E(A) \subseteq E(M)$. For, otherwise, assume that there exists $B$ in $D(M)$ and $u$ in $E(A)-X(B)$. Since $B \subseteq A \subseteq B$ we have $u \in X(AB)$
by lemma 3.7. But $X(AB)=X(A)$ by lemma 3.15, a contradiction with $u \in E(A)$.
Therefore $E(A) \subseteq E(M)$, and since $A \neq 0$, we get $E(M) \neq 0$ by lemma 3.11. $\square$

This permits us to define the notion of normal derivation issued from a term $M$, similarly to what happens in $\lambda$-calculus :

* If $MeNF$, the normal derivation issued from $M$ is $0$.

* Otherwise, let $u$ be the leftmost occurrence in $E(M)$, $A$ the elementary derivation : $M \stackrel{u}{\longrightarrow} N$. The normal derivation issued from $M$ is $A$ followed by the normal derivation issued from $N$.

Of course, if $M$ has no normal form, the normal derivation issued from $M$ is infinite. If $M$ has a normal form $N$, let $A$ be some derivation from $M$ to $N$ : $A:M \stackrel{*}{\longrightarrow} N$. Let $B$ be any derivation in $D(M)$. We have $B:A$, and thus $X(A) \subseteq X(B)$ by lemma 3.7, which shows $X(M)=X(A)$. Assume now there exists $u$ in $(X(A) \cap R(M)) - R(A)$. According to lemma 3.8 we have $u \setminus A = \{u\}$, contrary to the hypothesis that $N$ is in normal form. This shows that $E(M)=E(A)$ and using a simple induction on $|A|$, implies that $st(A)$ is the normal derivation issued from $M$. In other words, if $M$ has a normal form, the normal derivation issued from $M$ terminates in its normal form, and is standard.

To summarize :

**Normal derivation theorem**

If $M$ admits a normal form $N$, the normal derivation issued from $M$ will end in $N$; it is the standard in the class of derivations going from $M$ to $N$.

The notion of normal derivation may be considered as the generalisation to term rewriting systems of the call by name computation rule for recursive equations [3,7,10,30]. In the terminology of [26], it shows that all our systems are d-outer, using the dominance ordering $d$ defined by :

$$u(dM)v \quad \text{iff} \quad u \leq v \quad \text{or} \quad u \nvDash v, u \in X(M) \quad \text{and} \quad v \notin X(M).$$

In the next section, we are going to extend these results to define a call by need computation rule, for terms possessing a normal form. Before that, let us remark that it is possible to extend lemma 3.15 to external redex occurrences, yielding a canonical form for the standard of external derivations issued from a given term.

**Lemma 3.17** Let $A : M \underset{int}{\stackrel{*}{\longrightarrow}} A \subseteq N$. For any $B$ in $D(N)$, we have $E(AB)=E(A)$.

**Proof** : Let $u \in R(AB) - R(A)$. We have $u \notin Out(AB)$, and therefore $u \notin E(AB)$. $\square$
**Lemma 3.18** Let $A : M \underset{\text{int}}{\stackrel{*}{\rightarrow}}^{\Lambda} N$. For any $B$ in $\mathcal{D}(N)$, $AB$ is standard iff $A$ and $B$ are standard.

**Proof** : easy induction on $|A|$, using 3.17 above. $\square$

**Corollary** : Let $A = M \underset{\text{int}}{\stackrel{*}{\rightarrow}}^{\Lambda} N$ be standard. For every external $B$ in $\mathcal{D}(N)$ we have $\text{st}(B)=\text{AC}$, with $C = \text{st}(B\setminus A)$.

**Proof** : If $B$ is external, it is easy to show that $A\llcorner B$. Consider $C = \text{st}(B\setminus A)$. Since $A$ is standard, $AC$ is standard by lemma 3.18. But $C\equiv B\setminus A$ implies then that $AC\equiv B$. By unicity of standard derivations, we get $\text{st}(B)=\text{AC}$. $\square$

### 3.3 Call by need

**Definition** : If $M$ has a normal form $N$, then $u\in\mathcal{R}(M)$ is a redex occurrence needed for the normal form iff, for any $A : M \stackrel{*}{\rightarrow} N$, then $u\in\mathcal{R}(A)$. In short, write $u\in\mathcal{N}(M)$.

We have shown in the last section that $\mathcal{E}(M)=\mathcal{E}(A)$. Therefore $\mathcal{E}(M)\subset\mathcal{N}(M)$ and $\mathcal{N}(M)\neq\emptyset$ for any $M$ not in normal form, but having a normal form. Of course the problem is non-trivial only if for some rule $\alpha\rightarrow\beta$ in $\Sigma$ we have $\mathcal{V}(\alpha)-\mathcal{V}(\beta)\neq\emptyset$, since otherwise $\mathcal{N}(M)=\mathcal{R}(M)$.

In order to prove further properties of needed redexes, consider first a few technical lemmas about outside-in derivations. In the following, we abbreviate outside-in into oi.

**Lemma 3.19** If $A\equiv B$ with $A$ oi, then $R(A)\subset R(B)$.

**Proof** : Let $A=A_1A_2$ with $A_1 : M \stackrel{u}{\rightarrow} M'$. Then $u\in\mathcal{E}(A)=\mathcal{E}(B)$. Thus $u\in\mathcal{R}(B)$. Furthermore $R(A_2)\subset R(B\setminus A_1)$ by induction. Therefore $R(A)\subset R(B)$. $\square$

**Corollary** : If $M$ has the normal form $N$, then $\mathcal{N}(M)=\mathcal{R}(A)$, where $A$ is any oi derivation from $M$ to $N$.

**Lemma 3.20** If $A$ is oi and $B\llcorner A$, then $A\setminus B$ is oi (except for some empty steps).

**Proof** : Let $A=A_1A_2$ with $A_1 : M \stackrel{u}{\rightarrow} N$. By induction, we already know that $A_2\setminus(B\setminus A_1)$ is oi. Consider now $A_1\setminus B$, i.e. $u\setminus B$. If $u\setminus B=\emptyset$, then $A\setminus B$ is obviously oi. Suppose now $u\setminus B\neq\emptyset$. Since $A$ is oi and $A\equiv B\llcorner A$, we know that $u\in\mathcal{E}(A)=\mathcal{E}(B\setminus A)$. Thus $u\in\mathcal{Out}(B\llcorner A)$ by lemma 3.14 and $u\setminus B=\{u\}$. Now, for all $C\equiv A\setminus B$, one has $u\in\mathcal{Out}(C)$ since $BC\equiv A$ and $u\in\mathcal{E}(A)$. Again by 3.14, one has $u\in\mathcal{E}(A\setminus B)$. $\square$
**Lemma 3.21** If A,B are oi and A≡B, then |A|=|B|.

**Proof** : If |A|=0, then B=0 and B=0 since B is oi. Similarly if |B|=0. Now

let $A=A_1A_2$ and $B=B_1B_2$ with $A_1: M_1^U \to N$ and $B_1: M_1^V \to P$. Denote temporarily by $C'$ the derivation $C$ where the empty steps are suppressed. As $E(A)=E(B)$ and $u \in E(A)$, $v \in E(B)$, we have $u$ and $v$ disjoint. Thus, if $B_3=B_1 \setminus A_1$ and $A_3=A_1 \setminus B_1$, one has $B_3: N \to Q$ and $A_3: P \to Q$. Therefore, using the previous lemma and an induction on $|A|+|B|$, we get $|A|=|1+A_2|=|1+(B \setminus A_1)|'=2+|(B_2 \setminus A_3)|'$. Again by induction $|(B_2 \setminus A_3)|'=|(A_2 \setminus B_3)|'$. But one also has $|B|=2+|(A_2 \setminus B_3)|'$. $\Box$

**Notation** : Let $d(A)=|st(A)|$.

By the previous lemma, since $st(A)$ is oi, one has $d(A)=|B|$ for any B oi such that $B \equiv A$. Now this notion of distance associated to A has properties involved by the preservation of external redexes until they are reduced.

**Lemma 3.22** If $A \searrow B$, then $d(A) \ge d(A \setminus B)$.

**Proof** : Obvious from the two previous lemmas. $\Box$

**Lemma 3.23** If $A \searrow B$ and $|B|=1$, then $d(A) > d(A \setminus B)$ iff $R(A) \cap R(B) \ne \emptyset$..

**Proof** : Let $C=st(A)$ and $C=C_1C_2$ with $C_1: M_1^U \to N$. Let $B=M_1^V \to P$. Then, with $C \equiv A \searrow B$, we get $C \equiv B \cup C$ and $u \in Out(B \cup C)$, since $u \in E(C)=E(B \cup C)$. This means that $u \setminus B = \emptyset$ iff $u \in V$. Now the lemma follows by induction on $|C|$, since $A \setminus B \equiv C \setminus B$ and using lemmas 3.20 and 3.21. $\Box$

Now, denoting by $d(M)$ the length of the standard reduction of $M$ to its normal form, when it exists:

**Corollary** : Let $M$ have the normal form $N$. Then :

a) $d(M)=0$ iff $M=N$

b) Let $M \to M'$. Then, if $U \cap W(M)=\emptyset$, one has $d(M)=d(M')$. Otherwise $d(M)>d(M')$.
This is summarized in Fig. 4.

<figure><img src="image_9.png" /><figcaption>Fig. 4</figcaption></figure>

Therefore, any derivation contracting a sufficiently large number of needed redex occurrences ends at the normal form (Remark : the standard derivation has a maximum length among the derivations contracting only needed redexes and ending at the normal form. Now, the problem is to find effectively the needed redexes in a given term. At present time, the only way is to use the corollary of Lemma 3.19 which involves some "look-ahead". We will see that this problem is connected to the notion of "sequentiality" already defined by Berry [1], Kahn-Plotkin [i5], Milner [23], Vuillemin [30].

## 4. Sequentiality :

### 4.1 Sequential systems :

We consider the predicate "M has a normal form" on terms and consider its properties when we order the set of terms by the prefix ordering and the set $T = \{tt, ff\}$ of truth values by $ff[tt]$. We first extend the set $T$ of terms to a set $T_\Omega$ of $\Omega$-terms by adding a new constant $\Omega$ (new nullary function symbol), and define the prefix ordering $\prec$ on $T_\Omega$ by :

$$ \begin{cases} \Omega \prec M & \text{for any } M \in T_\Omega \\ F(M_1, M_2, \dots, M_n) \prec F(N_1, N_2, \dots, N_n) & \text{if } M_i \prec N_i \text{ for } 1 \le i \le n \end{cases} $$

All the previously defined operations on terms are obviously extended to $\Omega$-terms. One just adds a very few new notions.
If $M \preceq P$ and $N \preceq P$, then $M$ and $N$ are said compatible, written $M \uparrow N$. The greatest lower bound (glb) of two $\Omega$-terms $M$ and $N$, written $M \sqsupseteq N$, and the least upper bound (lub) of two compatible $\Omega$-terms $M$ and $N$, written $M \sqsubseteq N$, are defined by :

$$ \begin{cases} M \sqsupseteq N = \Omega & \text{if } M=\Omega \text{ or } N=\Omega \text{ or } M \text{ and } N \text{ incompatible} \\ F(M_1, \dots, M_n) \sqsupseteq F(N_1, \dots, N_n) = F(M_1 \sqsupseteq N_1, \dots, M_n \sqsupseteq N_n) \end{cases} $$

$$ \begin{cases} \Omega \sqsupseteq M = M \sqsupseteq \Omega = M \\ F(M_1, \dots, M_n) \sqsupseteq F(N_1, \dots, N_n) = F(M_1 \sqsupseteq N_1, \dots, M_n \sqsupseteq N_n) \end{cases} $$

It will be convenient to write $M_{\Omega}$ for $\sigma(M)$ where $\sigma$ is the substitution such that $\sigma(x)=\Omega$ for all variables $x$.

We define a predicate nf on $\Omega$-terms by $nf(M)=tt$ iff has a normal form, i.e. $\exists N \in NF$ s.t. $M \stackrel{*}{\rightarrow} N$. Remark that we require $N$ to be a term, i.e. without $\Omega$'s. An $\Omega$-term $N$ such that $R(N)=\emptyset$ will be called an $\Omega$-normal form.

If $M \stackrel{*}{\rightarrow} N$ and $M \stackrel{\sim}{\rightarrow} M'$, it is straightforward to check that there is an $N'$ such that $M' \stackrel{*}{\rightarrow} N'$ and $N \stackrel{\sim}{\rightarrow} N'$. Thus the predicate nf is monotonic increasing, since $N=N'$ when $N \stackrel{\sim}{\rightarrow} N'$ and $N \in NF$. Summarizing :

**Lemma 4.1** If $M \preceq N$, then $nf(M) \sqsubseteq nf(N)$.

We now prove that the predicate nf is conditionally multiplicative (see Berry [2] in which this property is called stability). For this, consider a new kind of rewriting rules, the $\omega$-rules, associated to any system $\Sigma$, defined by $M \rightarrow N$ iff, for some $u \in O(M)$ and redex scheme $\alpha$ in $\Sigma$, one has $M/u \stackrel{\alpha}{\rightarrow} N$ but not $\alpha \stackrel{\omega}{\rightarrow} M/u$ and $N=M[u \leftarrow \Omega]$. (I.e., $M/u$ is compatible with a redex scheme, but is not a redex.)

**Lemma 4.2** ($\rightarrow u \rightarrow \omega$)\* is confluent.

**Proof** : We know already that $\rightarrow^*$ is confluent. Now, if we write temporarily $M \stackrel{\Sigma}{\rightarrow} N$ for $M \rightarrow N$ or $M=N$, and similarly for $M \stackrel{\omega}{\rightarrow} N$, the non-ambiguity condition of our systems enables us to prove the lemma via the two properties summarized in the two
diagrams of Fig. 5 :

<figure><img src="image_10.png" /><figcaption>Fig. 5</figcaption></figure>

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

The w-rules will be also useful for the semantics of our systems.
(Remark : They correspond exactly to the ones defined by Wadsworth [31] in the
λ-calculus.) Finally, let ∧ denote also the trivial glb operation in the truth
values domain T (i.e. the usual "and".) Now, we prove Berry's property : nf is
conditionally multiplicative.

**Lemma 4.3** If M↑N, then nf(M↑N) = nf(M)∧nf(N).

**Proof** : By monotonicity, one has easily nf(M↑N) ⊑ nf(M)∧nf(N). Conversely, the only problem is when nf(M)∧nf(N)=tt, i.e. when M and N have a normal form. By monotonicity, we know that nf(M↓N)=tt. We work by induction on the length d(M↓N) of any outside-in derivation A from M↓N to its normal form. Let A=A₁A₂ with A₁:M↓N→^{u}P. Then u∈E(M↓N). We claim that u∈R(M↑N). Otherwise, we have 3 cases.

1) $u=u_1u_2$ with $(M\uparrow N)/u_1=\Omega$ and $u\in R(M)$. Then, since $N\leq(M\downarrow N)[u\leftarrow\Omega]$, we know by monotonicity that $(M\downarrow N)[u\leftarrow\Omega]$ has a normal form. Contradiction with $u\in E(M\downarrow N)$.

2) $u=u_1u_2$ with $(M\uparrow N)/u_1=\Omega$ and $u\in R(N)$. Same as in 1).

3) $u\in O(M\uparrow N)$, but $u\notin R(M\uparrow N)$. This means that, if $\alpha$ is the redex scheme such that $(M\downarrow N)/u=\sigma\alpha$, one has $M/u\preceq(M\downarrow N)/u\uparrow\alpha_{\Omega}$ and similarly $N/u\uparrow\alpha_{\Omega}$. Now, since $u\notin R(M\uparrow N)$, one cannot have $M/u\geq\alpha_{\Omega}$ and $N/u\geq\alpha_{\Omega}$. Assume for instance that not $\alpha_{\Omega}\leq M/N$. Then $M\rightarrow^{\omega}M[u\leftarrow\Omega]$. By the previous confluence property $M[u\leftarrow\Omega]$ has a normal form. Let $M_1=M[u\leftarrow\Omega]$. We conclude that $(M_1\downarrow N)[u\leftarrow\Omega]$ has a normal form by reasoning as in the first two cases, and by monotonicity $(M\downarrow N)[u\leftarrow\Omega]$ has a normal form. Contradiction with $u\in E(M\downarrow N)$.

Thus $u \in R(M \uparrow N)$. Now, let $M \uparrow t'$ and $N \uparrow N'$. Since $nf(M) = nf(N) = tt$, one has
also $nf(M')=nf(N')=tt$. Furthermore $M \models N \rightarrow M' \models N'$. Finally, by induction, we know that $M' \models N'$ has a normal form, and thus $nf(M \models N)=tt$. □

**Corollary :** For any $\Omega$-term $M$ having a normal form, there is a (unique) minimum prefix $N$ of $M$ having a normal form.

This is not true, in general, in ambiguous systems. Take $\Sigma = \{F(A,x) \to A, F(x,A) \to A\}$, which computes the well-known "parallel or". Then, if $M = F(A,A)$, both $F(A,\Omega)$ and $F(\Omega,A)$ have a normal form, but not $F(\Omega,\Omega)$. However, in non ambiguous systems, for any given $M$ having a normal form, there is a minimum prefix of $M$ to compute in order to get the normal form.

But, usually, the computation of a term is done without any look-ahead. Take for instance $\Sigma \supset \{F(A,B,x) \to C, F(x,A,B) \to C, F(B,x,A) \to C\}$. Now, if $T=F(T_1,T_2,T_3)$, we know that there is a minimum prefix of $T$ having a normal form, if $nf(T)=tt$. But nothing ensures us that, for all $T$'s of this form, we need to compute always a fixed argument of $F$. Here, this is false since $nf(F(\Omega,\Omega,\Omega))=ff$, but $nf(F(A,B,\Omega))=tt$, $nf(F(\Omega,A,B))=tt$ and $nf(F(B,\Omega,A))=tt$. (This example is a syntactic view of the one in Berry [2].) Technically, we want that the predicate "M has a normal form" be sequential. So, let us first recall what is a sequential predicate in the sense of Kahn-Plotkin [15].

**Definition :** Let $P$ be a monotonic predicate on $T_\Omega$ (with the truth values domain $T$ ordered as before). An occurrence of $M$ is said to be an *index* of $P$ in $M$ iff $M/u=\Omega$ and $\forall N \supseteq M P(N)=tt$ implies $N/u \neq \Omega$. Then $P$ is *sequential* at $M$ iff whenever $P(M)=ff$ and $\exists N \supseteq M P(N)=tt$, it follows that there exists an index of $P$ in $M$. Finally $P$ is said to be *sequential* iff it is sequential at every $M$ in $T_\Omega$.

Thus, if $P$ is a sequential predicate, $M$ is not in normal form and $P(M)=ff$, there is a critical $\Omega$ in $M$ to increase in order to make true the predicate.

**Definition :** $\Sigma$ is a *sequential system* iff $nf$ is a sequential predicate.

Now, let $\omega'(M)$ be $M$ where all redexes are replaced by the constant $\Omega$. If the indexes of the $nf$ predicate are computable, an easy terminating strategy can be designed : for any term $M$, contract a redex at occurrence $u$ which is an index of $nf$ in $\omega'(M)$. (Then $u \in N(M)$ if $M$ has a normal form.) But, in general, these indexes are not computable. For instance, take $\Sigma$ containing the following four rules :
F(G(A,x),B)→K
F(G(x,A),C)→K
F(D,x)→K
G(E,E)→...

Then, if $M=F(G(\Omega,\Omega),\Omega)$, the occurrence $u=2\in O(M)$ is an index iff $G(E,E)$ cannot derive to D, which is not decidable, since $\Sigma$ can have many other rules. But before overcoming this problem, let us remark that $\Sigma$ is sequential iff the nf predicate is sequential only at terms in $\Omega$-normal forms.

**Lemma 4.4** $\Sigma$ is a sequential system iff the predicate nf(M) is sequential at any $\Omega$-normal form M (i.e. such that $M=\omega'(M)$.)

**Proof** : by induction on $n=\text{Min}\{d(N) \mid N \supseteq M\}$, $nf(N)=\text{tt}$. Let $n=0$. Then, there is $N$ in normal form such that $N \supseteq M$. Thus $M=\omega'(M)$ and this case is trivial. Let $n>0$ and $u$ be an index of nf in $\omega'(M)$. We have two possibilities. First $M/u=\Omega=\omega'(M)/u$. As $\omega'(M) \not\supseteq M$, the occurrence $u$ is also an index in $M$. Secondly $M/u \neq \Omega$, which means $M/u$ is a redex. Then $nf(N[u \leftarrow \Omega])=\text{ff}$ for all $N$ such that $N \supseteq M$ and $nf(N)=\text{tt}$. Thus $u \in N(N)$. Let $M_k^u \supseteq M'$ and $N_k^u \supseteq N'$, then $d(N')<d(N)$ by lemma 3.23. Therefore by induction there is an index $v'$ of nf in $M'$. Now, let $v$ be the occurrence of $M$ defined by : $v=v'$ if $u$ and $v'$ are disjoint, $v=uw'$ if $v'=uw'u$ where $\alpha_k^u/w=\beta_k^u/w' \in V$. Then one checks easily that $v$ is an index of nf in $M$. $\square$

Thus, a sequential system $\Sigma$ is exactly a system where, for any term $M$ not in normal form, it is possible to find a needed redex occurrence without any look-ahead, i.e. an occurrence $u \in R(M)$ such that, for all $N \supseteq \omega'(M)$ with $u \in R(N)$, one has $u \in N(N)$.

## 4.2 Strongly sequential systems :

However, indexes are not computable in general. Neither is decidable the sequentiality of a system $\Sigma$. In order to make these two questions effective, we consider more restricted systems. The idea is to give the possibility for any redex to produce any term.

**Notation** : Let $M$ and $N$ be two $\Omega$-terms. Then $M \to' N$ iff $N=M[u \leftarrow P]$ for some redex occurrence $u \in R(M)$ and $\Omega$-term $P$. Furthermore, let $nf'(M)=\text{tt}$ iff $M \to'^* N$ for some term $N$ in normal form.
**Definition**: $\Sigma$ is a strongly sequential system iff the predicate nf' is sequential at any M in $\Omega$-normal form. We denote by $I(M)$ the set of indexes of nf' in M.

The restriction to $\Omega$-normal forms is purely technical, because the previous lemma is no more true with the nf' predicate (Take $\Sigma = \{F(A,B,x) \to K, F(B,x,A) \to K\}$ and consider $M=F(R,\Omega,\Omega)$ where R is a redex, then $\omega'(M)=F(\Omega,\Omega,\Omega)$ has an index for nf', but M has not.) However, since nf'(M)=ff if M is in $\Omega$-normal form and nf(M) implies nf'(M) for any M, a strongly sequential system is sequential with the help of the previous lemma.

**Definition**: A redex occurrence $u \in R(M)$ is strongly needed iff $u \in I(\omega'(M))$.

Clearly, if $u \in R(M)$ is strongly needed, then $u$ is needed, i.e. $u \in N(M)$. We want to show that strongly needed redex occurrences in M can be found effectively and that the strong sequentiality of any system $\Sigma$ can be decided. A priori this is not too straightforward. Consider for instance $\Sigma$ having the following redex schemes : $F(G(A,x),F(B,y)),F(G(x,A),F(C,y)), G(D,D)$. Then the smallest $\Omega$-term making $\Sigma$ not strongly sequential is $M=F(G(\Omega,\Omega),F(G(\Omega,\Omega),\Omega))$.

### 4.3 Decision procedure for strongly needed redexes :

Let us first introduce a few notations. If $E$ is any set of $\Omega$-terms we write $M \preceq E$ iff $\exists N \in E$ $M \preceq N$. Similarly for $M \uparrow E$ and $M \downarrow E$. Finally, with $\overline{red}_{\Omega} = \{\alpha_{\Omega} | \alpha \in red\}$, we write $M \uparrow$ for $M \uparrow \overline{red}_{\Omega}$.

**Definition**: For any $\Omega$-term $M$, we define its direct approximation $\omega(M)$ and internal direct approximation $\overline{\omega}(M)$ by :

$$\omega(x) = \overline{\omega}(x) = x$$

$$\omega(\Omega) = \overline{\omega}(\Omega) = \Omega$$

$$\overline{\omega}(F(M_1, M_2, \dots, M_n)) = F(\omega(M_1), \omega(M_2), \dots, \omega(M_n))$$

$$\omega(F(M_1, M_2, \dots, M_n)) = \begin{cases} \Omega & \text{if } \overline{\omega}(F(M_1, M_2, \dots, M_n)) \uparrow \\ \overline{\omega}(F(M_1, M_2, \dots, M_n)) & \text{otherwise.} \end{cases}$$
**Remark**: We can see $\omega(M)$ as the $\omega$-normal form of $\omega'(M)$. It follows that $\omega(M)=\Gamma\{N|M^{*'}N\}$. Intuitively, $\omega(M)$ is the minimum prefix of M guaranteed to exist in any N which can be derived from M, whatever could be the right-hand sides of the rules in $\Sigma$. Our terminology is consistent with [31] for $\lambda$-calculus, or [25,27] for recursive program schemes.

We note that in the TRS's that we consider subparts of redex schemes
are their own direct approximation :

**Lemma 4.5** : Let $\alpha \in \text{red}$. For every $u$ in $O(\alpha)$, we have $\omega(\alpha_{\Omega}/u) = \alpha_{\Omega}/u$.

**Proof** : Induction on the size of $\alpha_{\Omega}/u$. If $\alpha_{\Omega}/u=\Omega$ it is trivial. Otherwise by induction hypothesis we get $\overline{\omega}(\alpha_{\Omega}/u)=\alpha_{\Omega}/u$. By non-ambiguity we cannot have $\alpha_{\Omega}/u↑$, and thus $\omega(\alpha_{\Omega}/u)=\alpha_{\Omega}/u$.□

It follows easily from its definition that $\omega$ is monotonic increasing, i.e.
$M\preceq N$ implies $\omega(M)\leq\omega(N)$, idempotent, i.e. $\omega(M)=\omega^2(M)$ and a projection, i.e. $\omega(M)\prec M$.
More important, if $M\stackrel{*}{\to} N$, then $\omega(M)\leq\omega(N)$. Namely, approximation is increasing with
derivation (In fact, this is true also with $\to^*$). Finally, an $\Omega$-term $M$ is said to
be $\omega$-maximum iff, for every $N$ such that $N\not\preceq M$, we have $\omega(N)=\omega(M)$.

Now, we connect strongly sequential systems and the direct approximation
function by showing that nf'(M)=tt iff M is $\omega$-maximum.

**Notation** : Let $x \in V$. For any $M \in T_\Omega$, we define $M_x$ as $M$ in which all $\Omega_s'$ are replaced by $x'$, i.e. $M_x = M[x \leftarrow x | M/u = \Omega]$.

**Lemma 4.6** : $M \stackrel{*}{\to} N$ iff $\omega(M_x) \preceq_N x$ for some $x \notin V(M) \cup V(N)$.

**Proof** : First, let $M \stackrel{*}{\to} N$. Then $M_x \stackrel{*}{\to} P$ for some $P$ such that $N \preceq_P N_x$. Thus $\omega(M_x) \le \omega(P) \le \omega(N_x) \preceq_N x$. Conversely, let us use an induction on the size of $M$. If $M=\Omega$, then $M_x=x=\omega(M_x)=N_x$. As $x \notin V(N)$, then $N=\Omega$ and $M \stackrel{*}{\to} N$. The case $M=x$ is impossible since $x \notin V(M)$ and the case $M=y \ne x$ is straightforward. Now let $M=F(M^1, M^2, \dots, M^n)$. Take $n=1$ for simplifying. The definition of $\omega(M_x)$ gives two cases :

1) $\omega(M_x) = F(\omega(M_x^1)) \preceq_N x$. This means $N = F(N^1)$ and by induction $M \xrightarrow{1,} N^1$.
Hence $M \stackrel{*}{\to} N$.

2) $\omega(M_x) = \Omega$ because $F(\omega(M_x^1)) \uparrow \alpha_\Omega$ for some redex scheme $\alpha$. Thus $\alpha = F(\alpha^1)$ and $\omega(M_x^1) \uparrow \alpha_\Omega^1$. Hence $\omega(M_x^1) \preceq_P^1$ and $\alpha_\Omega^1 \preceq_P^1$ for some $P^1$. Consider the substitution $\sigma$ such that $\sigma(x)=\Omega$ and $\sigma(y)=y$ for all $y \ne x$. Let $Q^1=\sigma(P^1)$. Then $x \notin V(Q^1)$ and $Q_x^1 = P_x^1 \supseteq P^1$. By induction $M \xrightarrow{1,} Q^1$. Therefore $M \stackrel{*}{\to} F(Q^1)=Q$. But $\sigma(P^1) \supseteq \sigma(\alpha_\Omega^1) = \alpha_\Omega^1$ as $P^1 \supseteq \alpha_\Omega^1$. This implies that $Q \supseteq \alpha_\Omega$. Finally $Q \to N$. $\square$
**Lemma 4.7** Let $x \in V$ and $u \in O(M)$ such that $M/u=\Omega$. Then $\omega(M)=\omega(M[u \leftrightarrow x])$ iff $\omega(M)=\omega(M[u \leftrightarrow N])$ for all $\Omega$-terms $N$.

*Proof:* Obvious, once one remarks that $M[u \leftrightarrow x] \vdash$ implies $M[\dot{u} \leftrightarrow N] \vdash$ for every $N$. □

**Lemma 4.8** $nf'(M)=tt$ iff $M$ is $\omega$-maximum iff $\omega(M)=\omega(M_x)$, where $x$ is any variable.

*Proof:* Let $nf'(M)=tt$. Then $M \stackrel{*}{\to}'N$ for some normal form $N$. Thus $\omega(M_y) \leq_N y$ by

lemma 4.6 if $y \notin V(M) \cup V(N)$. But $N_y=N$ as $N$ is a normal form (without $\Omega_s'$). Thus $y \notin V(\omega(M_y))$ and $\omega(M_y) \leq_M N$. By monotonicity, one gets $\omega(\omega(M_y)) \leq \omega(M)$. Hence $\omega(M_y) \leq \omega(M)$; since $\omega$ is idempotent. Finally $\omega(M)=\omega(M_y)$ because $M \leq_M N_y$. By lemma 4.7, the $\Omega$-term $M$ is $\omega$-maximum. Conversely, let $M$ be $\omega$-maximum. Then $\omega(M)=\omega(M_y)$ for some $y \notin V(M)$. Thus $\omega(M_y) \leq_M N \leq_M N_z$ for some $z \neq y$. Therefore $M \stackrel{*}{\to}'M_z$ since $y \notin V(M) \cup V(M_z)$ by lemma 4.6, and $nf'(M)=tt$. Now $M$ is $\omega$-maximum iff $\omega(M)=\omega(M_x)$ by lemma 4.7. □

Therefore, one can decide easily if $nf'(M)=tt$ by testing $\omega(M_x)=\omega(M)$. Similarly, an index of the $nf'$ predicate can also be found effectively with the help of the following lemma.

**Lemma 4.9** Let $x \in V$ and $u \in O(M)$ such that $M/u=\Omega$. Then $u \in I(M)$ iff $\omega(M) \neq \omega(M[u \leftrightarrow x])$ iff $u \in O(\omega(M[u \leftrightarrow x]))$.

*Proof:* Let $u \notin J(M)$. That is, there is some $N \supsetneq M$ such that $\omega(N)=\omega(N_x)$, and $N/u=\Omega$. Then $M[u \leftrightarrow x] \leq_N N_x$, and $\omega(M[u \leftrightarrow x]) \leq \omega(N_x)=\omega(N)$. Without loss of generality, by lemma 4.7, we may assume $x \notin V(N)$. Thus $u \notin O(\omega(M[u \leftrightarrow x]))$, and $\omega(M[u \leftrightarrow x]) \leq_M N$, which implies $\omega(M[u \leftrightarrow x]) \leq \omega(M)$. Therefore $\omega(M)=\omega(M[u \leftrightarrow x])$.

Conversely, assume $\omega(M)=\omega(M[u \leftrightarrow x])$. This implies that $\Sigma$ is not empty. Let $\alpha$ be any redex scheme, and consider $N=M[v \leftarrow \alpha | M/v=\Omega$ and $v \neq u]$. We have $N \supsetneq M$, and $\omega(N_x)=\omega(M[u \leftrightarrow x])=\omega(M) \leq \omega(N)$. Thus $\omega(N_x)=\omega(N)$, and since $N/u=\Omega$ we have $u \notin J(M)$. Finally $\omega(M)=\omega(M[u \leftrightarrow x])$ implies $u \notin O(\omega(M[u \leftrightarrow x]))$, which concludes the proof. □

In order to find a strongly needed redex occurrence $u$ in any given term $M$, one has just to test $u \in O(\omega(M[u \leftrightarrow x]))$ for some redex occurrence $u$ and any given variable $x$. Thus a strongly needed redex is a redex which may increase, after its reduction, the direct approximation. (This may seem contradictory with the usual "correct evaluation strategies" considered in [1,7,23,30], but remember that we are in some kind of syntactic or free interpretation.)
Let us now give a few properties of indexes, which will be needed in the following.

**Lemma 4.10** If $uv \in I(M)$ and $\omega(M/u) = \Omega$ imply $u \in I(M[u \leftrightarrow \Omega])$.

*Proof:* $\omega(M[uv \leftrightarrow x]) \neq \omega(M) = \omega(M[u \leftrightarrow \Omega])$ and therefore $\omega(M[u \leftrightarrow x]) \neq \omega(M[u \leftrightarrow \Omega])$ using lemma 4.7 with $N=M/u[v \leftrightarrow x]$. □

**Lemma 4.11** If $uv \in I(M) \Rightarrow v \in I(M/u)$.

*Proof:* Let $uv \in I(M)$ and $v \notin I(M/u)$. Then $\omega(M/u) = \omega(M/u[v \leftrightarrow x])$ by lemma 4.9, and therefore $\omega(M) = \omega(M[u \leftrightarrow \omega(M/u)]) = \omega(M[u \leftrightarrow \omega(M/u[v \leftrightarrow x])]) = \omega(M[uv \leftrightarrow x])$, contradiction with $uv \in I(M)$. □

**Lemma 4.12** If $\omega(M/u) = \Omega$, then for every $v$ such that $v \uparrow u$ we have $v \in I(M) \Longleftrightarrow v \in I(M[u \leftrightarrow \Omega])$.

*Proof:* Obvious, since $\omega(M/u) = \Omega$ implies $\omega(M) = \omega(M[u \leftrightarrow \Omega])$ and $\omega(M[v \leftrightarrow x]) = \omega(M[u \leftrightarrow \Omega][v \leftrightarrow x])$. □

We are now left with the problem of deciding whether a TRS $\Sigma$ is strongly sequential or not. Since this property is closely related to the organization of the matching of redexes, we shall first consider this problem.

## 4.4 Sequential sets, Directions

**Definition:** Let $E$ be any set of $\Omega$-terms. We consider the predicate *match* defined by $match(M,E) = tt$ iff $M \succ E$. We say that $E$ is *sequential* iff $match(M,E)$ is sequential at every $M$. The set $Dir(M,E)$ of the indexes of this predicate in $M$ is called the set of *directions from $M$ to $E$*. As a particular case, we shall consider the predicate $isredex(M) = match(M,red_\Omega)$, and will abbreviate its set of indexes $Dir(M,red_\Omega)$ as $Dir(M)$. We have of course $I(M) \subset Dir(M)$, and we shall show below that if $\Sigma$ is strongly sequential, then $isredex$ is also sequential, which is decidable.

**Notation:** We write $M \not\equiv N$ iff $M$ and $N$ are incompatible, i.e. not $M \uparrow N$. Also $M \not\equiv E$ iff not $M \uparrow E$, i.e. $M \not\equiv N$ for all $N$ in $E$, and $M \not\equiv$ iff $M \not\equiv red_\Omega$.
**Lemma 4.13** Let M be an Ω-term and E be a set of Ω-terms. Then the following are equivalent :

(i) $u \in \mathit{Dir}(M,E)$

(ii) $M/u=\Omega$ and, for all $N \in E$ such that $N \uparrow M$, one has $u \in O(N)$ and $N/u \neq \Omega$

(iii) $M/u=\Omega$ and $M[u \leftarrow x] \neq E$ where $x$ is not a variable of any Ω-term in E.

**Proof** : Obvious. □

**Lemma 4.14** If $N \in E$ and $N \uparrow M$, then $\mathit{Dir}(M,E) = \mathit{Dir}(M \uparrow N, E')$ where $E' = \{P \in E | P \uparrow M\}$.

**Proof** : Suppose $u \in \mathit{Dir}(M,E)$. Then $M/u=\Omega$. But, since $N \in E$ and $N \uparrow M$, lemma 4.13 says that $u \in O(N)$. Thus $u \in O(M \uparrow N)$ and $(M \uparrow N)/u=\Omega$. Now, if $P \in E'$ and $P \uparrow (M \uparrow N)$, then $P \uparrow M$ and $u \in O(P)$ with $P/u \neq \Omega$. Thus $u \in \mathit{Dir}(M \uparrow N, E')$. Conversely, since $(M \uparrow N)/u=\Omega$ and $N \in E'$ with $N \uparrow (M \uparrow N)$, one has $u \in O(N)$ and $N/u \neq \Omega$. Thus $M/u=\Omega$ because $N \uparrow M$. Now take any $P \in E$ such that $P \uparrow M$. Then $P \in E'$ and $P \uparrow (M \uparrow N)$. Thus $u \in O(P)$ and $P/u \neq \Omega$. That is, $u \in \mathit{Dir}(M,E)$. □

**Lemma 4.15** If E is finite, one can decide if E is sequential. (One just checks that $\mathit{match}(M,E)$ is sequential at every M such that $M \leq E$.) Furthermore, if $\Sigma$ is a strongly sequential system, then isredex must be a sequential predicate.

**Proof** : If E is sequential, then $\mathit{match}(M,E)$ is sequential at every M, and in particular at every Ω-term prefix of some element of E. Conversely, E is sequential iff $\mathit{Dir}(M,E) \neq \emptyset$ for all M not in normal form such that $\mathit{match}(M,E)=\mathit{ff}$. Now, if $M \neq E$, then $\mathit{Dir}(M,E) = \{u \in O(M) | M/u=\emptyset\} \neq \emptyset$, since M is not in normal form. Assume that $M \uparrow N$ for some $N \in E$. Then $\mathit{Dir}(M,E) = \mathit{Dir}(M \uparrow N, E)$ by lemma 4.14. But $M \uparrow N \leq N$ and $\mathit{match}(M \uparrow N, E) = \mathit{ff}$, since $\mathit{match}(M,E) = \mathit{ff}$. Thus $\mathit{Dir}(M \uparrow N, E) \neq \emptyset$, which implies $\mathit{Dir}(M,E) \neq \emptyset$.

Now, let $\Sigma$ be strongly sequential. Then $\mathit{nf}'$ is sequential at every M in Ω-normal form (i.e. $\omega'(M)=M$), by definition. Thus, isredex is sequential at every Ω-normal form M. But, since $\Sigma$ is not ambiguous, every N such that $N \leq \mathit{red}_\Omega$ is in Ω-normal form. Thus $\mathit{isredex}(M)=\mathit{match}(M, \mathit{red}_\Omega)$ is sequential at every M according to the first part of the proof.□

Intuitively, a set E of Ω-terms is sequential iff we can factorize the matching of any term against E. As in Curien [8] for the general case of sequential functions, this factorization can be achieved here by a tree gathering all possible patterns. For instance, take

$$E = \{F(A,\Omega), F(G(E,\Omega),B), F(G(\Omega,E),C)\}$$

which is sequential. The corresponding matching tree is shown in Fig. 6,
where a node $\u$ corresponds to a query of the function symbol at occurrence u in the datum M, branches from u are the different successful alternatives for this function symbol query, and leaves are conventionally written as success nodes $\S_i$. These matching trees generalize the trie structures used to store dictionaries of strings.

<figure><img src="image_12.png" /><figcaption>Fig. 6</figcaption></figure>

This tree can easily be built up from $\Omega$-terms M such that $M \le E$, by considering the $Dir(M,E)$ sets. We shall see in the next paragraph how, in the case of strongly sequential systems, we may construct matching dags which permit to factorize local and global matches, yielding an efficient (linear) match algorithm.

## 4.5 Matching dags

We shall need here an hypothesis stronger than $red_{\Omega}$ sequential. The next paragraph will show that this hypothesis is equivalent to strong sequentiality.
**Notation** : We shall write $M\langle red_{\Omega} \rangle$ for $M\llcorner red_{\Omega}$ and $M\lceil red_{\Omega}$, and $M\uparrow\uparrow$ for $M\uparrow$ and $M\neq\Omega$.

**Hypothesis** : We assume the existence of a function Q mapping every $\Omega$-term M such that $M\llcorner red_{\Omega}$ into a non-empty set of its directions : $\emptyset\neq Q(M)\subset Dir(M)$, and such that $\forall u\in Q(M), \forall N\llcorner red_{\Omega}$, if $M[u\leftrightarrow N]\llcorner red_{\Omega}$ then :

$$ 
\begin{array}{l}
Q_1: \exists v \ uv\in Q(M[u\leftrightarrow N]) \\
\text{and} \\
Q_2: \nabla v \ uv\in Q(M[u\leftrightarrow N]) \Rightarrow v\in Q(N).
\end{array}
$$

**Construction of a matching dag associated with Q verifying the hypothesis above.**

Let $red=\{\alpha_1, \dots, \alpha_n\}$. We consider $Occ=\bigcup_{i\le n} \tilde{O}(\alpha_i)$, and a set $Succ=\{S_1, \dots, S_n\}$ of success tokens disjoint from Occ. We construct a graph whose nodes are all :

a) pairs $<M,v>$ such that $M\llcorner red_{\Omega}, v\in Q(M)$, and $\nabla u M/u\uparrow\uparrow \Rightarrow u\lhd v$.

b) pairs $<\alpha_i, S_i>$, $1\le i\le n$ (the success nodes.)

Let $<M,v>$ be a node, F a function symbol in F, and $M'=M[v\lhd F\lhd\Omega]$. If $<M',*>$ is a node, where * denotes any element of OccUSucc, we draw an arc :

$$ <M, v> \xrightarrow{F} <M',*>. $$

It is clear that our graphs are directed acyclic. We shall therefore call them *matching dags*.

**Definition** : The node $<M,*>$ is said to be *accessible* iff either it is the origin node $<\Omega,\Lambda>$ or there is some accessible node $<M_1,v_1>$ and $F\in F$ such that

$$ <M_1, v_1> \xrightarrow{F} <M,*>. $$

**Lemma 4.16** If $<M,v>$ is accessible, then for every u such that $M/u\uparrow\uparrow$ the pair $<M[u\leftrightarrow\Omega],u>$ is an accessible node and there exists in the matching dag a path : $<M[u\leftrightarrow\Omega],u> = <M[u\leftrightarrow N_1],uw_1> \xrightarrow{F_1} <M[u\leftrightarrow N_2],uw_2> \xrightarrow{F_2} \dots <M[u\leftrightarrow N_k], uw_k> = <M,v>.$

Furthermore for every such path there exists in the matching dag an identically labeled path :

$$ <\Omega, \Lambda> = <N_1, w_1> \xrightarrow{F_1} <N_2, w_2> \xrightarrow{F_2} \dots <N_k, w_k> = <M/u, v/u>. $$

**Proof** : Induction on the definition of accessible.

If $M=\langle\Omega,\Lambda\rangle$, it is trivial. Otherwise, assume $<M,v>$ is an accessible node satisfying the condition above such that $<M,v> \xrightarrow{F} <M',v'\rangle$. Now let u be such
that $M'/u^{\uparrow\uparrow}$. Since $\langle M', v' \rangle$ is a node, we have $u \prec v'$. Similarly $\langle M, v \rangle$ being a node, the case $u|v$ is impossible, and therefore $u \prec v$.

$M'[u \leftrightarrow \Omega] = M[u \leftrightarrow \Omega]$, and $M'/u = M/u[v/u \leftrightarrow F^\rightarrow \Omega]$, and thus $M/u^\rightarrow$.

**case 1** $u=v$. Then $\langle M'[u \leftrightarrow \Omega], u \rangle = \langle M, v \rangle$ is accessible by hypothesis. Also $M'/u = F^\rightarrow \Omega$, and $M'/u^\rightarrow$ implies $M'/u \prec \text{red}_\Omega$.

**case 2** otherwise, we get $M'/u^{\uparrow\uparrow}$, and by induction hypothesis we get $\langle M'[u \leftrightarrow \Omega], u \rangle = \langle M[u \leftrightarrow \Omega], u \rangle$ accessible, and $\langle M/u, v/u \rangle$ is a node. In particular $M/u \prec \text{red}_\Omega$, and $v/u \in Q(M/u) \subset \text{Dir}(M/u)$. Therefore in this case too $M'/u \prec \text{red}_\Omega$.

In both cases we have shown $\langle M'[u \leftrightarrow \Omega], u \rangle$ is an accessible node, and the existence of the first path for $\langle M', v' \rangle$ follows, since $\forall j \le k \ M[u \leftrightarrow N_j] = M'[u \leftrightarrow N_j]$, assuming the existence of the path for $\langle M, v \rangle$ like in the statement of the lemma. Let us now show that the corresponding path for $\langle M/u, v/u \rangle$ can be extended.

We have shown above $M'/u \prec \text{red}_\Omega$. But since $\langle M', v' \rangle$ is a node, $M' \prec \text{red}_\Omega$. We get easily $M'/u \prec \text{red}_\Omega$, because either $u=\Omega$, or else using the non-ambiguity condition. Also for all $u'$, $M'/uu'^{\uparrow\uparrow}$ implies $u' \prec v'/u$. Finally, using $u \in Q(M[u \leftrightarrow \Omega]) = Q(M'[u \leftrightarrow \Omega])$, we get by condition $Q_2$ that $v'/u \in Q(M', u)$, and therefore $\langle M/u, v/u \rangle \xrightarrow{F} \langle M'/u, v'/u \rangle$. $\square$

**Lemma 4.17** Let $\langle M, v \rangle$ be an accessible node, and $M' = M[v \leftrightarrow F^\rightarrow \Omega]$. If $M'^{\uparrow}$, then there is some node $\langle M', * \rangle$ such that $\langle M, v \rangle \xrightarrow{F} \langle M', * \rangle$.

**Proof** : First of all, since $M' \prec \text{red}_\Omega$ and $v \in Q(M) \subset \text{Dir}(M)$, the hypothesis $M'^{\uparrow}$ implies $M' \prec \text{red}_\Omega$.

**case 1** $M' = \alpha_{i_1 \Omega}$. Then $\langle M, v \rangle \xrightarrow{F} \langle M', S_i \rangle$.

**case 2** $M' \prec \text{red}_\Omega$. Let $u$ be such that $M'/u^{\uparrow\uparrow}$.

Either $u=v$, or $M'/u^{\uparrow\uparrow}$, and therefore $u \prec v$. Thus in all cases $u \prec v$. Now consider the maximum such $u$. Like in the proof of lemma 4.16, we get easily $u \in Q(M[u \leftrightarrow \Omega])$ and $M'/u \prec \text{red}_\Omega$. Using $Q_1$, we get $\exists v' \supset u$ such that $v' \in Q(M')$. By maximality of $u \prec M', v'$ is a node. Therefore $\langle M, v \rangle \xrightarrow{F} \langle M', v' \rangle$. $\square$
**Corollary** : When we remove non-accessible nodes from the matching dag, the terminal nodes are exactly all the success nodes.

This allows us to get rid of non-accessible nodes, which we shall assume from now on.

We use our matching dags to store the redex schemes of $\Sigma$. The search for a strongly needed redex is driven by the matching dag, in which are factored local and global matches. We need some extra information to know how to continue the search, when the global match has failed but some local ones may be still successful. The idea is similar to the one used in the extension to multiple patterns of the Knuth-Morris-Pratt string pattern matching algorithm [19].

**Definition** : Let $<M,v>$ be a non-success accessible node different from $<\Omega,\Lambda>$, and u be the minimum non-null prefix of v such that $M/v^+$. We define $Fail(<M,v>)$ as $<M/u,v/u>$, which is an accessible node by lemma 4.16.

We shall indicate in our matching dags $w'=Fail(w)$ by a dotted arc going from $w$ to $w'$. Also we shall drop the first component of the nodes, which is redundant since it is uniquely determined from a path accessing it. This first component is only convenient during the construction, and in proofs concerning our dags.

**Example**

Let $\Sigma = \{F(F(x,A),B) \to F(D,x), F(C,F(C,F(D,x))) \to F(x,A)\}$.

The matching dag associated with $red_\Sigma$ is given in Fig. 7.

<figure><img src="image_13.png" /><figcaption>Fig. 7</figcaption></figure>
We shall defer for the moment the computation of sets Q verifying our hypothesis. However, the next lemma shows us that they must be chosen among indexes.

**Lemma 4.18** Let M, u and v be such that <M/u,v> is an accessible node, and $\forall w M/w^{\rightarrow+} \Rightarrow w \geq u$. Then $uv \in I(M)$.

**Proof** : First of all we remark that for any $w \in O(M)$ such that $w|uv$, we have $\omega(M/w)=M/w$, by lemma 4.5. Now, for any $w$ such that $w \not\leq uv$, let $M_w =M[uv \rightarrow x]/w$. We show $\omega(M_w)=M_w$, by induction on $|uv/w|$. For $w=uv$, this is obvious. Otherwise, we get $\overline{\omega(M_w)}=M_w$, from above and the induction hypothesis. Let us show $M_w \neq$.

**case 1** $M/w^\#$. Then obviously $M_w^\#$.

**case 2** Otherwise, $M/w^{\rightarrow+}$. By hypothesis, $w \geq u$. By lemma 4.16 $w/u \in Q(M[w \leftarrow \Omega]/u)$ and $M/w \leftarrow \overline{red}_{\Omega}$. Using property $Q_2$ we get $uv/w \in \text{Dir}(M/w)$, and thus $M_w \neq$.

In all cases we get $\omega(M_w)=M_w$. When $w=\Lambda$ this shows $\omega(M[uv \rightarrow x])=M[uv \rightarrow x] \neq \omega(M) \subsetneq M[u \leftarrow \Omega]$, and therefore $uv \in I(M)$. $\square$

**Corollary** : If <M,v> is accessible, we have $v \in I(M)$. Assuming the existence of a matching dag, we shall now give an algorithm that computes, for any term M not in normal form, a strongly needed redex occurrence of M. We assume, without loss of generality, that M has no variables (Otherwise, treat them as constants).

We present A annotated with assertions $\{\dots\}$.

**Algorithm A**

Begin $\{M \in T, V(M)=\emptyset\}$
$u \leftarrow \Lambda$; $P \leftarrow \Omega$; $v \leftarrow \Lambda$; $w \leftarrow <\Omega, \Lambda>$;
getsymbol : $\{w=<P/u,v>, w \text{ accessible}, uv \in I(P), P \subsetneq M,$
$P[u \leftarrow \Omega] \subsetneq \omega'(M), \forall u' P/u' \rightarrow + \Rightarrow u' \geq u\}$
Let F be the head symbol of M at uv; $P \rightarrow P$; $P \rightarrow P[uv \leftarrow F\Omega]$;
search : $\{w=<P^-/u,v>, w \text{ accessible}, uv \in I(P^-), P^- \subsetneq M,$
$P[u \leftarrow \Omega] \subsetneq \omega'(M), \forall u' P/u' \rightarrow + \Rightarrow u' \geq u\}$
By cases on the matching dag at node w :

case 1 $w \xrightarrow{F} w' = <\alpha_i, S_i>: \{u \in I(P[u \leftarrow \Omega]), P/u = \alpha_i, \Omega\}$
exit with answer "redex of type i at u"

case 2 $w \xrightarrow{F} w' = <P', v'>: uv' \in I(P), P/u = P'$
$v \leftrightarrow v'$; $w \leftrightarrow w'$; go to getsymbol ;

otherwise {P/u#}

case 3 $w \not= <\Omega, \Lambda$: Let $w'=\text{Fail}(w) = <v', P'>$;
Let $u'$ such that $v=u'v'$;
$\{u'$ min such that $\Lambda \neq u' \leq v$ and $P^-/uu' \uparrow, P'=P^-/uu'\}$
$u \leftrightarrow uu'$; $v \leftrightarrow v'$; $w \leftrightarrow w'$; go to search ;

case 4 otherwise: {$w=<\Omega, \Lambda>, P^-/u=\Omega, v=\Lambda, \alpha' \in u' P/u' \uparrow +$}
choose u such that $P/u=\Omega$;
if no such u then {P=M, $\omega'(M)=M$}
exit with answer "normal form"
else go to getsymbol ;

End.

Matching dag theorem

Let M be a term without variables. If M is in normal form, algorithm A applied to M terminates with answer "normal form". Otherwise, it terminates with answer "redex of type i at u", with $u \in I(\omega'(M))$ and $M/u \approx_{\alpha_i \Omega} \emptyset$.

**Proof** : We use Floyd's method to prove the weak correctness of algorithm A, annotated with its assertions. We leave it to the reader to show the invariance of these assertions, using lemmas 4.10, 4.16, 4.17 and 4.18. The termination of the algorithm is easily established, since at getsymbol $|M|-|P|$ decreases, and at search $|v|$ decreases, with $|M|-|P|$ constant.

When A terminates at exit "normal form", we get $\omega'(M)=M$, i.e. $M \in NF$. When it terminates at exit "redex of type i at u", we get $M/u \not\rightarrow P/u=\alpha_i \Omega$. Therefore $\omega'(M)/u=\Omega$. Furthermore $P[u \leftarrow \Omega] \leq \omega'(M)$, and $u \in I(P[u \leftarrow \Omega])$. Therefore, by definition of index we get $u \in I(\omega'(M))$. □

Now that we have proven the correctness of our algorithm, we give a more
lisible version of it. We remove the redundant first component of the nodes in the
matching dag, and implement P by marking the occurrences explored in M. Also
variable u' now stands for uv of algorithm A, and we use the notation u' \div v to
denote u such that u' = uv.
Algorithm B

Input : term M, with $V(M)=\emptyset$.

Begin
u<Λ ; w< Λ ;
init : u'<u ;

getsymbol : let F be the head symbol of M at u' ;
mark occurrence u' in M ;

search : by cases on the matching dag at node w :

case 1 w<-> Sᵢ : exit "redex of type i at u"

case 2 w<-> w' = v' : u'<uv' ; w<-> w' ; go to getsymbol ;

otherwise

case 3 w≠ Λ : let w'=Fail(w)=v' ;
u<u'÷v' ; w<->w' ; go to search ;

case 4 otherwise

if all occurrences in M marked exit "normal form"

else choose u unmarked and go to init ;

End.

Algorithm B is non-deterministic for two reasons. The first one comes from the choice of u in case 4. It is natural to implement this choice by taking for u the first unmarked occurrence in M, say in preorder. By keeping a pointer (Free) to the last chosen occurrence, one pass in M will suffice for all the necessary choices. We assume below the existence of a function Searchfree (Free), which returns the first unmarked occurrence of M following Free in preorder, and the special value Done if there is none.

The second cause of non-determinism is that there may be several nodes w' in the matching dag satisfying case 2. This can be easily eliminated by making our matching dags deterministic, keeping only one arc labeled F from any node w. This does not mean that we can impose Q(M) to be a singleton, since the extremity of a deleted arc may be reachable through a failure arc. For instance, in Fig. 7, we may delete one of the two arcs issued from the origin node, but we must keep all the nodes.
When the matching dag is made deterministic, it is natural to store it
in a double array Next(w,F), indexed firstly by the nodes of the dag, and secondly
by the function symbols in F. This way the computation of which case to choose
at search is constant, i.e. independent of the size of red.

For a given Σ algorithm B is linear in the size of M, since an occurrence
of M is marked at every passage at getsymbol, and searchfree makes one pass in M.
However, the computations done at search depend on the length of v', i.e. on red,
and algorithm B has a running time O(h×|M|), where h is the maximum height of a
redex scheme. We shall now describe one more refinement, in which we get rid of
this h factor.

We need pointer u' only to read the occurrence in M at getsymbol. The new
value of u' updated at case 2 may be at some distance from the old value, but in
any case it is the son of some node in M that has been already explored. If we
keep in a stack all accesses of M at getsymbol, we shall be able to get directly at
this father, in a way that depends only from the path chosen in the matching dag.
We can precompute the corresponding displacement in the matching dag as follows.

Let v.k be the label of node w, and let $w_0$ be the node with label v on
some access path leading to w :

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

We shall keep as information for node w the *virtual address* <-n,k>, indicating
that a query corresponding to node w is effected by accessing the k-th son of the
node of M accessed at time -n. If we keep these accesses in a stack Display, with
current index Top, we have direct access to this node through Display (Top-n).

We must now make sure that our virtual addressing mechanism is correct,
independently of the path chosen to access w. The only difficulty comes from
the sharing in the dag. More precisely, we may have two paths of different lengths
leading from a node labeled with v to node w. Whenever this is the case, we shall
duplicate the common nodes of these two paths, so as to associate a unique virtual
address with every node.
After this unsharing has been effected we compute the fail arcs. More precisely, let $w=<M,v>$, and $u$ the minimum non-empty prefix of $v$ such that $M/u$. Let $w_1,F_1,w_2,F_2,...,w_k$ be the sequence whose existence is given by lemma 4.16. Lemma 4.16 tells us that by following this sequence from the origin, we arrive at some node $w'$. We must take precisely $Fail(w)=w'$, and we shall be sure this way that our virtual addressing will be correct, even when backtracking through the fail arcs. In particular, note that $w$ and $Fail(w)$ have the same virtual address.

### Example

Let us consider the system

$$ \Sigma \left\{ \begin{array}{l} G(F(A,x)) \to \dots \\ F(F(x,H(A)),B) \to \dots \\ G(F(F(x,H(y)),C)) \to \dots \end{array} \right. $$

with corresponding matching dag shown in Fig. 8. The node marked X has two distinct virtual addresses, and there is no way to get rid of the conflicting paths by making the dag deterministic. Fig. 9 shows the corresponding virtual matching dag, after duplication of node X, computation of virtual addresses, computation of fail arcs and suppression of non-determinism.

<figure><img src="image_15.png" /><figcaption>Fig. 8</figcaption></figure>
<figure><img src="image_16.png" /><figcaption>Fig. 9</figcaption></figure>

We are now ready to present the next refinement of our algorithm. We assume that the non-success nodes of the dag are coded with successive integers, with the origin coded 0. For $w$ a dag address and $F$ a function symbol, $Next(w,F)$ contains the address of its $F$-successor, if it exists, or $S_i$, or 0 to indicate failure. For $w \neq 0$, $Node(w)$ contains a virtual address $<-n,k>$. Finally, for every success node $S_i$ we keep in $Size(i)$ the size of $red_{i\Omega}$ (i.e. the length of any path leading from the origin in the dag to $S_i$); this is used as virtual address of the redex in case of success. We use pointer $P$ (represented in algorithm B by occurrence $u'$) to access term $M$, and $M(P)$ denotes the top function symbol of $M$ at $P$.
Algorithm C

Begin
  Free←origin of M;
  init : Top←0 ; w←0 ; P←Free;
  getsymbol : F←M(P) ; Mark P;
  Display(Top)←P ; Top←Top+1 ;
  search : w'←Next(w,F) ; by case on w' :
    - Sᵢ : exit "redex of type i at Display(Top-Size(i))"
    - 0 : if w≠0 then w←Fail(w) ; go to search ;
        else Free←Searchfree (Free) ;
          if Free=Done then exit "normal form"
          else go to init ;
    - otherwise : <-n,k>←Node(w') ;
                  P←k-th son at Display(Top-n) ;
                  w←w' ; go to getsymbol ;
End

End

Algorithm C is a generalization to trees of the extension of the Knuth-Morris-Pratt fast string matching algorithm to several patterns. It is straightforward to show that C has a running time of $O(|M|)$, independently of red.

Our final refinement consists in getting rid of the inner loop at search
by iterating sequences of global failures at compile time. The array Next is
now computed as follows. Let us consider the chain of Fail arcs issued from
node w in the dag : w₁=w, wᵢ₊₁=Fail(wᵢ) for 1≤i≤p, wₚ=0. Let F∈F.
There are two cases :

case 1 : For some i, 1 ≤ i ≤ p, there is an arc w_i → F w_i'. We set
Next(w, F) ← w'_m, for in the minimum such i.

case 2 : Otherwise : Next(w,F)←0, indicating failure of all local
and global searches.

We can now get rid of Fail(w) altogether, and the final version of
our algorithm is given below.
## Algorithm findredex

Begin

Free ← origin of M;

init : Top ← 0 ; w ← 0 ; P ← Free ;

getsymbol : F ← M(P) ; Mark P ;

Display(Top) ← P ; Top ← Top + 1 ;

w' ← Next(w,F) ; by cases on w' :

- Sᵢ : exit "redex of type i at Display(Top-Size(i))"

- O : Free ← Searchfree(Free) ;

if Free=Done then exit "normal form"

else go to init ;

- otherwise : <-n,k> ← Node(w') ;

P ← k-th son at Display(Top-n) ;

w ← w' ; go to getsymbol ;

End.

Note that more nodes may now be garbage-collected as non-accessible.
The resulting structure Next is no more a dag, but rather a finite automaton
transition graph. It is not clear whether this graph should be implemented
as lists rather than arrays. This space-time trade-off depends on the
structure of the particular Σ.

### Exemple :

With Σ as above, we construct from Fig. 9 the information given
in Table I. With input term

$$M=G(F(F(F(A,H(A)),B),H(B)),B))$$

algorithm findredex will explore M in the order shown by the numbers on
Fig. 10, and will stop with answer "redex of type 2 at x", with x the address
of the node labeled 7.
<table><thead><tr><th rowspan="2">w</th><th rowspan="2">Node (w)</th><th colspan="6">Next</th></tr><tr><th>F</th><th>G</th><th>H</th><th>A</th><th>B</th><th>C</th></tr></thead><tbody><tr><td>0</td><td></td><td>2</td><td>1</td><td>0</td><td>0</td><td>0</td><td>0</td></tr><tr><td>1</td><td>-1,1</td><td>3</td><td>1</td><td>0</td><td>0</td><td>0</td><td>0</td></tr><tr><td>2</td><td>-1,2</td><td>2</td><td>1</td><td>0</td><td>0</td><td>4</td><td>0</td></tr><tr><td>3</td><td>-1,1</td><td>5</td><td>1</td><td>0</td><td>S<sub>1</sub></td><td>0</td><td>0</td></tr><tr><td>4</td><td>-2,1</td><td>6</td><td>1</td><td>0</td><td>0</td><td>0</td><td>0</td></tr><tr><td>5</td><td>-1,2</td><td>2</td><td>1</td><td>7</td><td>0</td><td>4</td><td>0</td></tr><tr><td>6</td><td>-1,2</td><td>2</td><td>1</td><td>9</td><td>0</td><td>4</td><td>0</td></tr><tr><td>7</td><td>-3,2</td><td>2</td><td>1</td><td>0</td><td>0</td><td>8</td><td>S<sub>3</sub></td></tr><tr><td>8</td><td>-2,1</td><td>2</td><td>1</td><td>0</td><td>S<sub>2</sub></td><td>0</td><td>0</td></tr><tr><td>9</td><td>-1,1</td><td>2</td><td>1</td><td>0</td><td>S<sub>2</sub></td><td>0</td><td>0</td></tr></tbody></table>

Size(1)=3

Size(2)=Size(3)=5

<figure><img src="image_17.png" /><figcaption>Fig. 10</figcaption></figure>
The only non-constant space used by findredex (apart from the mark bits in M) is the stack Display. This stack is popped at init, i.e. every time all current searches fail. Actually we could do much better, since Display is accessed only at a maximum distance of h from its top, where h the maximum size of a redex scheme. We could therefore implement Display as a circular ring of length h. The instruction Top↔Top+1 would become Top↔(Top+1) mod h, and our algorithm would work in constant space (plus one bit for each node in M for the marks). However, this might not be desirable in practice, since if we want to implement a lazy interpreter using algorithm findredex, we should be able to dynamically restart it after effecting one step of reduction, and in that case we would need to keep the whole Display.

Note that in order to effect a reduction step, we must have unambiguous addresses for the variable occurrences in the redex scheme. For instance in the example above, we would distinguish between the two possible successes $S_2$, since variable x has virtual address -3,1 in one case and -2,1 in the other. This unsharing problem could be simplified by developing completely our dags as trees. Actually a slightly more general construction would be to directly construct matching trees, with nodes $w=\langle M, v \rangle$ such that $v \in Q(w)$, i.e. have Q depend on the access path to w, and not only on M.

We summarize this paragraph with:

**Fast tree pattern matching theorem**

Let $\Sigma$ be such that there exists a matching dag for $red_\Sigma$. For any term M not in normal form, the algorithm findredex will find a strongly needed redex occurrence of M in time $O(M)$.

## 4.6 Deciding strong sequentiality

We shall now show that strong sequentiality is equivalent to the conditions $Q_1$ and $Q_2$ of 4.5.

**Definition:** Let M be an $\Omega$-term. We define its set of increasing indexes as $J(M)$ defined by:

$$J(M) = \{u \in I(M) \mid \forall N \quad \omega(N) = \Omega \& \omega'(N) = N \Rightarrow \exists v \ge u \quad v \in I(M[u \leftarrow N]) \}.$$

Intuitively, an increasing index can be increased into an index whenever we replace it by a term which may become a redex after some reductions.
### Example

With
$$ \Sigma = \{F(G(A,x),B) \to \dots \\ F(G(x,A),C) \to \dots \\ G(E,E) \to \dots \}, $$
the first occurrence of $\Omega$ in $F(\Omega,\Omega)$ is a non-increasing index.

**Lemma 4.19** Let $\Sigma$ be strongly sequential. Then for any $M$ in $\Omega$-normal form we have $J(M) \neq \emptyset$.

**Proof** : Assume $\Sigma$ strongly sequential, and $M=\omega'(M)$. Let $I(M) = \{u_1, \dots, u_n\}$. Assume $J(M)=\emptyset$, i.e. for every $i \le n$, there exists $N_i$ such that $\omega(N_i)=\Omega$, $\omega'(N_i)=N_i$ and $\exists v \ge u_i \ v \in I(M[u_i \leftarrow N_i])$. Now consider :

$$ P = M[u_i \leftarrow N_i \mid 1 \le i \le n]. $$

We first show $\omega'(P)=P$. Since $M$ and the $N_i$'s are in $\Omega$-normal form, the only possible case of a redex in $P$ is when there is some $\alpha$ in red and $u$ in $\overline{\alpha}$ such that $\alpha_\Omega/u \not\le N_k$ for some $k \le n$. But then $\omega(\alpha_\Omega/u) \le \omega(N_k)=\Omega$, i.e. $\omega(\alpha_\Omega/u)=\Omega$, impossible by lemma 4.5. Thus $\omega'(P)=P$.

$\Sigma$ being strongly sequential, there exists $v$ in $I(P)$.

**case 1** $\exists k \le n \ u_k \nvDash v$. Then by repeated application of lemma 4.12 we get $v \in I(M[u_k \leftarrow N_k])$, contrary to the hypothesis on $N_k$.

**case 2** $\forall k \le n \ u_k \nvDash v$. Then by repeated application of lemma 4.12 we get $v \in I(M)$, impossible.

This completes the proof that $J(M) \neq \emptyset$.□

Let us now extend lemma 4.11 to $J$ :

**Lemma 4.20** $uv \in J(M) \Rightarrow v \in J(M/u)$.

**Proof** : Assume $uv \in J(M)$ and $v \notin J(M/u)$. That is, there exists $N$ such that $\omega'(N)=N$, $\omega(N)=\Omega$, and $\exists v' \ge v$ $v' \in I(M/u[v \leftarrow N])$. Now let $P=M[uv \leftarrow N]$. Since $uv \in J(M)$, there exists $w \ge uv$ such that $w \in I(P)$. By lemma 4.11, $w/u \in I(M/u[v \leftarrow N])$, a contradiction.□

Since $M \prec \overline{red}_\Omega$ implies $\omega'(M)=M$ and $J(M) \subset I(M) \subset \overline{Dir}(M)$, we get :

**Corollary** : If $\Sigma$ is strongly sequential, $J(M)$ satisfies $Q_2$.

An increasing index may, by definition, be increased into an index. Actually, it may even be increased into an increasing index :
**Lemma 4.21** Let $N$ be such that $\omega(N)=\Omega$ and $\omega'(N)=N$. For every $u \in J(M)$, there exists $v \ge u$ such that $v \in J(M[u \leftrightarrow N])$.

**Proof** : Assume $u \in J(M)$, $\omega(N)=\Omega$, $\omega'(N)=N$, and $w \ge u$ $v \in J(M[u \leftrightarrow N])$. Let $\{u_1, \dots, u_n\} = \{u_i \in I(M[u \leftrightarrow N]) | u_i \ge u\}$. For every $i \le n$ $u_i \notin J(M[u \leftrightarrow N])$ by hypothesis, that is there exists $N_i$ such that $\omega(N_i)=\Omega$, $\omega'(N_i)=N_i$ and $w \ge u_i$ $w \in I(M[u \leftrightarrow N_i[u_i \leftrightarrow N_{i+1}]])$, with $v_i=u_i/u$. Consider now $P=N[v_i \leftrightarrow N_i|1 \le i \le n]$. We get $\omega(P)=\Omega$ and $\omega'(P)=P$ like in the proof of lemma 4.19, and from $u \in J(M)$ we know that there exists $w \ge u$ such that $w \in I(M[u \leftrightarrow P])$. From above and repeated application of lemma 4.12 we must have $w|u_i \nV \le n$. Using lemma 4.12 again we get $w \in I(M[u \leftrightarrow N])$, impossible by definition of the $u_i$'s. $\square$

**Corollary** If $\Sigma$ is strongly sequential, $J(M)$ satisfies $Q_1$.

**Decidability of strong sequentiality theorem**

$\Sigma$ is strongly sequential iff there exists a matching dag for $red_{\Sigma}$.

**Proof** : If $\Sigma$ is strongly sequential, we have just seen that $J(M)$ satisfies $Q_1$ and $Q_2$.

Conversely, consider a matching dag as constructed in 4.5. Let $M$ be any $\Omega$-term such that $\omega'(M)=M$ and $\omega(M_x) \ne \omega(M)$. We shall show that there exists an index in $M$ by processing $M$ with algorithm A, slightly modified as follows. There are two more cases at getsymbol for the symbol read. If it is a variable, do as in "otherwise" (i.e. failure of global match).

If it is an $\Omega$, stop. We know from the assertions given for algorithm A, which are all valid still except that $P \not\in M$ at getsymbol should become $P \in M$, that in this last case we have $uv \in I(P)$. Since $M/uv=\Omega$, it follows that $uv \in I(M)$ by definition of index. Remark that this is the only way we may stop, since an exit at "normal form" is impossible by condition $\omega(M_x) \ne \omega(M)$, which implies $\exists w \in M$ $M/w=\Omega$, and an exit at "redex at u" is impossible by condition $\omega'(M)=M$. Therefore $I(M) \ne \emptyset$, which concludes the proof that $\Sigma$ is strongly sequential. $\square$
Remark that the statement of the theorem gives effectively a decision procedure : to test whether $\Sigma$ is strongly sequential, try constructing a matching dag as defined in 4.5. We may restrict conditions $Q_1$ and $Q_2$ to accessible nodes, and in that case $J$ is actually the maximum solution for $Q$. This is the solution we obtain if we start with $Q(M)=\text{Dir}(M)$, suppressing progressively elements with $Q_2$ and checking $Q_1$. In practice we might want to generate a smaller solution, starting with $Q(M)=\emptyset$, and adding elements with $Q_1$, checking $Q_2$. In either case several passes may be needed, and we do not know of an efficient algorithm (i.e. linear in the size of red) to build a matching dag for a strongly sequential $\Sigma$. Once a dag is found verifying $Q_1$ and $Q_2$, we effect the necessary unsharing and compute the fail arcs. (This process could be simplified by developping completely our dags as trees.) We then make the dag deterministic, complete the graph by iterating failures, garbage collect inaccessible nodes, and finally get an automaton table such as the one given in Table I. Some ingenuity may be needed in this process, if we want to minimize the size of the automaton. Of course this is done once and for all for a given $\Sigma$, and therefore we do not care very much about the cost of these operations. In practical terms, this is the cost of building a compiler for the programming language defined by $\Sigma$.

## 4.7 Recursive functions with constructors

We now consider a special case of our rewriting systems, corresponding to NPL programs [5]. We assume that the set $F$ of functions symbols is partitioned into two sets $F_R$ and $F_C$. $F_R$ is the set of recursive functions symbols and $F_C$ the set of constructors. Then any redex scheme $\alpha$ of red is of the form $F(\alpha_1, \alpha_2, ..., \alpha_n)$ where $F \in F_R$ and, for every $i$, the term $\alpha_i \in M(F_C, \nu)$ contains only constructor function symbols and variables. These particular systems will be called *systems with constructors*.

**Lemma 4.22** A system $\Sigma$ with constructors is strongly sequential iff the set $red_\Omega$ is sequential.

*Proof* : It is easy to check that, for every $M<red_\Omega$, the set $\text{Dir}(M)$ of directions of $M$ satisfies $Q_1$ and $Q_2$. $\square$
Furthermore, in this particular case, every failure arc of the matching dag leads to the origin node. Thus it is not necessary to store them. Therefore the dag is just the dag of directions for $red_Ω$. (In fact, any deterministic version of it will work.) Then, one finds strongly needed redexes by Algorithm C slightly modified. The failure case is now :

- O : **if** F ∈ $F_R$ **then** w ← O ; **go to** search ;
**else** as before

## 4.8 Simple systems

The algorithms of 4.5 factorize global and internal searches in order to get a strongly needed redex. This can be expressed exactly in terms of indexes by showing that, for any Ω-term M, the set I(M) of indexes can be given recursively by I(M)=I(M,red_Ω) where :

$$
I(M,E) = \begin{cases}
\{A\} & \text{if } M=\Omega \\
\{uv|u \in \text{Dir}(\bar{w}(M),E), v \in I(M/u,\text{red}_{\Omega} uE_u)\} & \text{otherwise,} \\
\text{with } E_u = \{\alpha/u|\alpha \in E, \alpha \uparrow \bar{w}(M)\}.
\end{cases}
$$

These sets $E_u$ are subsets of subexpressions of redex schemes. Thus, a very
natural restriction is to suppose them sequential. This leads to the following
definition.

**Definition :** Let $red_{\Omega}^* = \{\alpha_{\Omega}/u | \alpha \in \text{red}, u \in \bar{\mathcal{O}}(\alpha)\}$. Then $\Sigma$ is a sequential simple system iff all subsets of $red_{\Omega}^*$ are sequential sets.

Then, the set red is a simple forest in the sense of Hoffmann-O'Donnell [13]
since, if α and β are two compatible Ω-terms of red<sup>*</sup><sub>Ω</sub>, they must be comparable in
order to make the subset {α,β} sequential. But the algorithm defined in [13]
(Appendix C) does not work if non sequential simple systems are considered. In
the terminology of [13], the subsumption graph (i.e. the covering relation of ≲
in red<sup>*</sup><sub>Ω</sub>) is a tree where, at each node, there is an occurrence of Ω in the corres-
ponding Ω-term where the different branches are differenciated.
Let us define $\mathrm{Dir}^*(M)=\mathrm{Dir}(M,\mathrm{red}_\Omega^*)$, $I^*(\Omega)\equiv\{\Lambda\}$ and

$$I^*(M) = \{uv \mid u \in \mathrm{Dir}^*(\bar{w}(M)), v \in I^*(M/u)\}$$

when $M \neq \Omega$.

**Lemma 4.23** Let $\omega(M)=\Omega$. Then $I^*(M) \subset I(M)$.

**Proof** : Let $u \in I^*(M)$ and $x$ be any variable. We prove first by induction that $\omega(M[u \leftrightarrow x]) \neq \mathrm{red}_\Omega^*$. If $M=\Omega$, then $u=\Lambda$ and $\omega(M[u \leftrightarrow x])=x \neq \mathrm{red}_\Omega^*$, since $\Omega \not\in \mathrm{red}_\Omega^*$. Now suppose $M \neq \Omega$ and $\omega(M)=\Omega$. Then $u=\mathrm{vw}$ with $v \in \mathrm{Dir}^*(\bar{w}(M))$ and $w \in I^*(M/v)$. Let $M_v = \omega((M/v)[w \leftrightarrow x])$. By induction hypothesis $M_v \neq \mathrm{red}_\Omega^*$. Thus $M_v \neq \mathrm{red}_\Omega$ and $\bar{w}(M[u \leftrightarrow x]) = \bar{w}(M)[v \leftrightarrow M_v]$. Now, suppose that there is $\alpha \in \mathrm{red}_\Omega^*$ such that $\alpha \uparrow \bar{w}(M[u \leftrightarrow x])$. Since $\bar{w}(M) \leq \bar{w}(M[u \leftrightarrow x])$, we get $\alpha \uparrow \bar{w}(M)$. But $v \in \mathrm{Dir}^*(\bar{w}(M))$. Thus $v \in \mathcal{O}(\alpha)$ and $\alpha/v \neq \Omega$. Therefore $\alpha/v \in \mathrm{red}_\Omega^*$ and $\alpha/v \uparrow M_v$. Contradiction. Hence $\bar{w}(M[u \leftrightarrow x]) \neq \mathrm{red}_\Omega^*$. In particular $\bar{w}(M[u \leftrightarrow x]) \neq \mathrm{red}_\Omega$, which implies $\omega(M[u \leftrightarrow x]) = \bar{w}(M[u \leftrightarrow x])$ and $\omega(M[u \leftrightarrow x]) \neq \mathrm{red}_\Omega^*$.

Now, since $\omega(M)=\Omega$ and $\omega(M[u \leftrightarrow x]) \neq \Omega$, the occurrence $u$ is in $I(M)$ by lemma 4.9. $\square$

**Lemma 4.24** Any sequential simple system is strongly sequential.

**Proof** : Assume $\Sigma$ is a sequential simple system. We show first by induction that $I^*(M) \neq \emptyset$ for every $M$ such that $\omega(M)=\Omega$ and $\omega'(M)=M$. If $M=\Omega$, then $I^*(M) \equiv \{\Lambda\} \neq \emptyset$. Suppose now that $M \neq \Omega$, $\omega(M)=\Omega$ and $\omega'(M)=M$. Then $\bar{w}(M) \uparrow$. Thus because of the non ambiguity condition and since $\omega'(M)=M$, one cannot have $\alpha \leq \bar{w}(M)$ for some $\alpha \in \mathrm{red}_\Omega^*$. Therefore $\mathrm{Dir}^*(\bar{w}(M)) \neq \emptyset$ and by induction $I^*(M) \neq \emptyset$.

Now, if $M \subset \mathrm{red}_\Omega$, then $\omega(M)=\Omega$ and $\omega'(M)=M$ (again by non ambiguity). Thus $I^*(M) \neq \emptyset$ and $I^*(M)$ satisfies obviously $Q_1$ and $Q_2$. $\square$

The matching dag of a sequential simple system can be built up easily from $I^*(M)$ by induction on the size of $M$ as follows. Suppose $<N,v>$ is a node of the matching dag, $M=N[v \leftrightarrow \bar{F}\Omega]$ and $M' \subset \mathrm{red}_\Omega$. Then search, along the chain of failure arcs starting at $<N,v>$, the first node $<N',v'>$ with an outgoing arc labelled by $F$. If there is no such node, then choose any $u \in \mathrm{Dir}^*(M)$, create node $<M,u>$ with an $F$-arc from $<N,v>$ to $<M,u>$ and a failure arc from $<M,u>$ to $<\Omega,\Lambda>$. Otherwise, let $v=\mathrm{wv'}$ and $<M',u'>$ be the extremity of the $F$-arc outgoing from $<N',v'>$. Then, taking
u=wu', create node <M,u> with an F-arc from <N,v> to <M,u> and a failure arc from <M,u> to <M',u'>. Thus the matching dag (which is then a tree) can be efficiently built up in one top-down pass starting from the origin (not bottom-up as in [13]).

### Example

Let $\Sigma$ be such that $\text{red} = \{F(A, G(x, y, C)), F(B, G(D, x, C)), G(E, x, D)\}$. Then the two possible matching dags associated to the sequential simple system $\Sigma$ are given in Fig. 11.

<figure><img src="image_18.png" /><figcaption>Fig. 11</figcaption></figure>

Finally, O'Donnell [26] gave a sufficient condition for insuring the termination of the leftmost outermost derivation sequence. This condition is as follows. Remember that when $u, v \in O(M)$, then $u$ is said to be before $v$ in
preorder, written $u \leq_M v$, iff either $u \leq \nu$ or $u|v$ with u to the left of v. Let $\Sigma$ be a left system iff :

$$ \forall \alpha \in \text{red}_{\Sigma} \quad \forall u, v \in O(\alpha) \quad \alpha/u \in \mathcal{V} \ \& \ u \leq_{\alpha} v \implies \alpha/v \in \mathcal{V}. $$

Thus, in redex schemes of a left system, after a variable there could be only variables in preorder. One can prove easily that left systems are particular sequential simple systems and that they correspond exactly to systems where the leftmost outermost redex of any term is strongly needed. One nice example of left systems, given in [26], is the combinatory logic case, i.e. when

$$ \Sigma = \{ A(I, x) \to x, \\ A(A(K, x), y) \to x, \\ A(A(A(S, x), y), z) \to A(A(x, z), A(y, z)) \} $$

## Conclusion

As usual, optimal evaluation strategies are expected by adding some sharing mechanism to call by need. Here, duplications of subterms can be avoided by implementing terms in dags. This optimality result seems to be provable along lines of [3,20]. Another issue is to generalize propositions of our paper to more complicated rewriting systems. For instance, does one really need the non ambiguity condition ? Can we treat systems with bound variables, such as the $\lambda$-calculus ? Or with imperative features ? For the semantics of our systems, some fully abstraction result as in [27] can be proved, which shows that not all continuous functions need to be considered, but only stable ones [2]. Finally, it seems possible to consider the general problem of tree pattern matching along the lines of this paper, and thus to define sets of patterns where a linear top-down matching algorithm could exist. However, this problem differs from finding strongly needed redexes since then one has not to consider replacement of matching subterms.
REFERENCES

[1] G. BERRY, "Séquentialité de l'évaluation formelle des lambda-expressions", Proc. 3rd International Colloquium on Programming, Paris, March 1978, Dunod.

[2] G. BERRY, "Stable Models of Typed Lambda-calculi", Proc. 5th ICALP Conf., Udine, 1978, Italy.

[3] G. BERRY, J-J. LEVY, "Minimal and Optimal Computations of Recursive Programs", Proc. 3rd POPL Conf., Santa Monica, Jan. 1977. Also JACM Vol 26, N° 1, 1979.

[4] G. BERRY, J-J. LEVY, "Letter to the Editor, Sigact News, 11, 1, Summer 1979.

[5] R. BURSTALL, "Design Considerations for a Functional Programming Language", Infotech State of the Art Conf., Copenhagen, 1977.

[6] R. BURSTALL, J.A. GOGUEN, "Putting Theories Together to Make Specifications", 5th IJCAI Conf., Boston, 1977.

[7] J-M. CADIOU, "Recursive Definitions of Partial Functions and their Computations", Ph. D. Thesis, Stanford, March 1972.

[8] P.L. CURIEN, "Algorithmes séquentiels sur structures de données concrètes", Thèse de 3ème Cycle, Université de Paris VII, Mars 1979.

[9] H.B. CURRY, R. FEYS, "Combinatory Logic", Vol 1, North Holland, 1958.

[10] P.J. DOWNEY, R. SETHI, "Correct Computation Rules for Recursive Languages", SIAM Journal, Vol 5, N° 3, Sept. 1976.

[11] H. EHRIG, B.K. ROSEN, "The Mathematics of Record Handling", Proc. 4th ICALP Conf., Turku, 1977.

[12] J.V. GUTTAG, E. HOROWITZ, D.R. MUSSER, "Abstract Data Types and Software Validation", Research Report 76-48, ISI, Aug. 1976.
[13] M. HOFFMANN, M. O'DONNELL, "Interpreter Generation using Tree Pattern Matching", Proceedings 6th POPL, San Antonio, Jan. 1979.

[14] G. HUET, "Confluent Reductions : Abstract Properties and Applications to Term Rewriting Systems", Proc. 18th FOCS Conf., 1977.

[15] G. KAHN, G. PLOTKIN, "Domaines concrets", Rapport Laboria N° 336, Décembre 1978.

[16] S.C. KLEENE, "Introduction to Metamathematics", North-Holland, 1952.

[17] J.W. KLOP, Ph. D. Thesis, Utrecht, To appear.

[18] D.E. KNUTH, P.B. BENDIX, "Simple Word Problems in Universal Algebras", Computational Problems in abstract algebra, Ed J. Leech, Pergamon Press 1970, pp. 263-297.

[19] D.E. KNUTH, J. MORRIS & V. PRATT, "Fast Pattern Matching in Strings", SIAM Journal on Computing, Vol. 6, N° 2, 1977, pp. 323-350.

[20] J-J. LEVY, "Réductions correctes et optimales dans le lambda-calcul", Thèse, Paris 7, Jan. 1978.

[21] J. McCARTHY, "A Basis for a Mathematical Theory of Computation", Computer Programming and Formal Systems, Eds. P. Braffort and D. Hirschberg, North-Holland, 1963, pp. 33-70.

[22] R. MILNER, "Implementation and Application of Scott's Logic for Computable Functions", Proc. ACM Conf. on Proving Assertions about Programs, SIGPLAN Notices 7.1, Las Cruces, Jan. 1972.

[23] R. MILNER, "Fully Abstract Models of Typed Lambda-calculi", TCS, Vol 4, N° 1, Feb. 1977.

[24] D.R. MUSSER, "A Data Type Verification System Based on Rewrite Rules", 6th Texas Conf. on Computing Systems, Austin, Nov. 1978.
[25] M. NIVAT, "On the Interpretation of Recursive Polyadic Program Schemes",
Symposia Mathematica, Vol XV, Istituto Nazionale di Alta Matematica,
Italy, 1975, pp. 225-281.

[26] M. O'DONNEL, "Computing in Systems Described by Equations", LNCS N° 58,
Eds. G. Goos and J. Hartmanis, Springer, 1977.

[27] J-C. RAOULT, J. VUILLEMIN, "Operational and Semantic Equivalence between Recursive Programs", 10th SIGACT Conf., San Diego, 1978.

[28] B.K. ROSEN, "Tree Manipulation Systems and Church-Rosser Theorems", JACM,
Vol 20, N° 1, 1973.

[29] J. STAPLES, "Computation on Graph-like Expressions", Report N° 2/77,
Math & Comp. Science, Queensland Institute of Technology, Brisbane,
Australia, 1977.

[30] J. VUILLEMIN, "Correct and Optimal Implementation of Recursion in a
Simple Programming Language", JCSS, Vol 9, N° 3, 1974, pp. 332-354.

[31] C.P. WADSWORTH, "Semantics and Pragmatic of the λ-Calculus", Ph. D. Thesis,
Oxford, 1971.