# On the definition of classes of interpretations

Bruno Courcelle

► To cite this version:

Bruno Courcelle. On the definition of classes of interpretations. [Research Report] IRIA-RR-231, IRIA. 1977, pp.17. hal-04716453

HAL Id: hal-04716453

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

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>
RIA
laboria

Institut de Recherche
d'Informatique
et d'Automatique

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

laboratoire de recherche
en informatique
et automatique

ON THE DEFINITION
OF
CLASSES OF INTERPRETATIONS

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

Bruno COURCELLE

Rapport de Recherche N° 231

Mai 1977
ON THE DEFINITION OF CLASSES OF INTERPRETATIONS

Bruno Courcelle

IRIA

Résumé :

Une classe d'interprétations C est algébrique si et seulement si (grosso modo), pour tout couple $\phi, \phi'$ de schémas de programmes récursifs C-equivalents, cette équivalence peut être prouvée par induction sur le calcul [9]. Les classes d'interprétations peuvent être définie par des conditions logiques et/ou de théorie des ordres. On examine ici plusieurs cas d'algébricité, en particulier si les classes sont définissables au premier ordre, et de non-algébricité.

Abstract :

A class C of interpretations is algebraic if, roughly speaking, for every two recursive program schemes $\phi$ and $\phi'$, the equivalence of $\phi$ and $\phi'$ with respect to C can be proved by an induction on the length of computation [9] if it holds. Classes of interpretations can be defined by logical, and/or order theoretical conditions. We examine several cases of algebraicity (for classes defined by first-order conditions) and non-algebraicity.

N.B. - Ce travail sera présenté au quatrième Colloque I.C.A.L.P., Turku (Finlande) Juillet 1977 et doit être cité comme tel.

N.B. - This work will be presented at 4th I.C.A.L.P., Turku (Finlande) July 1977 and should be so refered.
<figure><img src="image_3.png" /></figure>

# 1 - Introduction

The equivalence between programs is an essential concept in the mathematical theory of computation and programming, but 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 split into a program scheme $\phi$ (i.e. a program where the domain of computation and the base functions are left unspecified) and an interpretation I (i.e. the specification of a domain $D_I$ and a function $f_I = D_I^k \to D_I$ for each k-ary base function symbol). We denote by $\phi_I$ the function computed by $\phi$ 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 schemes, 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.

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 [3] 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 [14] 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, \quad \phi_I^{(n)} \le_I^{\phi'} \phi_I^{(m)} $$

equivalently,

$$ (2) \quad \forall n \exists m, \quad \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, \quad \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 [9]. 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)} \le_C \phi^{(m)} $$

can be deduced from:

$$ \exists m, \phi^{(n)} \le_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.

In nonalgebraic classes, other proofs are required.

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

$I = \langle D_I, \le_I, \perp, 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, true, false\}$, and $\forall m, p_I(f_I^m(a_I)) \neq \perp$

3. $h_I(x,y,z) = \text{if } x \text{ then } y \text{ else } z$

4. $\exists n \in \mathbb{N}$ such that $p_I(f_I^n(a_I)) = true$

(The reader is referred to the main text for the missing details).

Let $\Sigma$ be the following RPS :
$$ \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. $\square$

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 \mathbb{N}} D_I^{(n)}$, it suffices to prove by induction on $n$ that for all $n \in \mathbb{N}$:

$$ \forall d_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 [2].

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 are 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'$)

In this paper, we relate the algebraicity of classes of interpretations with their definition by logical conditions, properties of programs etc...

Our two main results are the following ones :

(1) a first-order class of discrete interpretations is algebraic (theorem 2),

(2) the intersection of an algebraic class with a relational class of interpretations is not necessarily algebraic (theorem 5).

## 2 - Recursive Program Schemes

We recall quickly a few basic notions. (See [4] and [10] for more details).

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 set of equations or a context-free tree grammar of the form :
$$ \sum_i \begin{cases} \phi_i(v_1, \dots, v_{k_i}) = t_i + \Omega \\ 1 \le i \le n, k_i = \rho(\phi_i), t_i \in M(F \cup \Phi, V_{k_i}) \end{cases} $$

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

Let $L(\Sigma, \phi_1) \subset M(F, V)$ be the tree language generated by $\Sigma$ with axiom $\phi_1(v_1, \dots, v_{k_1})$.

**Lemma 1 (Nivat [10]):** $L(\Sigma, \phi_1)$ is directed w.r.t. $\prec$.

In order to consider such systems as program schemes, we must define their semantics.

**Definition 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_I, \dots, \Delta_k))$ for directed $\Delta_I, \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$ if there is no ambiguity, defined by :

$$ \phi_I(d_1, \dots, d_K) = \text{Sup} \{ t_I(d_1, \dots, d_K) / t \in L(\Sigma, \phi_1) \} $$

This value does exist since the mapping $t \rightsquigarrow 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 [8]. See [13],[10] for the proof.

In fact 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 $\{ \langle I, c_1, \dots, c_k \rangle / c_i \in D_I \}$.
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:** The least upper bound of

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

<figure><img src="image_4.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.

### 3 - 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 \le_C T'$ iff $T_I \le_I T'_I$ for all $I \in C$, and $T \equiv_C T'$ iff $T \le_C T'$ and $T' \le_C T$. Hence $(\Sigma, \phi_1)$ and $(\Sigma', \phi'_1)$ are $C$-equivalent iff $T(\Sigma, \phi_1) \equiv_C T(\Sigma', \phi'_1)$.

A class $C$ is *algebraic* (see [4] for a justification of the terminology) if for all $t \in M(F)$, and $T' = \sup_{n \ge 0} (t_n') \in M^{\infty}(F)$ (where $t_n' \in M(F)$ for $n \ge 0$), $t \le_C T'$ iff $t \le_C t_n'$ for some $n$.

The class $I$ of all interpretations is algebraic since $\le_I$ is exactly $\prec_I$ (see [4], [13]). More generally, let $R$ be a possibly infinite subset of $M(F,V) \times M(F,V)$ and $C_R = \{I/I \mid I \text{ is an interpretation and } t_I \le_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 1** ([4]): Every relational class is algebraic

An interpretation $I$ is *discrete* if $(D_I, \le_I)$ satisfies the following :

$$ \forall x, y \in D_I, x \le_I y \iff x = \perp \text{ or } y = x. $$

Most concrete examples of R.P.S.'s use discrete interpretations. Many papers on recursive program schemes only consider discrete interpretations. See section 4 for a precise correspondance between these definitions and ours.

The family $D$ of discrete interpretations is proved to be algebraic in [1]. We will extend this result in section 4.

Let us note that for $I \in D$, and $T \in M^{\infty}(F)$ :

(i) either $t_I = \perp$, for all $t \prec_I T$, then $T_I = \perp$ (divergence)
(ii) or $t_I = d \neq \perp$ for some $t \prec T$ and $T_I = d$ (termination)

**Proposition 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 \prec T$ for some $t_1 \in M(F)$ since C is algebraic. Similarly $t \leq_C$, $t_2 \prec T$. Let $t_3$ be the least upper bound of $t_1$ and $t_2$ in $M(F)$. Then $t_3 \prec 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$. []

Theorem 5 will show that $C \cap C'$ need not be algebraic. But theorem 4 defines a class F of algebraic families which is closed by intersection.

## 4 - First-order classes for interpretations

The family I 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 the end of section 5).

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 $\leq$. Let us define :

Mod (A) to be the set of models of A (Schoenfield [12])

Int (A) = I ∩ Mod (A), the class of interpretations which are models of A.

Since I is not first-order definable, Int (A) need not be Mod (A') for any first-order theory A'.

**Definition 2** : A class of interpretations C is first-order if $C = Mod(A)$ for some first-order theory A.

**Example** : D is a first-order family. In fact, conditions 1 and 2 of definition 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 \leq y \Leftrightarrow 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 = Mod(A_D)$.

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

We state and prove two theorems ; the second one is positive and will have several interesting corollaries.

**Theorem 1** : For a first-order theory A, Int (A) is not algebraic in general.

**Theorem 2** : For a first-order theory A, $D(A)$ is algebraic.
*Proof of theorem 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 \Rightarrow a \leq x]$

Let $T = \text{Sup} \{f^n(\Omega)/n \geq 0\}$ be the least fixed point of $x = f(x)$

in $M^\infty(F)$ and $C = \text{Int}(A)$. Then a $\leq_C T$ follows from A since $f_I(T_I) = T_I$ in every interpretation $I \in C$. But there is no $n \in \mathbb{N}$ such that a $\leq_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_5.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 2:* This proof will be based on the compactness theorem for first-order logic.

Assume that $C = D(A) = \text{Mod}(A')$ is not algebraic, that $t' \in \text{M}(F)$ and $T = \text{Sup} \{ t_n / n = 0, 1, \dots \} \in M^\infty(F)$ with $t_0 < t_1 < t_2 < \dots < t_n < \dots$ such that :

(1) $t' \leq_C T$,

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

By (2), each of $A' \cup \{\neg (t' \leq t_n)\}$ has a model $I_n \in C$. In fact, $I_n$ is a model of $A' \cup \{\neg (t' \leq t_0), \neg (t' \leq t_1), \dots, \neg (t' \leq t_n)\}$ since for each $i = 0, \dots, n$, $t_i < t_n$; hence $t'_n \leq t_i I_n$ would imply $t'_I \leq t_n I_n$.

By the compactness theorem for first-order logic [12], $A' \cup \{\neg (t' \leq t_0), \neg (t' \leq t_1), \dots, \neg (t' \leq t_n), \dots\}$ has a model I. Hence $I \in \text{Mod}(A') = D(A)$. Since I is discrete there exists $n$ such that $T_I = [t_n]_I$. Hence $t'_I \leq [t_n]_I$ by hypothesis (1). But this contradicts the definition of I. $\square$

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 $\neq$ $\Omega$ and false $\neq$ $\Omega$ and true $\neq$ false.

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

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

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

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

*Corollary 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 $[0]$ as an example. A typical R.P.S. is

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

An interpretation is some $I = \langle D, p_I, q_I, f_I, g_I \rangle$ where $p_I, q_I$ are total functions :

$D \to \{\text{true, false}\}$ and $f_I, g_I$ are total functions : $D \to D$

We write the same scheme :

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

$$ J = \langle D \cup \{\perp, \text{true, false}\}, \perp, \leq, p_J, q_J, f_J, g_J, h_J \rangle $$

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

$$ p_J(d) = p_I(d) \quad \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. (The meaning of $\perp$ is : *undefined*). Clearly, $J \in D_{\text{cond}}$. The function $\phi_I$ (defined as in [0]) 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 \leq t'] $$

for all $(t,t') \in R$.

*Corollary 2 :* For $R \subset M(F,V)^2$, $D(R) = D \cap C_R$ is algebraic.

This partially answers to a question of [6]. 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_R$'s), the first-order classes of discrete interpretations
(i.e. the $D(A)'s$) and is closed by finite union and finite intersection. Then

**Theorem 3 :** Every $C \in B$ is algebraic

*Proof :* Let $C \in 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 D(A_1) \cap \dots \cap D(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 D(A_1) \cup \dots \cup A_\ell$

$= D(A_1 \cup \dots \cup A_\ell \cup A_{R_1} \cup \dots \cup R_k)$ and is algebraic by theorem 2. By proposition 2, C is algebraic. $\square$

## 5 - Families defined by properties of programs

It has been proved in [4] that the family of all interpretations in which two given program schemes are equivalent is not algebraic.

We now consider the class of discrete interpretations in which a given program terminates. This class is not algebraic in general.

Let $\phi$ be a RPS, let $D_{\phi} = \{I \in D / \phi_I \neq \perp\}$ and $D_{\text{cond},\phi} = \{I \in D_{\text{cond}} / \phi_I \neq \perp\}$. Then

**Theorem 4 :** $D_{\phi}$ and $D_{\text{cond},\phi}$ are not algebraic in general.

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

Let $(\Sigma, \phi)$ be the following RPS :

$$\begin{cases} \phi = f(\Omega, \psi(a)) \\ \psi(v_1) = f(v_1, \psi(g(v_1))) \end{cases}$$

Then $T = T(\Sigma, \phi) = \text{Sup} \{ t_n / n \in \mathbb{N} \}$ where $t_n = f(\Omega, t')$ and

$t'_n =$

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

Let also $T' = \text{Sup} \{ t'_n / n \ge 0 \}$. Then $T = f(\Omega, T')$.

Let $C = D_{\phi}$ and $t = f(b, \Omega)$. We first prove that $t \le_C T$. Let $I \in C$. If $t_I = \perp$ then $t'_I \le T_I$. If $t_I = d \neq \perp$ and $f_I(\perp, \perp) \neq \perp$ then $d = t_I = f_I(\perp, \perp) = T_I$.

If $t_I = d \neq \perp$ and $f_I(\perp, \perp) = \perp$ then $T_I = d' \neq \perp$ by definition of C.
Hence $d' = f_I(\perp, d'')$ where $d'' = T_I' \nsim \perp$. Since I is discrete, $d = f(b_I, \perp) \nsim \perp$ and $d' = f(\perp, d'') \nsim \perp$ imply that $d = f(b_I, d'') = d'$; hence $t_I = T_I$.

We now prove that $t \nmid_C t_n$ for each $n$. For $n \in \mathbb{N}$ let $I$ be the discrete interpretation with domain $D = \{\perp, c_0, c_1, \dots, c_{n+1}\}$ such that:

$$ 
\begin{array}{l@{\qquad}l}
a_I = c_0 & \\
b_I = c_{n+1} & \\
\left\{
\begin{array}{l}
g_I(c_i) = c_{i+1} & \text{for } i = 0, 1, \dots, n \\
g_I(\perp) = \perp \\
g_I(c_{n+1}) = c_{n+1}
\end{array}
\right. & \\
\left\{
\begin{array}{l}
f_I(\perp, d) = c_n & \text{if } d = c_n \\
& = \perp \text{ otherwise} \\
f_I(c_i, d) = c_n & \text{if } d = c_n \\
& = \perp \text{ otherwise} \\
f_I(c_{n+1}, d) = c_n & \text{for all } d \in D
\end{array}
\right. & \text{for } i = 0, 1, \dots, n
\end{array}
$$

One easily checks that $I \in D$ and that:

$$ 
\left\{
\begin{array}{l@{\qquad}l}
[g^i(a)]_I = c_i & \text{for } i = 0, 1, \dots, n+1, \\
[t'_{n+1}]_I = c_n & \text{and } T'_I = c_n, \\
T_I = c_n \nsim \perp, & \text{hence } I \in C \\
[t'_n]_I = \perp & \text{and } [t_n]_I = \perp \\
t_I = f_I(c_{n+1}, \perp) = c_n
\end{array}
\right.
$$

Hence this shows that $t \nmid_C t_n$. Hence $D_\phi$ is not algebraic.

That $D_{\text{cond},\phi}$ is not algebraic follows from example 1 of the introduction. It is not difficult to see that $D_{\text{cond},\phi} \supseteq C \cap D$ ($\phi$ and $C$ are defined in example 1). For every $n$, one can easily build an interpretation $I \in C \cap D$ such that $\phi_I^{(n)} = \perp, b_I \nsim \perp$. Hence $b \le_C \phi$ but $b \le_{C'} \phi^{(n)}$ for no $n \in \mathbb{N}$ where $C' = D_{\text{cond},\phi}$. []

*Remark* : 1. Theorem 4 entails that $D_\phi$ and $D_{\text{cond},\phi}$ are not $D(A)$ for any first-order theory A. This has already been proved by Kfoury and Park [7] (for $D_{\text{cond}}$ and flowcharts).
2. Powerful logical calculi such that $2^{nd}$-order-logic, µ-calculus or L $\omega_1\omega$ (see Park [11]) allow to express properties of programs such that equivalence or termination. It is clear from theorem 4 that classes of interpretations which are definable by such calculi are not algebraic in general.

## 6 - Intersection of algebraic classes

It is known from [6] 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 :

$$ \textcircled{1} \quad C'_{R'} \cap C_R = C_{R \cup R'} \quad \text{(algebraic by proposition 1)} $$

$$ \textcircled{2} \quad D \cap C_R = D(R) \quad \text{(algebraic by corollary 2)} $$

This is not the case :

**Theorem 5 :** 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 2 :** The order relations $\leq_C$ and $\leq_{D_0}$ are the same

The class $D_0$ is algebraic by theorem 2 and so is C by lemma 2. 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) \leq b_I $$

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

$$ \Sigma \left\{ \begin{array}{l} \phi = \psi(a) \\ \psi(v_1) = f(v_1, \psi(g(v_1))) \end{array} \right. $$
Hence $T = \sup_n (t_n)$ where $t_n$ is

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

Technically, we define

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

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

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

Let $I \in C'$ and $n$ such that $[t_{n,n}]_I \ne \perp$. 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 \ne \perp$ 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, \le, \perp, f,g, \dots \rangle$$

$$D = \{\perp, \alpha_0, \alpha_1, \alpha_2, \dots, \alpha_n, \beta\}$$

$$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') = \begin{cases} \beta & \text{if } d = \alpha_n \text{ or } (d \ne \perp \text{ and } d' = \beta), \\ \perp & \text{otherwise} \end{cases}$$
A straight-forward verification shows that $I \in C'$. In particular $t_{n,n_I} = \beta$ but
$[t_{m,m}]_I = \perp$. Hence $[t_{m,m-1}]_I = f(g^{m-1}(a), t_{m,m})_I = 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. $\Box$

Before starting the proof of lemma 2, we describe a construction on interpretations
which has been introduced in [1]. 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

$$
\begin{align*}
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 ; \quad b_J = \langle b_I, b \rangle
\end{align*}
$$

$$
\begin{align*}
g_J(\langle d, t \rangle) &= \langle \perp, \Omega \rangle && \text{if } g_I(d) = \perp \\
&= \langle g_I(d), g(t) \rangle && \text{otherwise,}
\end{align*}
\begin{align*}
f_J(\langle d_1, t_1 \rangle, \langle d_2, t_2 \rangle) &= \langle \perp, \Omega \rangle && \text{if } f_I(d_1, d_2) = \perp, \\
&= \langle f(d_1, \perp), f(t_1, \Omega) \rangle && \text{if } f_I(d_1, \perp) \neq \perp \\
&= \langle f(d_1, d_2), f(t_1, t_2) \rangle && \text{otherwise}
\end{align*}
$$

The interpretation J is in fact the $\mathcal{SD}$-free interpretation associated with I of [1].
We denote it here by $F(I)$.

Lemma 3 : Let $t \in M(F)$

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

$$
(\alpha) \quad t_J = \langle t_I, t' \rangle
$$

$$
(\beta) \quad t_I = t'_I
$$

$$
(\gamma) \quad 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 $(\alpha)$, $(\beta)$ and $(\gamma)$ follow from the definition of J. Assume now that $t = g(u)$. If $g_I(u_I) = \perp$, then $t_J = \langle \perp, \Omega \rangle$, 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 = \langle u_I, u' \rangle$ with $u' \prec u$ and $u'_I = u_I$. Then $t_J = \langle g_I(u_I), g(u') \rangle$ 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^n(a)_J = \langle g^n(a)_I, g^n(a) \rangle$ then $g^n(a) \prec t$ by (1) and this implies $g^n(a) = t$. □

**Lemma 4 :** 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 \text{ otherwise} $$

by our definition of J.

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

*Proof of lemma 2:* 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^0$ iff $t \leq_{D_0} T'$. Since $C \subset D_0$ the if direction is trivial. We will prove that if $t_I \not\leq T'_I$ for some $I \in D_0$, then $t_J \not\leq 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' \prec T'$. Let $n$ be a positive integer such that $g^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 :

$$ 
\begin{align*}
D_J &= D_{I'} \\
\perp_J &= \perp_{I'} \ , \quad a_J = a_{I'} \ , \quad b_J = b_{I'} \ , \quad g_J &= g_{I'} \\
f_J(d_1, d_2) &= f_{I'}(d_1, d_2) \quad \text{if } d_1 \nleq g^n(a)_{I'} \\
&= \delta \quad \text{if } d_1 = g^n(a)_{I'} \text{, where } \delta \text{ is some fixed element of} \\
& \phantom{=} D_J - \{\langle \perp, \Omega \rangle\}
\end{align*}
$$

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 interpretation. Furthermore, $J \in D_0$. We only verify that $F_4$ is satisfied, the other verifications being similar. Let $d_1 \in D_J - \{\perp_J\}$. If $d_1 = g^n(a)_{I'}$, then $f_J(d_1, b_I) = \delta \neq \perp_J$. If $d_1 \nleq g^n(a)_{I'}$, then $f_J(d_1, b_I) = f_{I'}(d_1, 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^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 \nleq g^n(a)_{I'}$.
An easy inductive argument shows that $u_J = u_{I'}$. By lemma 3, $u_{I'}' = 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'}'$. From the initial assumption that $t_I \neq t_I'$, we get $t_I' \neq t_{I'}$ and $t_J \neq t_{J'}$. Similarly, $t_I \neq \bot$ implies $t_{I'} \neq \bot$ and $t_J \neq t_{J'}$. The same holds for $t'$. Hence $t_J \neq t_{J'}$. Q.E.D.

**Second case:** Let $I \in D_0$ such that $t_I \neq \bot$ and $t_I' = \bot$ for all $t' \in M(F)$ such that $t' \prec T'$. We aim to define $J \in C$ such that $t_J \notin 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)}' = \bot$ for every $t' \prec T'$, then we can take $J = I(n)$ and we are done since $t_{I(n)} \neq \bot$ as in the first case. Otherwise, if $t_{I(n)}' \neq \bot$ for some $t' \prec T'$, let us take $J = F(I(n))$. This interpretation belongs to $C$ since $I(n) \in C$ and by lemma 4. Clearly, $t_J \neq \bot$ and $t_J' \neq \bot$. 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 3, $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' = \bot$. This implies $u_I = \bot$ and $u_{I'} = \bot$ (since $I' = F(I)$). Hence $d = u_{I(n)} = \bot$ by lemma 3 again, but $d = t_{I(n)}$ and we get a contradiction since $t_{I(n)} \neq \bot$, by the proof of the first case. Hence we have proved that $t_J \notin T_J'$. $\Box$

## 7 - Conclusion

1. Most classes of interpretations which naturally occur when one considers recursive program schemes are of the form $D(A)$, hence are algebraic by theorem 2. In order to perform proofs of valid relations $\phi \leq_D (A) \phi'$ by computation induction, one needs a characterization of $t \leq_D (A) t'$ for $t, t' \in M(F)$. In most cases, $t \leq_D (A) t'$ will be undecidable but a semi-decidability result is still of interest for proofs about programs.

2. To summarize, algebraic classes are essentially of the following types :

1) $C_R$ (relational),

2) $D(A)$ (first-order discrete). (*)

Most other definitions yield nonalgebraic classes.

## References :

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

<footnote>(*) discrete can be replaced by *bounded*: increasing chains have a bounded length. This will be considered in a forthcoming paper.</footnote>
[1] 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.

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

[3] 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.

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

[5] S.A. Greibach, "Theory of program Structures : Schemes, Semantics, Verifications" Lecture Notes in Computer Science Vol 36 (1975) Springer Verlag.

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

[7] J. Kfoury, D. Park, "On termination of program schemas" Inf. and Control Vol 29 (1975) pp. 243-251.

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

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

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

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

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

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

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