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

HAL
open science

# The algebraic semantics of recursive program schemes

Bruno Courcelle, Maurice Nivat

► To cite this version:

Bruno Courcelle, Maurice Nivat. The algebraic semantics of recursive program schemes. [Research Report] IRIA-RR-300, IRIA. 1978, pp.17. hal-04716551

HAL Id: hal-04716551

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

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
RIA

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

THE ALGEBRAIC SÉMANTICS
OF RECURSIVE
PROGRAM SCHEMES

Bruno COURCELLE
Maurice NIVAT

Rapport de Recherche N° 300

Mai 1978
THE ALGEBRAIC SEMANTICS OF RECURSIVE PROGRAM SCHEMES

Bruno Courcelle*, Maurice Nivat**

Résumé :

Ce rapport est une vue d'ensemble des propriétés des schémas de programme récursifs et des classes d'interprétations.

Abstract :

This is a survey of the general properties of recursive program schemes and classes of interpreta-
tions.

N.B. : Ce travail est une communication invitée au symposium MFCS, Zakopane, Pologne (septembre 1978)

N.B. : This work is an invited communication to the Symposium MFCS (Mathematical Foundations of Computer Science) Zakopane, Poland (september 1978)

* IRIA, Rocquencourt - 78150 Le Chesnay, (France)

**IRIA and University Paris 7, France (mailing address : 167 bld Malesherbes, 75017 Paris, France)
# I. Introduction

The equivalence between programs is essential in the mathematical theory of computation and programming. The facts that a program is correct or that program transformation preserves the computed function can be formulated in terms of equivalence between programs. But this relation is very difficult to study for well-known theoretical reasons. Program schemes have been introduced to overcome this difficulty as much as possible.

A program $P$ is divided into a program scheme $\phi$ (i.e. a program where the domain of computation and the base functions are left unspecified) and an interpretation $I$ (i.e. the specification of a domain $D_I$ and a function $f_I = D_I^k \to D_I$ for each $k$-ary base function symbol). We denote by $\phi_I$ the function computed by $\phi$ in $I$ i.e. the function computed by the program $P$.

We express the equivalence of two programs $P = (\phi, I)$ and $P' = (\phi', I)$ as the equivalence of the two program schemes $\phi$ and $\phi'$ in the interpretation $I$ i.e. by the condition $\phi_I = \phi_I'$.

A great deal of work has already been devoted to *proofs of programs* and in particular to methods for proving equivalences of programs.
These methods can be classified in two categories :

(1) *Informal proofs*, performed in the ordinary mathematical language with possible ad hoc shortcuts and omissions of trivialities. Some important examples are McCarthy [18], Morris [22], Burstall [3], Manna and Vuillemin [16].

(2) *Formal proofs*, written in a formal system with axioms and inference rules, mapped on first order logic. Proofs in such systems are lengthy (trivialities cannot be omitted) but they can be *mechanized* as in Milner's LCF [1]. Formal proof systems have been considered in particular by De Bakker [13] and also De Bakker and De Roever [14].

A proof $\Pi$, either formal or informal, that P is equivalent to $P'$ i.e. that $\phi_I = \phi_I'$
uses in an intricate way properties of the interpretation I (for instance that some
function is associative) and properties of the control structure of P and $P'$ i.e.
of the program schemes $\phi$ and $\phi'$. Let now C be the class of all interpretations which
satisfy the properties of I used in $\Pi$. It is clear that $\phi$ will be equivalent to $\phi'$
in every interpretation J of C (we say that $\phi$ and $\phi'$ are C-equivalent and we use
the notation $\phi \equiv_C \phi'$) and that $\Pi$ is a proof of the assertion $\phi \equiv_C \phi'$.

This formulation has at least two advantages :

First it helps to understand why two programs are equivalent, showing what is
used in the proof, and it incitates to reduce the hypotheses (i.e. to enlarge C).
Secondly, if Q and Q' are other programs such that Q = (φ,J), Q' = (φ',J) and
J ∈ C, then Π also proves that Q and Q' are equivalent. A library of <φ,φ',C>
such that φ ≡_C φ' has been used to improve programs by Burstall and Darlington
[12] (and the corresponding informal proofs are provided in Huet and Lang [15]).

The purpose of this paper is to investigate the general properties of the equivalence
≡_C for classes of interpretations C, with respect to recursive program schemes
without assignments. It will be convenient to consider the conditional construct
if...then...else... as a 3-adic function rather than a piece of control structure,
that is to replace it by a 3-adic function symbol h(..., ..., ...,...) which may be in-
terpreted by a 3-adic function satisfying certain properties.

In fact we shall not obtain practical results for arbitrary classes C, but we shall
have mathematical arguments showing why certain classes are comparatively easy to
deal with.
Let us be more precise about the syntax. A recursive program scheme (rps) is a pair <Σ, τ> consisting of a set of equations, each of the form φᵢ(v₁, ..., vₖᵢ) = αᵢ (1 ≤ i ≤ n) representing a "procedure declaration" where φᵢ is the "name" of a "function procedure", v₁, ..., vₖᵢ are the "formal parameters" (of "base type"; we do not allow "procedure parameters") and αᵢ is the "body", a well formed term written with all the φᵢ's, the base function symbols and v₁, ..., vₖᵢ. And τ is a term similar to αᵢ which plays the role of the "main program".

We now presented four key ideas upon which this paper is based.

1) A precise distinction will be made between two concepts of interpretation, namely **functional interpretation** and **total interpretation**, improving the authors' previous works where only total interpretations are considered [6,8,9].

A **functional interpretation** I consists in a domain $D_I$ ordered by $≤_I$ (which means approximation) and functions on $D_I$ corresponding to the base function symbols (and satisfying some axioms listed in section 2).

A **total interpretation** J is a functional interpretation I equipped with values $v_1, v_2, v_3, ...$ from $D_I$ given to the variables $v_1, v_2, v_3, ...$ respectively. We shall write then $J = <I, v_1, v_2, v_3, ...>$. We call it total since all symbols of $F \cup V$ ($F$ is the set of base function symbols and $V = \{v_1, v_2, v_3, ...\}$) have an interpretation.

In a functional interpretation I, a scheme <Σ, τ> defines a **function** $τ_I : D_I^k \to D_I$ (where the variables occurring in τ are $v_1, v_2, ..., v_k$) ; in a total interpretation $J = <I, v_1, v_2, v_3, ...>$, it defines a **value** $τ_J$ belonging to the domain $D_I$. Of course we shall have $τ_J = τ_I(v_1, v_2, ..., v_k)$.

In the first case, $τ_I$ is defined by means of $<φ_{1I}, ..., φ_{kI}>$, the least solution of Σ considered as a system of equations to be solved in the set of continuous functions : $D_I^1 \to D_I$.

All proof methods quoted above are based on this semantic.

In the second case, $τ_J$ is defined as the least upper bound of all the results of the partial finite computations performed using ALGOL's copy rule, the given data $v_1, v_2, ...$ and the base functions of J. This latter definition is closer from a real computation than the former. It can be proved to yield the same result.

2) An elegant proof of this last fact will be provided using **infinite trees**, (i. e. infinite well-formed terms written with base functions symbols : a formal
power series is a good example of such). We denote by $M_{\Omega}^{\infty}(F,V)$ the set of in-
finite trees and order it by $\prec$. (the notation $CT_F(V)$ is used in [1] for the
same set).

An infinite tree $T(\Sigma, \tau)$ is associated with $(\Sigma, \tau)$, and $\tau_I$ is defined in terms
of $T(\Sigma, \tau)$ by $\tau_I = T(\Sigma, \tau)_I$. (A function $T_I : D_I^k \to D_I$ is associated with
$T \in M_{\Omega}^{\infty}(F, \{v_1, \dots, v_k\})$ as an analytic function $C^k \to \mathbb{C}$ is associated with a
formal power series in $k$ variables).

3) Let $C$ be a class of interpretations, either total of functional. In order to study $C$-equivalences of recursive program schemes, we define an equivalence $\equiv_C$ on $M_{\Omega}^{\infty}(F,V)$ by $T \equiv_C T'$ iff $T_I = T'_I$ for all $I \in C$. It is in fact more convenient to introduce a preorder $\le_C$ by $T \le_C T'$ iff $T_I \le_I T'_I$ for all $I \in C$ (the order $\le_I$ of $D_I$ extends to functions). Hence $\tau \equiv_C \tau'$ iff $T(\Sigma, \tau) \le_C T(\Sigma', \tau')$ and $T(\Sigma', \tau') \le_C T(\Sigma, \tau)$.

Our investigations about a class C will be concentrated on $\le_C$. This point is stressed by the following definition : $C \approx C'$ (read "C and C' are equivalent") if $\le_C$ and $\le_{C'}$ are the same. We shall compare classes of interpretations with respect to $\approx$ rather than with respect to set equality, since in a proof of C-equivalence of two program schemes, only $\le_C$ matters, not what is and what is not in C.

4) Finally, all properties of $\le_C$ can be summarized in one interpretation which is essentially $M_{\Omega}^{\infty}(F,V) / \equiv_C$, called the Herbrand interpretation of C, due to its syntactical nature.

This paper is a systematic survey of results about classes of interpretations obtained by the authors in collaboration with I. Guessarian, J.C. Raoult and others. Some of them have already been presented to conferences [6,8], will appear in journals [7,9,10,11]. All proofs are omitted but references are given. Complete proofs will be given in [10].

## II. Basic definitions.

Let $V = \{v_1, v_2, \dots\}$ be the set of variables, $F$ the set of base function symbols with arity $(f \in F$ as arity $\rho(f) \in \mathbb{N})$, and $\Omega$ an extra symbol of arity 0. We denote by $M_{\Omega}^{\infty}(F,V)$ the set of finite well-formed terms written with all these symbols and identify them (as usual) with finite trees.

Letters $t, t', t_1, s, \dots$ will denote elements of $M_{\Omega}^{\infty}(F,V)$. We denote by $M(F,V)$ the set of elements of $M_{\Omega}^{\infty}(F,V)$ with no occurrence of $\Omega$.
The set $M_{\Omega}^{\infty}(F,V)$ is embedded in $M_{\Omega}^{\infty}(F,V)$, the set of infinite trees (denoted by $CT_{F}(V)$ in ADJ [1]), ordered by $\prec$. Every $T \in M_{\Omega}^{\infty}(F,V)$ is the least upper bound of a directed subset of $M_{\Omega}^{\infty}(F,V)$. Every directed subset of $M_{\Omega}^{\infty}(F,V)$ has a least upper bound.

Letters $T, T', T_1, S, \dots$ will denote the elements of $M_{\Omega}^{\infty}(F,V)$.

A **functional interpretation** is a complete F-magma ([8]), also called a continuous F-algebra in ADJ [1] i.e. an object $I = \langle D_I, \le_I, \Omega_I, \langle f_I \rangle_{f \in F} \rangle$ with **domain** $D_I$ (a set), partially ordered by $\le_I$, with a least element $\Omega_I$ (read "bottom" also denoted $\bot$) and $f_I : D_I^{\rho(f)} \to D_I$ for each $f \in F$, such that :

(1) $\le_I$ is **complete** i.e. every directed subset $\Delta$ of $D_I$ has a least upper bound $\text{Sup}(\Delta)$ in $D_I$,

(2) the $f_I$'s are order-preserving and **continuous** i.e.
$f_I(\text{Sup}(\Delta_l), \dots, \text{Sup}(\Delta_k)) = \text{Sup} (f_I(\Delta_l, \dots, \Delta_k))$ for directed subsets $\Delta_l, \dots, \Delta_k$ of $D_I$.

To each $t \in M_{\Omega}^{\infty}(F, V_k)$ ($V_k = \{v_1, \dots, v_k\}$) corresponds a continuous (which from now on also means order preserving) mapping $t_I : D_I^k \to D_I$ in a natural way ; in particular $v_{ik}$ is the $i$th projection. (To be very precise, $t_I$ depends on $t$ and $k$). The set $[D_I^k \to D_I']$ of continuous mappings (where $I'$ is a complete F-magma) ordered by $\alpha \le_I \alpha'$ iff $\alpha(d_1, \dots, d_k) \le_I \alpha'(d_1, \dots, d_k)$ for all $d_1, \dots, d_k \in D_I$, is also a complete partial order (c.p.o.).

Then $T_I : D_I^k \to D_I$ can be defined for $T \in M_{\Omega}^{\infty}(F, V_k)$ by $T_I = \text{Sup}\{t_I/t \prec T\}$.

Let $\alpha \in [D_I^k \to D_I]$ and $\beta_1, \dots, \beta_k \in [D_I^l \to D_I]$ ; we denote by $\alpha[\beta_1, \dots, \beta_k]$ the function of $[D_I^l \to D_I]$ such that $\alpha[\beta_1, \dots, \beta_k] (d_1, \dots, d_l) = \alpha(\beta_1 (d_1, \dots, d_l), \dots, \beta_k (d_1, \dots, d_l))$.
It will be called the **composition** of $\alpha, \beta_1, \dots, \beta_k$. This operation is continuous.

A corresponding operation can be defined on infinite trees : namely $T[T_1, \dots, T_k]$ for $T \in M_{\Omega}^{\infty}(F, V_k)$ and $T_1, \dots, T_k \in M_{\Omega}^{\infty}(F, V_\ell)$ such that :

$$
(2.1) \quad T_I[T_1, \dots, T_k] = (T[T_1, \dots, T_k])_I. \text{ One takes}
$$
$$
T[T_1, \dots, T_k] = \text{Sup}\{t[T_1, \dots, T_k] / t \prec T, t_i \prec T_i \text{ for } i = 1, \dots, k\} \text{ where}
$$
$$
t[T_i, \dots, T_k] = t[T_i / v_1, \dots, T_k / v_k] \text{ is the \underline{substitution} of } t_i \text{ to each occurrence of } v_i \text{ for } i = 1, \dots, k. \text{ We call this operation the \underline{composition of trees}.}
$$

A total interpretation is some $J = \langle I, v_1, v_2, \dots \rangle$ such that $I$ is a functional interpretation and $v_i \in D_I$ is a value given to the variable $v_i$ (the "data"). Hence any
t ∈ M<sub>Ω</sub>(F,V) defines an element of D<sub>I</sub> denoted by t<sub>J</sub>. For T ∈ M<sub>Ω</sub><sup>∞</sup>(F,V), we define
T<sub>J</sub> = Sup{t<sub>J</sub> / t < T}. In some sense, the variables are considered here as <u>constants</u>
i.e. nullary elements of F. We denote by J the "underlying" functional interpretation
I of J = &lt;I, v<sub>1</sub>, v<sub>2</sub>, ...&gt;. If I is a functional interpretation, ⃗I is the set of total
interpretations of the form J = &lt;I, v<sub>1</sub>, v<sub>2</sub>, ...&gt; where the v<sub>i</sub>'s range arbitrarily over D<sub>I</sub>.
If C is a class of functional interpretations, ⃗C is the union of the ⃗I's for I ∈ C.

The total interpretation H = <M_Ω^∞(F,V), v_1, v_2, ...> is initial ([1], [6]): for every
total interpretation J = <I, v_1, v_2, ...> there exists a unique continuous morphism
h_J : H → J such that h_J(v_i) = v_i, namely h_J(T) = T_J (defined above). We call H the
<u>Herbrand</u> (total) interpretation due to its syntactical nature.

### III. Semantics of recursive program schemes.

A <u>recursive program scheme (rps)</u> is a pair Σ,τ> consisting of a system
Σ = <φ<sub>i</sub>(v<sub>1</sub>,...,v<sub>k<sub>i</sub></sub>) = α<sub>i</sub>> |<sub>i≤n</sub> such that k<sub>i</sub> = ρ(φ<sub>i</sub>) and α<sub>i</sub> ∈ M(F ∪ φ,V<sub>k<sub>i</sub></sub>) for
i = 1,...,n (φ = {φ<sub>1</sub>,...,φ<sub>n</sub>} is the ranked alphabet of functional variables) and
a term τ ∈ M(F ∪ φ,V<sub>k</sub>).

We shall frequently omit Σ when the context defines it clearly. We shall also some-
times take φᵢ(v₁, ..., vₖᵢ) for τ and write it simply φᵢ.

Two semantics will be defined, each with an algebraic ("initial" in the sense of
[1]) variant.

(3.1) The "least fixpoint" semantics.

Let (Σ,τ) be a rps and I be a functional interpretation. It is well known that Σ has
a least solution in I which we denote by <φ<sub>1I</sub>,...,φ<sub>nI</sub>>. To be precise, φ<sub>iI</sub> belongs
to [D<sub>I</sub><sup>k</sup> → D<sub>I</sub>]. The definition of the <u>computed function</u> τ<sub>I</sub> : [D<sub>I</sub><sup>k</sup> → D<sub>I</sub>], is now strai-
ghtforward, using the f'<sub>I</sub>'s and the φ<sub>iI</sub>'s.

An alternative way is to take first the least solution <A(Σ,φ₁),...,A(Σ,φₙ)> or Σ
in M<sub>Ω</sub><sup>∞</sup>(F,V). To be precise, A(Σ,φᵢ) ∈ M<sub>Ω</sub><sup>∞</sup>(F,V<sub>kᵢ</sub>) (and the composition of infinite trees
replaces the composition of functions). Then φᵢI is defined as A(Σ,φᵢ)I. By (2.1)
and the continuity of the compositions of trees and functions, the theorem of Mezei-
Wright [20] asserts that the two definitions of φᵢI coincide.
(3.2) The "operational" semantics

Let now J be a total interpretation. Then a value $\tau_J$ is computed in J by $(\Sigma, \tau)$ as
opposed to a function in case (3.1).

A partial computation of $\tau$ in J is a sequence $t_0 \to t_1 \to \dots \to t_m$ where each $t_j$
belongs to $M(F \cup \Phi, D_J)$, $t_0 = \tau[v_1, \dots, v_k]$ and $t_j$ rewrites into $t_{j+1}$ either :

(1) by the replacement of some "procedure name" $\phi_i$ by the corresponding "body"
$\alpha_i$ according to the "copy-rule" (i.e. this is a step of derivation w.r.t.
$\Sigma$ considered as a context-free tree grammar)

(2) by the replacement of some subterm $\phi_i(u_1, \dots, u_{k_i})$ of $t_j$ by $\Omega_j$. This is a
technical trick by which partial computations provide a result in $D_j$ (pos-
sibly undefined).

(3) by the replacement of some subterm $f(d_1, \dots, d_\ell)$ by $d$ if $d_1, \dots, d_\ell \in D_J$ and
$d = f_J(d_1, \dots, d_\ell)$.

If $t_m \in D_J$, then $t_m$ is the result of the partial computation. With some lemmas of
Nivat [23] it can be shown that the set of results of partial computations of $\tau$ in
J is directed, hence has a least upper bound in $D_J$, which will be $\tau_J$. If $h: J \to J'$
is a morphism of total interpretations, then $\tau_J = h(\tau_J)$.

Alternatively, one can compute first in the total interpretation H, one obtains $\tau_H$.
And then $\tau_J = h_J(\tau_H)$ where $h_J$ is the canonical morphism : $H \to J$.

Let us denote $\tau_H = T(\Sigma, \tau)$. The infinite tree $T(\Sigma, \tau)$ is generated by $\Sigma$ considered as a tree grammar (see Courcelle [5]). One can also consider $T(\Sigma, \tau)$ as obtained by "symbolic computation", i.e. without any use the properties of the base functions.

$\mathcal{C}f$

The two definitions are related by :

(3.3) **Theorem** : Let $(\Sigma, \tau)$ be a rps, let $J = \langle I, v_1, v_2, \dots \rangle$ be a total interpretation.
Then $\tau_J = \tau_I(v_1, v_2, \dots, v_k)$.

*Proof* : It suffices to show that $A(\Sigma, \phi_i) = T(\Sigma, \phi_i)$ for $i = 1, \dots, n$. (A Schüt-
zenberger's theorem). This is done in Nivat [23].

(3.4) Corollary : For all r.p.s (Σ,τ) and (Σ',τ') the following are equivalent

(1) $\tau_J \leq_J \tau'_J$ for all total interpretation J
(2) $\tau_I \leq_I^\tau \tau'_I$ for all functional interpretation I

(3) $T(\Sigma, \tau) \prec T(\Sigma', \tau')$

Applications to decision problems can be found in Courcelle [5].

#### IV. Classes of interpretations

**Definitions**: The word *class* (equivalently *family*) is taken in the sense of set theory. Let $C$ be a class of interpretations either total of functional. We associate with $C$ a preorder $\leq_C$ and an equivalence $\equiv_C$ on $M_\Omega^\infty(F,V)$ by :

$T \leq_C T'$ iff $T_I \leq T'_I$ for all $I \in C$.

$T \equiv_C T'$ iff $T_I = T'_I$ for all $I \in C$ (iff $T \leq_C T'$ and $T' \leq_C T$)

We shall compare classes in terms of the induced preorders :

$C \prec_C C'$ iff $T \leq_C T'$ $\Rightarrow_T T \leq_C T'$ for all $T,T'$

$C \nsim_C C'$ iff $T \leq_C T'$ $\Rightarrow_T T \leq_C T'$ for all $T,T'$, (iff $C \prec_C C'$ and $C \nsim_C C'$).

In particular, $C \subseteq C'$ implies $C \prec_C C'$.

(4.1) **Proposition**: If $C$ is a class of total interpretations, $\leq_C$ is a continuous preorder on $M_\Omega^\infty(F,V)$ i.e.

(1) $T \leq_C T'$ if $T \prec_T T'$,

(2) $\text{Sup}_I(T_i) \leq_C T'$ if $(T_i)_{i \in I}$ is directed w.r.t. $\prec$ and $T_i \leq_C T'$ for all $i \in I$.

(3) $f(T_1, \dots, T_k) \leq_C f(T'_1, \dots, T'_k)$ if $T_i \leq_C T'_i$ for $i = 1, \dots, k$.

If $C$ is a class of functional interpretations, $\leq_C$ is also compatible with composition i.e. satisfies :

(4) $T_o[T_1, \dots, T_k] \leq_C T'_o[T'_1, \dots, T'_k]$ if $T_i \leq_C T'_i$ for $i = 0, \dots, k$.

We shall state a converse to (4.1).

Let $C$ be a class of total interpretations, and $J_o$ be a total interpretation not necessarily in $C$. It is said *C-universal* if for all $J \in C$ there exists a unique morphism $h: J_o \to J$. It is said *C-Herbrand* is $C \nsim_J \{J_o\}$.

Let $C$ be a class of functional interpretations. An interpretation $I_o$ is *C-Herbrand* if $C \nsim_o \{I_o\}$.
For a preorder $\pi$ on $M_{\Omega}^{\infty}(F,V)$, let $T_{\pi}$ be the class of total interpretations J such that $\pi \subseteq \leq_{\{J\}}$; let $C_{\pi}$ be the class of functional interpretations I such that $\pi \subseteq \leq_{\{I\}}$.

(4.2) **Theorem**: Let $\pi$ be a continuous preorder on $M_{\Omega}^{\infty}(F,V)$; there exists a total interpretation $K_{\pi}$ such that:

1) $\pi = \leq_{\{K_{\pi}\}}$ hence $K_{\pi} \in T_{\pi}$,

2) $K_{\pi}$ is $T_{\pi}$-universal,

3) $\{K_{\pi}\} \cong T_{\pi}$ i.e. $K_{\pi}$ is $T_{\pi}$-Herbrand.

Furthermore, if $\pi$ is compatible with composition :

1') $\pi = \leq_{\{\tilde{K}_{\pi}\}}$ hence $\tilde{K}_{\pi} \in C_{\pi}$,

2') $K_{\pi}$ is $\tilde{C}_{\pi}$-universal,

3') $\{\tilde{K}_{\pi}\} \cong C_{\pi}$ hence $\tilde{K}_{\pi}$ is $C_{\pi}$-Herbrand.

**Proof** : The natural candidate for $K_{\pi}$ is clearly the quotient p.o. $M_{\Omega}^{\infty}(F,V) / \tilde{\pi}$ where $\tilde{\pi}$ is the equivalence canonically associated with the preorder $\pi$. But it is not complete in general. So we complete it appropriately (see [11]) and we obtain $K_{\pi}$.□

Let us take $\pi = \leq_C$ for some class C of total interpretations. Then $K_{\pi}$ is C-universal and C-Herbrand. But unfortunately, the construction of $K_{\pi}$ is rather complicated, using transfinite induction, and does not help very much for studying $\leq_C$. (The existence of $K_{\pi}$ seems also to follow from general categorical arguments [19].□

## V. Algebraicity

We shall give conditions on $\pi$ under which the interpretation $K_{\pi}$ can be defined in an elegant way as the completion by ideals (Markowsky and Rosen [17], Courcelle and Nivat [8]) of a quotient of $M_{\Omega}^{\infty}(F,V)$.

### Definitions :

A continuous preorder $\pi$ on $M_{\Omega}^{\infty}(F,V)$ is said **algebraic** [8] if for all $t \in M_{\Omega}^{\infty}(F,V)$ and $T' \in M_{\Omega}^{\infty}(F,V)$ :

(5.1) $t \pi T' \Leftrightarrow \exists t' < T'$ such that $t \pi t'$. Equivalently, for all $T, T'$ :

(5.2) $T \pi T' \Leftrightarrow \forall t < T, \exists t' < T'$ such that $t \pi t'$

A class C of functional or total interpretations is **algebraic** if $\leq_C$ is algebraic.
Condition (5.2) expresses that the preorder $\pi$ on $M_{\Omega}^{\infty}(F,V)$ can be defined in terms of its restriction $\pi^{\circ}$ to $M_{\Omega}(F,V)$.

Let us consider some consequences for recursive program schemes.

Given a rps $(\Sigma, \phi)$ and an interpretation $I$, let $\phi_I^{(m)} \le_I^{\phi_I}$ be the approximation of $\phi_I$ which can be computed with at most $m$ levels of recursion. A term $\phi^{(m)} \in M_{\Omega}(F,V)$ can be defined which represents $\phi_I^{(m)}$.

Let $(\Sigma, \phi)$ and $(\Sigma', \phi')$ be two r.p.s. and $C$ be a class of interpretations :

$$1) \phi \le_C \phi' \text{ iff}$$

$$2) \forall I \in C, \phi_I \le \phi_I^{\prime} \text{ iff}$$

$$3) \forall I \in C, \forall \vec{d} \in D_I^k, \phi_I(\vec{d}) \le \phi_I^{\prime}(\vec{d}) \text{ if}$$

$$4) \forall I \in C, \forall \vec{d} \in D_I^k, \forall n \in \mathbb{N}, \exists m \in \mathbb{N} \ \phi_I^{(n)}(\vec{d}) \le \phi_I^{(m)}(\vec{d})$$

But if $C$ is algebraic, (1) is equivalent to

$$5) \forall n \in \mathbb{N}, \exists m \in \mathbb{N}, \phi^{(n)} \le_C \phi^{(m)}$$

which is equivalent to :

$$6) \forall n \in \mathbb{N}, \exists m \in \mathbb{N}, \forall I \in C, \forall \vec{d} \in D_I^k, \phi_I^{(n)}(\vec{d}) \le \phi_I^{(m)}(\vec{d})$$

The only difference between (4) and (6) lies in the place of $\forall n \exists m$. Hence $\phi_I(\vec{d}) \le_I^{\phi_I} \phi_I(\vec{d}')$ for all $I \in C$ and $\vec{d} \in D_I^k$ in a *uniform way* if $C$ is algebraic.

The proof method of Morris [22] consists in proving (5) by induction on $n$ ; and (1) can be inferred from (5).

If $C$ is algebraic then (1) $\iff$ (5), (but we do not assert that an inductive argument always exist when (5) holds).

There are also some relations with the concept of an *algebraic c.p.o.* used in Milner [21] (and many other works). Let us recall some definitions. Let $\langle D, \le \rangle$ be a p.o. set.

A element $d$ of $D$ is *compact* (Markowsky and Rosen [17]) if for all directed subset $\Delta$ of $D$ having a least upper bound $d'$ then $d \le d'$ if and only if $d \le \delta$ for some $\delta$ in $\Delta$. Such elements are called *finite* in [21].

A subset $B$ is a *base* of $D$ if every $d \in B$ is compact and every $d \in D$ is the least upper bound of a directed subset of $B$. A c.p.o. having a base is said *algebraic*. A systematic study of related definitions is done in Thatcher et al. [24].

Let $\pi$ be an algebraic preorder on $M_{\Omega}^{\infty}(F,V)$, and $[t]$ denote the canonical image of $t \in M_{\Omega}(F,V)$ in $M_{\Omega}^{\infty}(F,V) / \pi$. Then, condition (5.1) expresses exactly that each $[t]$
is compact in $M_\Omega^\infty(F,V) / \pi$. Hence $[[t] / t \in M_\Omega(F,V)]$ is a base for $M_\Omega^\infty(F,V) / \pi$ and the only reason for which $M_\Omega^\infty(F,V) / \pi$ is not necessarily algebraic is that it may be not complete.

A total interpretation $I$ is said *algebraic* if it is an algebraic c.p.o. with base $B_I = \{t_I / t \in M_\Omega(F,V)\}$. (Not algebraic, considered as a class reduced to a single total interpretation).

(5.3) **Remarks :** 1) $\{J\}$ is an algebraic class if $J$ is an algebraic* total interpretation. The converse may fail.

2) An algebraic class may consist of non-algebraic* interpretations and a non-algebraic class of algebraic* interpretations only.

Since we are interested in properties of preorders $\le_C$ we shall consider algebraic classes of interpretations rather than algebraic* interpretations. But some sort of converse to remark 1 will be nevertheless given (theorem (5.8)).

We now consider an important way of defining algebraic classes of interpretations.

(5.4) Relational classes of interpretations

A class of interpretations of the form $C = C_R = \{I / t_I \le t_I' \text{ for all } (t,t') \in R\}$ where $R$ is some subset of $M_\Omega(F,V) \times M_\Omega(F,V)$ is said *relational*. We shall also consider *equational* classes i.e. $E_R = C_{R\cup R} - I = \{I / t_I = t_I' \text{ for all } (t,t') \in R\}$.

We simplify the notation $\le_C$ into $\le_R$ and $\equiv_C$ into $\equiv_R$.

We shall be able to characterize $\le_R$.

For $s,s' \in M_\Omega(F,V)$ let $s \underset{R}{\to} s'$ if and only if :

$s = s'' [t_1/v_\ell]$ and $s' = s''[t'_1/v_\ell]$ for some $s'' \in M_\Omega(F,V)$ with one occurrence of $v_\ell$
$t_1 = t[u_1, \dots, u_k]$ and $t'_1 = t'[u_1, \dots, u_k]$ for some $u_1, u_2, \dots, u_k \in M_\Omega(F,V)$ and
$(t,t') \in R \cap (M_\Omega(F,V_k) \times M_\Omega(F,V_k))$.

Then $\le_R = (\prec_R \cup \prec_R^*)^*$ is a preorder on $M_\Omega(F,V)$ and $\prec_R$ the associated equivalence relation. We get canonically an ordered quotient $F$-magma denoted by $M_\Omega(F,V) / \prec_R$. Let $\hat{H}_R$ be its completion by ideals (Markowsky and Rosen [17], Courcelle and Nivat [8], adapting a classical construction for lattices, Birkhoff [1a]). Let $H_R$ be the total interpretation $\hat{H}_R \times [v_1]_{\prec_R} \times [v_2]_{\prec_R} \times \dots$.

(5.5) **Proposition** : The total interpretation $H_R$ is $\overline{C_R}$-universal

For a class $C$ of interpretations, let us also introduce $\hat{C} = C \underset{\subset C}{\le}$, the class of
all interpretations I such that $t_I \le t'_I$ for all $t, t' \in M_\Omega(F, V)$ such that $t \le_C t'$.
It is clear, that $C_R = C_R^\wedge$ for a relational class $C_R$.

(5.6) **Theorem**: Let $C$ be class of functional interpretations. The following properties are equivalent:

1) $C$ is algebraic

2) $C \cong \tilde{C}$

3) $C \cong C_R$ for some $R \subseteq M_\Omega(F, V)^2$

4) $\bar{C} \cong \{H_R\}$ for some $R \subseteq M_\Omega(F, V)^2$ i.e. $H_R$ is $\bar{C}$-Herbrand; $C \cong \{H_R\}$ i.e. $H_R$ is $C$-Herbrand.

5) there exists an algebraic* $\bar{C}$-Herbrand total interpretation.

**Proof**: 1) $\Rightarrow$ 2) $\Rightarrow$ 3) $\Rightarrow$ 4) $\Rightarrow$ 5) $\Rightarrow$ 1). $\square$

(5.7) **Corollary**: A relational class $C_R$ is algebraic; the preorders $\le_R^0$ and $\le_R^\infty$ coincides.

(5.8) **Theorem [8]**: Let $C$ be a class of total interpretations. The following properties are equivalent:

1) $C$ is algebraic;

2) $C \cong \{H \le_C 0\}$ i.e. $H \le_C 0$ is $C$-Herbrand,

3) there exists an algebraic* $C$-Herbrand total interpretation.

(5.9) What classes are algebraic?

Let us summarize the main results of [6,8,9]. The classes $C$ and $C'$ are algebraic, $R$ is a subset of $M_\Omega(F, V) \times M_\Omega(F, V)$, $A$ is a first order logical theory, $C_n$ is the class of interpretations I the domain of which has increasing chains of length $n+1$ at most. Hence $C_1 = \mathcal{D}$, the class of discrete interpretations investigated in [9] (a product of $n$ discrete interpretations belongs to $C_n$).

<table><thead><tr><th>Algebraic</th><th>Non necessarily algebraic</th></tr></thead><tbody><tr><td>$C \cup C'$</td><td>$C \cap C'$, $C \cap C_R$</td></tr><tr><td>$C_R, E_R$</td><td>$E_{\{\phi, \psi\}} = \{I / \phi_I = \psi_I\}$</td></tr><tr><td>$\{I / I \in C_n \text{ and } I \models A\}$<br>$\mathcal{D}_R = C_R \cap \mathcal{D}$</td><td>$\{I / I \text{ is an interpretation and } I \models A\}$</td></tr></tbody></table>
(5.10) A non algebraic class

Let $C = E_{\{\phi, \psi\}}$ where $\phi$ and $\psi$ are the following schemes :
$\phi v_1 = f(v_1, \phi hv_1)$ and $\psi v_1 = g(v_1, \psi hv_1)$.

Then $C$ is clearly non empty, and it can be shown that $\leq_C^o = \prec$. Hence $C$ is not algebraic, otherwise $\leq_C = \prec$ which is clearly not the case since $T(\phi) \neq T(\psi)$ but $\phi \equiv_C \psi$.

Let $\theta$ be defined by the rps : $\theta v_1 = f(v_1, g(hv_1, \theta h.hv_1))$. Since $\phi v_1 \equiv_C f(v_1, \phi hv_1) \equiv_C f(v_1, \psi hv_1) \equiv_C f(v_1, g(hv_1, \psi hhv_1)) \equiv_C f(v_1, g(hv_1, \phi hhv_1))$ then $\theta \leq_C \phi$. It can be shown that $\theta \not\equiv_C \phi$. An open problem is to find a characterization of $\leq_C$.

(5.11) Some "good" equational classes. (see [7]).

Let $C = E_R$ where $R$ is finite and each $t \in M_\Omega(F,V)$ has a unique $R$-normal form $c_R(t)$ such that $t \xrightarrow{\cdot} c_R(t)$ and $c_R(t) \xrightarrow{\cdot} t'$ for no $t' \in M_\Omega(F,V)$. Let us also assume that $c_R$ is monotone, i.e. $c_R(t) \prec c_R(t')$ if $t \prec t'$.

If this holds, one can define for every $T \in M_\Omega^\infty(F,V)$ its $R$-normal form $c_R(T) = \text{Sup}\{c_R(t) / t \prec T\}$, and prove that
$$T \leq_R T' \iff c_R(T) \prec c_R(T').$$

We obtain a "concrete" description of $H_R$, its domain being $\{c_R(T) / T \in M_\Omega^\infty(F,V)\}$ ordered by $\prec$. In certain cases, we can also insure that $c_R(T(\Sigma, \phi))$ is maximal with respect to $\prec$ (for some recursive scheme of the form $<\phi(v_1, ..., v_k) = \alpha>$). If this holds, then $\Sigma$ has a unique solution in $M_\Omega^\infty(F,V) / \equiv_R$ (any other solution defined by some $T \in M_\Omega^\infty(F,V)$ would satisfy $T(\Sigma, \phi) \leq_R T$ hence $c_R(T(\Sigma, \phi)) \prec c_R(T)$ hence $c_R(T(\Sigma, \phi)) = c_R(T)$).

In order to prove that $\phi \equiv_R \phi'$, it suffices to prove that $\phi' \equiv_R \alpha\{\phi' / \phi\}$, by checking equations and without use of any of the "induction principles" described in [16].

This applies to certain correctness proofs given in [15] of program transformations of [12] and to program transformations defined with the unfold-fold-redefine technique of [4].
References :

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

[1a] G. Birkoff, *Lattice Theory*, AMS (1967).

[2] S. Bloom, *Varieties of ordered algebras*, JCSS 13 (1976), pp 200-212.

[3] R. Burstall, *Proving properties of programs by Structural induction*, Comp. Journal 12 (1969) 41-48.

[4] R. Burstall, J. Darlington, *A transformation system for developing programs*, JACM 24 (1977) 44-67.

[5] B. Courcelle, *A representation of trees by languages*, to appear in TCS (1978).

[6] B. Courcelle, *On the definition of classes of interpretations*, 4th ICALP Turku (1977) Lec,notes in Comp. Sc. Vol.52. (Springer Verlag).

[7] B. Courcelle, *On recursive equations having a unique solution*, Laboria report 285.

[8] B. Courcelle, M. Nivat, *Algebraic families of interpretations*, 17th Symposium on F.O.C.S (Houston 1976) and Laboria report 189.

[9] B. Courcelle, I Guessarian, *On some classes of interpretations*, to appear in J.C.S.S. (and Laboria report 253).

[10] B. Courcelle, M. Nivat, in preparation.

[11] B. Courcelle, J.C. Raoult, *Completions of ordered magmas*, to appear in Fundamenta Informaticae.

[12] J. Darlington, R. Burstall, *A system which automatically improves programs*, 3rd IJCAI, SRI (1973) 537-542.

[13] J. De Bakker, *Recursive Procedures*, Mathematical center Tract 24, Amsterdam 1971.
[14] J. De Bakker, W.P. De Roewer, *A calculus for recursive program schemes in Automata, Languages, Programing*, (Nivat ed.)
North-Holland, Amsterdam 1972.

[15] G. Huet, B. Lang, *Proving and applying program transformations expressed with 2nd order patterns*, to appear in *Acta Informatica* (Laboria report 266).

[16] Z. Manna, J. Vuillemin, *Fixpoint approach to the Theory of Computation*, CACM 15 (1972), pp 528-536.

[17] G. Markowsky, B. Rosen, *Bases for Chain-complete posets*, IBM Jour. of Res. and Dev. vol.20 (1976) pp 138-147.

[18] J. McCarthy, *A basis for a mathematical theory of computation in Computer programing and Formal systems*, Braffort and Hirshberg ed., North-Holland, Amsterdam (1963).

[19] J. Messeguer, *On order Complete Universal Algebra and Enriched Factorial Semantics*, FCT 77 (Poznan), Lecture Notes in Computer Sciences, Springer-Verlag

[20] J. Mezei, J.B. Wright, *Algebraic automata and context-free sets*, Inf. and Control 11 (1967) pp 3-29.

[21] R. Milner, *Fully abstract models of typed λ-calculi*, TCS 4 (1977) 1-22.

[22] J.H. Morris, *Another Recursion Induction Principle*, CACM Vol. 14, n° 5 (1971).

[23] M. Nivat, *On the interpretation of polyadic recursive schemes*, Symposia Mathematica, vol. 15, Academic Press (1975).

[24] J.W. Thatcher, E.G. Wagner, J.B. Wright, *A uniform approach to inductive posets and inductive closure*, to appear in T.C.S.