Iw: 03318 RR253

IRIA
laboria

Institut de Recherche
d'Informatique
et d'Automatique

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

laboratoire de recherche
en informatique
et automatique

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

ON SOME CLASSES
OF INTERPRETATIONS

Bruno COURCELLE
Irène GUESSARIAN

Rapport de Recherche N° 253

September 1977

48p.
# ON SOME CLASSES OF INTERPRETATIONS

Bruno COURCELLE

IRIA / LABORIA

Irène GUESSARIAN

Laboratoire Informatique Théorique et Programmation, Paris

**Résumé:**

On associe à chaque classe d'interprétations une relation d'équivalence sur l'ensemble des schémas de programmes. Notre but est de relier les propriétés de cette équivalence à la définition de la classe par des conditions de logique ou de théorie des ordres. Nous examinons en particulier l'algébricité d'une classe. Cette propriété est nécessaire pour l'existence de preuve par induction sur la longueur des calculs des équivalences valides entre schémas de programmes (relativement à la classe). Certaines classes définies par des conditions logiques du premier ordre sont algébriques.

**Abstract:**

An equivalence on recursive program schemes is associated with a class of interpretations. We aim to relate the properties of that equivalence with the definition of the class by logical and/or order-theoretical conditions. In particular we investigate the algebraicity of a class. This property is necessary for the existence of a proof by induction on the length of computation of the equivalence of recursive program schemes with respect to the class. Certain classes defined by first order logical conditions are proved to be algebraic.

<figure><img src="image_2.png" /></figure>
# I - INTRODUCTION

The equivalence between programs is an essential concept in the mathematical theory of computation and programming. That a program is correct, that a program transformation (for example [6]) 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 these difficulties as much as possible.

A program $P$ is splitted 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 \rightarrow D_I$ for each k-ary base function symbol). We denote by $\phi_I$ the function computed by $\phi$ under $I$ i.e. the function computed by the program $P$.

We only consider in this paper recursive program schemes without assignments. The corresponding schemes have no interpreted base functions. The conditional operator `if ... then ... else ...` is replaced by a 3-adic symbol `h(..., ..., ...)` which can be interpreted by an arbitrary 3-adic function.

The corresponding equivalence relation on schémes, namely $\phi \equiv \phi'$ iff $\phi_I = \phi'_I$ for every interpretation $I$, is very restrictive, and does not help very much for the study of interesting equivalences between real programs. (See exemple 2.2 below).

In order to get more concrete results, we use the notion of a *class of interpretations C* ; the associated equivalence between program schemes is then :
$\phi \equiv_C \phi' \text{ iff } \phi_I = \phi'_I \text{ for every } I \in C$

A similar concept has been introduced by other authors. In [6] a system is described which uses pairs of program schemes which are equivalent under conditions, i.e. with respect to a certain class of interpretations.

In [7] a program scheme is given with a first-order formula $\phi$ and one only considers interpretations which validate $\phi$. The order $\le_I$ of an interpretation is extended to functions as usual and still denoted $\le_I$.

We also define $\phi \le_C \phi'$ iff $\phi_I \le_I \phi'_I$ for all $I \in C$.

Clearly $\phi \equiv_C \phi$ if $\phi \le_C \phi'$ and $\phi' \le_C \phi$.

Let $\phi$ be a R.P.S. (i.e. a recursive program scheme), let $I$ be an interpretation and for each positive integer $n$ let $\phi_I^{(n)}$ be the approximation of $\phi_I$ which can be computed with at most $n$ nested recursive calls. This function can be defined by a finite term (written with base function symbols only) which we denote by $\phi^{(n)}$.

Let $\phi$ and $\phi'$ be R.P.S's, let $C$ be a class of interpretations such that,

$$ (1) \quad \forall n \exists m \forall I \in C, \phi_I^{(n)} \le_I \phi_I^{(m)} $$

equivalently,

$$ (2) \quad \forall n \exists m, \phi^{(n)} \le_C \phi^{(m)}; $$

then, since $\phi_I$ is the least upper bound of the $\phi_I^{(n)}$'s, we obtain that :

$$ (3) \quad \forall I \in C, \phi_I \le_I \phi'_I $$

or equivalently :

$$ (4) \quad \phi \le_C \phi' $$
This situation precisely occurs when (4) is provable by induction on the computation [15]. Many induction principles (including "Scott's induction principle") reduce to that one. An actual proof requires that, for every $n$,

$$ \exists m, \phi^{(n+1)} \leq_C \phi^{(m)} $$

can be deduced from :

$$ \exists m, \phi^{(n)} \leq_C \phi^{(m)} $$

which may be technically difficult to prove. But the main point for us is whether (2) holds or not.

A class $C$ of interpretations is *algebraic* if for every two RPS's $\phi$ and $\phi'$, (4) implies (2). Hence, for an algebraic class of interpretations $C$, it is reasonable to search for proofs by induction on the computation.

A *relational class* (i.e. the class of all interpretations which satisfy a given set of inequalities of the form $t \le t'$ for finite terms $t$ and $t'$) is a typical example of algebraic class (see [10], [12], and [9]).

Let us consider an example of a non-algebraic class :

**Example 1.1** : Let $C$ be the class of interpretations of the form

$I = \langle D_I, \le_I, \perp_I, p_I, f_I, h_I, a_I, b_I \rangle$ such that

1. $D_I$ contains the truth values *true*, *false*

2. $p_I$ is a continuous mapping : $D_I \to \{\perp, \textcolor{blue}{\underline{true}}, \textcolor{red}{\underline{false}}\}$, and $\forall m, p_I(f_I^m(a_I)) \neq \perp$

3. $h_I(x,y,z) = \textcolor{blue}{\underline{if}} x \textcolor{red}{\underline{then}} y \textcolor{blue}{\underline{else}} z$

4. $\exists n \in \mathbb{N}$ such that $p_I(f_I^n(a_I)) = \textcolor{blue}{\underline{true}}$
$$ \begin{cases} \phi = \psi(a) \\ \psi(v_1) = h(p(v_1), b, \psi(f(v_1))). \end{cases} $$

One is easily convinced that $\phi \equiv_C b$, that $\phi^{(n)} \le_C b$ holds (and can be proved by induction on $n$) but $b \le_C \phi^{(n)}$ does not hold for any $n$. Hence $b \le_C \phi$ cannot be proved by induction on the computation. An ad hoc proof by induction on the integer $n$ of condition 2 above is possible but is not of a great theoretical interest. ☐

It is often possible to prove a valid equation $\phi_I = \phi_I'$ by an induction "on the domain". If $D_I = \bigcup_{n \in N} D_I^{(n)}$, it suffices to prove by induction on $n$ that for all $n \in N$:

$$ Vd_1, \dots, d_k \in D_I^{(n)}, \phi_I(d_1, \dots, d_k) = \phi_I'(d_1, \dots, d_k). $$

This is called a structural induction in [5].

But such a proof is only valid for one interpretation. On the other hand, proofs by induction on the computation, which only use relations between base functions, are valid for every interpretation which satisfies those relations hence is of more general interest.

Hence, in this approach, the relevant questions about a given family $C$ of interpretations are the following ones:

(1) Is it algebraic ?

(2) If it is, find some characterization of $t \le_C t'$ (for finite terms $t$ and $t'$).

This characterization should be semi-decidable if we want any application to program proofs. For example, a relational class $C$ is algebraic
$\le_C$ is semi-decidable and axiomatized by a formal system (see [10])
but its negation is not semi-decidable in general (since the word
problem is undecidable). On the other hand, $\le_D$ (where $D$ is the class
of discrete interpretations, see [3] and definition 2.2 below) is
decidable but no good characterization is yet known.

This paper examines these questions for classes of interpretations
defined by order theoretical and/or first-order logical conditions.

Our main results are the following ones :

1. The preorder $\le_F$ associated with the class $F$ of finite interpretations coincides with $\le_J$ ($J$ is the class of all interpretations) and $\not\le$ (the syntactic ordering).

2. The class $D$ is algebraic and $\le_D$ is decidable on $M(F)$. An algorithm is provided (see also [3]).

3. Classes of interpretations which are models of first-order theories have bounded increasing chains and are algebraic. They include the class $D(R)$ of discrete interpretations which satisfy a certain set $R$ of inequations between finite terms, and classes of interpretations usually used in schematology.

4. The intersection of an algebraic class with a relational class is not necessarily algebraic.
Preliminary versions of certain of these results can be found in
[13], [3] and [9].

We thank G.Berry, J.C. Raoult and M. Nivat for their helpful comments
and many stimulating discussions.
## 2 - PRELIMINARIES

We review quickly some basic facts and fix our notations. More details can be found in [10] or [11].

Let $F$ be a finite set of function symbols with arity $(f \in F)$ has arity $\rho(f) \ge 0$) which contains a special symbol $\Omega$ of arity 0. Let $V_k = \{v_1, \dots, v_k\}$ for $k \ge 1$ and $V = V_K$ (for some fixed large enough $K$) be the set of variables.

Let $M(F,V)$ denote the set of finite well formed terms written on $F \cup V$ according to arities. This set is ordered by $\prec$, the least order relation such that:

(1) $\Omega \prec t$ for any $t \in M(F,V)$

(2) $f(t_1, \dots, t_k) \prec f(t'_1, \dots, t'_k)$ if $t_i \prec t'_i$ for $i = 1, \dots, k$

A recursive program scheme is a system 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, k_i = \rho(\phi_i), t_i \in M(F \cup \Phi, V_{k_i}) \end{array} \right. $$

where $\Phi = \{\phi_1, \dots, \phi_n\}$ is the set of function variables.

We usually consider $\phi_1$ as the "main program", i.e. the function computed by $\Sigma$ with help of $\phi_2, \dots, \phi_n$ as auxiliary functions.
In order to define the semantics we introduce the context-free tree grammar $\Sigma_{\Omega}$ associated with $\Sigma$ (see [10], [11], [16])

$$ \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. $$

and we take $\phi_1(v_1, \dots, v_{k_1})$ as *axiom*, then $L(\Sigma_{\Omega}, \phi_1)$ is the tree language generated.

**Lemma 2.1** (Nivat [16]) : $L(\Sigma_{\Omega}, \phi_1)$ is directed w.r.t. $\prec$.

Let us recall that a subset $\Delta$ of $D$ is *directed w.r.t. some order relation* $\le$ on $D$ if :

$$ \forall d, d' \in \Delta, \exists d'' \in \Delta, d \le d'' \text{ and } d' \le d'' $$

An element of $L(\Sigma_{\Omega}, \phi_1)$ is a finite term which represents an approximation of the function computed by $\Sigma$. Lemma 2.1 means that every two approximations are compatible. We now define interpretations and semantics.

**Definition 2.1.** : An *interpretation* $I$ is an object

$I = \langle D_I, \le_I, \perp, \langle f_I \rangle_{f \in F} \rangle$ (also called a *complete ordered F-magma*) such that

1. $\le_I$ is a partial order with least element $\perp$ and $\perp = \Omega_I$.

2. for each k-ary $f \in F$, $f_I$ is an increasing mapping : $D_I^k \to D_I$.

3. every directed subset $\Delta$ of $D_I$ has a least upper bound $\text{Sup}(\Delta)$.
4. Each $f_I$ is continuous, i.e. $f_I(\text{Sup}(\Delta_I), \dots, \text{Sup}(\Delta_k)) = \text{Sup}(f_I(\Delta_1, \dots, \Delta_k))$ for directed $\Delta_1, \dots, \Delta_k \subset D_I$.

Every $t \in M(F,V)$ clearly defines a function $t_I : D_I^K \to D_I$ which is increasing and continuous.

The function computed by $(\Sigma, \phi_1)$ in $I$ is $(\Sigma, \phi_1)_I$ also denoted by $\phi_{I I}$ if there is no ambiguity, defined by :

$$ \phi_{I I}(d_1, \dots, d_K) = \operatorname{Sup} \{t_I(d_1, \dots, d_K) / t \in L(\Sigma, \phi_1)\} $$

This value does exist since the mapping $t \to t_I(d_1, \dots, d_K)$ is increasing and by lemma 1.

This semantics coincides with the classical definition by fixed-points used for instance in Milner [14]. See [10], [16] for the proof.

We now give an example of R.P.S. and interpretation.

**Exemple 2.1 : The integers as an interpretation.**

Let $N_\perp$ be the ordered set $\langle N \cup \{\perp\}, \subseteq \rangle$ where $\perp$ is a special symbol (not in $N$) and $\subseteq$ is the partial ordered defined by :

$$ n \subseteq m \text{ iff } n = \perp \text{ or } n = m $$

Intuitively, the value of an object is undefined (i.e. is $\perp$) or is completely known.

A partial mapping $\phi : N^k \to N$ will be considered as the increasing mapping $\phi_\perp : N_\perp^k \to N_\perp$ defined by
$\phi_{\perp}(n_1, \dots, n_k) = \phi(n_1, \dots, n_k)$ if $n_1, \dots, n_k \in N$ and $\phi(n_1, \dots, n_k)$ is defined,

$= \perp$ otherwise

But dealing in general with increasing mappings $N_{\perp}^k \to N_{\perp}$ instead of partial mapping $N^k \to N$ allows to consider mappings which have a value, even if some of their arguments are undefined (see below the example of the multiplication).

Let $F = \{p, m, t, z, a, b, \Omega\}$ with $\rho(p) = \rho(m) = \rho(t) = 2$, $\rho(z) = 3$, $\rho(a) = \rho(b) = \rho(\Omega) = 0$.

Then we make $N_{\perp}$ into an $F$-interpretation by defining :

$\bar{a} = 0, \bar{b} = 1$

$\bar{p}(n,n') = n + n'$ if $n, n' \neq \perp$

$\bar{t}(n,n') = 0$ if $n = 0$

$\bar{z}(n, n', n'') = n''$ if $n \in \{1,2,3,\dots\}$

Let $S(n,p) = \sum_{i=n}^{n+p} i^2$ for $n, p \in N$

It can be computed by the recursive definition :

$S(n,p) = \text{if } p = 0 \text{ then } n^2 \text{ else } n^2 + S(n+1, p-1)$
A corresponding recursive scheme is :

$$ \phi(v_1, v_2) = z(v_2, t(v_1, v_1), p(t(v_1, v_1), \phi(p(v_1, b), m(v_1, b))))) $$

But note that one could also use the following scheme :

$$ \theta(v_1) = z_1(v_1, c(t(v_1, v_1)), p(c(t(v_1, v_1)), \theta(f(v_1))))) $$

with the interpretation $N_⊥ \times N_⊥$ (with the component-wise ordering, $\bar{p} \times \bar{p}$ for $p, \bar{t} \times \bar{t}$ for $t$ etc.). The new symbols $z_1, c, f$ are interpreted as follows :

$$ \bar{c}((n_1, n_2)) = (n_1, 0) \quad \text{for all } n_1, n_2 $$

$$ \begin{align*} \bar{z}_1((n_1, n_2), u, u') &= u & \text{if } n_1 &= 0 \\ &= u' & \text{if } n_1 \in \{1, 2, 3, \dots\} \\ &= (\perp, \perp) & \text{if } n_1 &= \perp \\ & \text{(where } u, u' \in N_⊥ \times N_⊥) \end{align*} $$

$$ \begin{align*} \bar{f}((n_1, n_2)) &= (n_1 + 1, n_2 - 1) & \text{if } n_1, n_2 \in N \text{ and } n_2 \ge 1 \\ &= (\perp, \perp) & \text{otherwise} \end{align*} $$

Hence there is not a unique way to consider a recursive program as the pair of a RPS and an interpretation. This flexibility may be useful for practical purposes [6]. ☐

We now go back to definitions.

**Definition 2.2.** : An interpretation which is defined as $N_⊥$ by adding an undefined element to an unordered set is called a **discrete interpretation**. More precisely, an interpretation $I$ is discrete if $(D_I, \le_I)$ satisfies the following :
for all $d, d' \in D_I$, $d \le_I d'$ iff $d = \perp$ or $d = d'$.

We denote by $\mathcal{D}$ the class of all discrete interpretations (with respect to some ranked alphabet $F$).

**Definitions 2.3.**

Two R.P.S.'s $(\Sigma, \phi)$ and $(\Sigma', \phi')$ are said to be **strongly equivalent** if $\phi_I = \phi'_I$ for all interpretation $I$.

But this equivalence is too restrictive, so we will relativize it to **classes of interpretations**. Let $C$ be a class of interpretation, then $(\Sigma, \phi)$ and $(\Sigma', \phi')$ are **$C$-equivalent** if $\phi_I = \phi'_I$ for all $I \in C$. Similarly, we define **$C$-inclusion**: $\phi \le_C \phi'$ iff $\phi_I \le \phi'_I$ for all $I \in C$ and $\le_I$ also denotes the extension of $\le_I$ to functions, namely $f \le_I g$ iff $f(d_1, \dots, d_k) \le_I g(d_1, \dots, d_k)$ for all $d_1, \dots, d_k \in D_I$ (and $f, g : D_I^k \to D_I$).

**Example 2.2** : The function $S$ of example 2.1 can also be defined by the following recursive program :

$$S(n,p) = \text{ if } p = 0 \text{ then } n^2 \text{ else } (n+p)^2 + S(n,p-1)$$

and the corresponding RPS, to be interpreted in $N_\perp$:

$$\psi(v_1, v_2) = z(v_2, t(v_1, v_1), p(t(p(v_1, v_2), p(v_1, v_2)), \psi(v_1, m(v_2, b)))))$$

It is not difficult to see that $\phi$ is not equivalent to $\psi$. But $\phi_I = \psi_I$ for other interpretations than $N_\perp$. (For instance, with the same domain, $t$ may be arbitrarily interpreted and $\phi$ remains equivalent to $\psi$). $\square$

The topic of this paper is to study the relation $\le_C$ on RPS's induced by a class of interpretations $C$. But some further conventions will simplify our formulation.
1. We will only consider RPS's($\Sigma$, $\phi$) such that $\rho(\phi) = 0$. Hence $\phi_I$ is an element of $D_I$ and not a function. This is not a loss of generality. Let ($\Sigma$, $\phi$) with $\rho(\phi) = k$ and $I$ be an interpretation. Add the new constants $c_1, \dots, c_k$ to $F$, a new 0-ary function symbol $\phi'$ to $\Phi$, the equation $\phi' = \phi(c_1, \dots, c_k)$ to $\Sigma$. Instead of studying $\phi_I : D_I^k \to D_I$ we will study $\phi'_J$ where $J$ ranges over $\{<I, c_1, \dots, c_k> / c_i \in D_I\}$.

2. We denote by $M^{\infty}(F,V)$ the set of "infinite well formed" terms. They can be formally defined as least upper bounds of directed subsets of $M(F,V)$ or, more intuitively, as infinite trees.

**Example 1:** The least upper bound of

is

$$ \Delta = \{\Omega, f(v_1, \Omega), f(v_1, f(g(v_1), \Omega)), \dots\} $$

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

Hence, by lemma 1 there exists $T(\Sigma, \phi_1) = \text{Sup}(L(\Sigma, \phi_1))$ in $M^{\infty}(F,V)$. The semantics of $(\Sigma, \phi_1)$ is completely defined by $T(\Sigma, \phi_1)$. If $\rho(\phi_1) = 0$ then $T(\Sigma, \phi_1) \in M^{\infty}(F)$. For simplicity we will consider in this paper any element of $M^{\infty}(F)$ as defined by a R.P.S., i.e. we will give definitions relative to arbitrary elements of $M^{\infty}(F)$ and not to those which are associated with RPS's.

Note that every $T \in M^{\infty}(F)$ as a value $T_I$ in an interpretation $I$ defined by:

$$ T_I = \text{Sup} \{t_I / t \in M(F) \text{ and } t \prec_I T\}. $$
## Families of interpretations

We call family or class of interpretations a class of interpretations in the sense of set-theory.

Let $C$ be a class of interpretations. For $T, T' \in M^{\infty}(F)$ we define $T \preceq_C T'$ iff $T_I \preceq_I T'_I$ for all $I \in C$, and $T \equiv_C T'$ iff $T \preceq_C T'$ and $T' \preceq_C T$. Hence $(\Sigma, \phi_I)$ and $(\Sigma', \phi'_I)$ are $C$-equivalent iff $T(\Sigma, \phi_I) \equiv_C T(\Sigma', \phi'_I)$.

A class $C$ is *algebraic* (see [11] for a justification of the terminology) if for all $t \in M(F)$, and $T' \in M^{\infty}(F)$ then $t \preceq_C T'$, if and only if $t \preceq_C t'$ for some $t' \in M(F)$ such that $t' \prec T'$.

Let us first consider the class $J$ of all interpretations :

This class contains $M^{\infty}(F)$ as an interpretation, called the Herbrand interpretation which we denote by $H$.

**Theorem 2.1** ([11],[10]) : For $T, T' \in M^{\infty}(F)$, $T_H = T$ and the following properties are equivalent :

1. $T \prec T'$ (resp. $T = T'$)

2. $T_H \preceq_H T'_H$ (resp. $T_H = T'_H$)

3. $T \preceq_J T'$ (resp. $T \equiv_J T'$)

It follows that $J$ is algebraic.

Let $R$ be a possibly infinite subset of $M(F,V) \times M(F,V)$ and $C_R = \{I/I \text{ is an interpretation and } t_I \preceq_I t'_I \text{ for all } (t,t') \in R\}$. For example, the class of interpretations such that some binary function is commutative is of that form. $C_R$ is called a *relational class*.

**Proposition 2.1** ([11]) : Every relational class is algebraic.

In this paper, we will relate the properties of $\preceq_C$ (and in particular the algebraicity of $C$) with the definition of $C$ by logical and/or
order theoretical conditions.

The following proposition is an easy consequence of the definitions :

**Proposition 2.2 :** If C and C' are algebraic, C u C' is algebraic.

**Proof :** Let $t \leq_C U C'$, $T$ for $t \in M(F)$, $T \in M^{\infty}(F)$ then $t \leq_C T$ hence $t \leq_C t_1 < T$ for some $t_1 \in M(F)$ since C is algebraic. Similarly $t \leq_C t_2 < T$. Let $t_3$ be the least upper bound of $t_1$ and $t_2$ in M(F). Then $t_3 < T$, $t_1 \leq_C t_3$. Hence $t \leq_C t_3$. Similarly, $t \leq_{C'} t_3$ hence $t \leq_C U C'$, $t_3$. $\square$

Theorem 4.4 will show that $C \cap C'$ need not be algebraic. But theorem 4.3 defines a class B of algebraic families which is closed by intersection.
### 3 - SOME FAMILIES DEFINED BY ORDER-THEORETICAL CONDITIONS

The family $\mathcal{D}$ of discrete interpretations (definition 2.2) is typically defined by conditions on $(D_I, \le_I)$. We consider in this section various classes $\mathcal{C}$ similarly defined, compare the associated $\le_C$, consider their algebraicity and, finally, give an algorithm for deciding $\le_D$ on $M(F)^2$. With a partial order $(D, \le)$ we associate $\mathfrak{Ch}(D, \le)$, the set of countable increasing sequences of elements of $\mathcal{D}$, i.e. the set of $\delta = (d_n)_{n \in \mathbb{N}}$ such that $d_o \le d_1 \le \dots \le d_n \le \dots$. For $\delta \in \mathfrak{Ch}(D, \le)$ let $|\delta|$ be the cardinality of $\{d_o, d_1, \dots, d_n, \dots\}$. For an interpretation $I$, let $\mathfrak{Ch}(I) = \mathfrak{Ch}(D_I, \le_I)$.

We now define some families of interpretations.

Let $\mathcal{F}$ be the family of finite interpretations (i.e. of interpretations with a finite domain).

Let $C_n = \{I \in \mathcal{J} / \text{for all } \delta \in \mathfrak{Ch}(I), |\delta| \le n + 1\}$ for $n \ge 1$,

$$C_{\infty} = \bigoplus_{n \ge 1} C_n,$$

$$C_{\omega} = \{I \in \mathcal{J} / \text{for all } \delta \in \mathfrak{Ch}(I), |\delta| \text{ is finite}\}.$$

**Remarks 3.1** : $D = C_1$ and the cartesian product of $n$ discrete interpretations belongs to $C_n$ (see example 2.2).

We obtain the following strict hierarchy :

$$D = C_1 \subsetneq C_2 \subsetneq \dots \subsetneq C_n \subsetneq \dots \subsetneq C_{\infty} \subsetneq C_{\omega} \subsetneq \dots \subsetneq J$$
### Example 3.1:

Let $C$ be the class of interpretations, the domain of which is the set of subsets of some finite set, ordered by inclusion. Then $C \subseteq C_\omega$.

Consider the familiar algorithm for finding the non-terminals of a context-free grammar which generate a non empty language. One usually search for the least fixed point of

$$A = f_G(A)$$

where $A$ ranges over $P(N)$ the power set of $N$, the set of non terminals of $G$ and $f_G(A)$ is defined as $A \cup \{S \in N/S \supseteq_G u, u \in (X \cup A)\}$ ($X$ is the terminal alphabet). □

### Remark 3.2
For all $T \in \mathcal{M}^\infty(F)$ and $I \in C_\omega$ there exists $t \in M(F)$ such that $t \prec T$ and $t_I = T_I$. Hence, the value of a program can be obtained by a finite computation. This is not the case if one works with a **functional domain** (one cannot compute every value of a function in a finite amount of times) or even with real numbers (one can only compute an approximation of $\sqrt{2}$). Our study of these families of interpretations will use the following definition:

### Definition 3.1
An interpretation $I$ is a **subinterpretation** of an interpretation $I'$, denoted $I \underline{[} I'$ if the following conditions are satisfied:

(1) $D_I \subseteq D_{I'}$

(2) for all $d, d' \in D_I, d \leq_I d'$ if and only if $d \leq_{I'} d'$,

(3) $\Omega_I = \Omega_{I'}$,

(4) for every directed subset $\Delta$ of $D_I$, $\text{Sup}_I(\Delta) = \text{Sup}_{I'}(\Delta)$,

(5) for $\epsilon \in F$ with $\rho(f) = 0, f_I \leq_{I'} f_{I'}$,

(6) for $f \in F$ with $\rho(f) = k \geq 1$ and $d_1, \dots, d_k \in D_I, f_I(d_1, \dots, d_k) \leq_{I'} f_{I'}(d_1, \dots, d_k)$
**Definition 3.2** : Let $A \subseteq M(F)$. An interpretation $I$ is an $A$-subinterpretation of $I'$, which is denoted $I \llcorner_A I'$ if $I \llcorner I'$ and $t_I = t_{I'}$, for every $t \in A$.

Let us give a concrete example of this concept.

**Example 3.2** : Let $F$ be as in example 2.1 and $I = N_{\perp}$. Let $J = Z_{\perp}$ be the following discrete interpretation :

$$D_J = Z \cup \{\perp\}$$

$p_J, t_J, a_J, b_J$ are defined as $p_I, t_I, a_I, ...$ in example 2.1 respectively.

$$m_J(n,n') = n - n' \quad \text{if } n, n' \neq \perp$$

$= \perp$ otherwise

$$z_J(n,n',n'') = n' \quad \text{if } n \neq \perp \text{ and } n \le 0$$

$= n'' \quad \text{if } n \neq \perp \text{ and } n > 0$

$= \perp$ if $n = \perp$

In this definition $\le$ and $>$ denote the usual ordering of $Z$. It is clear that $N_{\perp} \llcorner Z_{\perp}$. $\square$

The proof of the following lemma is left to the reader.

**Lemma 3.1** : Let $I \llcorner I'$ and $T \in M^{\infty}(F)$. Then $T_I \leq_{I'} T_{I'}$.

We now state and prove a technical lemma about $\llcorner_A$.

By using the following definitions and notations :

For $A \subseteq M(F)$, and $I \in \mathcal{J}$, $A_I$ denotes $\{t_I/t \in A\}$.

For $t \in M(F)$, $\text{Sub}(t)$ is the set of subterms of $t$ which is inductively defined by :

$$\text{Sub}(f) = \{f\} \quad \text{if } \rho(f) = 0$$
$$ \mathrm{Sub}(f(t_1, \dots, t_k)) = \{f(t_1, \dots, t_k)\} \cup \bigoplus_{1 \le i \le k} \mathrm{Sub}(t_i) $$

$$ \text{For } A \subset \mathcal{M}(\mathcal{F}), \mathrm{Sub}(A) = \bigoplus_{t \in A} \mathrm{Sub}(t). $$

We finally introduce a technical definition : let D be ordered by $\le$;
a subset D' of D is a good subset if every $\Delta \subseteq D'$ which is bounded
in D has a least upper bound in $(D', \le)$ which is also its least upper
bound in $(D, \le)$.

**Lemma 3.2** : Let A be a finite subset of M(F) such that :

$$ (1) \quad \mathrm{Sub}(A) \subseteq A \quad \text{and} \quad \Omega \in A $$

and I be an interpretation such that :

$$ (2) \quad A_I \text{ is a good subset of } D_I \text{ with respect to } \le_I. $$

There exists a finite A-subinterpretation J of I which is minimal with
respect to $\llcorner_A$, i.e. $J \llcorner_A I$ for all interpretation I' such that $I' \llcorner_A I$.

**Proof** : Let $D_J = A_I$, $\Omega_J = \Omega_I$ and $\le_J$ is the restriction of $\le_I$ to $D_J$.

Since $D_J$ is finite, for a directed $\Delta \subseteq D_J$, there exists $d \in \Delta$ such that $d = \mathrm{Sup}_I(\Delta)$. Clearly $d = \mathrm{Sup}_J(\Delta)$ and (4) of definition 3.1 is satisfied. Let us now define the $f_J$'s.

For a nullary $f \in \mathcal{F}$ let :

$$ \begin{aligned} f_J &= f_I && \text{if } f \in A, \\ &= \perp && \text{otherwise.} \end{aligned} $$

For a k-ary $f \in \mathcal{F}$ and $d_1, \dots, d_k \in D_J$ let $B$ be the set of $t \in A$ such that, for some $t_1, \dots, t_k \in A$ the following holds :
(i) $t \preceq f(t_1, \dots, t_k)$

(ii) $t_{nI} \le d_n$ for $n = 1, 2, \dots, k$

It is clear that $B_I$ is bounded by $f_I(d_1, \dots, d_k)$ hence we can define $f_J(d_1, \dots, d_k) = \sup_J(B_I)$ and $f_J(d_1, \dots, d_k) \le \sup_I f_I(d_1, \dots, d_k)$ by hypothesis (2). (Note that $B$ always contains $\Omega$). The case of nullary $f$'s is a special case of this one but we have displayed it separately for purpose of clarity.
We must show that the $f_J$'s are monotone. Let $d_1 \le d'_1, \dots, d_k \le d'_k$ and $B$, $B'$ associated with $(d_1, \dots, d_k)$ and $(d'_1, \dots, d'_k)$ respectively as above.
Obviously $B \subseteq B'$ hence $\sup_J(B_I) \le \sup_J(B'_I)$ and $f_J(d_1, \dots, d_k) \le f_J(d'_1, \dots, d'_k)$.
Since $D_J$ is finite, continuity follows from monotonicity. Hence $J$ is a finite interpretation.

Conditions (5) and (6) of definition 3.1 obviously hold : hence $J \subseteq I$.
If $t_1, \dots, t_k \in A$, $f(t_1, \dots, t_k) \in A$, and $t_{1I} = t_{1J} = d_1, \dots, t_{kI} = t_{kJ} = d_k$ then $f_J(d_1, \dots, d_k) = f_I(d_1, \dots, d_k)$. It follows that $t_I = t_J$ for all $t \in A$ by an obvious inductive argument. Hence $J \subseteq I$.

We now consider the minimality property of $J$. Let $I' \subseteq I$. Then $D_I$ must contain $A_I = D_J$. Let us verify (6) of definition 3.1. Let $d_1, \dots, d_k \in D_J$, $t_1, \dots, t_k \in A$ such that $t_{nI} \le d_n$ for $n = 1, \dots, k$ and $t \in A$ such that $t \preceq f(t_1, \dots, t_k)$. Then :

$$ 
\begin{align*} 
t_I &= t_{I'} \quad \text{since } I' \subseteq I \text{ and } t \in A, \\ 
&\le f_{I'}(t_{1I'}, \dots, t_{kI'}), \\ 
&= f_{I'}(t_{1I}, \dots, t_{kI}) \quad \text{since } I' \subseteq I \text{ and } t_1, \dots, t_k \in A, \\ 
&\le f_I(d_1, \dots, d_k). 
\end{align*} 
$$

Hence $f_J(d_1, \dots, d_k)$ which is the least upper bound of all such $t_I$'s is certainly less than $f_I(d_1, \dots, d_k)$.
The other verifications are left to the reader. [ ]

Example 3.3 below will prove that hypothesis (2) cannot be removed.

Two families of interpretations $C$ and $C'$ are equivalent if $\le_C$ and $\le_{C'}$ are the same (denoted $C \stackrel{\sim}{\approx} C'$).

We denote $C \stackrel{\sim}{\le} C'$ if $T\le_C T'$ implies $T \le_{C'} T'$ for all $T, T' \in M^\infty(F)$.

**Theorem 3.1 :** $F \stackrel{\sim}{\approx} C_\infty \stackrel{\sim}{\approx} C_\omega \stackrel{\sim}{\approx} J$.

**Proof :**

We denote $M_n(F)$ the set finite terms having no branch (in the tree representation) longer than $n$.

Since $F \subseteq C_\infty \subseteq C_\omega \subseteq J$ we obtain $F \stackrel{\sim}{\le} C_\infty \stackrel{\sim}{\le} C_\omega \stackrel{\sim}{\le} J$. We need only prove that $J \stackrel{\sim}{\le} F$. Let $t \in M(F)$ and $T' \in M^\infty(F)$ such that $t \not\le_J T'$ hence $t_H \not\le_{T'} t$ and $t \not\le_{T'} T'$ by theorem 2.1.

Two cases can occur :

(i) $T'$ is finite, $T' \not\le t$ and $T' \ne t$,

(ii) for some $t' \in M(F)$, $t' \not\le T'$ and for no $t'' \in M(F)$ $t \not\le t''$ and $t' \not\le t''$.

Let $A_o = \{t\}$ in case (i) and $A_o = \{t, t'\}$ in case (ii).
There exists an integer $n$ such that $A_o \subseteq M_n(F)$. It is fairly obvious
that $M_n(F)$ is a good subset of $(M(F), \prec)$. Let us take $A = M_n(F)$
(it is finite).

Let $H$ be the Herbrand interpretation of theorem 2.1. Since $u_H = u$
for every $u \in M(F)$ the pair $(A,H)$ verifies the hypotheses of lemma 3.2.
Let $J$ be the finite $A$-subinterpretation of $H$. In case (i) we get
$T'_J = T' \prec_J t_J = t$. In case (ii) we get $t' = t'_J \prec_J T'_J = t''$ for some
$t'' \in A_H$ such that $t' \prec t''$ but $t \not\prec t''$. Hence $t_J \not\prec_J T'_J$. In both cases we
obtain $t_J \not\prec_J T'_J$ for some $J \in F$ as desired. $\Box$

A different proof was given by J.C. Raoult (unpublished). This result
shows that $t \leq_F t'$ iff $t \prec t'$ for $t$ and $t' \in M(F)$. For recursive program
schemes $\phi$ and $\phi'$, $\phi \leq_F \phi'$ is undecidable since $\phi \leq_J \phi'$ is and
$\phi \equiv_F \phi'$ is equivalent to $\phi \equiv_J \phi'$. This last decision problem is equivalent
to the decision problem for DPDA's, hence open (Courcelle [8]). Similar
results hold for $\leq_{C_\infty}$ and $\leq_{C_\omega}$.

**Corollary 3.1.** : Each of $F, C_\infty, C_\omega$ is algebraic.

We now turn to discrete interpretations. We have already noted that
$D \stackrel{\sim}{\subset} J$, hence theorem 3.1 cannot be extended to $D$. For a family $C$ and
an integer $m$, we denote $C^{(m)} = \{I \in C / \text{Card}(D_I) \leq m \text{ and}$
$\text{Card}(\{x \in F_o \cup V_{x_I} \neq \emptyset\}) \leq m\}$.

**Lemma 3.3.** : Let $t \in M(F)$ and $m = |\text{Sub}(t)| + 1$. Then for every $T' \in M^\infty(F)$
$t \prec_D T'$ iff $t \leq_D (m') T'$.
**Proof** : Assume that $t \not\le_D T'$. Let $I \in D$ such that $t_I \not\le T'_I$ and $A = \text{Sub}(t) \cup \{\Omega\}$. Condition (2) of lemma 3.2 is trivially verified since $I$ is discrete hence we obtain an $A$-subinterpretation $J$ of $I$ such that $|D_J| \le m$; it is discrete since it is a subinterpretation of a discrete interpretation and $J \in D^{(m)}$. Now $t_J = t_I$ and $T'_J \le T'_I$. If $t_J \le T'_J$ then $t_J = t_I \le T'_I$ which contradicts the initial assumption. On the other hand $t \le_D T'$ implies $t \le_D (m) T'$. $\Box$

**Theorem 3.2.** : The family $D$ is algebraic and $t \le_D t'$ is decidable for $t, t' \in M(F)$.

**Proof** : Given $t$ and $t' \in M(F)$, one can compute the integer $m$ defined in lemma 3.3. and enumerate the finite class of finite interpretations $D^{(m)}$. For each $I \in D^{(m)}$ one can compute $t_I$ and $t'_I$ and check for inequality. Hence $t \le_D t'$ can be decided. The result of the test holds for $t \le_D t'$ by lemma 3.3.

Let now $T' \in M^\infty(F)$ with $t$ and $m$ as before. Assume that $t \le_D T'$. For each $I \in D^{(m)}$ there exists $t^{(I)} \in M(F)$ such that $t^{(I)} < T'$ and $T'_I = t_I^{(I)}$. The least upper bound $t'$ of $\{t^{(I)} | I \in D^{(m)}\}$ is finite since $D^{(m)}$ is finite, $t' < T'$ and, clearly, $t \le_D t'$ is decided. By lemma 3.3, $t \le_D t'$ and the algebraicity of $D$ is established. $\Box$

Before giving a test for $t \le_D t'$ (for $t, t' \in M(F)$) we give an example showing that lemma 3.2 does not extend to the classes $C_n$ and that (2) of lemma 3.2 could not be simply removed. However, it follows from a result of [13] that the classes $C_n$ are algebraic (see also theorem 4.2 below) and that $t \le_{C_n} t'$ is decidable for $t, t' \in M(F)$.
**Example 3.3.** : Let $F = \{f, \Omega, a, b\}$ with $\rho(f) = 2$, $\rho(a) = \rho(b) = \rho(\Omega) = 0$.

Let $I$ be the interpretation with domain $D = \{\perp, \alpha, \beta, \gamma_0, \gamma_1, \gamma_2\}$.

The order $\le$ is represented by the Hasse diagram of figure 3.1(a). Let $a_I = \alpha, b_I = \beta$, and $f_I$ be defined by the table of figure 3.1(b) (where $\gamma$ means any of $\gamma_0, \gamma_1, \gamma_2$).
<figure><img src="image_4.png" /><figcaption>(a)</figcaption></figure>

<table><caption>(c)</caption><thead><tr><th></th><th>⊥</th><th>α</th><th>β</th><th>γ<sub>i</sub></th></tr></thead><tbody><tr><th>⊥</th><td>⊥</td><td>⊥</td><td>β</td><td>β</td></tr><tr><th>α</th><td>α</td><td>α</td><td>γ<sub>i</sub></td><td>γ<sub>i</sub></td></tr><tr><th>β</th><td>⊥</td><td>⊥</td><td>β</td><td>β</td></tr><tr><th>γ<sub>i</sub></th><td>α</td><td>α</td><td>γ<sub>i</sub></td><td>γ<sub>i</sub></td></tr></tbody></table>

<table><caption>(b)</caption><thead><tr><th>2nd arg<br>1st arg</th><th>⊥</th><th>α</th><th>β</th><th>γ</th></tr></thead><tbody><tr><th>⊥</th><td>⊥</td><td>⊥</td><td>β</td><td>β</td></tr><tr><th>α</th><td>α</td><td>α</td><td>γ<sub>o</sub></td><td>γ<sub>o</sub></td></tr><tr><th>β</th><td>⊥</td><td>⊥</td><td>β</td><td>β</td></tr><tr><th>γ</th><td>α</td><td>α</td><td>γ<sub>o</sub></td><td>γ<sub>o</sub></td></tr></tbody></table>

<caption>Figure 3.1</caption>
Clearly, $I \in C_3$.

Let $A = \{\Omega, a, b, f(\Omega, b), f(a, \Omega)\}$.

For $i = 1,2$ let $J_i$ be the interpretation with domain $D_i = \{\perp, \alpha, \beta, \gamma_i\}$,
ordered by $\le_i = \le \cap (D_i \times D_i)$. Let $a_{J_i} = \alpha, b_{J_i} = \beta$ and $f_{J_i}$ be defined by
the table of figure 3.1(c). It is clear that $J_1$ $\underline{\underline{[}}_A I$ and $J_2$ $\underline{\underline{[}}_A I$. If
$J$ $\underline{\underline{[}}_A I$ and $J$ is minimal with respect to $\underline{\underline{[}}_A$ then $J$ $\underline{\underline{[}}_A J_1$, $J$ $\underline{\underline{[}}_A J_2$ and the
domain of $J$ must be $\{\perp, \alpha, \beta\}$. But $f_J(\alpha, \beta)$ should be greater than both
$f_J(\alpha, \perp) = [f(a, \Omega)]_J = \alpha$ and $f_J(\perp, \beta) = [f(\Omega, b)]_J = \beta$ but this cannot
hold since $\alpha \neq \beta$ and $\beta \neq \alpha$. $\square$

By a crude argument we have shown in theorem 3.2 that $t \le_D t'$ is deci-
dable for $t, t' \in M(F)$. We now sketch a usable algorithm.

Let $t, t' \in M(F)$ and $t \le_D t'$ to be tested. Let $A = \text{Sub}(t) \cup \{\Omega\} = \{\Omega, a_1, \dots, a_m\}$.
A consequence of the proof of lemma 3.3 is :

Fact 3.1 : $t \le_D t'$ if and only if $t \le_{D_A} t'$ where $D_A = \{I \in D/D_I = A_I$ and $I$ is minimal with respect to $\underline{\underline{[}}_A\}$.

The domain of any $I \in D_A$ can be described as the quotient-set
$A/\equiv_I$ (and $u \equiv_I u'$ if and only if $u_I = u'_I$ for $u, u' \in M(F)$).

Fact 3.2 : *An equivalence relation $E$ on $A$ is $\equiv_I$ for some $I \in D_A$ if and only if it satisfies the following :*

1. if $b_i \in \mathcal{R}_1$ for $i = 1, \dots, k$, $f(b_1, \dots, b_k) \in A$ and $f(c_1, \dots, c_k) \in A$ then $f(b_1, \dots, b_k) \in \mathcal{R}_2$
2. if $c_i \leq Rb_i$ and $c'_i \leq Rb'_i$ for $i = 1, \dots, k$, if $b, b' \in A$, $b \in \Omega$, $b' \in \Omega$ then $b < f(c'_1, \dots, c'_k)$ and $b' < f(c'_1, \dots, c'_k)$, where $R$ is the binary relation on $A$ defined by $b \leq R c$ if and only if $b \in \Omega$ or $b \in \Omega$ then $b' \in \Omega$.

We denote by $\mathbb{A}$ the set of such equivalence relations.

**Proof** : These conditions are clearly necessary from the properties of discrete interpretations. To prove the sufficiency we construct $I = I_E$ from $E$. Let $D_I = A/E$ ordered by $[c]_E \leq_I [b]_E$ if and only if $c \leq Rb$. Hence $\leq_I$ is a discrete order with $[\Omega]_E$ as least element.

We take $f_I([b_1], \dots, [b_k]) = [b]$ if $b < f(c_1, \dots, c_k)$, for some $b, c_1, \dots, c_k \in A$ such that $c_i \leq Rb_i$ for $i = 1, \dots, k$ and $b$ is not equivalent to $\Omega$.

$= [\Omega]$ otherwise.

Condition 2 implies that $f_I$ is well defined. It is clearly monotone (hence continuous). The minimality of $I$ with respect to $\mathbb{A}$ is left to the reader. []

It is possible to reduce $D_I$ once more.

Let $E, E' \in \mathbb{A}$; we define $E \ll E'$ if $E \subseteq E'$ and $[\Omega]_E = [\Omega]_{E'}$.

This means that $I_E'$ is obtained from $I_E$ by identifying certain elements of $I_E$ different from $\emptyset$.
Clearly, for $u, u' \in M(F)$, if $E \ll E'$ and $u_{I_E} \le u'_{I_E}$ then $u_{I_{E'}} \le u'_{I_{E'}}$ : there exists an homomorphism of interpretations i.e. a continuous homomorphism of $F$-magmas (see [10] and [11])

$\phi : I_E \to I_{E'}$, and $\phi(u_{I_E}) = u_{I_{E'}}$.

Let $E_A^{\min}$ be the set of elements of $E_A$ which are minimal with respect to $\ll$. Let $D_A^{\min} : \{I_E/E \in E_A^{\min}\}$. Hence:

**Fact 3.3** : $t \le_D t'$ if and only if $t \le_{D_A^{\min}} t'$.

We now show how to compute $D_A^{\min}$.

Let $B$ be a subset of $A$. Let $E(B)$ be the least equivalence (if any) on $A$ such that:

(i) $[\Omega]_E = B$,

(ii) if $b_i E b'_i$ for $i = 1, \dots, k$, $f(b_1, \dots, b_k) \in A$ and $f(b'_1, \dots, b'_k) \in A$ then $f(b_1, \dots, b_k) E f(b'_1, \dots, b'_k)$,

(iii) if $b_i R b'_i$ for $i = 1, \dots, k$, $f(b_1, \dots, b_k) \in A$ and $f(b'_1, \dots, b'_k) \in B$ then $f(b_1, \dots, b_k) \in B$,

(iv) if $c_i R b_i$ and $c'_i R b'_i$ for $i = 1, \dots, k$, if $b, b' \in A - B$ and $b \prec f(c_1, \dots, c_k)$ and $b' \prec f(c'_1, \dots, c'_k)$ then $b \in B$ and $b' \in A$ then $b \in B$.

It is not difficult to see that if there exists $E$ satisfying conditions (i) to (iv) there exists a minimal one with respect to $\subseteq$ i.e. to $\ll$ by condition (i). This equivalence, denoted by $E(B)$, can be constructed by successive applications of conditions (ii) and (iv). A failure occurs if an equivalence $b \in B$ and $c \in A - B$ (i.e. condition (i) is not satisfied), or if condition (iii) is not satisfied. This failure means that $E(B)$ does not exist.
If $E(B)$ can be obtained, then $E(B) \in E_A$ since under hypothesis (i), conditions (ii) to (iv) are equivalent to conditions 1 to 2 of fact 3.2. Hence $E(B) \in E_A^{\min}$. The interpretation $I_{E(B)}$ can be obtained from $E(B)$. Hence $I_{E(B)}^{\min} = \{I_{E(B)} / B \subseteq A\}$.

**Example 3.4** : An example will suggest a practical way of computing $I_{E(B)}^{\min}$ and some improvements.

Let $t = f(f(\Omega, f(x,\Omega)), \Omega)$ and $t' = f(\Omega, f(\Omega, f(f(x,\Omega),\Omega)))$.

Let us take $A = \{\Omega, x, a_1, a_2, t\}$ with

$a_1 = f(x, \Omega),$

$a_2 = f(\Omega, a_1),$

$t = f(a_2, \Omega).$

We arrange the different cases into a tree (see figure 3.2).
<figure><img src="image_5.png" /><figcaption>Figure 3.2</figcaption></figure>
Each branching represents an alternative for an element of A whether it is in B or not. Each rectangular box indicates the consequences of the previous choices via the conditions (ii) and (iv) above (we use $\equiv$ instead of $E$). As an example, $x \equiv \Omega$ and $a_1 \not\equiv \Omega$ imply $a_2 \equiv a_1$ and $t \equiv a_1$ by condition (iv). And similarly, $a_1 \equiv a_2$ follows from $x \not\equiv \Omega$ and $a_1 \not\equiv \Omega$ and $a_2 \not\equiv \Omega$.

To each leaf corresponds an element $\equiv$ of $E_A^{\min}$ and an interpretation $I_{\equiv} \in D_A^{\min}$. Note that if $t \equiv \Omega$, $t \le t'$ will certainly hold in $I_{\equiv}$ and there is nothing to do. In our example this case occurs at leafs 1,3,4,6. Let us consider the two other ones :

**Leaf 2 :** The domain of $I_{\equiv}$ is $\{[\Omega], [t]\} = \{\perp, \alpha\}$.

The constant $x$ has value $\perp$ and $f(\perp, \perp) = \alpha$. Clearly the value of $t'$ is $\alpha$ also.

**Leaf 7 :** The domain of $I_{\equiv}$ is $\{[\Omega], [x], [a_1]\} = \{\perp, \alpha, \beta\}$.

The constant $x$ has value $\alpha$, $f(\perp, \alpha) = \perp$, $f(\alpha, \perp) = f(\perp, \beta) = f(\beta, \perp) = \beta$ and the other values of $f$ are defined by monotonicity. It follows that $t'$ has value $\beta$.

Hence we have shown that $t \le_D t'$ and finally that $t \le_D t'$.
# 4 - FIRST-ORDER CLASSES OF INTERPRETATIONS

The family of all interpretations is the class of all models of a certain second-order theory. This is clear by the definition of an interpretation.

In fact second-order theories are very powerful and define algebraic as well as nonalgebraic classes (see proposition 4.1).

We will consider classes defined by *first-order conditions*.

Let $A$ be a set of first-order closed formulas on a set of function symbols including $F$ and a set of predicate symbols including $\le$. Let us define :

$\mathcal{Mod}(A)$ to be the class of models of $A$ (Schoenfield [18]).

$\mathcal{Int}(A) = \mathcal{J} \cap \mathcal{Mod}(A)$, the class of interpretations which are models of $A$.

Since $\mathcal{Int}(A)$ is not first-order definable, $\mathcal{Int}(A)$ need not be $\mathcal{Mod}(A')$ for any first-order theory $A'$.

**Definition 4.1** : A class of interpretations $C$ is *first-order* if $C = \mathcal{Mod}(A)$ for some first-order theory $A$.

**Example 4.1** : $D$ is a first-order family. In fact, conditions 1 and 2 of definition 2.1 are first-order. Let $A_0$ be a (finite) set of first-order formulas expressing them. Let $F_D$ be the following closed formula :

$$ \forall x \forall y [x \le y \Longleftrightarrow x = \Omega \text{ or } x = y], $$

and $A_D = A_0 \cup \{F_D\}$. It is fairly easy to prove that conditions 3 and 4 of definition 1 are implied by $A_D$ hence $D = \mathcal{Mod}(A_D)$.

For a first-order theory $A$, let $D(A) = D \cap \mathcal{Mod}(A)$. Then $D(A) = \mathcal{Mod}(A \cup A_D)$ hence is a first-order class.

Similarly, a closed formula $F_n$ can be constructed which expresses that every chain is of length $n+1$ at most. It follows that $C_n = \mathcal{Mod}(A_0 \cup \{F_n\})$.
For a first-order theory A we also introduce $C_n(A) = C_n \cap \text{Int}(A) = \text{Mod}(A_o \cup \{F_n\} \cup A)$.

We now state three results :

**Theorem 4.1.** : Every first-order class of interpretations is of the form $C_n(A)$ for some $n \in N$ and first-order theory A.

**Theorem 4.2.** : A first-order class of interpretations is algebraic.
These results should be contrasted with :

**Proposition 4.1** : For a first-order theory A, $\text{Int}(A)$ is not algebraic in general.

We give first an example proving proposition 4.1.

**Proof of proposition 4.1** :

Let $F = \{a, f\}$ with $\rho(a) = 0$ and $\rho(f) = 1$.

Let A consist of the following formula : $\forall x [f(x) = x \Longleftrightarrow a \le x]$

Let $T = \text{Sup} \{f^n(\Omega) / n \ge 0\}$ be the least fixed point of $f = f(x)$ in $M^\infty(F)$ and $C = \text{Int}(A)$. Then a $\le_C T$ follows from A since $f_I(T_I) = T_I$ in every interpretation $I \in C$. But there is no $n \in N$ such that $a \le_C f^n(\Omega)$. To see that, it suffices to take $I$ with $D_I = \{\perp, \alpha, \beta_1, \dots, \beta_m, \dots, \omega\}$ ordered as follows :

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

with $f_I(\perp) = f_I(\alpha) = \beta_1$, $f_I(\beta_i) = \beta_{i+1}$, $f_I(\omega) = \omega$ and $a_I = \alpha$. $\square$
**Proof of theorem 4.1** : Let $C = \text{Mod}(a) \subseteq J$. It suffices to prove that $C \subseteq C_n$ for some $n$. Let us assume the contrary and obtain a contradiction.

There exists a sequence $(I_n)_{n \ge 1}$ of elements of $C$ and for each $n$ a mapping $\theta_n : N \to D_{I_n}$ such that :

$$ \iota = \theta_n(0) < \theta_n(1) < \dots < \theta_n(n) \text{ and} $$

$$ \theta_n(i) = \theta_n(n) \quad \text{for } i \ge n $$

(where $<$ is the strict order of the interpretation $I_n$).

Let $U$ be a non trivial ultrafilter on $\{1,2,\dots\}$ and $I = \Pi I_n/U$ the ultraproduct of $(I_n)_{n \ge 1}$ associated with $U$. We will prove that $I$ is not an interpretation $(D_I$ is not complete) and obtain a contradiction since the class of models of a first-order theory is closed by ultraproducts.
(See [2]).

We briefly recall the definition of $I = \Pi I_n/U$. Let $\Pi I_n$ be the set of mappings $\rho \{1,2,\dots\} \to U D_{I_n}$ such that $\rho(i) \in D_{I_n}$ for $n \ge 1$. An equivalence relation with respect to $U$ is defined by $\rho \equiv \rho'$ (mod $U$) if and only if $\{i/\rho(i) = \rho'(i)\} \in U$. The class of $\rho$ is denoted $[\rho]_U$ and the domain $D_I$ of $I$ is $\{[\rho]_U / \rho \in \Pi I_n\}$. The ordering on $D_I$ is defined by $[\rho]_U \le [\rho']_U$ if and only if $\{i/\rho(i) \le \rho'(i)\} \in U$.

The mapping $f_I$ for a $k$-ary $f \in F$ is defined by

$$ f_I([\rho_1]_U, \dots, [\rho_k]_U) = [\rho]_U $$

where $\rho(n) = f_I(\rho_1(n), \dots, \rho_k(n))$ for $n \in \{1,2,\dots\}$.

Let $([\rho_n]_U)_{n \ge 0}$ be the sequence of elements of $D_I$ associated with the mappings $\rho_n : \{1,2,\dots\} \to U D_{I_n}$ such that :
$$ \rho_n(k) = \theta_k(n) \quad \text{for } n \ge 0, k \ge 1 $$

Let $n < m$. Then $\theta_k(n) < \theta_k(m)$ for $k \ge m$. It follows that $[\rho_n]_U < [\rho_m]_U$, hence we have defined a strictly increasing sequence.

This sequence is bounded by $[\delta]_U$ where :

$$ \delta(k) = \theta_k(k) \quad \text{for } k \ge 1 $$

since $\rho_n(k) = \theta_k(n) \le \theta_k(k) = \delta(k)$ for all $n$ and $k \ge n$.

Assume now that $[\mu]_U$ is the least upper bound of $([\rho_n]_U)_{n \ge 0}$.

Then $\mu(k) \le \theta_k(k)$ for all $k$ belonging to some $A$ in $U$. For all $k \in A$, let $j_k$ be the largest integer such that $j_k \le k$ and $\theta_k(j_k) < \mu(k)$. Let also $\mu'(k) = \theta_k(j_k)$ so that $[\mu']_U < [\mu]$ ($\mu'$ can be arbitrarily defined outside of $A$). If we prove that $[\rho_n]_U \le [\mu']$ for all $n$, we will prove that $[\mu]$ is not the least upper bound of $([\rho_n]_U)_{n \ge 0}$ and obtain a contradiction as desired. If

$$ \{k \in A / \rho_n(k) = \theta_k(n) \le \theta_k(j_k)\} \notin U $$

then

$$ B = \{k \in A / \theta_k(n) > \theta_k(j_k)\} \in U. $$

Now $\rho_{n+1}(k) = \theta_k(n+1) \le \mu(k)$ for all $k$ in some $A' \in U$ and $\theta_k(j_k) < \theta_k(n) < \theta_k(n+1) \le \mu(k)$ if $k \in B \cap A' \cap \{k/k \ge n+1\}$ (this set belongs to $U$ hence is not empty) but this contradicts the definition of $j_k$. Hence $[\rho_n]_U \le [\mu']$ and the contradiction is obtained. $\Box$
**Proof of theorem 4.2**: This proof will be based on the compactness theorem for first-order logic. Let $C = \text{Mod}(A') \subset J$.

Assume that $C$ is not algebraic, that $t' \in \text{M}(\mathcal{F})$ and

$T = \text{Sup}\{t_n/n = 0,1,...\} \in \mathbb{M}^{\infty}(\mathcal{F})$ with $t_0 < t_1 < t_2 < ... < t_n < ...$ such that :

(1) $t' \le_C T$,

(2) $t' \notin_C t_n$ for each $n$.

By (2), each of $A' \cup \{\lceil t' \le t_n \rceil\}$ has a model $I_n \in C$. In fact, $I_n$ is a model of $A' \cup \{\lceil t' \le t_0 \rceil, \lceil t' \le t_1 \rceil, ..., \lceil t' \le t_n \rceil\}$ since for each $i=0,...,n$, $t_i < t_n$; hence $t'_i \le t_{iI_n}$ would imply $t'_i \le t_{nI_n}$.

By the compactness theorem for first-order logic [18].

$A' \cup \{\lceil t' \le t_0 \rceil, \lceil t' \le t_1 \rceil, ..., \lceil t' \le t_n \rceil, ...\}$ has a model I. Hence $I \in \text{Mod}(A') = C$. By theorem 4.1 and remark 3.2 there exists $n$ such that $T_I = \lceil t_n \rceil_I$. Hence $t'_I \le \lceil t_n \rceil_I$ by hypothesis (1). But this contradicts the definition of I. []

As a first application, we consider classes of discrete interpretations with *interpreted conditionals*.

Let $F$ contain a special triadic symbol $h$, special constants *true* and *false* and a set of special functions called *predicate* symbols ($p, p', q, q', r, r'$ will be reserved to predicate symbols). The domain $D_I$ of an interpretation $I$ contains the truth values *true*$_I$ and *false*$_I$ which are assumed to be distinct and not $\perp$. For simplicity we will omit the subscript $I$.

Let $D_{\text{cond}}$ be the class of discrete interpretations satisfying the following conditions :

(1) *true* ≠ Ω and *false* ≠ Ω and *true* ≠ *false*.
(2) $\forall x_1, \dots, x_k [p(x_1, \dots, x_k) = \Omega \text{ or } p(x_1, \dots, x_k) = \underline{\text{true}} \text{ or } p(x_1, \dots, x_k) = \underline{\text{false}}] \text{ for each k-ary predicate } p.$

(3) $\forall x, y, z [x \neq \underline{\text{true}} \text{ and } x \neq \underline{\text{false}} \implies h(x,y,z) = \Omega]$

(4) $\forall x, y [h(\underline{\text{true}}, x, y) = x \text{ and } h(\underline{\text{false}}, x, y) = y]$

Then $D_{\text{cond}}$ is clearly first-order and

**Corollary 4.1 :** $D_{\text{cond}}$ is first-order and algebraic.

In fact most papers on program schemes use only interpretations of $D_{\text{cond}}$ with, possibly some extra conditions. Let us take $[1]$ as an example. A typical R.P.S. is

$$ \phi(x) = \underline{\text{if}} \ p(x) \ \underline{\text{then}} \ (\underline{\text{if}} \ q(x) \ \underline{\text{then}} \ f(x) \ \underline{\text{else}} \ \phi(g(\phi(x)))) \ \underline{\text{else}} \ x $$

An interpretation is some $I = <D, p_I, q_I, f_I, g_I>$ where $p_I, q_I$ are total functions : $D \to \{\underline{\text{true}}, \underline{\text{false}}\}$ and $f_I, g_I$ are total functions : $D \to D$
We write the same scheme :

$\phi(x) = h(p(x), h(q(x), f(x), \phi(g(\phi(x)))), x)$ and take the discrete interpretation :

$$ J = <D \cup \{\perp, \underline{\text{true}}, \underline{\text{false}}\}, \perp, \leq, p_J, q_J, f_J, g_J, h_J> $$

where $p_J(\perp) = p_J(\underline{\text{true}}) = p_J(\underline{\text{false}}) = \perp$

$p_J(d) = p_I(d) \text{ if } d \in D$

and similarly for $q_J, f_J, g_J$. The function $h_J$ is defined by (3) and (4) above. Clearly, $J \in D_{\text{cond}}$. The function $\phi_I$ (defined as in [1]) is related with $\phi_J$ by the following :

$\phi_J(d) = \phi_I(d) \quad \text{if } \phi_I(d) \text{ is defined}$

$\phi_J(d) = \perp \quad \text{if } d = \perp \text{ or } \phi_I(d) \text{ is undefined}$

We now consider discrete interpretations defined by relations.
Let $R \subset M(F,V) \times M(F,V)$ and $C_R$ be the relational class associated
with $R$ as defined in section 3. Let $D(R) = D \cap C_R$. Then $D(R) = D(A_R)$
where $A_R$ is the set of formulas

$$
\forall v_1, \dots, v_K [t \le t']
$$

for all $(t,t') \in R$. Let similarly $C_n(R) = C_n \cap C_R = C_n(A_R)$.

**Corollary 4.2 :** *For* $R \subset M(F,V)^2$, $n \in N$, $C_n(R)$ *and* $D(R)$ *are algebraic.*

This partially answers to a question of [12] . This result can be
slightly extended. Let B be the least family of classes of interpretations
which contains the relational classes (i.e. the C<sub>R</sub>'s), the first-order
classes (i.e. the C<sub>n</sub>(A)'s) and is closed by finite union and finite inter-
section. Then

**Theorem 4.3 :** Every *C* ∈ *B* is algebraic.

**Proof :** Let $C \in \mathcal{B}$. Then $C = \bigcup_{i=1}^{n} C_i$ where each $C_i$ is the form :

$$
C_{R_1} \cap C_{R_2} \cap \dots \cap C_{R_k} \cap C_{n_1} (A_1) \cap \dots \cap C_{n_\ell} (A_\ell)
$$

If $\ell = 0$ then $C_i = C_{R_1} \cup \dots \cup R_k$ is algebraic (proposition 1).

If $\ell \ge 1$ then $C_i = C_{R_1} \cup \dots \cup R_k \cap C_m(A_1) \cup \dots \cup A_\ell$ where

$$
m = \min \{n_1, \dots, n_\ell\}
$$

$$
= C_m(A_1 \cup \dots \cup A_\ell \cup A_{R_1} \cup \dots \cup R_k) \text{ and is algebraic by theorem}
$$

4.2. By proposition 2.2, C is algebraic. □

Intersection of algebraic classes

It is known from [12] that the algebraicity of classes is not preserved
under intersection. One could suspect that the algebraicity is preserved
by intersection with a relational class $C_R$ since this holds in two cases :

(1) $C_R' \cap C_R = C_R \cup R'$ (algebraic by proposition 2.1)

(2) $C_n \cap C_R = C_n(R)$ (algebraic by corollary 4.2)

This is not the case :

**Theorem 4.4.** : There exists an algebraic class of discrete interpretations $C$ and $R = \{(t, t')\}$ such that $C \cap C_R$ is not algebraic.

*Proof* : Let $F = \{f,g,a,b,\Omega\}$ with $\rho(f) = 2$, $\rho(g) = 1$, $\rho(a) = \rho(b) = 0$.

Let $A$ be the set of first order formulas consisting of :

$$F_0 : b \neq \Omega$$

$$F_1 : g(\Omega) = \Omega$$

$$F_{2,n} : g^n(a) \neq \Omega \quad \text{for } n = 0,1,2,...$$

$$F_3 : \forall x [f(\Omega,x) = \Omega]$$

$$F_4 : \forall x [x \neq \Omega \Rightarrow f(x,b) \neq \Omega]$$

Let $D_0 = D(A)$ and $C = \{I \in D_0 / [f(g^n(a), \Omega)]_I \neq \emptyset \text{ for some integer } n\}$.

The proof uses the following lemma which will be proved later :

**Lemma 4.1.** : $C \cong D_0$

This means that $\leq_C$ and $\leq_{D_0}$ are the same. Hence the class $D_0$ is algebraic by theorem 4.2 and so is $C$. Let $R = \{(f(v_1,b),b)\}$ and $C' = C \cap C_R$.
Hence $C'$ is the class of interpretations I of C satisfying :

$$
R : \forall d \in D_I, f_I(d, b_I) \le b_I
$$

which we will refer to in the sequel as condition R. We claim that C'
is not algebraic. Let T = T(Σ,φ) where Σ is following scheme :

$$
\sum \left\{
\begin{array}{l}
\phi = \psi(a) \\
\psi(v_1) = f(v_1, \psi(g(v_1)))
\end{array}
\right.
$$

Hence $T = \text{Sup}(t_n)$ where $t_n$ is

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

Technically, we define

$$
t_{n,n} = f(g^n(a), \Omega) \quad \text{for } n = 0, 1, 2, \dots \text{ and}
$$

$$
t_{n,m} = f(g^m(a), t_{n,m+1}) \quad \text{for } 0 \le m < n
$$

Hence $t_n = t_{n,0}$.

Let $I \in C'$ and $n$ such that $[t_{n,n}]_I \neq \emptyset$. Since $I$ is discrete,
$f(g^n(a),b)_I = [t_{n,n}]_I$ and the common value is $b_I$ by condition R. By
$F_4$ and $F_2$, $[t_{n,n-1}]_I \neq \emptyset$ and the value must be $b_I$ by condition R again.
By the same argument, we get that

$$b_I = [t_{n,n-1}]_I = [t_{n,n-2}]_I = \dots = [t_{n,0}]_I$$

Hence $b \equiv_C T$. If $C'$ is algebraic, there exists an integer $m$ such that $b \le_C t_m$. Let $n > m$ and $I$ be the following interpretation :

$$I = \langle D, \leq, \perp, f, g, \dots \rangle$$

$$D = \langle \perp, \alpha_0, \alpha_1, \alpha_2, \dots, \alpha_n, \beta \rangle$$

$$a_I = \alpha_0$$

$$b_I = \beta$$

$$g_I(\perp) = g_I(\beta) = \perp$$

$$g_I(\alpha_i) = \alpha_{i+1} \quad \text{if } 0 \le i < n$$

$$g_I(\alpha_n) = \alpha_n$$

$$f_I(d, d') = \beta \text{ if } d = \alpha_n \text{ or } (d \neq \perp \text{ and } d' = \beta), \\ = \perp \text{ otherwise}$$

A straight forward verification shows that $I \in C'$. In particular $t_{n,n} = \beta$ but $[t_{m,m}^I] = \perp$. Hence $[t_{m,m-1}^I] = f_I(g^{m-1}(a), t_{m,m}) = f_I(\alpha_{m-1}, \perp) = \perp$ and similarly $[t_{m,m-1}^I] = [t_{m,m-2}^I] = \dots = [t_{m,0}^I] = \perp$. Hence $b_I \notin [t_m^I]$ and $b \notin_C t_m$ : this shows that $C'$ is not algebraic. $\llcorner$

Before starting the proof of lemma 4.1, we describe a construction on interpretations which has been introduced in [3]. We redefine it in order to have a self-contained proof.

Let $I \in D_0$. We associate with $I$ a discrete interpretation $J$ which is defined as follows

$$D_J = \{ \langle d, t \rangle \in D_I \times M(F) / t_I = d \},$$

$$\perp_J = \langle \perp, \Omega \rangle,$$

$$a_J = \langle a_I, a \rangle ; b_J = \langle b_I, b \rangle$$
$$ g_J(<d,t>) = <\perp, \Omega> \quad \text{if } g_I(d) = \perp \\ = <g_I(d), g(t)> \quad \text{otherwise} $$

$$ f_J(<d_1,t_1>, <d_2,t_2>) = <\perp, \Omega> \quad \text{if } f_I(d_1,d_2) = \perp, \\ = <f(d_1,\perp), f(t_1,\Omega)> \quad \text{if } f_I(d_1,\perp) \neq \perp \\ = <f(d_1,d_2), f(t_1,t_2)> \quad \text{otherwise} $$

The interpretation J is in fact the *SD*-free interpretation associated with I of [3]. We denote it here by $F(I)$.

**Lemma 4.2 :** Let $t \in M(F)$

1. There exists $t' \in M(F)$ such that :

(α) $t_J = <t_I, t>'$

(β) $t_I = t_I'$

(γ) $t' \prec t$

2. $t_J = \perp_J$ if and only if $t_I = \perp_I$,

3. $t_J = g_I^n(a)_J$ if and only if $t = g_I^n(a)$.

**Proof :** We prove (1) by induction on t. If $t \in \{\Omega, a, b\}$ then (α), (β) and (γ) follow from the definition of J. Assume now that $t = g(u)$. If $g_I(u_I) = \perp$, then $t_J = <\perp, \Omega>$, this case is trivial. If $g_I(u_I) = t_I \neq \perp$, then $u_I \neq \perp_I$ by condition $F_I$ and $u_J = <u_I, u'>$ with $u' \prec u$ and $u'_I = u_I$. Then $t_J = <g_I(u_I), g(u')>$ and (α), (β), (γ) are satisfied. If $t = f(u_1, u_2)$ the proof is similar.

(2) The only if direction is obvious. The other one follows from the definition of J and (1).
(3) If $t_J = g_I^n(a)_J = \langle g_I^n(a) \rangle$, $g_I^n(a) > \langle t_J^n(a) \rangle$ then $g_I^n(a) \not\prec t$ by (1) and this implies $g_I^n(a) = t$. [ ]

**Lemma 4.3 :** *The interpretation J belongs to $D_0$. If $I \in C$ then $J \in C$.*

**Proof :** We only verify $F_4$. If $\langle d,u \rangle \in D_J - \{\langle \perp, \Omega \rangle\}$ then $f_I(d, b_I) = d' \neq \perp_I$ since $I \in D_0$. Then $b_J = \langle b_I, b \rangle$ and $f_J(\langle d, u \rangle, b_J) = \langle d', f(u, \Omega) \rangle$ if $f_I(d, \perp) \neq \perp$ (hence $f_I(d, \perp) = d'$)

= $\langle d', f(u,b) \rangle$ otherwise

by our definition of J.

If $f(g_I^n(a), \Omega)_I = d \neq \perp_I$, then $f(g_I^n(a), \Omega)_J = \langle d, f(g_I^n(a), \Omega) \rangle \neq \langle \perp, \Omega \rangle$.
Hence, if $I \in C$ then $J \in C$. [ ]

**Proof of lemma 4.1. :** In order to prove that $\leq_{D_0}$ and $\leq_C$ coincide on $M^\infty(F)$, we need only prove for all $t \in M(F)$ and $T' \in M^\infty(F)$, $t \leq_C T'$ iff $t \leq_{D_0} T'$. Since $C \subset D_0$ the if direction is trivial. We will prove that if $t_I \neq t_{I'}$ for some $I \in D_0$, then $t_J \neq t_{J'}$ for some $J \in C$ which will complete the proof.

**First case :** $t_I = d \neq \perp$ and $t_{I'} = t_I' = d' \notin \{\perp, d\}$ for some $t' \not\prec T'$. Let $n$ be a positive integer such that $g_I^n(a)$ is not a subterm of $t$ or $t'$. Let $I' = F(I)$ and $J = I(n)$ be the discrete interpretation defined as follows :

$$D_J = D_{I'}$$

$$\perp_J = \perp_{I'}$$

$$f_J(d_1, d_2) = f_I(d_1, d_2) \text{ if } d_1 \neq g_I^n(a)$$

$= \delta \text{ if } d_1 = g_I^n(a)$$

$D_J - \{\langle \perp, \Omega \rangle\}$
The verification that $f_J$ is increasing w.r.t. the discrete ordering
is left to the reader. It suffices to prove that $J$ is a discrete inter-
pretation. Furthermore, $J \in D_0$. We only verify that $F_4$ is satisfied, the
other verifications being similar. Let $d_I \in D_J - \{\perp_J\}$. If $d_I = g^n(a)_{I'}$,
then $f_J(d_I, b_I) = \delta \neq \perp_J$. If $d_I \neq g^n(a)_{I'}$, then $f_J(d_I, b_I) = f_{I'}(d_I, b_I) \neq \perp_J$
since $I' \in D_0$. Clearly $f(g^n(a), \Omega)_J = f_J(g^n(a_J), \perp) = f_J(g_{I'}^n(a_{I'}), \perp) = \delta \neq \perp_J$
hence $J \in C$.

Finally we prove that $t_J \neq \perp$ and $t'_J \neq t_J$.

Let $u \in M(F)$ such that :

(1) for every subterm $u'$ of $u$, $u_I^{t'} \neq g^n(a)_{I'}$.

An easy inductive argument shows that $u_J = u_{I'}$. By lemma 4.2,
$u_I^{t'} = g^n(a)_{I'}$, if and only if $u' = g^n(a)$, hence by our choice of
$n$, $t_J = t_{I'}$ and $t'_J = t_{I'}^t$. From the initial assumption that $t_I \neq t_I^{t'}$, we get
$t_{I'} \neq t_I^{t'}$ and $t_J \neq t'_J$. Similarly, $t_I \neq \perp$ implies $t_I \neq \perp$ and $t_J \neq \perp$. The
same holds for $t'$. Hence $t_J \not\perp t'_J$. Q.E.D.

**Second case :** Let $I \in D_0$ such that $t_I \neq \perp$ and $t_I^{t'} = \perp$ for all $t' \in M(F)$
such that $t' \not\prec T'$. We aim to define $J \in C$ such that $t_J \not\prec t'_J$. Choose an
integer $n$ such that $g^n(a)$ is not a subterm of $t$. Let $I(n)$ be associated
with $I$ and $n$ as in the first case. If $t_{I(n)}^{t'} = \perp$ for every $t' \not\prec T'$, then
we can take $J = I(n)$ and we are done since $t_{I(n)} \neq \perp$ as in the first
case. Otherwise, if $t_{I(n)}^{t'} \neq \perp$ for some $t' \not\prec T'$, let us take $J = F(I(n))$.
This interpretation belongs to $C$ since $I(n) \in C$ and by lemma 4.3.
Clearly, $t_J \neq \perp$ and $t'_J \neq \perp$. Let us prove that $t_J \neq t'_J$. Assume that
$t_J = t'_J = \langle d, u \rangle$ for some $d \in D_{I(n)}$ and $u \in M(F)$. By lemma 4.2, $u \prec t$
and $u$ has no subterm of the form $g^n(a)$ by our choice of $n$. Hence
$u_{I(n)} = u_{I'}$. Also $u \prec t'$ and $t_I^{t'} = \perp$. This implies $u_I = \perp$ and $u_{I'} = \perp$
(since $I' = F(I))$. Hence $d = u_{I(n)} = \perp$ by lemma 4.2 again, but $d = t_{I(n)}$
and we get a contradiction since $t_{I(n)} \neq \perp$, by the proof of the first case.
Hence we have proved that $t_J \not\prec t'_J$. $\square$
REFERENCES

[1] E. Ashcroft, Z. Manna, A. Pnueli "Decidable properties of monadic functional schemas", JACM Vol. 20 (1973) pp. 489-499.

[2] J. Bell, A. Slomson, "Models and Ultraproducts", North-Holland, London (1971)

[3] G. Berry, B. Courcelle, "Program Equivalence and Canonical forms in stable discrete interpretations", Proc. of 3rd colloquium on Automata, Languages and Programming, Edinburgh, (1976), pp. 168-188.

[4] G. Birkhoff, "Lattice Theory", American Mathematical Society, 3rd edition (1967), Providence.

[5] R. Burstall, "Proving properties of programs by structural induction", Comp. Journal (12) pp. 41-48.

[6] R. Burstall, J. Darlington, "A system which automatically improves programs", Proc. of 3rd Int. joint conf. artif. intelligence, S.R.I. (1973), pp. 537-542.

[7] A. Chandra, "Generalized program schemas", SIAM J. on computing Vol. 5 (1976), pp. 402-413.

[8] B. Courcelle "Recursive schemas algebraic trees and deterministic languages", Proc. of the 15th Symp. on Switching and Automata theory, New-Orléans, (1974), pp. 52-62.
[9] B. Courcelle, "On the definition of classes of interpretations", 4th ICALP, Turku (July 1977) and Laboria Report 231.

[10] B. Courcelle, I. Guessarian, M. Nivat, "The algebraic semantics of recursive program schemes", submitted for publication.

[11] B. Courcelle, M. Nivat, "Algebraic Families of interpretations", 17th symp. on F.O.C.S., Houston (1976) (also available as Laboria Report n° 189).

[12] I. Guessarian, "Semantic equivalence of program schemes", Proc. of 3rd coll. on Aut., Languages and Programming, Edinburgh (1976), pp. 189-200.

[13] I. Guessarian, "Equivalences Sémantiques et classes d'interprétations", Doctoral Dissertation, Paris (1976).

[14] R. Milner, "Models of LCF", Memo Stanford AIM-184 (1973).

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

[16] M. Nivat, "On the interpretation of polyadic recursive schemes", symp. Mathematica, vol. 15, Academic Press (1975).

[17] D. Park, "Finiteness is μ-ineffable", Report n° 3, Warwick University (1974).

[18] J.R. Schoenfield, "Mathematical Logic", Addison-Wesley (1967).