# On recursive equations having a unique solution

Bruno Courcelle

► To cite this version:

Bruno Courcelle. On recursive equations having a unique solution. [Research Report] IRIA-RR-285, IRIA. 1978, pp.57. hal-04716552

HAL Id: hal-04716552

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

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

Distributed under a Creative Commons Attribution 4.0 International License
wiv. 03860

RR 285

RIA

laboria

laboratoire de recherche
en informatique
et automatique

ON RECURSIVE EQUATIONS
HAVING
A UNIQUE SOLUTION

Bruno COURCELLE

Rapport de Recherche N° 285

Mars 1978

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20
ON RECURSIVE EQUATIONS HAVING A UNIQUE SOLUTION

Bruno Courcelle

IRIA

Résumé :

On donne des conditions sur un système de réécriture confluent S qui permettent de définir la **forme normale** d'un terme (arbre) infini. On obtient ainsi une caractérisation de l'équivalence des schémas de programme récursifs modulo l'ensemble S d'équations.

On donne aussi des conditions suffisantes pour qu'un schéma de programme Σ soit S-univoque c'est-à-dire ait une et une seule solution modulo S (en considérant Σ comme un système d'équations). On obtient des preuves d'équivalence qui ne font appel à aucun «principe d'induction» mais seulement à des vérifications d'équations.

Ce résuitat est étendu ensuite à des théories équationnelles de la forme R = SUE où S est comme ci-dessus et E est un ensemble non-noetherien d'équations.

Abstract :

We give conditions on a Church-Rosser term rewriting system S allowing to define S-normal forms for infinite trees (i.e.infinite terms). We obtain in this way a characterization of the S-equivalence of recursive program schemes (i.e. equivalence of recursive program schemes in all interpretations which validate S now considered as the set of axioms of an equational theory).

We give sufficient conditions for a recursive program scheme Σ to be S-univocal i.e. to have only one solution up to S-equivalence (considering Σ as a system of equations). For such schemes, we obtain proofs of S-equivalence which do not use any «induction principle» but only consist in checking equations.

This result can be extended to an equational theory of the form R = S ∪ E where S is as above and E is a set of equations generating a non noetherian reduction.
# 1 - INTRODUCTION

(1.1) Investigations on recursive programs have been
developped in different directions :

(1) Formal proofs that two recursive programs are equivalent.

Different methods have been proposed after
Mc Carthy [16], most of them based on the consideration
of a program as a system of functional equations and
the computed function as the least fixpoint of the
system. See [18].

(2) Algebraic definition of the semantics ([6]).

An infinite tree ([5], [1]) (i.e. an infinite term)
$T(\phi)$ can be associated with a recursive program scheme
(i.e. a recursive program containing uninterpreted
function symbols). The function $\phi_I$ computed by $\phi$ in
an interpretation $I$ (providing meaning to function
symbols) is the image of $T(\phi)$ under a certain canonical
homomorphism.

(3) Classes of interpretations ([2], [3], [6])

Two recursive program schemes $\phi$ and $\psi$ are
C-equivalent (where C is a class of interpretations)
if $\phi_I = \psi_I$ for all $I \in C$. Triples $\langle\phi, \psi, C\rangle$ such that
$\phi \equiv_C \psi$ (i.e. $\phi$ and $\psi$ are C-equivalent) may be used to
transform programs as for instance in [4] and [11]. And
a proof that two recursive programs are equivalent is
clearer if it is written as a proof of a C-equivalence
of two recursive program schemes φ and ψ, for some class
C being both as large as possible but specified in
a usable way (it is clearly not interesting to take for
C the class of all interpretations I such that φᵢ = ψᵢ).
In this paper, usable will mean *equational* i.e. of the
form C = E<sub>R</sub> = { I/tᵢ = t'ᵢ for all (t, t') ∈ R } where R
is a set of pairs of finite terms (which are to define
equal functions).

We now present informally some questions raised and
partially solved in this paper. See section 2 for the
notations.

(1.2) This paper is concerned with the following problems :

(α) find characterizations of ≡<sub>E<sub>R</sub></sub> (simply denoted by ≡<sub>R</sub>),

(β) find proofs methods for φ ⇔ R ψ,

(γ) having proved that φ ⇔ R τ for some finite term
containing φ, is it possible to take φ = τ as a new
definition of φ ( in interpretations of E_R) ?

This question arises in particular in [4] (see
also [13]) where recursive programs are transformed as
follows.

Starting with a set R of axioms and a recursive
scheme φ (more precisely a system Σ of functional
equations, φ being one of the function variables) one
rewrites φ into a E<sub>R</sub>-equivalent term τ using Σ
as a thue rewriting system (i.e. in the two directions :
"folding" and "unfolding") and R ("laws about primitives")
(formally, $\phi \stackrel{*}{\rightarrow}_{R \cup \Sigma} \Sigma$).

It may be interesting to redefine $\phi$ by the equation

$$ \Sigma': \phi = \tau $$

provided ($\Sigma', \phi$) $\equiv_R$ ($\Sigma, \phi$) (i.e. $\phi$ defined by $\Sigma'$ is $E_R$-equivalent to $\phi$ defined by $\Sigma$).

Since $\phi$ defined by $\Sigma$ is a solution of $\Sigma'$ modulo $\equiv_R$
and the function defined by an equation is its least
solution :

$$ ( \Sigma', \phi ) \leq_R ( \Sigma, \phi ) $$

But the equivalence does not necessarily hold as
shown by :

(1.3) **Example :**

$$ R : \text{gf}_{v_1} = \text{fg}_{v_1} $$

$$ \Sigma : \left\{ \begin{array}{l} \phi = f\phi \\ \psi = g\phi \end{array} \right. $$

Then we obtain :

$$ \psi \equiv_R g\phi \equiv_R gf\phi \equiv_R fg\phi \equiv_R f\psi $$

The question is whether one can take

$$ \Sigma' : \psi = f\psi $$

as a new definition of $\psi$, i.e. whether $\psi \equiv_R \phi$.

$$ \text{Let } T(\phi) = f^{\omega} = \text{Sup}_n \{f^{n}_{\Omega}\}, \quad T(\psi) = gf^{\omega} = \text{Sup}_n \{gf^{n}_{\Omega}\} \text{ then} $$
T(Ψ) ≠_R T(φ) since for no n,m ∈ N, gf<sup>n</sup>_Ω ≤_R f<sup>m</sup>_Ω
(and by (2.3.1.) and (2.3.4.) below). Hence ψ ≠_R φ and
ψ ≠_R φ . □

The answer to (Y) is positive if we know that the
new equation φ = τ has a unique solution modulo ≡_R.
Such an equation is said R-univocal and the definition
extends naturally to systems of equations. Hence a new
question :

(δ) which systems of equations are R-univocal ?

To know that an equation φ = τ is R-univocal can
help in proving an equivalence of the form φ ≡_R ψ
for some other recursive scheme ψ. It suffices to prove
the equivalence ψ ≡_R τ {ψ/φ} . This schema of proof has
been introduced by Mc Carthy in [16] for recursive equa-
tions that define total functions and, for this reason,
have a unique solution.

An infinite tree T is R-*maximal* if for all infinite
tree T', T ≤_R T' implies T ≡_R T'. It is clear that φ
is R-univocal if T (φ) is R-maximal. Hence the following
question, related to both (α) and (δ) :

(ε) Which infinite trees are R-maximal ?

Let us sketch the answers given to these questions.

In section 3 we consider sets R of equations which
can be arranged to form a <u>confluent</u> <u>noetherian</u> <u>reduction</u>
S ( [9] or a Church-Rosser term rewriting system such
that every sequence of rewritings is finite). Hence each
finite term (tree) t has a unique S-*normal* form c_S(t)
(and $t \stackrel{*}{\rightleftharpoons}_S t'$ iff $c_S(t) = c_S(t')$).

We also assume that S is *monotone* i.e. that it
commutes in a certain sense with $\prec$, the order on trees.
It follows in particular that $t \prec t'$ implies $c_S(t) \prec c_S(t')$.
Thus the *S-normal form* of an infinite tree T can be defi-
ned by $c_S(T) = \text{Sup} \{c_S(t) / t \prec T\}$ and we get an
answer to question (α) by :

$T \le_S T'$ iff $c_S(T) \prec c_S(T')$

and to question (ε) by :

T is S-maximal if $c_S(T)$ is maximal w.r.t. $\prec$. Suffi-
cient conditions for a reduction S to be monotone and for
a scheme $\Sigma$ to be S-univocal are thus obtained.

We extend these results in section 4 to equational
theories R of the form S U E where S is as above and
E is a set of non noetherian equations. We also require
for E certain commutation properties with $\underset{S}{*} \to$ and $\prec$,
the finiteness of $[t] \underset{E}{*} \to$ for all finite t and we obtain :

$T \le_R T'$ iff $c_S(T) \sim_E c_S(U) \prec c_S(T')$ for some U
and
$T$ is R-maximal if $c_S(T)$ is maximal w.r.t. $\prec$.

We give sufficient conditions for <S,E> to be mono-
tone and the conditions on recursive schemes given in
section 3 insure they are R-univocal.

The relations S,E and E⁻¹ are assumed left-finear in
sections 3 and 4 (we simply say that <S,E> is linear).
In section 5 we sketch a method for dealing with non linear
equational theories <S,E>. All the necessary background
about recursive schemes, interpretations and reductions is
given in section 2.
## 2 - DEFINITIONS AND PRELIMINARIES.

### (2.1) Finite and infinite trees (terms).

Let $V_k = \{v_1, \dots, v_k\}$ and $V = \bigcup_{k \ge 1} V_k$ be the set of variables, F be a set of function symbols with arity $(f \in F$ has arity $\rho(f) \in N$ and $F_i = \{f \in F \mid \rho(f) = i\})$.

Let $M(F,V)$ be the set of finite well-formed terms on $F \cup V$, written in Polish prefix notation. In order to increase the readability, especially in examples, we add parentheses and commas to isolate the arguments of a $k$-ary symbol for $k \ge 2$. As an example, if we take

$\rho(f) = \rho(g) = 1, \rho(k) = 2$ and $\rho(h) = 3$
the term

$hfv_1gv_2kkv_1v_2fv_3v_1$

will be written

$h (fk(v_1,gv_2), k(k(v_1,v_2),fv_3), v_1)$.

The elements of $M(F,V)$ will also be called finite trees.

Let $\Omega$ be an extra symbol of arity 0 and $M_\Omega(F,V) = M(F \cup \{\Omega\}, V)$ the set $M_\Omega(F,V)$ is ordered by $\prec$ defined as follows (for $t, t_1, \dots, t'_k \in M_\Omega(F,V)$):

$$ (1) \quad \Omega \prec t $$

$$ (2) \quad \text{if } x \in V \cup F_0 \text{ then } x \prec t \text{ iff } t = x, $$

$$ (3) \quad \text{ft}'_1 \dots t'_k \prec t \text{ iff } t = ft_1 \dots t_k \text{ and } \\ t'_i \prec t_i \text{ for } i = 1, \dots, k. $$

The letters $s,t,u,z,s',t', \dots$, $s_1, s_2, \dots$ will always denote elements of $M_\Omega(F,V)$.
A term $u$ is a **subterm** of $t$ if $u = t$ or $t = f^1 t_1 \dots t_k$ and $u$ is a subterm of some $t_i$ (recursive definition $^n$ !).

A subset $\Delta$ of $M_\Omega(F,V)$ is **directed** if for all $t_1, t_2 \in \Delta$ there exists $t_3 \in \Delta$ such that $t_1 \prec t_3$ and $t_2 \prec t_3$.

Every such $\Delta$ has a least upper bound which is an infinite tree $\text{Sup}(\Delta)$. Let $M_\Omega^\infty(F,V)$ be the set of finite and infinite trees, constructed formally in [5] and in [1] under the notation $\text{CT}_F(V)$. The order extends $M_\Omega^\infty(F,V)$ and each $T \in M_\Omega^\infty(F,V)$ is the least upper bound of $\{ t \in M_\Omega^\infty(F,V) \mid t \prec T \}$ (which is directed).

We denote by $M_\Omega^\infty(F,V)$ the set of maximal elements of $M_\Omega^\infty(F,V)$. In a pictorial representation, $T \in M_\Omega^\infty(F,V)$ iff $\Omega$ does not occur in $T$, hence the notation. Remark also that $M(F,V)$ is the set of maximal elements of $M_\Omega(F,V)$.

The letters $T, U, T'$, ... will always denote elements of $M_\Omega^\infty(F,V)$.

It will be useful to have a precise way to denote occurrences of symbols in a tree.

Let $N_+ = \{1, 2, 3, \dots\}$. Let $x \in F \cup V \cup \{\Omega\}$.
For all $t \in M_\Omega^\infty(F,V)$ the set $O(x,t) \subseteq N_+$ of occurrences of $x$ in $t$ is defined as follows:

if $t \in F \cup V \cup \{\Omega\}$ then $O(x,t) = \{\epsilon\}$, the empty word if $t = x = \emptyset$ otherwise
if $t = ft_1 \dots ft_k$, $\rho(f) = k$ and $t_1, \dots, t_k \in M_\Omega(F, V)$
then :

$$
\begin{align*}
O(x,t) &= \{\epsilon\} \cup \{i\mu / \mu \in O(x,t_i) \text{ and } 1 \le i \le k\} \text{ if } x = i \\
&= \{i\mu / \mu \in O(x,t) \text{ and } 1 \le i \le k\} \text{ if } x \ne f.
\end{align*}
$$

Let $|t|_x$ be the cardinality of $O(x,t)$ and
$[t| = \sum \{|t|_x / x \in F \cup V \cup \{\Omega\}\}.$

Let $\text{Var}(t) = \{v \in V / O(v,t) \neq \emptyset\}$. A term $t$ is *linear in* $V$ if $|t|_V \le 1$ for all $v \in V$.

The *distance of* $x$ *to the root of* $t$ is $\|t\|_x$, the minimum length of an element of $O(x,t)$ (and $\infty$ if $O(x,t) = \emptyset$).

Finally, if $t_n$ is an increasing sequence in $M_\Omega(F,V)$ with least upper bound $T \in M_\Omega^\infty(F,V)$, then $T \in M^\infty(F,V)$ iff $\|t_n\|_\Omega \to \infty$ when $n \to \infty$.

We now define various kinds of substitutions.

Let $t, u \in M_\Omega(F,V)$ and $\mu$ be an occurrence in $t$.
Then $t' = t [\mu' \leftarrow u]$ is defined as follows by induction
on $|\mu|$:

$$
\left\{
\begin{array}{ll}
t' = u & \text{if } \mu = \epsilon \\
t'_i = t_i [\mu' \leftarrow u] & \text{if } \mu = i\mu' \text{ and } t = ft_l \dots ft_k \\
\text{and } t' = \rho t_1 \dots t_i \dots t_k &
\end{array}
\right.
$$

This is the *substitution of* $u$ *at the occurrence* $\mu$ *in* $t$.

A mapping $\sigma : V \rightarrow M_{\Omega}(F,V)$ is called a *first-order*
*substitution*.
It is extended into $\sigma : M_{\Omega}(F, V) \to M_{\Omega}(F, V)$ by

$$ \sigma (ft_1 \dots t_k) = f \sigma(t_1) \dots \sigma(t_k) $$

and

$$ \sigma t = t \text{ for } t \in F_o \cup \{\Omega\}. $$

The notation $t[t_1/v_{i_1}, \dots, t_k/v_{i_k}]$ will be used for $\sigma(t)$ when $\sigma(v_{i_j}) = t_j$ and $t[t_1, \dots, t_k]$ for $t[t_1/v_1, \dots, t_k/v_k]$.

Let $\Phi$ be a set of function symbols (with arity). A mapping $\theta : \Phi \to M_{\Omega}(F \cup \Phi, V)$ such that $\text{Var}(\theta(\phi)) \subseteq V_{\rho}(\phi)$ is called a second-order substitution. A mapping $\hat{\theta} : M_{\Omega}(F \cup \Phi, V) \to M_{\Omega}(F \cup \Phi, V)$ is associated with $\theta$ as follows:

$$ \hat{\theta}(x) = x \quad \text{if } x \in F_o \cup \{\Omega\} \cup V $$

$$ \hat{\theta}(ft_1 \dots t_k) = f \hat{\theta}(t_1) \dots \hat{\theta}(t_k) $$

$$ \hat{\theta}(\phi t_1 \dots t_k) = \theta(\phi) \quad [\hat{\theta}(t_1), \dots, \hat{\theta}(t_k)] $$

We shall also use for $\hat{\theta}(t)$ the notation

$$ t \{ \alpha_1 / \phi_{i_1}, \dots, \alpha_n / \phi_{i_n} \} $$

if

$$ \theta(\phi_{i_j}) = \alpha_j \text{ for } j = 1, \dots, n. $$

Since these substitutions are monotone in their arguments, we can define:

$$ T_o[T_1/v_{i_1}, \dots, T_k/v_{i_k}] = $$

$$ \sup \{ t_o[t_1/v_{i_1}, \dots, t_k/v_{i_k}] / t_j < T_j \text{ for } 0 \le j \le k \} $$

and, if $T_j \in M_{\Omega}^{\infty}(F, V_{\ell_j})$ where $\ell_j = \rho(\phi_{i_j})$ for $j = 1, \dots, k$,
$$ T_o\{T_l/\phi_{i_l}, \dots, T_k/\phi_{i_k}\} = \\ \sup \{t_o\{t_l/\phi_{i_l}, \dots, t_k/\phi_{i_k}\} / t_j \prec T_j \text{ for } 0 \le j \le k\} $$

(2.2) **Reductions (term rewriting systems)**

We shall borrow much from [9]

Let $S \subset M_{\Omega}(F,V) \times M_{\Omega}(F,V)$. A binary relation $\prec_S$ on $M_{\Omega}(F,V)$ is defined by : $t \prec_S t'$ iff $t = s[\mu \leftarrow \sigma(z)]$, $t' = s[\mu \leftarrow \sigma(z')]$ for some $s \in M_{\Omega}(F,V)$, some occurrence $\mu$ in $s$, some $<z,z'> \in S$ and some first-order substitution $\sigma$. Its transitive and reflexive closure is denoted by $\prec_S^*$ . The relation $\prec_S^*$ is called a **reduction** (since in most cases $t \prec_S t'$ implies $|t'| \le |t|$) but we often say "let $S$ be reduction such that..." It is said **confluent** ([9]) or **Church-Rosser** if for all $t, t_1, t_2$ such that $t \prec_S^* t_1$ and $t \prec_S^* t_2$ there exists $t_3$ such that $t_1 \prec_S^* t_3$ and $t_2 \prec_S^* t_3$. This can be represented by a diagram as follows :

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

were the dotted arrows are defined in terms of the non dotted ones. Such diagrams will be used frequently in the sequel to illustrate definitions and proofs.

A reduction $\to_S$ is **noetherian** if there exists no infinite sequence $(t_n)_{n \in N}$ such that $t_n \to_S t_{n+1}$.

A term $t$ is **S-irreducible** if $t \prec_S t'$ for no $t'$.
If $\Sigma$ is both confluent and noetherian, for every $t$ there exists a unique $S$-irreducible $t'$ such that $t - \Sigma^* t'$ called the $S$-normal form of $t$ and denoted by $c_S(t)$. Clearly $t \stackrel{*}{\rightleftharpoons} \Sigma t'$ if and only if $c_S(t) = c_S(t')$ (where $\stackrel{\leftleftharpoons}{\Sigma}$ denotes $\Sigma \to \Sigma^{-1}$). Let $N(S) = \{t/t = c_S(t)\} = \{t/t \stackrel{\leftleftharpoons}{\Sigma} t'\}$.

An element of $N(S)$ is also said to be in $S$-normal form.

We shall say that $S$ is confluent (or noetherian) if $\Sigma^* S$ is.

If $S$ is noetherian, the principle of noetherian induction says that a property of the form $\forall t P(t)$ is implied by $\forall t [\forall t' (t \stackrel{+}{\rightleftharpoons} t' \Rightarrow P(t')) \Rightarrow P(t)]$. See [9] for the proof.

(2.3) Recursive schemes.

A recursive scheme is a system of equations of the form $\Sigma = <\phi v_1 \dots v_{k_i} = \tau_i, 1 \le i \le n>$ where $\phi = \{\phi_1, \dots, \phi_n\}$ is the set of function variables,

$$k_i = \rho(\phi_i) \text{ and } \tau_i \in M(F \cup \Phi, V_{k_i})$$

for $i = 1, \dots, n$. It is in Greibach normal form if the leftmost symbol of $\tau_i$ belongs to $F$. We often give such a recursive scheme with some $\tau \in M(F \cup \Phi, V_k)$ playing the role of the "main program", the $\phi_i$'s being auxiliary "function procedures".

An infinite tree $T(\Sigma, \tau) \in M_\Omega^\infty(F, V_k)$ is generated by $\Sigma$ considered as a tree-grammar with $\tau$ as axiom (see [5]). We abbreviate $T(\Sigma, \phi_i v_1 \dots v_{k_i})$ into $T(\Sigma, \phi_i)$ and omit $\Sigma$ when the context makes it clear.
An *interpretation* I is an object $<D_I, \le_I, \Omega_I, <f_I>, f \in F>$ consisting of a complete partial order $<D_I, \le_I>$ with least element $\Omega_I$ and continuous functions : $f_I : D_I^\rho(f) \to D_I$.

A continuous function $T_I : D_I^k \to D_I$ is canonically associated with $T \in M_\Omega^\infty(F, V_k)$ (see [6], [1]) and the function computed by $(\Sigma, \tau)$ in the interpretation I is $T(\Sigma, \tau)_I$ denoted by $(\Sigma, \tau)_I$ or $\tau_I$. This definition coincides with the classical definition with least fixpoints.

Let $\hat{C}$ be a *class of interpretations* ("class" is taken in the sense of set-theory). A preorder and an equivalence relation on $M_\Omega^\infty(F, V_k)$ and on the set of recursive schemes are associated with $\hat{C}$ by :

$T \preceq_C T'$ (resp. $T \equiv_C T'$) iff $T_I \preceq_I T'_I$ (resp. $T_I = T'_I$) for all $I \in \hat{C}$;

$(\Sigma, \tau) \preceq_C (\Sigma', \tau')$ (resp. $(\Sigma, \tau) \equiv_C (\Sigma', \tau')$) iff
$T(\Sigma, \tau) \preceq_C T(\Sigma', \tau')$ (resp. $T(\Sigma, \tau) \equiv_C T(\Sigma', \tau')$).

Triples of the form $< (\Sigma, \tau), (\Sigma', \tau'), C >$ such that $(\Sigma, \tau) \equiv_C (\Sigma', \tau')$ are used in program transformations ([8] and [11]) and, as explained in the introduction, we aim to investigate equivalences $\equiv_C$ on the set of recursive schemes. Let us recall some definitions and results from [6] and [2] :

A class of interpretations $\mathcal{C}$ is *algebraic* [6] if for all $T, T' \in M_\Omega^\infty(F, V)$.
(2.3.1) $T \le_C T'$ iff $\forall t < T \exists t' < T'$ such that $t \le_C t'$.

This means that the preorder $\le_C$ on $M_\Omega^\infty(F,V)$ is defined in terms of its restriction $\le_C^\circ$ to $M_\Omega(F,V)$.

We now adapt a definition of [2]. Let $C$ be a class of interpretations.

A mapping $c : M_\Omega(F,V) \to M_\Omega(F,V)$ is a $C$-Projection if, for all $t, t' \in M_\Omega(F,V)$:

$$ (2.3.2) \quad c(t) \equiv_C t, $$

$$ (2.3.3) \quad t \le_C t' \quad \text{iff} \quad c(t) < c(t'). $$

Since $t < t'$ implies $t \le_C t'$, (2.3.3) entails that $c$ is monotone, i.e. $t < t' \Rightarrow c(t) < c(t')$. Hence we can define $c(T) = \text{Sup} \{ c(t) / t < T \}$ for $T \in M_\Omega^\infty(F,V)$. If $C$ is algebraic we get for all $T, T' \in M_\Omega^\infty(F,V)$:

$$ (2.3.2') \quad c(T) \equiv_C T $$

$$ (2.3.3') \quad T \le_C T' \quad \text{iff} \quad c(T) < c(T') $$

Let us prove the "only if" part of (2.3.3') : let $T \le_C T'$. If $t < c(T)$ then $t < c(t_1)$ for some $t_1 < T$ ; by (2.3.1) $t_1 \le_C t'_1$ for some $t'_1 < T'$ and by (2.3.3) $c(t_1) < c(t'_1)$ ; hence $t < c(T')$ and finally $c(T) < c(T')$.

We shall only consider *equational classes of interpretations* i.e. classes of the form

$$ E_R = \{ I / t_I = t'_I \text{ for all } <t,t'> \in R \} $$
where $R$ is some subset of $M_\Omega(F,V) \times M_\Omega(F,V)$. We let $\equiv_R$ and $\le_R$ denote respectively $\equiv_E$ and $\le_E$.

It has been proved in [6] that $E_R$ is algebraic and that

$$ (2.3.4) \qquad \le_R^O = (\prec \cup \prec_R)^* $$

An element $T$ of $M_\Omega^\infty(F,V)$ is R-maximal if, for all $T' \in M_\Omega^\infty(F,V)$ $T \le_R T'$ implies $T \equiv_R T'$.

A recursive scheme $\Sigma = \langle \phi_i v_1 \dots v_{k_i} \rangle = \tau_i$, $1 \le i \le n$ is R-univocal if, for all $T'_1, \dots, T'_n$ such that $T'_i \in M_\Omega^\infty(F, V_{k'_i})$

$$ (2.3.5) \quad T_i \equiv_R \tau_i \{T_1 / \phi_1, \dots, T_n / \phi_n\} \text{ for } i = 1, \dots, n. $$

implies

$$ (2.3.6) \quad T_i \equiv_R T(\Sigma, \phi_i) \text{ for all } i = 1, \dots, n. $$

In other words, $\Sigma$ has a unique solution in $M_\Omega^\infty(F,V) / \equiv_R$ (but this point will be developed elsewhere).

The consequence is the following inference rule which holds if $\Sigma$ is R-univocal, and

$$ \Sigma' = \langle \phi'_j v_1 \dots v_{\ell_j} \rangle = \tau'_j, \quad 1 \le j \le m $$

is an other scheme and $\alpha_i \in M(F \cup \{\phi'_1, \dots, \phi'_m\}, V_{k'_i})$ for $i = 1, \dots, n$:

$$ (2.3.7) \qquad \frac{\alpha_i \equiv_R \tau_i \{\alpha_1 / \phi_1, \dots, \alpha_n / \phi_n\} \text{ for } i = 1, \dots, n}{\alpha_i \equiv_R \phi_i \text{ for } i = 1, \dots, n} $$
which is an improvement of the "fixpoint induction"
method as stated in [18] for instance and introduced
in [16] in another case.

Since (2.3.5) implies $T(\Sigma, \phi_i) \le_R T_i$ for all $i = 1, \dots, n$, $\Sigma$ is R-univocal if each $T(\Sigma, \phi_i)$ is R-maximal. This is in fact the only method that we have to prove that a scheme $\Sigma$ is R-univocal.

Remarks :

(1) A R-univocal scheme $\Sigma$ may very well have several solutions in some $I \in E_R$. But there is only one solution common to all $I \in E_R$, i.e. only one solution in $M_\Omega^\infty(F, V) / \equiv_R$.

(2) The scheme of proof (2.3.7) also applies when $\Sigma'$ is a scheme of higher order type, as defined in [19]. For such schemes, the computed function $\alpha_{iI}$ is also defined as $T(\Sigma', \alpha_i)_I$ for a certain $T(\Sigma', \alpha_i) \in M_\Omega^\infty(F, V)$ and the argument given above goes through.
### 3 - MONOTONE REDUCTIONS.

#### A. Definitions and general properties.

Let $S$ be a reduction, i.e. a subset $S$ of $M_{\Omega}(F,V) \times M_{\Omega}(F,V)$ such that, for all $\langle t, t' \rangle \in S$, $\text{Var}(t') \subseteq \text{Var}(t)$ and $t \notin V \cup \{\Omega\}$ (to prevent pathological situations). The subscript $S$ will often be omitted in $c_S$ and $\rightarrow_S$

(3.1) We say that $S$ is *monotone* if the following two properties are satisfied:

(3.1.1) For all $t, t', z$ such that $t' \prec_S t^* \rightarrow_S z$ there exists $z'$ such that $t' \prec_S z' \prec_S z$.

(3.1.2) For all $t, t', z$ such that $t' \succ_S t^* \rightarrow_S z$ there exists $z'$ such that $t' \succ_S z' \succ_S z$.

Using diagrams these conditions can be represented by:

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

(3.1.1)

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

(3.1.2)

We get the following key result (by c.n.m. we mean confluent noetherian and monotone):

(3.2) **Proposition** : Let $S$ be a c.n.m. reduction. If $t \prec t'$ then $c_S(t) \prec c_S(t')$.
**Proof** : There exists by (3.1.1) some $z \prec c(t')$
such that $t \xrightarrow{*} z$. Since $z \xrightarrow{*} c(t)$, there exists
by (3.1.2) some $u$ such that $c(t) \prec u$ and $c(t') \xrightarrow{*} u$.
But we must have $u = c(t')$ hence $c(t) \prec c(t')$. $\square$

(3.3) **Theorem** : Let S be a c.n.m. reduction. Then $c_S$ is a $E_S$-projection.

**Proof** : By (2.3.4), $\leq_S^o = (\leftarrow u \leftarrow_S)^*$. Hence
$\exists_S c(t)$ since $t \xrightarrow{*} \zeta c(t)$. We must also prove
that $t \leq_S^o t'$ implies $c(t) \prec c(t')$. But :

$c(t) \prec c(t')$ if $t \prec t'$ by (3.2),
$c(t) \prec c(t')$ (since $c(t) = c(t')$) if $t \leftarrow S \rightarrow t'$.

Since the relation $c(t) \prec c(t')$ is reflexive and
transitive it contains $\leq_S^o$. Finally $c(t) \prec c(t')$ implies
$\exists_S t'$ and $c_S$ is a $E_S$-projection. $\square$

Hence the mapping $c_S$ can be extended to $M_\Omega^\infty(F, V)$ by :
$c_S(T) = \text{Sup} \, \{c_S(t) / t \prec T\}$ and $c_S(T)$ is the
$S$-normal form of $T$.

We get, using (3.3), (2.3.2') and (2.3.3') since
$E_S$ is an algebraic class :

(3.4) **Corollary** : 1) $T \leq_S T'$ iff $c_S(T) \prec c_S(T')$.

2) $T$ is $S$-maximal if $c_S(T) \in M^\infty(F, V)$.

The converse to (3.4.2) is not necessarily true :
let $S = \langle fv_1, f\Omega \rangle$ then $f\Omega$ is $S$-maximal but not in
$M^\infty(F, V)$.
(3.5) An infinite tree $T$ is in S-normal form if $c_S(T) = T$.

We let $N^\infty(S) = \{T \in M_\Omega^\infty(F, V) / c_S(T) = T\}$ and
$N(S) = N^\infty(S) \cap M_\Omega(F, V)$.

Then $T \in N^\infty(S)$ iff :

(3.5.1) $T$ is the least upper bound of an increasing sequence in $N(S)$ (increasing for $\prec$).

And this implies :

(3.5.2) No subtree of $T$ is of the form $\alpha[T_1, \dots, T_k]$ for some $T_1, \dots, T_k \in M_\Omega^\infty(F, V)$ and some $<\alpha, \beta> \in S$. But (3.5.2) does not imply (3.5.1) : take $S = <f_\Omega, \Omega>$ and $T = f^\omega = \text{Sup} \{f^n_\Omega / n \in N\}$.

(3.6) A recursive scheme $\Sigma = <\phi_i>v_1\cdots v_k> = \tau_i$; $1 \le i \le n$}
is S-proper if $c_S(T(\Sigma, \phi_i)) \in M_\Omega^\infty(F, V)$ for
$1 \le i \le n$. Hence each $T(\Sigma, \phi_i)$ is S-maximal if
$\Sigma$ is S-proper and :

(3.7) **Proposition** : $\Sigma$ is S-univocal if it is S-proper.

Applications to program proofs and program trans-
formations have been given in the introduction.

Sufficient conditions insuring that $\Sigma$ is S-proper
will be given in section 3.D. We now give sufficient
conditions insuring that a c.n. reduction $S$ is monotone.

B. *Criteria for monotonicity.*

From now on we shall consider _left-linear_ reductions
S i.e. such that $\alpha$ is linear for all $<\alpha,\beta> \in S$.
(3.8) **Proposition** : A left-linear reduction S is monotone iff (3.1.1) and (3.1.2) hold for all t, t', z such that <t,z> ∈ S.

**Proof**\* : The "only if" direction is obvious. Let us prove the other one.

It suffices to prove (3.1.1) and (3.1.2) for all t, t', z such that $t \to z$. The case $t \to z$ follows by an obvious induction.

Let $t$ and $z$ such that $t \to z$. Then $t = s[\mu \leftarrow \sigma(t_1)]$ and $z = s[\mu \leftarrow \sigma(z_1)]$ for some $s \in M_\Omega(F,V)$ some occurrence $\mu$ in $s$, some $<t_1, z_1> \in S$ and some substitution $\sigma$.

Let $t' \prec t$; then $t' = s'[\mu \leftarrow \sigma'(t'_1)]$ for some $s' \prec s$, $t'_1 \prec t_1$ and some substitution $\sigma'$ such that $\sigma'(v_i) \prec \sigma(v_i)$ for all $i$ (we denote this $\sigma' \prec \sigma$).

This property holds since $t_1$ is linear.

Let $z'_1$ such that $t'_1 \stackrel{*}{\to} z'_1 \prec z_1$. Then

$$ t' \stackrel{*}{\to} s' [\mu \leftarrow \sigma'(z'_1)] = z' \prec s [\mu \leftarrow \sigma(z_1)] = z. $$

Note that if $\mu$ is not an occurrence in $s'$, then $s' = z'$.

Having just proved (3.1.1) we now prove (3.1.2) similarly :

Let $t \prec t'$. Then $t' = s'[\mu \leftarrow \sigma'(t'_1)]$ where $t'_1 \prec t_1$, $\sigma \prec \sigma'$ and $s \prec s'$. Let $z'_1$ such that $t'_1 \stackrel{*}{\to} z'_1 \succ z_1$. Then $t' \stackrel{*}{\to} s'[\mu \leftarrow \sigma'(z'_1)] = z' \succ s[\mu \leftarrow \sigma(z_1)] = z$. $\square$
(3.9) **Remark** * : If in the proof of (3.1.2), $t_1$ has no occurrence of $\Omega$ then $t'_1 = t_1$ and one takes simply $z'_1 = z_1$. This means that (3.1.2) is always satisfied for a reduction $S \subseteq M(F,V) \times M_\Omega(F,V)$.

(3.10) **Examples** : The reduction $S = \{\langle ffv_1, fv_1 \rangle\}$ is c.n.m. Using (3.8) and (3.9) we must only consider :

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

and

Everything else in trivial.

The c.n. reduction $S' = \langle gfv_1, fgv_1 \rangle$ is not monotone since $g\Omega \prec gfv_1 \rightarrow fgv_1$ but $g\Omega$ is $S'$-irreducible.

We now give concrete conditions insuring (3.1) via (3.8).

(3.11) **Notation** : Let $t$ and $t' \in M_\Omega(F,V)$ such that $t \prec t'$.

Since $t'$ is obtained from $t$ by the substitution of terms $t'_1, \dots, t'_k$ to certain occurrences $\mu_1, \dots, \mu_k$ of $\Omega$ in $t$, we can find some $s \in M_\Omega(F,V \cup W)$, linear in $W$ (where $W = \{w_1, \dots, w_k\}$ is an auxiliary set of variables) and $t'_1, \dots, t'_k$ in $M_\Omega(F,V)$ such that:
$t = s$ [$\Omega / w_1, \dots, \Omega / w_k$], and

$t' = s$ [$t'_1 / w_1, \dots, t'_k / w_k$].

We denote this by $t \prec_{\text{w.r.t.}} t'$ ($s, t'_1, \dots, t'_k$).

(3.12) **Proposition**: Let $S = S_1 \cup S_2$ be a left-linear reduction such that:

(3.12.1) $S_1 \subseteq M(F,V) \times M(F,V)$ (i.e. $\Omega$ does not occur in $S_1$)

(3.12.2) $S_2 \subseteq M_{\Omega}(F,V) \times \{\Omega\}$

(3.12.3) If $\langle t, z \rangle \in S$, if $t' \in M_{\Omega}(F,V)$ and $t' \prec t$ w.r.t. ($s, t_1, \dots, t_{\ell}$) such that $t_1, \dots, t_{\ell} \notin V$, then $t' \stackrel{*}{\rightarrow_S} \Omega$.

Then $S$ is monotone.

*Proof*: By (3.8), it suffices to verify (3.1.1) and (3.1.2) for all $t, t', z$ such that $\langle t, z \rangle \in S$. Let us consider (3.1.2) first:

* if $\langle t, z \rangle \in S_2$ then $z \prec t$ and (3.1.2) holds trivially,

* if $\langle t, z \rangle \in S_1$ then (3.1.2) holds by remark (3.9).

We now check (3.1.1). Let $t' \prec t$ w.r.t. ($s, t_1, \dots, t_{\ell}$).

We consider two cases :

(1) $t_i \in V$ for $1 \le i \le \ell$, say $t_i = v_{j_i}$; then
$t' = t$ [$\Omega / v_{j_i}$, $1 \le i \le \ell$] and
$t' \rightarrow z'$ [$\Omega / v_{j_i}$, $1 \le i \le \ell$] $\prec z$.
(2) $t_i \notin V$ for $1 \le i \le \ell'$ and $t_i = v_{j_i}$ for $\ell' < i \le \ell$; let $t'' = \sigma(s)$ where $\sigma(w_i) = \Omega$ for $1 \le i \le \ell$ and $\sigma(w_i) = v_{j_i}$ for $\ell' < i \le \ell$. Hence $t'' \prec t$ w.r.t. $(s', t_1, \dots, t_{\ell'})$ with $s' = s$ [$v_{j_i} / w_i, \ell' < i \le \ell$] and $t'' \to^* \Omega$ by (3.12.3). Hence

$$t' = t'' [\Omega / v_{j_i}, \ell' < i \le \ell]^* \to \Omega \prec z. \Box$$

An example is $S = \{ \langle gf v_1, fg v_1 \rangle, \langle g \Omega, \Omega \rangle \}$ (see also (3.27)).

Recall that in order to apply the results of section 3.A, we must also be sure that $S$ is confluent and noetherian. If $S$ is noetherian, then confluence can be tested with the superposition algorithm of [12] and [9]. Whether $S$ is noetherian is undecidable in general [10] but sufficient conditions can be given [15]. Assuming (3.12) we get:

(3.13) **Proposition** : $S$ is noetherian iff $S_1$ is.

**Proof**\* : "if" direction (the other being trivial).

Remark first that $S_2$ is noetherian : since
$\langle\Omega, \Omega\rangle \notin S_2$ (by (3.1)) and by (3.12.2)
$0 \le |t| - |t|_{\Omega} < |t'| - |t'|_{\Omega}$ if $t' \xrightarrow{S_2} t$.

Remark also that $t' \xrightarrow{S_2} t$ implies $t \prec t'$; hence it suffices to show that $\xrightarrow{S_1} \succ$ is noetherian.

Let us prove $\forall t N(t)$ by noetherian induction on $\xrightarrow{S_1} t$ where $N(t)$ means : every sequence $t \xrightarrow{S_1} t_1 \succ t_2 \xrightarrow{S_1} t_3 \succ t_4 \xrightarrow{S_1} \dots$ is finite.

We show that for all $t$, $[\forall t', t \xrightarrow{S_1} t' \Rightarrow N(t')] \Rightarrow N(t)$:
assume that $t \underset{S_1}{\to} t_1 \to t_2 \to t_3 \to t_4 \to \dots$
is infinite but $N(t')$ for all $t'$ such that $t \xrightarrow{+} S_1 t'$.
Then by (3.9), $t_1 \underset{S_1}{\to} u \to t_3$ for some $u$ hence
$t_1 \underset{S_1}{\to} u \to t_4 \to S_1 t_5 \to t_6 \to \dots$ is infinite
$N(t_1)$ does not hold but $t \underset{S_1}{\to} t_1$ ; contradiction. □

### C. Applications to recursive program schemes.

(3.14) Let $\Sigma = \langle \phi_i | v_1 \dots v_{k_i} = \tau_i ; 1 \le i \le n \rangle$ with $\tau_i \in M(F \cup \Phi, V_{k_i})$ and $\Phi = \{\phi_1, \dots, \phi_n\}$ (and $\phi_i$ has arity $\rho(\phi_i) = k_i$).

The least fixed-point $\langle \phi_1, \dots, \phi_n \rangle$ of $\Sigma$ in an
interpretation $I$ is syntactically defined in terms
of the **Kleene-sequence** of $\Sigma$ :

$$ \tau_i^{(j)} \in M_{\Omega}(F, V_{k_i}) \text{ for } 1 \le i \le n \text{ and } j = 0, 1, 2, \dots $$

$$ \tau_i^{(\emptyset)} = \emptyset $$

$$ \tau_i^{(j+1)} = \tau_i \left\{ \tau_1^{(j)} / \phi_1, \dots, \tau_n^{(j)} / \phi_n \right\} $$

(recall that $\{\dots\}$ is the second-order substitution defined in (2.1)).

Then $T(\Sigma, \phi_i)$ is the least upper bound in
$M_{\Omega}^{\infty}(F, V)$ of $\{\tau_i^{(j)} / j \in N\}$ and $\phi_i = T(\Sigma, \phi_i)_I$
is the least upper bound of $\{\tau_i^{(j)} / j \in N\}$ in
$[D_I \to D_I]$.
Let S be a c.n. reduction and

$$ \Sigma' = \langle \phi_i v_1, \dots, v_{k_i} \rangle = \tau_i' ; 1 \le i \le n > $$

$$ \text{with } \tau_i' = c_S(\tau_i). $$

(3.15) **Proposition** : $\Sigma \equiv_S \Sigma' \text{ i.e. } (\Sigma, \phi_i) \equiv_S (\Sigma', \phi_i)$ for $i = 1, 2, \dots, n$.

**Proof** : For all $j \in N$, $\tau_i^{(j)} \underset{S}{\stackrel{*}{\longleftarrow}} \tau_i^{(j)}$. Hence
$T(\Sigma, \phi_i) \equiv_S T(\Sigma', \phi_i)$ for all $i$. $\square$

Let S be a c.n.m. reduction and $\Sigma$ be reduced to a single equation : $\langle \phi v_1 \dots v_k = \tau \rangle$ .

(3.16) **Proposition** : $\phi \equiv_S \Omega$ if and only if $c_S(\tau^{(1)}) = \Omega$.

**Proof** : $\phi \equiv_S \Omega \Rightarrow T(\Sigma, \phi) \equiv_S \Omega$
$\Rightarrow c(T(\Sigma, \phi)) = \Omega$ (by (3.1), $c(\Omega) = \Omega$)
$\Rightarrow c(\tau^{(1)}) = \Omega$ since $\tau^{(1)} \prec T(\Sigma, \phi)$.

Assuming $c(\tau^{(1)}) = \Omega$, consider the Kleene sequence :

$$ \tau^{(0)} = \Omega $$

$$ \tau^{(1)} = \tau\{\Omega / \phi\} \equiv_S \Omega $$

$$ \tau^{(2)} = \tau\{\tau^{(1)} / \phi\} \equiv_S \tau\{\Omega / \phi\} = \tau^{(1)} \equiv_S \Omega $$

And we get by induction, $\tau^{(j)} \equiv_S \Omega$ for all $j$, using the fact that $\tau\{s / \phi\} \equiv_S \tau\{t / \phi\}$ if $s, t \in M_\Omega(F, V_k)$ and $s \equiv_S t$. $\square$
Hence if $S$ is finite and given, the divergence of $\phi$ in $E_S$ is decidable. I conjecture that this decidability result also holds for system of equations.

(3.17) We shall give a sufficient condition for $\Sigma$ to be S-proper when $\Sigma$ is non-nested. Recall that $\Sigma$ is non-nested if each $\tau_i$ is of the form :

$$ (3.17.1) \quad \tau_i = \alpha [\phi_{j_1} \beta_1 / w_1, \dots, \phi_{j_\ell} \beta_\ell / w_\ell] $$
with $W = \{w_1, \dots, w_\ell\}$, $\alpha \in M(F, V \cup W)$, $\beta_s$ is a $\rho(\phi_{j_s})$-tuple of elements of $M(F, V)$ and $\phi \beta$ abbreviates $\phi \beta^{(1)} \beta^{(2)} \dots \beta^{(k)}$ if $\beta = (\beta^{(1)}, \dots, \beta^{(k)})$ and $k = \rho(\phi)$.

(3.18) Here are some definitions and notations :

Let $t \in M_\Omega(F \cup \Phi, V)$ let $x,y \in F \cup \Phi \cup V \cup \{\Omega\}$. Then $x$ is above $y$ in $t$ if $y$ has an occurrence $\mu$ and $x$ has an occurrence $\mu'$ in $t$ such that $\mu = \mu'^{\prime\prime}$ for some $\mu \in N^+$.

For a reduction $S$, let $\text{Left}(S) = \{ f \in F / <f \alpha_1, \dots, \alpha_k, \beta> \in S \text{ for some } \alpha_1, \dots, \alpha_k, \beta \text{ in } M_\Omega(F, V) \}$.

(3.19) Let us now consider the following set of conditions :

(1) $S$ is a c.n.m. reduction such that for $<\alpha, \beta> \in S$ :

$$ (3.19.1) \quad |\alpha|_{\Omega} \ge 1 \quad \text{iff} \quad |\beta|_{\Omega} \ge 1. $$

(2) $\Sigma$ is a non-nested recursive scheme such that for all $i = 1,2,\dots, n$ :
(3.19.2) $\Omega$ does not occur in $c_S(\tau_i)$;

(3.19.3) the leftmost symbol of $c_S(\tau_i)$ is not a function variable,

(3.19.4) no $f \in \text{Left}(S)$ is above any $\phi \in \Phi$ in $c_S(\tau_i)$.

(3.20) **Theorem**: $\Sigma$ is S-proper and S-univocal if conditions (3.19) hold.

*Proof*: We must prove that $c(T(\Sigma, \phi_i)) \in M^\infty(F,V)$ for $i = 1, \dots, n$.

In order to simplify the notations but without loss of generality we take $n = 1$, i.e. $\Sigma = \langle \phi_1^\top \dots v_k^\top \rangle = \tau$ with $\tau$ as in (3.17.1). By (3.15) we can assume that $\tau$ is S-irreducible i.e. that $\alpha$ and the components of the $\beta_i$'s are S-irreducible. By (3.19.2) they do not contain any occurrence of $\Omega$.

Let $\tau^{(0)} = \Omega \prec \tau^{(1)} \prec \dots \prec \tau^{(n)} \prec \dots$ be the Kleene sequence of $\Sigma$; hence $T(\Sigma, \phi) = \sup_n \tau^{(n)}$ and $c(T(\Sigma, \phi))$ is the least upper bound of the increasing sequence :

$$c(\tau^{(0)}) = \Omega \prec \dots \prec c(\tau^{(n)}) \prec \dots$$

Let $||t|| = ||t||_\Omega$, the distance of $\Omega$ to the root of $t$ (see(2.1)). We need only show that $||c(\tau^{(n)})||_\Omega \to \infty$ when $n \to \infty$.

We first show that $||\tau^{(n)}||_\Omega \to \infty$ when $n \to \infty$.
But $\tau^{(n)}$ is defined inductively by :

$$ \tau^{(0)} = \Omega \\ \tau^{(n+1)} = \alpha [\sigma_{1}^{(n)} / w_{1}, \dots, \sigma_{l}^{(n)} / w_{l}] $$

where $\sigma_i : \{v_1, \dots, v_k\} \to M(F, V_k)$ are substitutions such that $\beta_i = (\sigma_i(v_1), \dots, \sigma_i(v_k))$ (see (3.17.1)).

It is clear that $||\sigma_i\tau^{(n)}|| = ||\tau^{(n)}||$ and that $||\tau^{(n+1)}|| \ge 1 + \min_i ||\sigma_i(\tau^{(n)})||$ since $\Omega$ does not occur in $\alpha$ and $\alpha \notin W$ (by 3.19.3).

$$ \text{Hence } ||\tau^{(n)}|| \ge n \text{ for all } n \in \mathbb{N}. $$

Remark now that in all the $\tau^{(n)}$'s, symbols above $\Omega$ are not in Left (S). The following lemma shows that $||c(\tau^{(n)})|| \ge n$ which concludes the proof. $\Gamma$

(3.21) **Lemma**: Let $t \in M_\Omega(F, V)$ such that no symbol is above $\Omega$ in $t$ and in Left (S). Then $||c_S(t)|| = ||t||$.

**Proof**: Remark that if $ft_1 \dots t_k \xrightarrow{*} t'$ and $f \notin \text{Left}(S)$ then $t' = ft'_1 \dots t'_k$ and $t_i \xrightarrow{*} t'_i$ for $i = 1, \dots, k$. It follows that $c(ft_1 \dots t_k) = fc(t_1) \dots c(t_k)$.

Let now $t \in M_\Omega(F, V)$. If $\Omega$ does not occur in $t$ then $\Omega$ does not occur in $c(t)$ by (3.19.1) and $||t|| = ||c(t)|| = \infty$. If $t = \Omega$ then $c(t) = \Omega$ and $||t|| = ||c(t)|| = 0$. Otherwise $t = ft_1 \dots t_k$ for some $f \in \text{Left}(S)$ and :
$$
\begin{align*}
\|t\| &= 1 + \min_i \|t_i\| \\
&= 1 + \min_i \|c(t_i)\| \quad \text{(induction)} \\
&= \|fc(t_1) \dots c(t_k)\| \\
&= \|c(t)\| . \Box
\end{align*}
$$

An alternative to (3.19) will be given, insuring
that T( Σ , φᵢ) belongs to M∞(F,V) ∩ N∞(S).

(3.22) **Definition** : An element t of M<sub>Ω</sub>(F,V) is **strongly S-irreducible w.r.t. V** if σ(t) ∈ N(S) for all substitution σ such that σ(v) ∈ N(S) for all v ∈ V.

Let us consider the following set of conditions :

(3.23) Let S be a c.n.m. reduction satisfying (3.19.1),
let Σ be a non-nested scheme such that :

(3.23.1) $|\tau_i|_{\Omega} = 0$ and $\tau_i$ is S-irreducible.

(3.23.2) for each τᵢ written as in (3.17.1), α is
strongly S-irreducible w.r.t. V ∪ W.

(3.24) **Theorem** : *Under (3.23), T(Σ, φᵢ) ∈ M∞(F,V) ∩ N∞(S) for i = 1, ..., n.*

Hence Σ is S-proper and S-univocal.

**Proof** : An easy induction on j shows that each
element τᵢ(j) of the Kleene-sequence is S-irreducible. ∎
It is clear that theorems (3.20) and (3.23)
should be improved. But for practical application,
the conditions on Σ should be kept "easily testable".
On the other hand I conjecture that for a given
finite c.n.m. reduction S, whether Σ is S-proper
or not is decidable, but the algorithm may very well
be too complicated for practical use.

D. Examples.

$$
(3.25) \text{ Take } S=\emptyset, \text{ i.e. } c_S(T) = T \text{ for all } T \in \mathbb{M}_{\Omega}^{\infty}(F,V).
$$

It is clear that T( Σ , φᵢ₁ ) ∈ M∞(F,V) if Σ
is in Greibach normal form. Every such scheme is
S-univocal. Hence a redefinition à la Burstall
and Darlington is correct provided the new equa-
tion is in Greibach normal form.

Let us give an exemple of such :

$$
\left\{
\begin{array}{l}
\phi(v_1, v_2) = h(v_1, fv_2, \phi(\phi(gv_1, gv_2), \phi(gv_2, gv_2))) \\
\delta v_1 = \phi(v_1, v_1)
\end{array}
\right.
$$

$$
\begin{align*}
\text{Then } \delta v_1 &\equiv h(v_1, fv_1, \phi(\phi(gv_1, gv_1), \phi(gv_1, gv_1))) \\
&\equiv h(v_1, fv_1, \delta \delta gv_1)
\end{align*}
$$

Since it is in Greibach normal form, we can take

$$
\delta v_1 = h(v_1, fv_1, \delta \delta gv_1)
$$

as a redefinition of δ.
(3.26) The equivalence of monadic recursive scheme (i.e. such that $\rho(\phi) = 1$ for all $\phi \in \phi$) is considered in [7]. It is shown that for all monadic

$$ \Sigma = \langle \phi_i v_1 = \tau_i, 1 \le i \le n \rangle $$

one can construct another ("canonical") scheme

$$ \bar{\Sigma} = \langle \phi_i' v_1 = \tau_i', 1 \le i \le n \rangle $$

such that $\phi_i \equiv \tau_i' \{\phi_i / \phi_i'\}$. The equivalence $\phi_i \equiv \phi_i'$ follows immediately.

The formal proof using Scott's induction principle provided in theorem 3 ([7], p. 194) is rather complicated.

(3.27) Let us revisit example (1.3). Let us consider the following c.n.m. reduction :

$$ S = \begin{cases} gfv_1 & \rightarrow fgv_1 \\ g\Omega & \rightarrow \Omega \end{cases} $$

The equation $\phi = f\phi$ has a unique solution, namely $f^\omega$.

Remark now that $c(gf^\omega) = f^\omega$ since $c(gf^n\Omega) = f^n\Omega$. The transformation of (1.3) is now correct.

(3.28) Let S be as in (3.27). Let $\phi$ be defined by :

$$ \phi v_1 = k(v_1, \phi fgv_1) $$
Let $T = c_S(T(\Sigma, \phi))$; it is not difficult
to prove that the language of branches of $T$ is
$\{k_2^n k_1 f^n g^n v_1 / n \in \mathbb{N}\}$ (see [5]). This language
is not context-free hence $T$ is not $T(\Sigma', \phi')$ for
any recursive scheme $\Sigma'$.

But in order to use (2.3.7) we need not a
definition of $c_S(T(\Sigma, \phi))$ by a recursive scheme.
We need only know that $c_S(T(\Sigma, \phi)) \in M^\infty(F,V)$,
which can be achieved by theorem (3.20).

(3.29) **Example**: Let $S$ be the following reduction :

$$
\begin{align*}
k(v_1, k(v_2, v_3)) &\rightarrow k(k(v_1, v_2), v_3) \\
k(v_1, h(v_2, v_3, v_4)) &\rightarrow h(v_2, k(v_1, v_3), k(v_1, v_4)) \\
k(v_1, \Omega) &\rightarrow \Omega
\end{align*}
$$

Conditions (3.12) clearly hold, and it is not
difficult to prove that S is confluent and noetherian.

Let us now consider the following recursive
schemes :

$$
\begin{align*}
\Sigma_1 &: \quad \phi v_1 = h(v_1, fv_1, k(gv_1, \phi \, dv_1)) \\
\Sigma_2 &: \quad \left\{
\begin{aligned}
\theta v_1 &= h(v_1, fv_1, \psi(dv_1, gv_1)) \\
\psi(v_1, v_2) &= h(v_1, k(v_2, fv_1), \psi(dv_1, k(v_2, gv_1)))
\end{aligned}
\right.
\end{align*}
$$

Claim : $\phi \equiv_S \theta$

If h is interpreted as a conditional i.e. as
$\lambda x_1 x_2 x_3$. if $\pi x_1$ then $x_2$ else $x_3$ for some
continuous predicate $\pi$ then ($\Sigma_2, \theta$) can be con-
sidered as an iterative form of ($\Sigma_1, \phi$) (via
McCarthy's transformation of iterative programs
into recursive ones). The iterative program corres-
ponding to ($\Sigma_2, \theta$) is :
if $\pi(x)$ then $x \leftarrow fx$

else $y \leftarrow gx$; $x \leftarrow dx$;

while not $\pi x$ do $y \leftarrow k(y,gx)$;

$x \leftarrow dx$ od; $x \leftarrow k(y,fx)$ fi;

out put : x;

This is essentially the first transformation scheme of [8]. And our claim expresses the correctness of the transformation. Note that our conditions S do not use all the properties of the conditionals, hence are weaker than that of [8] where an explicit conditional operator is used. Hence our transformation scheme is more powerful. Note that replacing flowcharts by recursive procedures allows to consider if .. then .. else ... fi as a base function and not as a piece of control structure. Proofs are simpler in that way, dealing only with equations and more general.

Let us now prove the claim.

We first prove that $\psi(v_1, v_2) \equiv_S k(v_2, \phi v_1)$

It is clear by (3.20) that the second equation of $\Sigma_2$ is S-univocal (let $\tau_\psi$ denote its right hand side). Hence it is sufficient to verify that $k(v_2, \phi v_1)$ satisfies it modulo $\equiv_S$.

$$k(v_2, \phi v_1) \equiv_S k(v_2, h(v_1,fv_1),k(gv_1,\phi dv_1))) \quad \text{(by } \Sigma_1)$$

$$\equiv_S h(v_1,k(v_2,fv_1),k(v_2,k(gv_1,\phi dv_1))) \quad \text{(by S)}$$

$$\equiv_S h(v_1,k(v_2,fv_1),k(k(v_2,gv_1),\phi dv_1))) \quad \text{(by S)}$$

$$\equiv_S \tau_\psi \{k(v_2,\phi v_1) / \psi \} \text{ since}$$

$$k(v_2, \phi v_1) [dv_1, k(v_2, gv_1)] = k(k(v_2, gv_1), \phi dv_1).$$
Hence now

$$ \theta v_1 \equiv_S h(v_1, fv_1, \psi(dv_1, gv_1)) \equiv_S h(v_1, fv_1, k(gv_1, \phi dv_1)) \\ \equiv_S \phi v_1 \text{ (by } \Sigma_1). $$

And the proof is complete. Notice that we have not used any induction principle, (as in [11] for the same proof)
# IV - MONOTONE EQUATIONAL THEORIES.

This section is divided into four subsections exactly as section 3, proceeding from axiomatic properties to applications.

## A. Definitions and general properties.

We shall consider equational theories of the form
$$ R = S \cup E \subseteq M_{\Omega}(F,V) \times M_{\Omega}(F,V) $$
such that S is a c.n.m. reduction, E is a non noetherian relation
(e.g. $E = \langle k(v_1,v_2), k(v_2,v_1) \rangle$ ) compatible with $\mathcal{R}$
and $\mathcal{S}$ (see conditions (4.1.2) and (4.1.3) below)
such that the class of a finite term with respect to
$\leftarrow_E^*$ is finite (this is a weak form of noetherianism).

We shall use the notation $\mathcal{R} \vdash E$ for $\mathcal{R} \vdash E$ and $\sim_E^*$ for $\mathcal{R} \vdash E^*$. The subscripts E and S will often be omitted.

Here is the precise definition.

(4.1) A *monotone equational theory* is a pair <S,E> of subsets of $M_{\Omega}(F,V) \times M_{\Omega}(F,V)$ such that S is a monotone reduction (definition 3.1) and E satisfies the following :

(4.1.1) $\text{Var}(t) = \text{Var}(t')$ and $|t|_{\Omega} = |t'|_{\Omega} = 0$ for all $(t,t') \in E$.

(4.1.2) For all t, t', z such that $z \stackrel{\sim_E}{\to} t \to t'$, there exist u and z' such that $z \xrightarrow{\sim_E} u \to z'$. (this is property $\beta$ of [9]).
(4.1.3) For all $t, t', z$, such that $t' \prec t \sim_E z$
there exist $u, u'$ and $z'$ such that
$t' \stackrel{*}{\longrightarrow}_S u \sim_E u' \prec z' \stackrel{*}{\longleftarrow}_S z$.

(4.1.4) $[t]_{\sim_E}$ is finite for all $t \in M_{\Omega}(F, V)$.

The equational theory <S,E> is said *linear* if t is linear in V for all <t,z> ∈ S ∪ E ∪ E<sup>-1</sup>. This assumption will be made in all this section.

Remarks : Let us represent (4.1.2) and (4.1.3) with
diagrams :

<figure><img src="image_6.png" /><figcaption>(4.1.2)</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>(4.1.3)</figcaption></figure>

Condition (4.1.4) excludes the case of S = Ø,
E = {<ffv₁,fv₁>} (which satisfies (4.1.1) to (4.1.3)).
In fact, one should put such a pair in S as in
example (3.10).

Finally, a monotone equational theory <S,E>
will be said _confluent_ (noetherian) if S is so.

(4.2) **Proposition** : Let <S,E> be a c.n.m. equational theory.
For all $z,t,t',z'$ such that
$$ z \stackrel{*}{\leftarrow} t \stackrel{\sim_E}{\rightarrow} t' \stackrel{*}{\leftarrow} z' $$
there exist $u,u'$ such that $z \stackrel{*}{\rightarrow} u \stackrel{\sim_E}{\rightarrow} u' \stackrel{*}{\leftarrow} z'$.

**Proof :** By lemma 7 of [9]. (4.1.2) is exactly property $\beta$ and the confluence of $S$ is stronger than property $\alpha$, whence the result. []

With the same hypotheses we get :

(4.3) **Corollary :**

$$
(4.3.1) \quad t \stackrel{\sim_E}{\rightarrow} t' \text{ implies } c_S(t) \stackrel{\sim_E}{\rightarrow} c_S(t')
$$

$$
(4.3.2) \quad z \stackrel{\sim}{\leftarrow} t \stackrel{\sim_E}{\rightarrow} t' \text{ implies } c_S(z) \stackrel{\sim_E}{\rightarrow} u \stackrel{\sim}{\leftarrow} c_S(t') \\
\text{for some } u \in N(S)
$$

**Proof :** (4.3.1) is an immediate consequence of (4.2).

(4.3.2) Let us take by (4.1.3) $s, s'$ and $z'$ such that $z' \stackrel{*}{\rightarrow} s \sim s' \stackrel{<}{\leftarrow} z' \stackrel{*}{\leftarrow} t'$.
By (3.2) and (4.3.1) we get :

$$
c(z) = c(s) \sim c(s') \stackrel{<}{\leftarrow} c(z') = c(t')
$$

hence result with $u = c(s')$. Γ

(4.4) **Remark**\*: Let $\langle S,E \rangle$ be c.n.m. and linear. For all $t,u \in M_\Omega(F,V)$ such that $t \sim u$ there exists an auxiliary set of variables $W = \{w_1, \dots, w_\ell\}$ and $\bar{t}, \bar{u} \in M(F,V \cup W)$ such that :

$$
(1) \quad |\bar{t}|_{w_i} = |\bar{u}|_{w_i} = 1 \quad \text{for } i = 1, \dots, \ell,
$$
(2) $t = \sigma(\bar{t})$ and $u = \sigma(\bar{u})$ where $\sigma(w_i) = \Omega$ for $i = 1, \dots, l$,

(3) $\bar{t} \sim \bar{u}$

It follows in particular that $|t|_{\Omega} = |u|_{\Omega}$. The proof is an induction on $n$ such that $t|_{\bigwedge^n} u$.

With the hypotheses of (4.4):

(4.5) **Lemma**: If $t \prec_u \bar{u} \sim_E t$ then $t = u$.

**Proof**\* : Let $\bar{u}$ and $\bar{t}$ as in (4.4). Since $t \prec_u \bar{u}$, there exists $\sigma' : W \to M(F, V \cup W)$ such that $\bar{u} = \sigma'(\bar{t})$. Hence $\bar{t} \sim \sigma'(\bar{t}), \dots, \sigma'^n(\bar{t}) \sim \sigma'^{n+1}(\bar{t}), \dots$ and $\sigma'^n(\bar{t}) \sim \bar{t}'$ for all $n \in N$. By (4.1.4), $\sigma'^{p+n}(\bar{t}) = \sigma'^n(\bar{t})$ for some $p \ge 1$. By (4.4), $|\sigma'^n(\bar{t})| w_i = 1$ for all $n$ and $i = 1, \dots, l$. Hence $\sigma'^p$ must be the identity (i.e. $\sigma'^p(w_i) = w_i$ for all $i$) and $\sigma'$ is a permutation of $W$. It follows that $t = u$.

(4.6) **Proposition**: Let $<S,E>$ be a left-linear c.n.m. equational theory and $R = S \cup E$. For all $t,t' \in M_{\Omega}(F,V)$:

(4.6.1) $t \le_R t' \text{ iff } c_S(t) \sim_E u \prec_S c_S(t') \text{ for some } u \in N(S)$

(4.6.2) $t \equiv_R t' \text{ iff } c_S(t) \sim_E c_S(t')$.

**Proof**: Let $t \sqsubseteq t'$ iff $c(t) \sim u \prec c(t')$ for some $u \in N(S)$.

It is clear that $\sqsubseteq$ is included in $\le_R^0$. Recall that $\le_R^0$ (the restriction of $\le_R$ to $M_{\Omega}(F,V)$) is exactly $(\prec_S u \leftrightarrow u \prec_E u)^*$.
By (3.2), $t < t'$ implies $c(t) < c(t')$, by (4.3.1),
$\tilde{t} < \tilde{t}'$ implies $c(\tilde{t}) \sim c(\tilde{t}')$ and $\tilde{t} \xrightarrow{*} \tilde{t}'$ implies
$c(\tilde{t}) = c(\tilde{t}')$; hence $t \sqsubseteq \tilde{t}'$ holds in each of these
three cases. We need only show that $\sqsubseteq$ is transitive
to complete the proof. Let $t \sqsubseteq \tilde{t}' \sqsubseteq t''$.

Then $c(t) \sim c(u) \prec c(t') \sim c(u') \prec c(t'')$. By (4.3.2) there exists some $s$ such that $c(u) \sim c(s) \prec c(u')$ hence $c(t) \sim c(s) \prec c(t'')$ i.e. $t \sqsubseteq t''$.

Let now $t \equiv_R t'$. Then $c(t) \sim u \prec c(t') \sim u' \prec c(t)$
for some $u, u' \in N(S)$. There exists $s$ such that
$u \sim c(s) \prec u'$ hence $c(t) \sim c(s) \prec c(t)$. By (4.5)
$c(s) = c(t)$ hence $u' = c(t)$ and $c(t) \sim c(t')$. $\square$

Let us now define for $T,T' \in M_{\Omega}^{\infty}(F,V)$ $T \stackrel{\sim}{\rightarrow}_{E} T'$ iff
there exist two increasing sequences $(t_n)_{n \in N}$
and $(t'_n)_{n \in N}$ such that $t_n \sim_E t'_n$ for all $n$,
$T = \sup_n t_n$ and $T' = \sup_n t'_n$.

(4.7) **Theorem** : Let $<S,E>$ be a left-linear c.n.m. equational theory and $R = S \cup E$. For all $T, T' \in M_{\Omega}^{\infty}(F,V)$, $T \leq_R T'$ iff $c_S(T) \stackrel{\sim}{\rightarrow}_E U \prec c_S(T')$ for some $U \in \tilde{N}(S)$.

**Proof** : The "if" direction being obvious, we prove
the other one. Assume that $T \leq_R T'$, i.e. $c(T) \leq_R c(T')$.
Let $c(T) = \sup_n t_n$ for some increasing sequence $t_n$
in $N(S)$ w.r.t. $\prec$.

For each $n$ there exists $t' \prec c(T')$ such
that $t_n \leq_R t'$ hence $t_n \sim u \prec c(t')$ for some $u \in N(S)$
by (4.6.1). The set $A_n = \{u \in N(S) | u \prec c(T')$
and $u \sim t_n\}$ is non empty and finite by (4.1.4).
For all $u' \in A_{n+1}$, $t_n < t_{n+1} \sim u'$ hence
$t_n \sim u < u'$ for some $u \in A_n$ by (4.6.1). By
Koenig's lemma there exists a sequence $u_n$
such that $u_n < u_{n+1}$ and $u_n \in A_n$ for all $n$.
We take $U = \text{Sup}_n u_n$ and we get $c(T) \sim U < c(T')$. □

(4.8) **Proposition**: For $T$ and $U \in \mathcal{N}^\infty(S)$, if $T \sim_E U$ and $T \in \mathcal{M}^\infty(F,V)$ then $U \in \mathcal{M}^\infty(F,V)$.

**Proof**\* : Assuming that $U$ contains an occurrence
$\mu$ of $\Omega$, we shall obtain a contradiction.

Let $T = \text{Sup}_n (t_n)$ and $U = \text{Sup}_n (u_n)$ for
increasing sequences $t_u$ and $u_n$ such that $t_n$
and $u_n$ are S-irreducible and $u_n \sim t_n$ for all
$n \in \mathbb{N}$.

Let $n_o$ be the first integer such that $\mu$
is an occurrence of $\Omega$ in $u_{n_o}$. It is also an
occurrence of $\Omega$ in $u_n$ for $n > n_o$.

Using (4.4), let $\overline{u}_{n_o}$ such that
$u_{n_o} = \overline{u}_{n_o} [\Omega / w_1, \dots, \Omega / w_\ell]$ and $\mu$ is
an (the unique) occurrence of $w_1$ in $\overline{u}_{n_o}$.

Hence $u_n = \overline{u}_{n_o} [\Omega/w_1, u_2^{(n)}/w_2, \dots, u_\ell^{(n)}/w_\ell]$ and $\overline{u}_n = u_{n_o} [w_1/w_1, \overline{u}_2^{(n)}/w_2, \dots, \overline{u}_\ell^{(n)}/w_\ell]$ for all $n \ge n_o$.

Let $\overline{t}_n$ be the sequence corresponding
to $\overline{u}_n$ by (4.4). For $n \ge n_o$, we have :
$u' = \overline{u}_{n_o} [w_1/w_1, \Omega/w_2, \dots, \Omega/w_\ell] < \overline{u}_n \sim \overline{t}_n,$
where $u', \bar{u}_n$ and $\bar{t}_n$ are in $N(S)$ since (respectively)
$u_n^o, u_n$ and $t_n$ are in $N(S)$. By (4.6.1) there
exists $s_n$ such that $u' \sim s_n < \bar{t}_n$. It is clear
that $w_1$ has only one occurrence in $s_n$, which is
also its unique occurrence in $\bar{t}_n$. Hence
$\|s_n\|_{w_1} = \|\bar{t}_n\|_{w_1}$ (see (2.1)).

But $|| \bar{t}_n ||_{w_1} \xrightarrow{n \to \infty} \infty$ when $n \to \infty$ since
$|| \bar{t}_n ||_{w_1} \ge || t_n ||_{\Omega}$ and $|| t_n ||_{\Omega} \xrightarrow{\Omega \to \infty} \infty$ when $n \to \infty$
(since $T \in M^{\infty}(F, V)$).

This shows that {$s_n / n \in N$} is infinite
but this contradicts (4.1.4). □

We get finally using (4.8) and (4.7).

(4.9) **Theorem** : Let <S,E> be a left-linear c.n.m. equational theory and R = S ∪ E. Then T ∈ M<sup>∞</sup><sub>Ω</sub>(F,V) is R-maximal if c<sub>S</sub>(T) ∈ M<sup>∞</sup>(F,V).

**Proof** : Let $T \le_R T'$. Then by (4.6), $c(T) \sim U \prec_c c(T')$
for some $U$ in S-normal form. By (4.8), $U \in M^\infty(F,V)$
hence $c(T') = \emptyset$. It follows that $T \equiv_R T'$. □

(4.10) **Corollary** : *A recursive scheme Σ is R-univocal if it is S-proper.*

And our criteria of section 3.C will be
applicable for R-univocality as well.

B. *Criteria for monotonicity.*

The monotonicity of <S,E> is a property
of $\xrightarrow{*} S$ and $\sim_E$.

We shall express it in terms of $\xrightarrow{S}$ and
$\xrightarrow{\overline{E}}$ in such a way that it can be proved for
a given finite <S,E>.
(4.11) In all this section we shall assume that :

(1) S is finite, confluent, noetherian, monotone ;

(2) E is finite, linear and satisfies (4.1.1),

(3) The relation $\underset{S}{\stackrel{\sim}{\to}}_{E}$ is noetherian.

In order to apply the preceding results, one
must also have (4.1.2), (4.1.3) and (4.1.4).

Property (4.1.4) (i.e. for all {t' / t' ≁<sub>E</sub> t}
is finite) is undecidable ([10]). But sufficient
conditions can be given insuring it. In particular,
if |t| = |z| for all <t,z> ∈ E then |t'| = |z'| for all t',z' such that t' ≁<sub>E</sub> z' (since E is linear).

For t ∈ M<sub>Ω</sub>(F, V<sub>k</sub>), {z / z ≁<sub>E</sub> t} ⊆ {z/|z| = |t| and z ∈ M<sub>Ω</sub>(F', V<sub>k</sub>)} for some finite subset F' of F, hence is finite.

We now turn to (4.1.2) which is decidable if
(4.1.4) holds.

(4.12) **Proposition** : **Assuming (4.11), condition (4.1.2) is equivalent to :**

(4.12.1) **For all** $t, t', z$ **such that** $z \underset{E}{\stackrel{*}{\to}} t \underset{S}{\stackrel{\sim}{\to}} t'$
**there exist** $z'$ **and** $u$ **such that**
$t' \underset{S}{\stackrel{*}{\to}} u \sim_E z' \underset{S}{\stackrel{*}{\leftarrow}} z$.

**Proof** : We use [9] : property α holds since S
is confluent and property γ is exactly (4.12.1).
Hence (4.1.2) i.e. property β holds by lemma 8.[]
(4.13) **Remark** : Condition (4.12.1) can be practically tested with the critical pairs of E/S as defined in [9] (lemma 13). There is only a finite number of such to examine.

Since {$u / t' \xrightarrow[S]{*} u$} , {$z' / z \xrightarrow[S]{*} z'$} are finite and, by (4.1.4) $u \sim_E z'$ is decidable, condition (4.12.1) is decidable if (4.1.4) does hold.

We shall now do the same for (4.1.3).

Let us define $t \sim_E t'$ if

$t = t_1 \leqdot E t_2 \leqdot E t_3 \leqdot E \dots t \leqdot E t_n = t'$ and

t_i$ is S-irreducible for $i = 1, \dots, n$

(4.14) **Lemma** : $t \sim_E t'$ if $t \sim_E t'$ and $t, t'$ are S-irreducible.

**Proof** : Let $P(t)$ mean : $\forall z, c(t) \sim_E c(z) \Rightarrow c(t) \sim_E c(z)$.

We prove $\forall t P(t)$ by noetherian induction
with respect to $\sim \longrightarrow$.

Let us prove $P(t)$ assuming $P(s)$ for all
$s$ such that $t(\sim \longrightarrow)^+ s$.

Let $c(z) \sim_E c(t)$. If $t \longrightarrow s$ then
$c(t) = c(s) \sim_E c(z)$ and $c(t) = c(s) \sim_E c(z)$
by $P(s)$. Otherwise $t = c(t)$. If $c(t) \sim_E s \sim_E c(z)$
and $s \xrightarrow{+} c(s)$ then $t(\sim \longrightarrow)^+ c(s)$ and $P(c(s))$
yields $c(t) \sim_E c(s) \sim_E c(z)$, hence $c(t) \sim_E c(z)$. $\blacksquare$

(4.15) **Proposition** : Assuming (4.11) and (4.1.2), condition
(4.1.3) is equivalent to (4.15.1) : for all $t, t', z$
such that $t' \prec t$ and $<t, z> \in E \cup E^{-1}$ there exist
$u, u', z'$ such that $t' \xrightarrow[S]{*} u', u \prec z'$, $u \prec z' \xrightarrow[S]{*} z$.
**Proof :** 1. Assume (4.15.1). The same property holds with $t \mapsto z$ instead of $\langle t, z \rangle \in E \cup E^{-1}$ (the proof is similar to that of (3.8)).

2. Using now (3.2) and (4.3.1) which only depends on (4.1.2) and the assumption that S is a c.n.m. reduction, we get from (4.15.1):
(4.15.2) For all S-irreducible $t, t', z$ such that $t' \prec t \prec_F z$ there exist an S-irreducible u such that : $t' \sim_E u \prec z$.

3. We now prove (4.1.3). Let $t' \prec t \sim z$. Then $c(t') \prec c(t) \sim_E c(z)$ by (4.3.1) and (3.2) ; and $c(t) \sim_E c(z)$ by lemma (4.14). Let $t_1, \dots, t_n$ in S-normal form such that :
$$c(t) \vdash \dots \vdash t_1 \vdash \dots \vdash t_n \vdash c(z).$$
By a repeated use of (4.15.2), one can find S-irreducibles $u_1, u_2, \dots, u_n, u$ such that :

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

And the desired u is obtained, as shown by the following diagram :

<figure><img src="image_9.png" /></figure>
Remark that if E is finite, there is only a
finite number of triples $(t',t,z)$ to consider to
check (4.15.1).

As for (4.12.1) (see remark (4.13)), (4.15.1)
is decidable if (4.1.4) holds.

We now give a simple condition on E, similar
to (3.12.3) insuring (4.15.1).

(4.16) **Proposition 3** : Let S be a c.n.m. reduction satisfying (3.12) ; let <S,E> satisfy (4.11), (4.1.2), (4.1.4) and :

(4.16.1) **For all** <t,z> ∈ E ∪ E<sup>-1</sup> **and** t' ≺ t
**w.r.t.** (s,t<sub>1</sub>,...,t<sub>ℓ</sub>) **such that** t<sub>1</sub>,...,t<sub>ℓ</sub> ∉ V
**then** t' ↛ S Ω.

Then <S,E> is a c.n.m. equational theory.

**Proof** : The proof of (3.12) shows that for all
$t,t',z$ such that $t' \prec t$ and $<t,z> \in E \cup E^{-1}$
then, either $t' \vdash_E z' \prec z$ or $t' \stackrel{*}{\to} S \Omega \prec z$.
In both cases, (4.15.1) does hold. []

C. Applications to recursive program schemes.

In the last section, we have given methods to
show that a given <S,E> is c.n.m. In that case, (4.10)
shows that an S-proper scheme is R-univocal. Hence
our criteria (3.19) and (3.23), insuring that a
scheme is S-proper can be applied to prove that a
scheme is R-univocal.
(4.17) Application to permutative equations.

Let E be a finite set of permutative equations ([14]) i.e. of equations of the form <fv₁...vₖ, fvᵢ₁vᵢ₂...vᵢₖ> where (i₁,i₂,...,iₖ) is a permutation of (1,2,...,k). With S = Ø, all conditions of (4.16) are satisfied. Every T ∈ M∞(F,V) is E-maximal.

Since T(Σ, φᵢ) ∈ M∞(F,V) for a scheme in Greibach normal form :

(4.18) **Corollary** : Let E consist only of permutative equations.

Every recursive scheme in Greibach normal form is E-univocal.

D. Examples

$$
(4.19) \quad \text{E} \quad \begin{cases} k(v_1, k(v_2, v_3)) = k(k(v_1, v_2), v_3) \\ k(v_1, v_2) = k(v_2, v_1) \end{cases}
$$

$$
S \quad \begin{cases} k(v_1, \Omega) \rightarrow \Omega \\ k(\Omega, v_1) \rightarrow \Omega \end{cases}
$$

Conditions (4.16) are all satisfied, the less
obvious point being (4.12.1). A typical example of
a critical pair of E/S is <k(v₁,Ω), k(k(v₁,v₂),Ω)>
as shown by :

<figure><img src="image_10.png" /></figure>
The other critical pairs of E/S are similar.

A concrete case is the addition of integers.

This example will be enriched and used in (5.8).

Note that if we put the associativity in S as
we did in example (3.29) we cannot fulfill (4.12.1) :

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

Note also that $\mathcal{S} \cdot \mathcal{E}$ would not be noetherian.

$$
(4.20) \quad \mathcal{E} \left\{ \begin{array}{l} k(k(v_1, v_2), k(v_3, v_4)) = k(k(v_1, v_3), k(v_2, v_4)) \\ k(k(v_1, v_2), k(v_3, v_4)) = k(k(v_4, v_2), k(v_3, v_1)) \end{array} \right.
$$

$$
S \left\{
\begin{array}{l}
k(v_1, \Omega) \rightarrow \Omega \\
k(\Omega, v_1) \rightarrow \Omega
\end{array}
\right.
$$

The verification of (4.16) is similar to the
case of (4.19). A concrete case of S ∪ E is the
division on ]0,∞[ ∪ {⊥}.
# V. NON-LINEAR REDUCTIONS AND EQUATIONS.

Non left-linear reductions are often needed. A
typical example is

(5.1) $h(v_1,h(v_1,v_2,v_3),v_4) \longrightarrow h(v_1,v_2,v_4)$ which holds if $h$ is a conditional expression of the form $\lambda xyz. \text{ if } \pi x \text{ then } y \text{ else } z$ for some continuous predicate $\pi$.

We extend our results of sections 3 and 4
to include non left-linear reductions and non
linear equations.

This will be done in a very rough manner and
all this section should be considered as tentative.
All proofs are omitted.

We shall work with a proper subset $M_{\Lambda}(F,V)$
of $M_{\Omega}(F,V)$, a proper subset $M_{\Lambda}^{\infty}(F,V)$ of $M_{\Omega}^{\infty}(F,V)$
and recursive schemes $\Sigma$ such that $T(\Sigma, \phi_i) \in M_{\Lambda}^{\infty}(F,V)$.
And all results of sections 3 and 4 will be
applicable. In the case of (5.1), $M_{\Lambda}(F,V)$ will
be defined as follows : $t \in M_{\Lambda}(F,V)$ iff $t \in M_{\Omega}(F,V)$
and for every subterm of $t$ of the form
$ht_1t_2t_3,t_1 \in M(F,V)$ (i.e. does not contain any
occurrence of $\Omega$). Hence the applicability of rule
(5.1) to some $t \in M_{\Lambda}(F,V)$ depends on the equality
of two subterms of $t$ without $\Omega$.
(5.2) **Remark**: We do not use a reduction S as a set "simplification rules", part of the "operational semantics" (as for instance in [17]) but as a convenient way of writing certain valid equations. A "simplification rule" must be left-linear; otherwise one has to check the equality of two or more subterms before applying it, which is time-consuming. But equations like (5.1) are often needed for proving the equivalence of two recursive schemes, hence we cannot discard non linear reductions and equations.

(5.3) Definitions.

Let $\Lambda$ be a subset of $\{<i,f> / f \in F \text{ and } 1 \le i \le \rho(f)\}$.

We define $M_{\Lambda}(F,V)$ such that
$M(F,V) \subseteq M_{\Lambda}(F,V) \subseteq M_{\Omega}(F,V)$ as follows :

Let $t \in M_{\Omega}(F,V)$ : then $t \in M_{\Lambda}(F,V)$ iff :

$t \in V \cup \{\Omega\} \cup F_o$

or

$t = ft_1t_2...t_k$ with $t_i \in M_{\Lambda}(F,V)$ for $i = 1,2,...,k$ and $t_i \in M(F,V)$ whenever $<i,f> \in \Lambda$.

Let $M_{\Lambda}^{\infty}(F,V) = \{ \text{Sup}_n(t_n) / t_n \text{ is an increasing sequence in } M_{\Lambda}(F,V) \}$.

Note that $M^{\infty}(F,V) \not\subseteq M_{\Lambda}^{\infty}(F,V)$ if $\Lambda \neq \emptyset$. In particular $fT_1T_2...T_k \in M_{\Lambda}^{\infty}(F,V)$ if and only $T_i \in M_{\Lambda}^{\infty}(F,V)$ for all $i$ and $T_i \in M(F,V)$ (i.e. is finite without $\Omega$) for $i$ such that $<i,f> \in \Lambda$.
A recursive scheme $\Sigma$ (with functional variables $\phi_1, \dots, \phi_n$) is $\Lambda$-admissible if $T(\Sigma, \phi_i) \in M_{\Lambda}^{\infty}(F, V)$ for all $i$.

It is decidable whether a given scheme is $\Lambda$-admissible but the following sufficient condition will be enough :

(5.4) **Proposition :** A non nested scheme

$\Sigma = \langle \phi_i v_1 \dots v_k \rangle = \tau_i, 1 \le i \le n$
is $\Lambda$-admissible if for every subterm of every
$\tau_i$ of the form $\alpha_1 \dots \alpha_k, \alpha_j \in M(F,V)$ whenever
$<j,f> \in \Lambda$.

(5.5) Definitions :

Let $t \in M_{\Omega}(F \cup \Phi, V)$. An occurrence $\mu$ of a
symbol $x$ is below $\Lambda$ in $t$ if $\mu = \mu_1 j \mu_2$ for some
$\mu_1, \mu_2 \in N_+^*$, $j \in N_+$ such that $\mu_1$ is an occurrence
of some $f \in F$ and $<j,f> \in \Lambda$.

A symbol $x$ is *below* $\Lambda$ in $t$ if all its occurrences
are below $\Lambda$ in $t$.

An equational theory $<S,E>$ is $\Lambda$-admissible if,
for all $<t,t'> \in S \cup E \cup E^{-1}$ :

$$
(5.5.1) \quad |t|_{\Omega} \ge 1 \text{ iff } |t'|_{\Omega} \ge 1
$$
(5.5.2) a variable $v_i$ is below $\Lambda$ in $t$ and $t'$ or
no occurrence of $v_i$ is below $\Lambda$ in $t$ or
in $t'$.

(5.5.3) If $|t|_{v_i} > 1$ then $v_i$ is below $\Lambda$ in $t$
and in $t'$.

Assuming this (together with $\text{Var}(t') \subseteq \text{Var}(t)$
for $\langle t, t' \rangle \in S$ and (4.1.1) for E) we get :

(5.6) **Proposition** : If $t \in M_\Lambda(F,V)$ and $t \xrightarrow{S} t'$ or
$\exists E | t' \text{ then } t' \in M_\Lambda(F,V)$.

Remark that $t \in M_{\Omega}(F,V)$ belongs to $M_{\Lambda}(F,V)$
iff no occurrence of $\Omega$ is below $\Lambda$.

(5.7) **Claim** : Let <S,E> be $\Lambda$-admissible. All the results
of sections 3 and 4 hold if one takes $M_\Lambda(F,V)$
instead of $M_\Omega(F,V)$, $M_\Lambda^\infty(F,V)$ instead of $M_\Omega^\infty(F,V)$
and all recursive schemes involved are assumed
to be $\Lambda$-admissible. In particular, $t, t', z$
will range over $M_\Lambda(F,V)$ and $T, T', Z$...over $M_\Lambda^\infty(F,V)$.
Proofs depending on linearity of <S,E> have been
marked by * in sections 3 and 4. They must be
checked for the new interpretation. The other
ones are hold immediately. We conclude this
section with an example from [4].
(5.8) **Example**: Let $\Lambda = \{<1,h>\}$ and $R = S \cup E$ with

$$
\begin{array}{l@{\quad}l}
\text{S:} & \left\{ \begin{array}{l} k(h(v_1,v_2,v_3),h(v_1,v_4,v_5)) \to h(v_1,k(v_2,v_4),k(v_3,v_5)) \\ k(v_1,\Omega) \to \Omega \qquad k(a,v_1) \to v_1 \\ k(\Omega,v_1) \to \Omega \qquad k(v_1,a) \to v_1 \end{array} \right. \\ \\
\text{F:} & \left\{ \begin{array}{l} k(v_1,v_2) = k(v_2,v_1) \\ k(v_1,k(v_2,v_3)) = k(k(v_1,v_2),v_3) \end{array} \right.
\end{array}
$$

The equational theory <S,E> is Λ-admissible and
c.n.m. (by (4.16)).

Let $\Sigma$ be the following recursive scheme :

$$
\Sigma: \left\{
\begin{array}{l}
\phi v_1 = h(v_1, a, k(fv_1, \phi dv_1)) \\
\psi v_1 = h(v_1, a, k(gv_1, \psi dv_1)) \\
\theta v_1 = k(\phi v_1, \psi v_1)
\end{array}
\right.
$$

With the "fold-unfold-redefine" technique of
[4] we shall find a simpler definition for θ :

$$
\begin{align*}
\theta v_1 &\equiv_R k(\phi v_1, \psi v_1) \\
&\qquad (\text{unfolding } \theta) \\
&\equiv_R k(h(v_1, a, k(fv_1, \phi dv_1)), h(v_1, a, k(gv_1, \psi dv_1))) \\
&\qquad (\text{unfolding } \phi \text{ and } \psi) \\
&\equiv_R h(v_1, k(a, a), k(k(fv_1, \phi dv_1), k(gv_1, \psi dv_1))) \\
&\qquad (\text{using } R) \\
&\equiv_R h(v_1, a, k(k(fv_1, gv_1), k(\phi dv_1, \psi dv_1))) \\
&\qquad (\text{using } R) \\
&\equiv_R h(v_1, a, k(k(fv_1, gv_1), \theta dv_1)) \\
&\qquad (\text{folding } \theta)
\end{align*}
$$
Taking now $\Sigma'$ to be the equation :

$\theta'v_1 = h(v_1,a,k(k(fv_1, gv_1), \theta'dv_1))$ (redefinition)

we are to prove that $\theta' \equiv_R \theta$. We know that $\theta' \le_R \theta$.

It is clear by (5.4) that $\Sigma$ and $\Sigma'$ are both $\Lambda$-admissible.

Let us write $\Sigma'$ in the following (equivalent)
way :

$$ \Sigma'' \begin{cases} \theta'v_1 = h(v_1, a, \theta''v_1) \\ \theta''v_1 = k(k(fv_1, gv_1), h(dv_1, a, \theta''dv_1)) \end{cases} $$

Proposition (3.24) shows that $T(\Sigma'', \theta'')$ is in $S$-normal form and so is $T(\Sigma'', \theta') = T(\Sigma', \theta')$ (since $h \notin \text{Left}(S)$).

Hence $T(\Sigma', \theta')$ is $R$-maximal in $M_\Lambda^\infty(F, V)$. From $(\Sigma', \theta') \le_R (\Sigma, \theta)$ we can conclude $(\Sigma', \theta') \equiv_R (\Sigma, \theta)$.

This transformation generalizes that given in [4]
for a program which computes the sum of two scalar
products : $\vec{a} . \vec{b} + \vec{c} . \vec{d}$. The program of[4] is
obtained from our scheme $\Sigma$ by taking :

- $R \cup \{\perp\}$ as domain

- $f(n) = a[n].b[n]$ if $n \in N$, undefined otherwise

- $g(n) = c[n].d[n]$ if $n \in N$, undefined otherwise

- $h(x,y,z) = \text{if } x = o \text{ then } y \text{ else } z$

- addition for $k$

- minus one for $d$

- $o$ for the constant $a$

Our example proves the correctness of the
transformation of [4].
# VI. CONCLUSIONS.

This work relates two kinds of investigations about :

(1) classes of interpretations ([6], [2], [3])

(2) term rewriting systems ([9], [12], [15], [14]) and produces simple proof methods for the validation of transformations of programs ([8], [4]). It provides a basis for choosing "easy" classes $C_R$ to deal with, and a concrete construction of certain "universal" interpretations $H_C$.

A number of problems are left open :

(6.1) Let S be finite c.n.m. reduction. Is it possible to decide whether a given scheme $\Sigma$ is S-proper ? (I conjective it is). But any way, it is desirable to enlarge conditions (3.20) in such a way that they remain "easily testable".

(6.2) For which equational classes $E_R$ does there exist a $E_R$-projection ?

(6.3) What are the R-maximal infinite trees in the case of an arbitrary R ? of a set R of *inequations* (as in [6]) instead of equations ?

(6.4) Which recursive schemes $\Sigma$ are R-univocal in the situations of (6.3) ?

**Acknowledgements** : Thanks to G.Berry, G.Huet and R.Milner for their helpful comments.
References :

[1] ADJ, Initial algebra semantics and continuous algebras, JACM 24(77) pp 68-95.

[2] G. Berry, B. Courcelle : Canonical forms in stable discrete interpretations, 3<sup>rd</sup> ICALP, Edinburgh (1976).

[3] S. Bloom : Varieties of ordered algebras. JCSS (13) pp 200-212.

[4] R. Burstall, J. Darlington : A transformation System for developing recursive programs, JACM. 24(77) pp 44-67.

[5] B. Courcelle : A Representation of trees by languages, to appear in T.C.S.
or : Recursive schemes, algebraic trees and deterministic languages, 15<sup>th</sup> Symp. on Switching and automata theory, New Orleans (1974) pp 52-62.

[6] B. Courcelle, M. Nivat : Algebraic Families of Interpretations, 17<sup>th</sup> FOCS (1976), Houston.

[7] B. Courcelle, J. Vuillemin : Completeness results for the equivalence of recursive schemes, JCSS 12 (76) pp 179-197.

[8] J. Darlington, R. Burstall : A system which automatically improves programs, 3<sup>rd</sup> IJCAI, Stanford, pp 537-542.

[9] G. Huet : Confluent reductions, 18<sup>th</sup> FOCS (1977).
[10] G. Huet : Personal Communication.

[11] G. Huet, B. Lang : Proving and applying program transformations expressed with 2<sup>nd</sup> order patterns, to appear in Acta Informatica.

[12] D. Knuth, P. Bendix : Simple word problems in universal algebras, Computational problems in abstract algebra, (Leech ed) Pergamon (1970) pp 263-297.

[13] L. Kott : A propos du système de Burstall et Darlington, communication au 3<sup>ème</sup> Colloque sur la Programmation, Paris (Avril 1978).

[14] D. Lankford : Unpublished notes.

[15] R. Lipton, L. Snyder : On the halting of tree replacement systems, "A Conference on T.C.S.", Waterloo (Aug.77) pp. 43-46.

[16] J. McCarthy : A basis for a mathematical theory of computation.

[17] J. Vuillemin, J.C. Raoult : in preparation.

[18] Z. Manna, J. Vuillemin : Fix point approach to the theory of Computation, CACM (1972) 528-536.

[19] W. Damm, E. Fehr, K. Indermark : Higher type recursion and self-application as control structure, 1977 IFIP Working Conference on Formal Description of Programming Concepts, (Neuhold Ed.) North Holland.