# Algebraic families of interpretations

Bruno Courcelle, Maurice Nivat

► To cite this version:

Bruno Courcelle, Maurice Nivat. Algebraic families of interpretations. [Research Report] IRIA-RR-189, IRIA. 1976, pp.10. hal-04716351

HAL Id: hal-04716351

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

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
RIA

laboria

Institut de Recherche
d'Informatique
et d'Automatique

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

laboratoire de recherche
en informatique
et automatique

ALGEBRAIC FAMILIES
OF INTERPRETATIONS

Bruno COURCELLE
Maurice NIVAT

Rapport de Recherche N° 189

Juillet 1976
ALGEBRAIC FAMILIES OF INTERPRETATIONS

B. Courcelle, M. Nivat

Résumé :

A toute famille C d'interprétations correspond une équivalence entre schémas de programmes ; deux schémas sont C-équivalents s'ils calculent la même chose dans toute interprétation de C. Une famille C est algébrique si deux programmes sont C-équivalents ssi tout calcul partiel fini de l'un est C-equivalent à quelque calcul partiel fini de l'autre. On montre qu'une famille C est algébrique ssi elle peut se représenter (en ce qui concerne l'équivalence des programmes) par une unique interprétation, algébrique au sens de Scott.

Abstract :

To each family C of interpretations corresponds an equivalence relation among program schemes, namely the equivalence of the program schemes for all interpretation of C. A family C is algebraic if any two programs are C-equivalent iff every partial finite computation of one of them is C-equivalent to some partial finite computation of the other. Our main theorem states that a family C is algebraic iff it is represented with respect to the equivalence of programs by a single interpretation (a C-Herbrand interpretation) which is algebraic (in Scott's sense, roughly speaking). We give examples of algebraic and non algebraic families.

Ce travail sera présenté au 17ème «Symposium on Foundations of Computer Science», Houston, Octobre 1976 et
doit être cité comme tel.

This work is to be presented at a conference and should be referred as a communication to the 17th annual Symposium on Foundations of Computer Science, Houston, October 1976.
ALGEBRAIC FAMILIES OF INTERPRETATIONS

By Bruno COURCELLE, IRIA,

and Maurice NIVAT, IRIA and University of Paris-7,

IRIA, Domaine de Voluceau, 78150 LE CHESNAY (France).

**Abstract** : To each family C of interpretations corresponds an equivalence relation among program schemes, namely the equivalence of the program schemes for all interpretation of C. A family C is *algebraic* if any two programs are C-equivalent iff every partial finite computation of one of them is C-equivalent to some partial finite computation of the other. Our main theorem states that a family C is algebraic iff it is represented with respect to the equivalence of programs by a single interpretation (a C-Herbrand interpretation) which is *algebraic* (in Scott's sense, roughly speaking). We give examples of algebraic and non algebraic families.

I. Introduction :

A program can be considered as a pair consisting of a program scheme (i.e. a program where base functions have been replaced by function symbols) and an interpretation (i.e. a meaning given to the function symbols).

A proof that two programs are equivalent only uses certain properties of the base functions (let R denote these properties). Hence it is in fact a proof that the two program schemes are equivalent for every interpretation of the class C of interpretations where all properties of R are satisfied. The notion of a class (equivalently : family) of interpretations allows to handle mathematically what is really used in a proof of equivalence between two programs.

Let us now consider some examples.

**Example 1** : Let $\Phi: D \times D \to D$ be defined by the following recursive equation :

$$ \Phi(x,y) = \mathbf{if} \ p(x) \ \mathbf{then} \ y \ \mathbf{else} \ \Phi(k(x),h(y)) $$

(for some predicate P on D and monadic functions k, h : D → D). It satisfies the following :

$$ (1) \quad \Phi(x,h(y)) = h(\Phi(x,y)) $$

which can be proved by computation induction ([7]) as follows :

Let $\Phi_n : D \times D \to D$ be the restriction of $\Phi$ which can be computed using at most n calls of procedure $\Phi$. It can be expressed by a term $t_n(x,y)$. The $t_n$'s are inductively defined by :

$$ t_0 = \mathbf{if} \ p(x) \ \mathbf{then} \ y \ \mathbf{else} \ \mathbf{undefined} $$

$$ t_{n+1} = \mathbf{if} \ p(x) \ \mathbf{then} \ y \ \mathbf{else} \ t_n(k(x), h(y)) $$

By using the following properties :

$$ h(\mathbf{undefined}) = \mathbf{undefined} $$

$$ h(\mathbf{if} \ p(x) \ \mathbf{then} \ y \ \mathbf{else} \ z) = \mathbf{if} \ p(x) \ \mathbf{then} \ h(y) \ \mathbf{else} \ h(z) $$

one proves by induction on n that for all n : $t_n(x,h(y)) = h(t_n(x,y))$ whence

$$ (2) \quad \Phi_n(x,h(y)) = h(\Phi_n(x,y)) $$

Now, (1) clearly follows from (2), i.e. the equivalence of $\Phi(x,h(y))$ and $h(\Phi(x,y))$ follows from a set of equivalences between partial computations of these two programs.

**Example 2** : Let us consider :

$$ \begin{cases} \Phi(x) = \mathbf{if} \ x = a \ \mathbf{then} \ a \ \mathbf{else} \ \Phi(h(x)) \\ \text{assuming that } \forall x \in n, h^n(x) = a \end{cases} $$

We clearly have $\Phi(x) = a$ for all x.

The proof of example 1 does not work. Defining $\Phi_n(x)$ as before, we can only prove that $\Phi_n(x) \subseteq a$ (i.e. : $\Phi_n(x) = a$ if defined). Clearly, $a \supseteq \Phi_n(x)$ does not hold in general (choose x such that $h^i(x) \neq a$ for $O \in \mathfrak{O}$).
The proof that a $\subseteq \emptyset$ ($x$) needs another argument based on a termination property.

Hence, certain equivalence proofs only use a finite number of relations between the base functions when other ones require more accurate properties of the domains. This informal distinction is expressed as a property of the class of interpretations in which an equivalence proof is valid.

We now sketch our main definitions and results. If C is a class of interpretations, two schemes are *C-equivalent* iff they are equivalent in every interpretation of C. A class C is *algebraic* if, roughly speaking, any two schemes are C-equivalent iff every finite partial computation of one them is C-equivalent to some finite partial computation of the other.

For instance, classes of interpretations defined by relations between finite terms are algebraic. On the other hand the family of interpretations in which two given programs are equivalent is not algebraic in general.

An interpretation $H$ is *C-Herbrand* for some class C of interpretations if C-equivalence coincides with (H)-equivalence, that is if $H$ represents the whole class C with respect to the equivalence of programs schemes. Our main theorem states that a class C is algebraic iff it has an Herbrand interpretation which is algebraic (in the sense of lattice theory; cf Birkhoff [1], Scott [11]).

In the case of a class $C_R$ defined by a set $R$ of equations between finite terms, the Herbrand interpretation can be algebraically defined from $R$. A proof of the $C_R$-equivalence of two programs is in fact a proof of their equivalence in the Herbrand interpretation. The classes of discrete and stable discrete interpretations of [2] are algebraic but not definable by equations.

The paper is divided as follows : the algebraic framework is presented in section 2 ; recursive program schemes and their semantics are recalled in section 3 from previous works ; section 4 deals with C-Herbrand interpretations and algebraic classes ; relational classes of interpretations are considered in section 5.

## 2. Algebraic Framework.

Let $(D, \leq)$ be a (partially) ordered set. A subset $\Delta$ of $D$ is *directed* if : $\forall d_1, d_2 \in \Delta, 3d_3 \in \Delta \text{ s.t. } d_1 \leq d_3 \text{ and } d_2 \leq d_3$. An ordered set is *complete* if every directed subset $\Delta$ of $D$ has a least upper bound (denoted $\text{Sup}(\Delta)$). An *ideal* is a directed subset $\Delta$ of $D$ such that $\forall d_1, d_2 \in D, d_1 \leq d_2$ and $d_2 \in \Delta \Rightarrow d_1 \in \Delta$. The set $D^k$ whose elements are denoted $\bar{d}$ is ordered component-wise. Let $(D, \leq)$ and $(D', \leq')$ be ordered sets. A mapping $g: D^k \rightarrow D'$ is *increasing* if $\bar{d} \leq \bar{d}'$ implies $g(\bar{d}) \leq' g(\bar{d}')$ and *continuous* if for all directed subsets $\Delta_1, \dots, \Delta_k$ of $D$ having least upper bounds $\delta_1, \dots, \delta_k$ respectively, $g(\Delta_1, \dots, \Delta_k)$ has a least upper bound which is $g(\delta_1, \dots, \delta_k)$.

### Ordered F-magmas

Let $F$ be a possibly infinite fixed set of function symbols, each of which is given with an *arity* ($f \in F$ has *arity* $\rho(f) \geq 0$). The set $F$ contains a special symbol $\Omega$ of *arity* 0. An *F-magma* (or *F-algebra* but there is conflict with the classical notion of *algebra*) is an object $M = (D_M, (f_M)_{f \in F})$ where $f_M$ is a total mapping : $D_M^{\rho(f)} \to D_M$ for each $f \in F$. An *ordered F-magma* is some $M = (D_M, \leq_M, (f_M)_{f \in F})$ where $\leq_M$ is a partial order on $D_M$, $\Omega_M \leq_M \emptyset$ for all $d \in D_M$ and the $f_M$'s are increasing. It is *complete* if $(D_M, \leq)$ is complete and the $f_M$'s are continuous. (We frequently omit the subscripts $M$ when no confusion can occur. We also (traditionally) use $\perp$ for $\Omega_M$). For ordered F-magmas $M$ and $M'$, a morphism $\theta: M \to M'$ is *increasing* mapping $\theta : D_M \to D_{M'}$ such that, for all $f \in F$, $d_1, \dots, d_i, \dots \in D_M$ :

$$ \theta(f_M) = f_M, \text{ if } \rho(f) = 0, $$

$$ \theta(f_M(d_1, \dots, d_k)) = f_{M'}(\theta(d_1), \dots, \theta(d_k)) \text{ if } \rho(f) = k. $$

Let us denote $M(F)$ the set of terms written on $F$ and well formed with respect to arities. (We usually denote $s, s', t, t_1, \dots, u, u' \dots$ the elements of $M(F)$). It is an $F$-magma with $f_M(F)(t_1, \dots, t_k) = f(t_1, \dots, t_k)$ for $k = \rho(f)$ and $t_1, \dots, t_k \in M(F)$. We order $M(F)$ by s.t :

$$ (1) \quad \Omega \preceq t', $$

$$ (2) \quad f(t_1, \dots, t_k) \preceq t' \text{ iff } t' = f(t'_1, \dots, t'_k) \text{ and } t_1 \preceq t'_1, \dots, t_k \preceq t'_k. $$
Then $M(F)$ is an ordered F-magma and in fact the free one since :

**Proposition 1** : For any ordered F-magma $M$ there exists one and only one morphism $j_M : M(F) \to M$. (We often denote $t_M$ instead of $j_M(t)$).

Let now $V = \{v_1, v_2, ..., v_n, ...\}$, be a set of elements of arity 0 called **variables** (and $V_k = \{v_1, ..., v_k\}$ for $k \ge 1$). We use the notation $M(F, V_k)$ for $M(F \cup V_k)$. To any $t \in M(F, V_k)$ and F-magma $M$, there clearly corresponds a mapping $t_M : D_M^k \to D_M^{(1)}$. This mapping is increasing if $M$ is ordered and continuous if $M$ is complete. If $t, t_1, ..., t_k \in M(F, V)$, we denote $t[t_1/v_i, ..., t_k/v_i]$ the result of the substitution of $t_j$ to each occurrence of $v_i$ for all $1 \le j \le k$ ($v_i, ..., v_i$ is a list of pairwise distinct elements of $V$). We use the simplified notation $t[t_1, ..., t_k]$ for $t[t_1/v_1, ..., v_k/v_k]$.

**Quotient-magmas**

Let $M$ be an ordered F-magma. An F-magma **preorder** $\leq_M$ on $M$ is a reflexive and transitive relation on $D$ such that:

(1) $d \leq_M d' \Rightarrow d \leq_M d'$ for all $d, d' \in D$,

(2) $d_1 \leq_M d'_1, ..., d_n \leq_M d'_n \Rightarrow f_M(d_1, ..., d_n) \leq_M f_M(d'_1, ..., d'_n)$ for all $f \in F$ and $d_1, ..., d'_n \in D$.

The equivalence $\tilde{\pi}$ associated to $\pi$, classically defined by $d \tilde{\pi} d'$ iff $d \pi d'$ and $d' \pi d$ is an F-magma congruence, that is an equivalence relation satisfying (2) above.

Let $M/\pi$ be $<D/\tilde{\pi}, \leq_M, (f_M/\tilde{\pi}) \in \tilde{F}>$ where $D/\tilde{\pi}$ is the quotient set of $D$ by $\tilde{\pi}$, $[d]_{\tilde{\pi}}$ denotes the equivalence class of $d$ for $d \in D$, $[d]_{\tilde{\pi}} \leq_M [d']_{\tilde{\pi}}$ iff $d \pi d'$ and $f_M/\tilde{\pi}([d_1]_{\tilde{\pi}}, ..., [d_n]_{\tilde{\pi}}) = [f_M(d_1, ..., d_n)]_{\tilde{\pi}}$. Let $h : M \to M/\pi$ be defined by $h(d) = [d]_{\tilde{\pi}}$.

It is well known (and in fact easy to prove) that $\leq_M$ and the $f_M/\tilde{\pi}$'s are well-defined, that $h$ is a morphism and that the following holds :

**Proposition 2** : For every ordered F-magma $M'$ and morphism $\theta : M \to M'$ such that $d \pi d' \Rightarrow \theta(d) \leq_M \theta(d')$ for all $d, d' \in D_M'$, there exists a unique morphism $\mu : M/\pi \to M'$ such that the following diagram commutes :

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

**Remark** : The magma $M/\pi$ neednot be complete even if $M$ is complete.

**Completion of an ordered magma.**

We now recall the completion by ideals (Birkhoff [1], Markowsky-Rosen [8]) by which an ordered F-magma $M$ can be embedded into a complete one. Let $M$ be an ordered F-magma.

**Proposition 3** : There exists a complete F-magma $M^\infty$ and an injective morphism $i : M + M^\infty$ such that for any complete F-magma $M'$ and morphism $\psi : M \to M'$ there exists one and only one continuous morphism $\psi^\infty : M^\infty \to M'$ such that the following diagram is commutative :

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

**Proof** : Let us recall that $D_M^\infty$ is the set of directed ideals of $D_M$, that $\leq_M^\infty$ is the set-theoretical inclusion, that $f_M^\infty(\Delta_1, ..., \Delta_n) = \{d \in D / d \leq_M^\infty f_M(d_1, ..., d_n) \text{ for some } d_1 \in \Delta_1, ..., d_n \in \Delta_n\}$, that $i(d) = \{d' \in D_M / d' \leq_M^\infty d\}$ and finally that $\psi^\infty(\Delta) = \text{Sup}_M(\Delta)$. Verifications are left to the reader. $\square$

The following special case is important. We denote by $M^\infty(F)$ the completion of $M(F)$ and consider that $M(F) \subset M^\infty(F)$. The order relation on $M^\infty(F)$ is denoted $\prec$ and $T, T', U, U_1, U_2, ...$ usually denote elements of $M^\infty(F)$.

<footnote>(1) This notation is consistent with that of proposition 1.</footnote>
Elements of $M^{\infty}(F)$ may be visualized as infinite trees. For instance, the least upper bound in $M^{\infty}(F)$ of $\{f(a,\Omega), f(a,f(a,\Omega)), \dots\}$ is nothing else than :

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

Let us finally note that $M^{\infty}(F)$ is the free complete F-magma, that is :

**Proposition 4 :** For every complete F-magma $M$ there exists a unique continuous morphism : $M^{\infty}(F) \to M$.

We denote $T_M$ the image of $T \in M^{\infty}(F)$ under this morphism. In fact $T_M = j_M^{\infty}(T)$ (where $j_M$ is the canonical morphism : $M(F) \to M$ of proposition 1).

We will also use the obvious notion of *sub-ordered-F-magma*. In particular, any ordered F-magma $M$ contains a least sub-ordered-F-magma. Its domain is $B_M = \{t_M/t \in M(F)\}$. If $M$ is complete there is also a least complete sub-F-magma. Its domain is $\{\text{Sup}(\Delta)/\Delta \text{ is a directed subset of } B_M\}$.

### 3. Program schemes and their interpretation.

Let $F$ and $V$ be as in section 2. Let $\Phi$ be a finite ranked alphabet, $\Phi = \{\phi_1, \dots, \phi_n\}$. A *recursive program scheme* is a set of equations of the form :

$$ \Sigma \left\{ \begin{array}{l} \phi_i(v_1, \dots, v_{k_i}) = t_i, \\ 1 \le i \le n, \quad k_i = \rho(\phi_i), \quad t_i \in M(Fu\phi uV_{k_i}). \end{array} \right. $$

Intuitively, elements of $F$ are *base function symbols*, including a possibly infinite number of *constant symbols*, elements of $V$ are *formal parameters*, elements of $\Phi$ are *function variables* (i.e. *function procedure names*) ; each $t_i$ is the *body* of the corresponding procedure.

An *interpretation* for such a scheme is a complete F-magma.

We now define the function computed by $u \in M(Fu\phi v_k)$ in some interpretation $I$ with respect to program scheme $\Sigma$. It is a function : $D_I^k + D_I$ denoted $Val_{\Sigma,I}(u)$. It can be defined in several different ways.

(1) **By fixed-point** : it is well-known (see Milner [9]) that the interpretation of $\Sigma$ in $I$ is a system of functional equations in the variables $\phi_1, \dots, \phi_n$ which has a least solution $\langle \phi_1^k, \dots, \phi_n^k \rangle$ where $\phi_i^k : D_I^k \to D_I^k$, $\phi_n^k : D_I^k \to D_I$. Then, the definition of $Val_{\Sigma,I}(u)$ immediately follows with $\phi_i$ interpreted by $\phi_i^k$ for $1 \le i \le n$.

(2) **By Algol's copy-rule (Nivat [10])** : To $\Sigma$ defined as above we associate the tree grammar :

$$ \Sigma_{\Omega} \left\{ \begin{array}{l} \phi_i(v_1, \dots, v_{k_i}) = t_i + \Omega \\ 1 \le i \le n \end{array} \right. $$

The derivation relation $\to_{\Sigma_{\Omega}} \subset M(Fu\phi uV)^2$ is defined by :

$s \to_{\Sigma_{\Omega}} s'$ iff $s = \alpha \phi_i(u_1, \dots, u_{k_i}) \beta$ for some $\beta, \alpha \in (Fu\phi u(\cdot, \cdot), uV)^*$, $u_1, \dots, u_{k_i} \in M(Fu\phi uV)$ and $s' = \alpha t_i[u_1, \dots, u_{k_i}] \beta$ or $s' = \alpha \Omega \beta$. Let $L(u, \Sigma_{\Omega}) = \{u \in M(F)uV \mid u^* \to_{\Sigma_{\Omega}} u'\}$.

**Lemma 1 (Nivat [10])** : $L(u, \Sigma_{\Omega})$ is directed w.r.t. $\prec$.

Let us note also that for any interpretation $I$ and $\bar{d} \in D_I^k$, the mapping $u \mapsto u_I(\bar{d})$ defined from $M(F, v_k)$ into $D_I$ is increasing. It follows that $\{u_I(\bar{d}) / u' \in L(u, \Sigma_{\Omega})\}$ is directed. We take $Val_{\Sigma,I}(u)(\bar{d})$ to be its least upper bound. In fact our two definitions of $Val_{\Sigma,I}(u)$ give the same result (Nivat [10]).
**Example 3** : Let $\Sigma$ be the following :

$$ \phi(v_1, v_2) = h(v_1, v_2, v_1, \phi(f(v_1, v_2), v_2)) $$

Let I be the interpretation such that :

$$ \left\{ \begin{array}{ll} D_I = \mathbb{N} \cup \{\perp\} & \\ d \leq_I d' \text{ iff } d = \perp \text{ or } d = d' \text{ (this condition defines the notion of \underline{discrete} interpretation. See [5])} & \\ h_I(d,d',d'') = d & \text{if } d < d' \text{ and } d, d' \neq \perp \\ & = d'' \text{ if } d \geq d' \text{ and } d, d' \neq \perp \\ & = \perp \text{ otherwise} \\ f_I(d,d') = d - d' & \text{if } d' \leq d \text{ and } d, d' \neq \perp \\ & = \perp \text{ otherwise} \end{array} \right. $$

Then with $u = \phi(v_1, v_2)$ we get :

$$ L(u, \Sigma_{\Omega}) = \{\Omega, h(v_1, v_2, \Omega), h(v_1, v_2, h(f(v_1, v_2), v_2, \Omega)), \dots \} $$

Then $Val_{\Sigma, I}(u)(d, d')$ (the remaining of the euclidian division of $d$ by $d'$) is for $d = 7$ and $d' = 5$ :

$$ \text{Sup}(\perp, h_I(7,5,\perp), h_I(7,5,h_I(f_I(7,5),5,\perp)), \dots) = \text{Sup}\{\perp,\perp,2,2,\dots\} = 2. $$

In order to facilitate the algebraic formulation of our results we will only consider program schemes $(u, \Sigma)$ such that $u \in M(Fu\Phi)$, i.e. which compute a value and not a function. This means that we give a **name** to each input value for a program ; this is not a restriction since we can put in $F$ an infinite number of constants.

On the other hand this allows us to express conveniently some restrictions which naturally occur. For instance, in the case of $D_I = \mathbb{R}$, the set of real numbers a data can only be :

(1) a rational number defined by a pair of integers, or

(2) a finite decimal (or binary) approximation of a real number, or

(3) the result of another program (e.g. $\sqrt{2}$ or $\pi$).

Hence a formalization of the real numbers as an interpretation should use a countable set of constants denoting rational numbers and rational intervals.

Using this assumption, we get for $u \in M(Fu\Phi)$ : (see Thatcher, Goguen [6]).

**Proposition 5** : $Val_{\Sigma, I}(u) = [Val_{\Sigma, M^{\infty}(F)}(u)]_I$

**Proof** : For $u \in M(F)$, an easy induction shows that $u_{M^{\infty}(F)} = u$. Hence

$$ \begin{aligned} \text{Val}_{\Sigma, I}(u) &= \text{Sup}\{u'_I / u' \in L(u, \Sigma_{\Omega})\} \\ &= [\text{Sup}\{u' / u' \in L(u, \Sigma_{\Omega})\}]_I \\ &= [\text{Sup}\{u_{M^{\infty}(F)}' / u' \in L(u, \Sigma_{\Omega})\}]_I \\ &= [\text{Val}_{\Sigma, M^{\infty}(F)}]_I. \quad \Box \end{aligned} $$

**Comments** : $Val_{\Sigma, M^{\infty}(F)}(u)$ is the **symbolic evaluation** of $u$. This element of $M^{\infty}(F)$ contains all the necessary information to compute $Val_{\Sigma, I}(u)$. From now on we will give definitions relative to elements of $M^{\infty}(F)$ and not to recursive program schemes although certain elements of $M^{\infty}(F)$ are not associated to program schemes. But this will simplify our formulation without loss of generality at the present state of our work.

We now consider special kinds of interpretations derived from Scott's definition of an algebraic domain ; we use extra conditions relative to base functions.

**Definition** (adapted from Birkoff [1] and Scott [11]) : Let $<D, \leq_S>$ be a complete partial order. An element $d \in D$ is **isolated** if for every directed subset $\Delta$ of $D$, $d \leq_S \text{Sup}(\Delta)$ iff $d \leq_S d'$ for some $d' \in \Delta$. Let $B \subseteq D$. The c.p.o. $<D, \leq_S>$ is **algebraic with base B** if each element of B is isolated and each $d \in D$ is $\text{Sup}(\Delta)$ for some directed subset $\Delta$ of B. Let I be an interpretation and $B_I = \{d \in D_I / d = t_I \text{ for some } t \in M(F)\}$. Then I is **algebraic** iff $<D_I, \leq_S>$ is algebraic with base $B_I$.
**Comments** : The concept of an algebraic interpretation gives a special rôle to $B_I$, the set of elements which can be computed by finite programs working on admissible data ; if such an element is computed by an infinite program the computation only needs a finite number of steps. As an example, $\mathbb{R}$ is not an algebraic interpretation since $2 = 1.99999...$, (a finite element is a proper limit of finite elements); $M^\infty(\mathbb{F})$ and the discrete interpretation of example 3 are algebraic.

We get the following characterization :

**Theorem 1** : An interpretation is algebraic iff it is isomorphic to $[M(F)/\pi]^{\infty}$ for some $F$-magma preorder $\pi$.

**Proof** : Let $I$ be algebraic and $\pi$ be the binary relation on $M(F)$ defined by $t_{I} \leq t'_{I}$ iff $t_{I} \in t'_{I}$. This relation is clearly a magma preorder. There exists a unique homomorphism $\mu^{\infty} : [M(F)/\pi]^{\infty} \to I$ such that the following diagram commutes (see proposition 2 and 3) :

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

By definition of $\pi$, the morphism $\mu$ is one-to-one and its image is $B_I$. It follows that $\mu^{\infty}$ is onto : let $d \in D_I$, then $d = \text{Sup}(\Delta)$ for some directed subset of $B_I$ ; hence $\mu^{-1}(\Delta)$ is directed and $d = \mu^{\infty}(\text{Sup}(\mu^{-1}(\Delta)))$.

Let now $\Delta$ and $\Delta' \in [M(F)/\pi]^{\infty}$ and $\mu^{\infty}(\Delta) = \mu^{\infty}(\Delta')$ that is $\text{Sup}(\mu(\Delta)) = \text{Sup}(\mu(\Delta'))$. Since $\mu(\Delta)$ and $\mu(\Delta')$ consist of isolated points, for every $d \in \mu(\Delta)$, there exists $d' \in \mu(\Delta')$ s.t. $d \leq_I d'$ hence for every $\delta \in \Delta$, there exists $\delta' \in \Delta'$ s.t. $\delta \leq \pi \delta'$ and conversely. Since $\Delta$ and $\Delta'$ are ideals, $\Delta = \Delta'$. Hence $\mu^{\infty}$ is an isomorphism. $\square$

## 4. Families of interpretations.

Two program schemes $(u, \Sigma)$ and $(u', \Sigma')$ are equivalent if $\text{Val}_{\Sigma, I}(u) = \text{Val}_{\Sigma', I}(u')$ for every interpretation $I$. But this relation is too restrictive to be of practical interest. In general, the equivalence of two schemes in every interpretation satisfying certain conditions (e.g. associativity of a given base function) is to be considered.

Hence, from now on we will relativize our definitions to families of interpretations. We call class or family a set $C$ of interpretations (in some fixed universe of set-theory). Recall that we have decided to consider elements of $M^\infty(\mathbb{F})$ as program schemes. Hence we define for $T, T' \in M^\infty(\mathbb{F})$ :

$$T \leq_C T' \text{ iff } T_I \leq T'_{I} \text{ for all } I \in C$$

$$\text{and } T \cong_C T' \text{ iff } T_I = T'_{I} \text{ for all } I \in C, \text{ iff } T \leq_C T' \text{ and } T' \leq_C T.$$

**Definition** : Let $C$ be a family of interpretations. An interpretation $U$ (which need not belong to $C$) is C-universal if for every $I \in C$ there exists a unique continuous morphism $\phi_I : U \to I$ and C-Herbrand if for every $T, T' \in M^\infty(\mathbb{F})$, $T \leq_C T'$ iff $T_U \leq T'_{U}$.

**Remarks** : (1) If $U$ is C-universal, $I \in C$ and $T \in M^\infty(\mathbb{F})$ then $T_I = \phi_I(T_U)$.

(2) The term C-initial could be used instead of C-universal (cf Thatcher, Goguen [6]) but it suggests that $U \in C$. It is important not to require so : see [2].

**Proposition 6** : If $U$ is C-universal and $U \in C$ then $U$ is C-Herbrand.

**Proof** : $T_U \leq T'_{U}$ implies $T_I \leq T'_{I}$ for every $I \in C$ by the previous remark and $T \leq_C T'$ implies $T_U \leq T'_{U}$ since $U \in C$. $\square$

**Proposition 7** : Let $I$ be the class of all interpretations. Then $M^\infty(\mathbb{F})$ is an $I$-universal and $I$-Herbrand interpretation.
**Proof** : Clear from propositions 6 and 4. $\square$

**Remark** : We call $M^{\mathbb{N}}(F)$ an **Herbrand** interpretation since it is constructed in a purely syntactical way. Its main property becomes a definition when relativized to a specific class of interpretations.

Quite clearly, it may be easier to study the equivalence between programs under a **single** interpretation than under a **class** of interpretations. As an illustration of this, one can prove (using $M^{\mathbb{N}}(F)$) that the equivalence of recursive program schemes (under all interpretations) is a decision problem which is interreducible with the equivalence problem of DPDA's (Courcelle [3]). But in fact a C-Herbrand interpretation can be no more informative than C itself as shown by the construction of the following proposition.

**Proposition 8** : For any class C of interpretations, there exists a C-universal and C-Herbrand interpretation.

**Proof** : Let $K = \Pi\{I/\IcC\}$ be the infinite product of the elements of C. Its domain is $\Pi\{D_I/\IcC\}$ component-wise ordered. We leave the reader check that K is a complete F-magma. Let $K_O$ be the minimal complete sub-F-magma of K. It is clear that $D_{K_O} = \{d \in D_K/d = \text{Sup}(\Delta) \text{ for some directed } \Delta \subset B_K\}$ where $B_K = \{t_K/t \in M(F)\}$. For every $T \in M^{\mathbb{N}}(F)$, $T_{K_O} = (T_I)_I \in C$ hence $T_{K_O} \le T'_K$ iff $T_I \le T'_I$ for all $I \in C$. For every $I \in C$ the projection on $I$, $p_I : K_O \to I$ is a continuous morphism. Let $q : K_O \to I$ be any continuous morphism. For any $d = t_K \in B_K$, we must have $q(t_K) = t_I = p_I(t_K)$ (easy induction on $t$). By continuity we must have $q = p_I$ every where in $D_{K_O}$. $\square$

**Algebraic families**

**Definition** : A family C of interpretations is **algebraic** if for all $t \in M(F)$ and $T' \in M^{\mathbb{N}}(F)$ :

$t \le_C T'$ iff $t \le_C t'$ and $t' \not\le T'$ for some $t' \in M(F)$.

**Comments** : 1) The "if" part is satisfied for any class C of interpretations.

2) If I is algebraic, then $\{I\}$ is an algebraic class of interpretations.

3) Algebraic classes of interpretations are called nice in [2] and [5]. The present terminology is justified by the previous remark and theorem 2 below.

4) A class C is algebraic iff the canonical mapping $M^{\mathbb{N}}(F) \to M^{\mathbb{N}}(F)/\mathcal{S}_C$ is continuous.

5) If T is the infinite tree associated to a recursive program scheme, $t \in M(F)$ and $t \not\le T$ then t represents a finite partial computation of the program scheme.

More precisely if $\Sigma$ is a recursive program scheme, $u \in M(Fu\Phi)$ and $T = T(u, \Sigma)$ then $T = \text{Sup}\{w^{(n)}/n \ge 0\}$ where $w^{(n)} \in M(F)$ is the Kleene's sequence of $(u, \Sigma)$ (see Nivat [10]). It is (informally) defined by :

$- u^{(0)} = u$

$- u^{(n+1)}$ is obtained from $u^{(n)}$ by the simultaneous substitution of each procedure function symbol by the corresponding body,

$- w^{(n)}$ is obtained from $u^{(n)}$ by the simultaneous substitution of each procedure function symbol by $\Omega$.

Then for schemes $(u, \Sigma)$ and $(u', \Sigma')$ (with Kleene's sequences $w^{(n)}$ and $w'^{(n)}$) and an algebraic family C :
$$ u \equiv_C u' \text{ iff } \forall n \exists m (w^{(n)} \le_C w'^{(m)}) \text{ and } \forall n \exists m (w'^{(n)} \le_C w^{(m)}). $$

We now state and prove our main theorem.

**Theorem 2** : The following properties of a family C of interpretations are equivalent :

1) C is algebraic,

2) the interpretation $[M(F)/\mathcal{S}_C]^{\mathbb{N}}$ is C-Herbrand,

3) there exists an algebraic C-Herbrand interpretation.

**Proof** : 2 implies 3 by theorem 1. Assume now that H is an algebraic C-Herbrand interpretation. Let $t \in M(F)$ and $T' \in M^{\mathbb{N}}(F)$ such that $t \le_C T'$; then $t_H \le T'_H = \text{Sup}\{t'_H/t' \in M(F) \text{ and } t' \not\le T'\}$. Since H is algebraic $t_H \le t'_H$ for some finite $t' \not\le T'$. Then $t \le_C t'$ since H is C-Herbrand. We have proved that 3 implies 1.
Let $C$ be an arbitrary family of interpretations and $H$ be the interpretation $[M(F)/\varsigma_C]^\infty$. Then $H$ is $C$-universal by the following commutative diagram where each morphism is unique (and $I \in C$):

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

It follows that $T_H \le T'_H$ implies $T_I \le T'_I$ for every $I \in C$ hence $T \le_C T'$.

We now assume that $C$ is algebraic. Let $t \in M(F)$; then $t_H = [t]_{\equiv_C}^\infty$ by induction. Let now $T, T' \in M^\infty(F)$ such that $T \le_C T'$. Then for any $t \in M(F)$, if $t \not\le T$ there exists $t'$ $T'$ such that $t' \in M(F)$ and $t \le_C t'$; hence

$t_H = [t]_{\equiv_C} \le [t']_{\equiv_C} = t'_H$. It follows that $T_H \le T'_H$.

We have proved that $H$ is $C$-Herbrand if $C$ is algebraic, which completes the proof. $\square$

We now consider the important case of classes of interpretations which are defined by relations on finite terms.

Let $R_k$ be a possibly infinite binary relation on $M(F, V_k)$ and $R = \bigcup_{k \ge 1} R_k$. Let $C_R$ be the class of interpretations $I$ such that for all $(t, t') \in R$, if $t$ and $t'$ belong to $M(F, V_k)$ then for all $d_1, \dots, d_k \in D_I$, $t_I(d_1, \dots, d_k) \le_I t'_I(d_1, \dots, d_k)$. We now aim to characterize algebraically the relation $\le_C$.

Let $\mathcal{R}$ be the least magma preorder on $M(F)$ containing $\mathcal{R}$ and such that for all $t_1, \dots, t_k \in M(F), (u, u') \in R_k$ implies $u[t_1, \dots, t_k] \le_{\mathcal{R}} u'[t_1, \dots, t_k]$. Let $\equiv_{\mathcal{R}}$ be the associated equivalence relation.

**Lemma 2** : For $t, t' \in M(F)$, $t \le_R t'$ implies $t \le_{C_R} t'$.

**Proof** : Standard. $\square$

**Theorem 2** :

1) For $t, t' \in M(F)$, $t \le_{C_R} t'$ iff $t \not\le_R t'$.

2) $C_R$ is an algebraic family; its Herbrand interpretation $[M(F)/\mathcal{R}]^\infty$ belongs to $C_R$.

**Proof** : We prove first that the interpretation $H = [M(F)/\mathcal{R}]^\infty$ belongs to $C_R$.

Let $(u, u') \in R_k$. We must prove that for all $d_1, \dots, d_k \in D_H$, $u_H(d_1, \dots, d_k) \le u'_H(d_1, \dots, d_k)$. It is clearly sufficient to prove this for $d_1, \dots, d_k \in M(F)/\equiv_R$; the general case follows by the continuity of $u_H$ and $u'_H$. Hence, let $d_i = [s_i]_{\equiv_R}^\infty$ for $i \le k$. Then $w_H(d_1, \dots, d_k) = [w[s_1, \dots, s_k]]_{\equiv_R}^\infty$ for $w \in M(F, V_k)$ (by induction on $w$; the details are left to the reader), and $u[s_1, \dots, s_k] \mathcal{R} u'[s_1, \dots, s_k]$ (definition of $\mathcal{R}$); hence $u_H(d_1, \dots, d_k) \le u'_H(d_1, \dots, d_k)$. $\square$

We now prove that $H$ is $C_R$-universal.

Let $I \in C_R$ and consider the following diagram :

<figure><img src="image_7.png" /></figure>
The existence of $\mu$ follows from lemma 2. The morphisms are unique and the diagram is commutative. Hence $H$ is $C_R$-Herbrand by proposition 6. The class $C_R$ is algebraic by theorem 2. Finally, for $t, t' \in M(F)$, $t \le_C t'$ iff $t_H = [t]_{\equiv_R} \le t'_{H} = [t']_{\equiv_R}$ iff $t \prec_R t'$. $\square$

**Remark 1:** This theorem is stated without proof in [5] and proved in [4].

There also exist interesting classes which are algebraic without being of the form $C_R$ for any $R$: the class $D$ of discrete interpretations [5] and the class $SD$ of stable discrete ones (Berry, Courcelle [2]).

We prove now a negative result : the family of interpretations where two given programs are equivalent is not algebraic.

**Proposition 9:** There exist recursive schemes $(u, \Sigma)$ and $(u', \Sigma')$ such that :

1) $T(u, \Sigma) \prec T(u', \Sigma')$,

2) $C = (I/\text{Val}_{\Sigma,I}(u) = \text{Val}_{\Sigma',I}(u'))$ is not algebraic,

3) $C \cap D$ is not algebraic.

**Proof:** Let $\Sigma$ and $\Sigma'$ be the following schemes :

$$ \Sigma = \left\{ \begin{array}{l} u = \phi(a) \\ \phi(v_1) = f(v_1, \Omega, \phi(h(v_1))) \end{array} \right. \quad \text{and} $$

$$ \Sigma' = \left\{ \begin{array}{l} u' = \psi(a,a) \\ \psi(v_1,v_2) = f(v_1,v_2,\psi(h(v_1),k(v_2))) \end{array} \right. $$

The corresponding infinite trees are :

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

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

Hence, $T(u, \Sigma) \prec T(u', \Sigma')$.

Let $D'$ be the family of discrete interpretations such that :

(1) $f_I(x,y,z) = \underline{\text{if}} p_I(x) \underline{\text{or}} q_I(y) \underline{\text{then}} a_I \underline{\text{else}} z$ for all $x,y,z \in D_I$ where $p_I$ and $q_I$ are predicates, i.e. monotone functions from $D_I$ to the discrete domain $B = \{\perp, \text{True}, \text{False}\}$, where

$$ \left\{ \begin{array}{l} \underline{\text{True}} \text{ or } d = \underline{\text{True}} \quad \text{for all } d \in B, \\ d \text{ or } \underline{\text{True}} = \underline{\text{True}} \quad \text{for all } d \in B, \\ \underline{\text{False}} \text{ or } \underline{\text{False}} = \underline{\text{False}}, \\ d \text{ or } d' = \perp \quad \text{otherwise,} \end{array} \right. $$

(2) $h \in \mathbb{N}$ such that $p_I(h^1_I(a_I)) = \underline{\text{True}}$

(3) $h \in \mathbb{N}$ such that $q_I(k^1_I(a_I)) = \underline{\text{True}}$

Just looking at $T(u, \Sigma)$ and $T(u', \Sigma')$ we can see that for all $I \in D'$, $T(u, \Sigma)_I = T(u', \Sigma')_I = a_I$ hence, $D' \subseteq C = \{I/T(u,\Sigma)_I = T(u',\Sigma')_I\}$.

We now prove that any class of interpretations $C'$ such that $D' \subseteq C' \subseteq C$ is not algebraic which clearly implies 2) and 3). Let $w^{(n)}$ and $w'^{(n)}$ be the Kleene's sequence of $u$ and $u'$ that is :
$$
\begin{array}{l}
\begin{array}{l}
w^{(n)} = t^{(n)}[a] \quad \text{where} \\
t^{(0)} = f(v_1, \Omega, \Omega) \\
t^{(n+1)} = f(v_1, \Omega, t^{(n)}[h(v_1)]) \quad \text{and} \\
w^{(n)} = t^{(n)}[a, a] \\
t^{(0)} = f(v_1, v_2, \Omega) \\
t^{(n+1)} = f(v_1, \dot{v}_2, t^{(n)}[h(v_1), k(v_2)])
\end{array} \\
\\
\begin{array}{l}
\text{Assume now that some } C' \text{ s.t. } D' \subseteq C' \subseteq C \text{ is algebraic. Then } T(u, \Sigma) \stackrel{\sim}{=} C' \text{, } T(u', \Sigma') \text{ and } \forall n \text{ s.t. } w^{(n)} \subseteq C' \text{, } w^{(m)}. \\
\text{But for all } m \text{ and } n \text{ we can find } I \text{ in } D' \text{ such that } [w^{(m)}]_I = \perp \text{ and } [w^{(n)}]_I = a_I \text{; it suffices that} \\
P_I(h_I^i(a_I)) = \underline{\text{False}} \quad \text{for all } 0 \le i \le \max(m, n), \\
q_I(k_I^i(a_I)) = \underline{\text{False}} \quad \text{for all } 0 \le i < n, \\
q_I(k_I^n(a_I)) = \underline{\text{True}}.
\end{array}
\end{array}
$$

$$P_I(h_I^i(a_I)) = \underline{\text{False}} \quad \text{for all } 0 \le i \le \max(m,n),$$

$$q_I(k_I^i(a_I)) = \underline{\text{False}} \quad \text{for all } 0 \le i < n,$$

$$q_I(k_I^n(a_I)) = \underline{\text{True}}.$$

Hence a contradiction. []

The family of example 2 also is non-algebraic.

**Acknowledgements** : We thank I. Guessarian whose work contains many of the ideas developed here, W.P. de Roever for comments on a previous paper (he drew our attention on the link between Guessarian's "nice" families of interpretations and Scott's algebraic domains), and G. Berry for helpful criticisms on previous versions of this paper.

REFERENCES :

[1] G. Birkhoff, "Lattice Theory", American Math. Soc. 3rd edition, 1967.

[2] G. Berry, B. Courcelle, "Program Equivalence and Canonical Forms in Stable Discrete Interpretations", in Proc. of 3rd colloquium on Automata, Languages and Programming, Edinburgh, (1976).

[3] B. Courcelle, "Recursive Schemes, Algebraic Trees and Deterministic Languages", 15th S.W.A.T., New-Orleans 1974, pp 52-62.

[4] I. Guessarian, "Equivalences Sémantiques et Familles d'Interpretations", Thèse d'Etat, Université Paris 7, (1975).

[5] I. Guessarian, "Semantic Equivalence of Program schemes and its syntactic characterisation", 3rd Symp. on Automata, Languages and Programming, Edinburgh, (1976).

[6] J.A. Goguen, J.W. Thatcher, "Initial Algebra Semantics", 15th S.W.A.T., New-Orleans, 1974, pp 63-77.

[7] Z. Manna, S. Ness, J. Vuillemin, "Inductive Methods for proving properties of Programs", (1971), Memo Stanford AIM-154-CS-243.

[8] G. Markowsky, B. Rosen, "Bases for Chain-Complete Posets", 16th Ann. Symp. on Foundations of Computer Science, Berkeley (1975) pp. 34-47.

[9] R. Milner, "Models of LCF", Memo Stanford (1973).

[10] M. Nivat, "On the Interpretation of Polyadic Recursive Schemes", Symp. Mathematica Vol 15, (1975), Academic Press

[11] D. Scott, "Outline of a Mathematical Theory of Computation", Memo Oxford PRG2, (1972).