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

HAL
open science

# Semantics and axiomatics of a simple recursive language

Bruno Courcelle, Jean Vuillemin

► To cite this version:

Bruno Courcelle, Jean Vuillemin. Semantics and axiomatics of a simple recursive language. [Research Report] IRIA-RR-060, IRIA. 1974, pp.14. hal-04715909

HAL Id: hal-04715909

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

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_3.png" /></figure>

RIA
laboria

laboratoire de recherche
en informatique
et automatique

Semantics and axiomatics
of a
simple recursive language

B.Courcelle,J.Vuillemin

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

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
78150 - Le Chesnay
Tél. 954.90.20

Rapport de Recherche n° 60

Février 1974
SEMANTICS AND AXIOMATICS OF A SIMPLE

RECURSIVE LANGUAGE.

B. COURCELLE - J. VUILLEMIN

IRIA-LABORIA

78150, ROCQUENCOURT, France.

**Abstract :**

In this paper, we provide a simple recursive programming language with a semantics and a formal proof system, along the lines of [5], [17] and [23]. We show that the semantics used is the "best" possible if one admits the validity of Algol's copy rule, and that the proof system is complete with respect to the semantics. The definitions and methods used are meant to provide a basis for a broader theory of program schemas, which models parallel as well as sequential programs.

**Keywords :**

Semantics of programs. Fixed-points. Operational versus denotational semantics. Proofs of program properties. Deterministic simple languages. Decidability.

**Résumé :**

Dans ce papier, nous décrivons une sémantique et un système de preuves formelles associés à un langage de programmation simple, dans l'esprit de [5], [7] ou [23]. Nous montrons que la sémantique est la "meilleure" possible compatible avec la règle de recopie d'Algol, et que le système de preuve est complet vis à vis de cette sémantique. Nous pensons que les définitions et méthodes utilisées ici fournissent une base mathématique solide pour l'étude d'une large classe de schémas de programmes, qui inclut des schémas de programmes parallèles aussi bien que sequentiels.

**Mots clés :**

Sémantique des langages de programmation. Preuve de programme. Points fixes. Sémantique opérationnelle et sémantique dénotationnelle. Décidabilité. Complétude. Langages simples déterministes.

# 1. INTRODUCTION

The theory of program schemas, as illustrated for example in [1], [2], [10], [13], [15] or [22] has been mainly motivated by the study of sequential Algol or Fortran like programs. Within the framework of more ambitious semantic theories, such as those of Scott [23], where one also considers parallel programs or infinite loops with interesting side-effects (as, for instance, a program enumerating the prime numbers), the results about program schemas take a different flavor. Examples of work with the same starting points are [3], [7], [14], [20] or [27].

In this paper, we try both to provide a rigorous unifying basis for this type of approach, and to obtain results with enough intuitive content so as to convince us that we have indeed appropriate tools for studying programming languages.
A programming language and its semantics are described, in the manner of [19] or [25]. By semantics, we mean what has been called denotational semantics, i.e., a mapping between programs and their intended mathematical meaning as opposed to operational semantics, i.e., some kind of interpreter for the language. (1)

In [28], a canonical domain of interpretation, akin to the Herbrand universe for first order theories is constructed, and it is proved that (Theorem 1) semantic properties are true if and only if they are true in this particular interpretation.

Using Theorem 1 as a basic tool, we study a special class of programs, the *acceptable programs*. (Acceptable should be understood here as a technical term, meaning the class of programs for which we could carry through our proofs). We exhibit a *normal representation* for acceptable programs, and use it to show that equivalence between acceptable programs is decidable. It is also possible to obtain this decidability result via a coding of schemas into deterministic simple languages, where equivalence was shown to be decidable by Hopcroft-Korenjak [12].

Using this normal representation, we show (Theorem 2) that the semantic definition used is the best possible compatible with evaluation rules such as the copy rule. More precisely, we show that, in the terminology of Milner [17], *the semantics is both adequate and fully-abstract with respect to the copy rule*. Another way to put this is that the semantics chosen is compatible with all operational semantics for the language, and it is not more than this because all terms which are semantically equivalent are computationally equivalent with respect to a particular representation of the program.

Finally, we introduce a formal proof system, adapted from [3] and [17], and prove (Theorem 3) that *all equivalences between monadic terms or programs which are semantically valid are (effectively provable within the formal system)*. With minor modifications, we believe that this result should also apply to the formal systems described in [3], (where a similar result has already been obtained for a smaller class of languages), [4] or [11]. As a direct application, the authors prove in [7] the completeness of a similar proof system, restricted to the class of program schemas studied by Ashcroft-Manna-Pnueli [2].

## 2. SYNTAX AND SEMANTICS OF THE LANGUAGE

### 2.1. Syntax

In an approximation of BNF notation, the syntax is defined by:

```
<program> ::=
    F_1(X) <= <term 1>
  | F_k(X) <= <term k>

<term> ::= X | G_1(<term 1>, ..., <term p_1>)
          | G_2(<term 1>, ..., <term p_2>)
          ...
          | G_h(<term 1>, ..., <term p_h>)
          | F_1(<term>)
          ...
          | F_k(<term>)
```

Typical examples are: $F_1(X) <= G_1(X, F_1, F_1(X))$

or
$$ \begin{cases} F_1(X) <= G_1(X, F_2(X)) \\ F_2(X) = G_2(F_2(X), F_1(X)). \end{cases} $$

(1)

In the usual practice of logicians, the first one would be called semantics and the other one syntax.
## 2.2. Semantics

Let us first recall some definitions :

**Definition**: A complete partial order (c.p.o) is set D together with a partial order $\leq$ over D such that

(i) D has a minimal element $\bot_D$.

(ii) Every chain $x_1 \leq x_2 \leq \dots \leq x_n \leq \dots$ has a least upper (l. u. b) $\bigcup_{i \geq 0} x_i$.

**Axiom (Scott)** : Data types are c.p.o's.

Actually, Scott [23] used complete lattices instead of c.p.o's but, for various technical as well as non-technical reasons, c.p.o's seem to be easier to work with, and have been used for example by [5], [9], [14], [16], [17], [19] and [27]. Discussions regarding the choice of c.p.o's versus complete lattices are given in [9] and [28].

**Definition**: A mapping $f : D \to D'$ between two c.p.o's D and D' is said to be continuous if, for every chain $\dot{X} \subseteq D$, we have $\bigcup f(\dot{X}) = f(\bigcup X).$ (1)

**Axiom (Scott)** : Computable functions are continuous mappings between data-types.

We denote by $[D \to D']$ the set of continuous functions between the data-types (i.e, c.p.o's) D and D'.

**Lemma 1** : If D and D' are c.p.o's then $[D \to D']$ is a c.p.o.

**Lemma 2** : Every continuous $f \in [D \to D]$ has a least fixed point $Y(f) \in D$ and $Y(f) = \bigcup_{n \ge 0} f^n(\bot)$.

We can now define the semantic interpretation of our programming language. We shall only do so for programs with only one recursively defined function F. The generalization to mutually recursive systems is straightforward.

**Definition**: An interpretation $J$ of a program $\mathcal{J}$ consists of

(i) A data-type $D$.

(ii) To each function symbol $G_i$ with arity $p_i \ge 0$ is associated a function $g_i \in [D^{p_i} \to D]$.

Given an interpretation $J$, we construct the semantics $S[J \mid T]$, of the term $T$ in the context of the program $\mathcal{J}$ as follows : given a meaning $f \in [D \to D]$ and $a \in D$ for the variable names $F$ and $X$ respectively, we define the interpretation $S[J \mid T] \{f/F, a/X\}$ inductively as follows :

(i) $S[J \mid X] \{f/F, a/X\} = a$

(ii) $S[J \mid G(t_1, \dots, t_p)] \{f/F, a/X\} = g(t_1, \dots, t_p)$ where $g$ is the (continuous) function associated to $G$ in the interpretation and $t_i = S[J \mid T_i] \{f/F, a/X\}$ for $1 \le i \le p$.

(iii) $S[J \mid F(T)] \{f/F, a/X\} = f(S[J \mid T] \{f/F, a/X\})$.

For the sake of readability, we abbreviate $\lambda a.S[J \mid T] \{f/F, a/X\}$ by $S[J \mid T] \{f/F\}$ and $\lambda f.S[J \mid T] \{f/F\}$ by $S[J \mid T]$.

**Lemma 3** : For any term $T$, $S[J \mid T] \in [[D \to D] \to [D \to D]]$ and we denote $Y(S[J \mid T])$ the least fixed point of $S[J \mid T]$.

In the context of a program $F(X) \le P$, the interpretation $J \mid T] \mid T$ of a term $T$ is then defined as

$$J[J \mid T] = S[J \mid T] \{f_p/F\} \quad \text{where} \quad f_p = Y(S[J \mid T]).$$

<footnote>(1) Note that every continuous function is also monotone, i.e, $x \le y$ implies $f(x) \le f(y)$.</footnote>
For example, if the domain of interpretation is

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

and $F(X) <= G_1(X, G_2(X, FG_3(X)))$

with $g_1(x,y) = \mathbf{if} \ x = 0 \ \mathbf{then} \ 1 \ \mathbf{else} \ y$
$g_2(x,y) = x * y$ (x times y)

then $J \models F(X) \models = \lambda x.x!$ (x factorial).

**Definition**: Let $\mathcal{J}$ be a program, $T$ and $T'$ two terms. We say that $\mathcal{J} \models T \equiv T'$ if and only if $J \models T \models = J \models T' \models$ for all interpretations $J$.

We say that two programs $\mathcal{J}=<F_1(X) \leq P_1, \dots, F_k(X) \leq P_k>$ and $\mathcal{J}'=<F'_1(X) \leq P'_1, \dots, F'_k(X) \leq P'_k>$ are equivalent iff
$\mathcal{J} \models F_1(X) \equiv F'_1(X)$ and
$\mathcal{J}' \models F_1(X) \equiv F'_1(X)$.

In [28], a canonical interpretation $\mathcal{K}$ is constructed which has the property :

**Theorem 1**: For any terms $T, T'$ and program $\mathcal{J}$, the equality $\mathcal{J}=T \equiv T'$ holds if and only if $\mathcal{K}\models T \models = \mathcal{K}\models T' \models$.

**Proof**: (See [28]). It is convenient to view elements of $\mathcal{K}$ as infinite formulae. For example, if is $F(X) <= G(X, F(X))$, then $\mathcal{K}\models F(X) \models$ "behaves" like $G(X, G(X, G(X, \dots) \dots))$ ad-infinitum $\square$.

A direct consequence of this canonical interpretation is the following:

**Corollary**: $\mathcal{J} \models G_i(T_1, \dots, T_{p_i}) \equiv G_j(T'_1, \dots, T'_{p'_j})$ if and only if $i = j$ and $\mathcal{J} \models T_k \equiv T'_k$ for $1 \le k \le p_k$.

In order to show some applications of this theorem, let us define the notion of "non-constant"
program by associating to each term $T$ in the context of a program $\mathcal{J}: <F_1(X) \leq P_1, \dots, F_k(X) \leq P_k>$
a natural number $\delta(T)$ as follows :

(i) $\delta(X) = 0$.

$$
(ii) \delta(G_i(T_1, \dots, T_{p_i})) = 1 + \min_{1 \le j \le p_i} \delta(T_j).
$$

$$
(iii) \delta(F_j(T)) = \delta(P_j\{T\}).
$$

Here $P\{T\}$ denotes the result of substituting $T$ for all occurrences of $X$ in $P$.

Whenever $\delta(T)$ is not defined, we say that $\delta(T) = \infty$. For example;

if $F(X) \le G_1(X, FG_2(X))$ then $\delta(F(X)) = 1$ and $\delta(FF(X)) = 2$ while,

if $F(X) \le G_1(F(X),F(X))$ then $\delta(F(X)) = \infty$ and $\delta(G_1(F(X),X)) = 1$.

Intuitively, $\delta(T)$ measures the depth at which $X$ first occurs in the "infinite" formula representing $\mathcal{K}\models T \models$. The case $\delta(T) = \infty$ means that $X$ does not occur in $\mathcal{K}\models T\models$, i.e that $T$ is not dependent upon $X$. This use of the symbol $\infty$ is legitimate since it is clearly decidable whether $\delta(T) = \infty$ or not for any term $T$ and program $\mathcal{J}$.

From now on, we shall only concern ourselves with *acceptable* programs, defined as follows :
**Definition**: A program $\mathcal{J} = \langle F_1(X) \leq P_1, \dots, F_k(X) \leq P_k \rangle$ is acceptable iff
$\delta(F_i(X)) \neq \infty$ for all $1 \leq i \leq k$.

(Just for convenience, we also require that $\delta(F_i(X)) \neq 0$ in acceptable programs).

It is easily seen that, if $\mathcal{J}$ is acceptable, then any subterm $T'$ of an arbitrary term $T$ has a
finite $\delta(T')$, and,

**Lemma 4**: For any terms $T$ and $T'$, $\delta(T\{T'\}) = \delta(T) + \delta(T')$.

**Proof**:

The proof is by induction on $\delta(A)$ where $A = T\{T'\}$.

If $T = X$ then $\delta(T) = 0$, $A = T'$ and $\delta(A) = \delta(T') = \delta(T) + \delta(T')$.

If $T = G(T_1, \dots, T_p)$ then $A = G(A_1, \dots, A_p)$

where $A_j = T_j\{T'\}$ for $1 \leq j \leq p$. By definition of $\delta$, we know that there exists $j_o$ and $j_l$ in $[1, p]$ such that:

(i) $\delta(T) = \delta(T_{j_o}) + 1 \leq \delta(T_{j_l}) + 1$ and

(ii) $\delta(A) = \delta(A_{j_l}) + 1 \leq \delta(A_{j_o}) + 1$.

Since $\delta(A_{j_l}) < \delta(A)$ and $\delta(T_{j_l}) + \delta(T') < \delta(T) + \delta(T') = \delta(A)$, we know by induction that

$\delta(A_{j_o}) = \delta(T_{j_o}) + \delta(T')$ and $\delta(A_{j_l}) = \delta(T_{j_l}) + \delta(T')$. It then follows from (i) and (ii) that

$\delta(A) = \delta(T) + \delta(T')$.

If $T = F(T_1)$, then it is easily seen that $\delta F \neq \infty$ implies that $\exists T' \equiv T$ for some $T' = G(T_1', \dots, T_p')$ and we are back to the previous case. $\square$

It is proved in [28] that acceptable programs have the following properties of right and left simplifications :

**Lemma 5**: For any terms $T$, $T'$ and acceptable program $\mathcal{J}$,

$\mathcal{J} \models T''\{T\} \equiv T''\{T'\}$ iff $\mathcal{J} \models T \equiv T'$.

Note that this is not true if $\mathcal{J}$ is not acceptable, as shown by the counterexample :

$\mathcal{J} = F(X) \leq G(F(X)), T = X, T' = T'' = F(X)$.

### 3. DECIDABILITY OF EQUIVALENCE BETWEEN ACCEPTABLE PROGRAMS.

Let $\mathcal{J} = \langle F_1(X) \leq P_1, \dots, F_k(X) \leq P_k \rangle$ be an acceptable program. We associate to $\mathcal{J}$ an equivalent program $\mathcal{J}'$ as follows : first, each $P_i$ of the form $F_j(T)$ is replaced by $P_j\{T\}$ until all $P_i$'s are of the form $G_j(T_1, \dots, T_{p_j})$. (This is possible because $\mathcal{J}$ is acceptable). Then, to each proper-subterm of the $P_i$'s of the form $G_n(T_1, \dots, T_{p_n})$, we associate a different name, $F_{k+l_j}(X)$ through $F_m(X)$, and replace in $P_i$ the subterm by the corresponding $F_j(X)$. We obtain a new program $\mathcal{J}' = \langle F_1(X) \leq P_1', \dots, F_m(X) \leq P_m' \rangle$ where each $P_i$ is of the form $G_j(M_1, \dots, M_{p_j})$ with $M_q = F_{i_l} \dots F_{i_s}(X)$. We say that such a program $\mathcal{J}'$ is in standard form, and it is easily seen that $\mathcal{J}$ and $\mathcal{J}'$ are equivalent.

For example, if $\mathcal{J} = \langle F_1(X) \leq F_2 F_2(X) \\ F_2(X) \leq G(X, F_1(X)) \rangle$ then $\mathcal{J}' = \langle F_1(X) \leq G(F_2(X), F_1 F_2(X)) \\ F_2(X) \leq G(X, F_1(X)) \rangle$.
and, if $\mathcal{J} = \langle F_1(X) \rangle \leq G(G(X, F_1(X)), F_1 G(X, F_1(X)))$ then

$$ \mathcal{J}' = \left\{ \begin{array}{ll} F_1(X) & \leq G(F_2(X), F_1 F_3(X)) \\ F_2(X) & \leq G(X, F_1(X)) \\ F_3(X) & \leq G(X, F_1(X)) \end{array} \right. $$

To be precise, we should use different symbol letters, say $F_1'$ through $F_m'$ for the variables of $\mathcal{J}'$ but no confusion can arise here since $\mathcal{J}, \mathcal{J}' \models F_i(X) \equiv F_i'(X)$ for $1 \leq i \leq k$.

We can now concentrate our attention to programs in standard form. As a notational convenience, we reserve the letter M for terms of the form $F_i, \dots, F_i(X)$.

Before describing and algorithm for deciding the equivalence between standard programs, thus between acceptable programs, let us establish two preliminary results :

**Lemma 6** : The set of valid formulas of the form $\mathcal{J} \models F_i(X) \equiv M$ is finite and the letter $F_i$ appears in M iff $M = F_i(X)$.

**Proof** : By lemma 4, if $M = F_i, \dots, F_i(X)$ then $\delta M = \sum_{1 \leq j \leq s} \delta(F_i(X))$.

Since $\delta(F_i(X)) \geq 1$, the number of valid equalities $\mathcal{J} \models F_i \equiv M$ is bounded by, say, $k \cdot \delta(F_i)$ where $k$ is the number of $F_i$'s in $\mathcal{J}$. Furthermore, if $F_i$ occurs in $M$, it must be alone. ☐
Equations of the form $\mathcal{J} \models F_i(X) \equiv M$ will be called **elementary equations**.

**Lemma 7** : Let $\mathcal{J}$ be in standard form. If any equality $\mathcal{J} \models F_i(M_1) \equiv F_j(M_2)$ holds, with $\delta(F_i) \leq \delta(F_j)$, we can find $M_3$ such that :

$$ \mathcal{J} \models F_j(X) \equiv F_i(M_3) \text{ and } \mathcal{J} \models M_1 \equiv M_3\{M_2\}. $$

**Proof** : We prove the more general result ($\models M_i\{M_1\} \equiv M_j\{M_2\}$ and $\delta(M_i) \leq \delta(M_j)$ implies $\models M_j\{M_1\} \equiv M_i\{M_2\}$) by induction on $\delta(M_i)$.

If $\delta(M_1) = 0$, i.e, $M_1 = X$ we choose $M_3 = M_j$.

Otherwise, $M_i = F_i(M_i')$ and, since $\delta(M_j) \geq \delta(M_i)$, we must also have $M_j = F_j(M_j')$. Let $P_i = G(M_i', \dots, M_i)$ and $P_j = G(M_j', \dots, M_j)$ be the defining right-hand-side of $F_i(X)$ and $F_j(X)$ respectively in $\mathcal{J}$. Note that the two $G$'s are identical because of the corollary of Theorem 1. For the same reason, $\mathcal{J} \models M_i\{M_1\} \equiv M_j\{M_2\}$ implies $\mathcal{J} \models M_i\{M_1'\} \equiv M_j\{M_2'\}$ for all $1 \leq k \leq p$. Let us choose $k$ so that $\delta(M_i) = \delta(P_i) - 1$. It follows from Lemma 4 that $\delta(M_i\{M_i'\}) = \delta(P_i) + \delta(M_i') - 1 = \delta(M_i) - 1$.

By induction, we can therefore find $M_3$ such that $\mathcal{J} \models M_1 \equiv M_3\{M_2\}$. Its follows that $\mathcal{J} \models M_i\{M_1\} \equiv M_i\{M_3\{M_2\}\} \equiv M_j\{M_2\}$ and, by Lemma 5, $\mathcal{J} \models M_i\{M_3\} \equiv M_j$. ☐

The reader who is familiar with the results of [12] about simple deterministic languages has noticed the similarity between this last result and some of the Lemmas in [12]. The correspondence between our schemas and deterministic simple languages is explicit in [6] and results obtained in each formalism can be translated into the other.

We can now describe an algorithm for deciding if $\mathcal{J} \models M \equiv M'$, where $\mathcal{J}$ is any program in standard form. The structure of the algorithm is :

**start** : simplify ; generate new equations ; **go to** start ;

In the simplification part, all equations $M \equiv M'$ which are not elementary (i.e, of the form $F_i(X) \equiv M$) are replaced by a set of elementary equations through repeated use of Lemma 7. Once all equations are elementary, we replace $F_i(X) \equiv F_j(M')$ by $G_i(M_i', \dots, M_i) \equiv G_j(M_j', \dots, M_j)$.
If $i \neq j$, we terminate with a **no** answer. Otherwise, we replace this equation by

$$M_i := M_j \{M'\}, \dots, M_i \stackrel{p_i}{\rightleftharpoons} M_j \{M'\}.$$

The algorithm terminates with a **yes** answer when no new elementary equation is found after the simplification stage (the number of such equations is finite by Lemma 6); it terminates with a **no** answer when a false equation $\models G_i(M_1, \dots, M_i \stackrel{p_i}{\rightleftharpoons} G_j(M'_1, \dots, M'_j)$ with $i \neq j$ is generated at either stage.

For example, if $\mathcal{T} = \begin{cases} F_1(X) & \le G(X, F_3(X)) \\ F_2(X) & \le G(F_1(X), F_2 F_2(X)) \\ F_3(X) & \le G(F_2(X), F_3 F_2(X)) \end{cases}$

The algorithm, with input $F_2 \equiv F_1 F_1$ proceeds as follows:

$$F_2 \equiv F_1 F_1 \xrightarrow{\text{simplify}} F_2 \equiv F_1 F_1 \xrightarrow{\text{generate}} F_1 \equiv F_1, F_2 F_2 \equiv F_3 F_1 \xrightarrow{\text{simplify}} F_1 \equiv F_1, F_2 \equiv F_1 F_1, F_3 \equiv F_2 F_1 \\ \xrightarrow{\text{generate}} F_3 \equiv F_3, F_1 \equiv F_1, F_2 F_2 \equiv F_3 F, F_2 \equiv F_1 F_1, F_3 F_2 \equiv F_2 F_2 F_1$$

$\xrightarrow{\text{simplify}} F_3 \equiv F_3, F_1 \equiv F_1, F_2 \equiv F_1 F_1, F_3 \equiv F_2 F_1$. The algorithm terminates here with a **yes** answer since no new elementary equation (except the trivial one $F_3 \equiv F_3$) is generated. Of course, this is a crude presentation and there are many ways in which we could improve the efficiency of this algorithm.

### 4. EQUIVALENCE BETWEEN OPERATIONAL AND DENOTATIONAL SEMANTICS.

We now define a canonical representation for programs and for terms. Let us consider a standard program $\mathcal{T} = \langle F_1(X) \le P_1, \dots, F_m(X) \le P_m \rangle$ and valid equation $\mathcal{T} \models F_i(X) \equiv M$ which is not of the uninteresting form $\mathcal{T} \models F_i \equiv F_i$. Any such equation can be used to "simplify" $\mathcal{T}$ as follows: for all $j \neq i$, replace $F_j(X) \le P_j$ by $F_j(X) \le P_j \{M/F_i\}$ where $P_j \{M/F_i\}$ denotes the result of substituting in $P_j$ all subterms of the form $F_k(M_k)$ by $M \{M_k\}$. Replace then $F_i(X) \le P_i$ by $F_i(X) \le M$. We say that a variable $F_i$ which does appear in any of the right-hand-sides of the defining equations of a program $\mathcal{T}$ is **active**. In this sense, the variable $F_i$ is no longer active in the simplified program $\mathcal{T}$. We can perform simplifications in such a way that the defining equations $F_j(X) \le P_j$ are of two forms: either $F_j$ is active and $P_j = G_j(M_1, \dots, M_j)$ or $F_j$ is not active and $P_j = M$, in both cases, $M$ and the $M_i$'s are of the form $F_i^1, \dots, F_i^s$ where the $F_i^k$ are active variables.

**Definition 1:** A canonical representation $\overline{\mathcal{T}}$ of $\mathcal{T}$ is, among all such representations, one for which the number of active variables is minimal and such that the sum of the indices of active variables is also minimal.

$$\text{For example, if } \mathcal{T} = \begin{cases} F_1(X) & \le G(X, F_3(X)) \\ F_2(X) & \le G(F_1(X), F_2 F_2(X)) \\ F_3(X) & \le G(F_2(X), F_3 F_2(X)) \end{cases} \quad \text{then} \quad \overline{\mathcal{T}} = \begin{cases} F_1(X) & \le G(X, F_1 F_1 F_1(X)) \\ F_2(X) & \le F_1 F_1(X) \\ F_3(X) & \le F_1 F_1 F_1(X) \end{cases};$$

$$\text{if } \mathcal{T} = \begin{cases} F_1(X) & \le G(F_2(X), F_1 F_3(X)) \\ F_2(X) & \le G(X, F_1(X)) \\ F_3(X) & \le G(X, F_1(X)) \end{cases} \quad \text{then} \quad \overline{\mathcal{T}} = \begin{cases} F_1(X) & \le F_2 F_2(X) \\ F_2(X) & \le G(X, F_2 F_2(X)) \\ F_3(X) & \le F_2(X) \end{cases}.$$

Of course, we must prove that $\overline{\mathcal{T}}$ does not depend upon the order in which eliminations are performed, i.e.:

**Lemma 8:** The canonical representation $\overline{\mathcal{T}}$ of a program $\mathcal{T}$ is unique.
**Proof**: Assuming the existence of two canonical representations $\overline{\mathfrak{T}}_1$ and $\overline{\mathfrak{T}}_2$ of some program $\mathfrak{T}$, we prove that they are identical.

First we notice that the active variables must be the same in $\overline{\mathfrak{T}}_1$ and $\overline{\mathfrak{T}}_2$; otherwise, let us consider an i such that $F_i$ is active in $\overline{\mathfrak{T}}_1$ and not $\overline{\mathfrak{T}}_2$. Therefore $\overline{\mathfrak{T}}_2 \models F_i \equiv F_{j_1} \dots F_{j_s}$ hence $\overline{\mathfrak{T}}_1 \models F_i \equiv F_{j_1} \dots F_{j_s}$. If any of the $F_{j_k}$ is not active in $\overline{\mathfrak{T}}_1$, we can replace it by some $M = F_{n_1} \dots F_{n_p}$ where the $F_{n_k}$ are active in $\overline{\mathfrak{T}}_1$. It follows that $\overline{\mathfrak{T}}_1 \models F_i \equiv M'$ where $M' = F_{k_1} \dots F_{k_r}$ with the $F_{k_j}$ active in $\overline{\mathfrak{T}}_1$. But this is impossible, unless $M' = F_i$, otherwise, we could simplify $\overline{\mathfrak{T}}_1$ further and reduce the number of active equations by one. If $M' = F_i$, this implies that the defining equation of $F_i$ in $\overline{\mathfrak{T}}_2$ was $F_i(X) \le F_j(X)$, with $F_j$ active in $\overline{\mathfrak{T}}_2$. If $i < j$ we can use $F_i$ instead of $F_j$ as active variable in $\overline{\mathfrak{T}}_2$; but this is impossible since this would decrease the sum of the indices of active variables. If $j > i$, then $\overline{\mathfrak{T}}_1 \models F_i \equiv F_j$ and we could use $F_j$ instead of $F_i$ as active variable in $\overline{\mathfrak{T}}_1$; this is again a contradiction since it would decrease the sum of the indices of active variables in $\overline{\mathfrak{T}}_1$. It follows that active variables are the same in $\overline{\mathfrak{T}}_1$ and $\overline{\mathfrak{T}}_2$. We still have to show that the defining terms are the same in $\overline{\mathfrak{T}}_1$ and $\overline{\mathfrak{T}}_2$. For this purpose, it is sufficient to prove that, in a canonical representation $\overline{\mathfrak{T}}$ of $\mathfrak{T}$, valid equations $\overline{\mathfrak{T}} \models M \equiv M'$ where $M$ and $M'$ are of the form $F_i_1 \dots F_i_s (X)$ with $F_i$ active are of the trivial form $M \equiv M$, that is $\overline{\mathfrak{T}} \models M \equiv M'$ iff $M = M'$.

This is easy by induction on $\delta(M)$ : if $\delta(M) = 0$, then $\delta(M') = 0$ and $M = M' = x$. Otherwise, $M = F_i(M_1)$ and $M'=F_j(M_1')$ with say $\delta F_i \le \delta F_j$. If i where different from j, we could use Lemma 7 and generate an equation $F_j(X) \equiv F_i(M_2)$ which could be used to reduce by one the number of active variables in $\overline{\mathfrak{T}}$. Therefore $i = j$, and by Lemma 5, $\overline{\mathfrak{T}} \models M_1 \equiv M_1'$. By induction, this implies $M_1 = M_1'$ hence $M = M'$. $\square$

This representation is only canonical with respect to a given program, and not to all equivalent programs. For example,

$$ \overline{\mathfrak{T}}_1 = \begin{cases} F_1(X) \le G_1(X, F_2 F_3(X)) \\ F_2(X) \le G_2(F_2(X), X) \\ F_3(X) \le G_3(X, F_3(X)) \end{cases} \quad \text{and} \quad \overline{\mathfrak{T}}_2 = \begin{cases} F_1(X) \le G_1(X, F_2(X)) \\ F_2(X) \le G_2(F_2(X), F_3(X)), \\ F_3(X) \le G_3(X, F_3(X)) \end{cases} $$

which are both in canonical form are equivalent yet not identical.

Using the results of Courcelle [6] about simple languages, it is possible to define such a canonical representation, but it will not be necessary for the purpose of this paper.

We now define a canonical representation for terms (in the context of a given program $\mathfrak{T}$) :

**Definition**: A term $T$ is said to be reduced with respect to the program $\mathfrak{T}$ if it has no subterm $T' = G_i(T_1, \dots, T_{p_i})$ such that $\mathfrak{T} \models T' \equiv F_j(R)$ for some term $R$ and variable $F_j$.

**Lemma 9**: To each term $T$ and program $\mathfrak{T}$, we can associate a unique term $\overline{T}$ reduced with respect to $\mathfrak{T}$, which we call the canonical representation of $T$.

**Proof**: We first prove that $\overline{T}$ exists, then that it is unique.

First, we eliminate in $T$ all variables $F_i$ which are not active in $\overline{\mathfrak{T}}$; this is done by replacing $T$ by $T\{M/F_i\}$ where $F_i$ is defined by $F_i(X) \le M$ in $\overline{\mathfrak{T}}$. A term $T'$ such that $\overline{\mathfrak{T}} \models T' \equiv T$ is so obtained, in which all variables which do occur are active. Let us show that there exist $\overline{T}$ which is reduced with respect to $\overline{\mathfrak{T}}$ and such that $\overline{\mathfrak{T}} \models T' \equiv \overline{T}$ hence $\overline{\mathfrak{T}} \models \overline{T} \equiv T$.

The proof is by induction on the structure of $T$.

If $T = X$ then $\overline{T} = X$ is reduced.

If $T = F_i(T')$ then we know by induction that $\overline{T}'$ exists and we take $\overline{T} = F_i(\overline{T}')$.

If $T = G_i(T_1, \dots, T_{p_i})$, we know by induction that $\overline{T}_1, \dots, \overline{T}_{p_i}$ exist. Let $T' = G_i(\overline{T}_1, \dots, \overline{T}_{p_i})$.

Suppose that $\overline{\mathfrak{T}} \models T' \equiv F_j(R)$ for some $R$ and active $F_j$. The defining equation $F_j(X) \le P_j$ of $F_j$ in $\overline{\mathfrak{T}}$ must be of the form $P_j = G_i(M_1, \dots, M_{p_i})$, and therefore $\overline{\mathfrak{T}} \models \overline{T}_i \equiv M_i(R)$ for $1 \le i \le p_i$. It easy to see (using Lemma 7
again) that such an equation implies that $\overline{T}_i = M_i(\overline{T}_i')$ with $\overline{\mathcal{J}} \models \overline{T}'_i \equiv R$ and $\overline{T}'_i$ reduced with respect to $\overline{\mathcal{J}}$. We can then take $\overline{T} = F_j(\overline{T}_i')$.

In order to prove that $\overline{T}$ is unique let us consider $\overline{T}_1$ and $\overline{T}_2$ and prove by induction on the structure of $\overline{T}_1$ that $\overline{\mathcal{J}} \models \overline{T}'_1 \equiv \overline{T}'_2$ iff $\overline{T}_1 = \overline{T}_2$.

If $\overline{T}_1 = X$ then $\overline{T}_2$ must also be equal to X.

If $\overline{T}_1 = F_i(\overline{T}_1')$ then $\overline{T}_2$ cannot be of the form $X$ or $G(\overline{T}_1'', \dots, \overline{T}_p'')$, otherwise it would not be reduced. It is therefore of the form $\overline{T}_2 = F_j(\overline{T}_2')$ and $j = i$ otherwise, by Lemma 7, $\overline{\mathcal{J}}$ would not be canonical. By Lemma 5, $\overline{\mathcal{J}} \models \overline{T}'_1 \equiv \overline{T}'_2$ and, because of the induction hypothesis; $\overline{T}'_1 = \overline{T}'_2$ hence $\overline{T}_1 = \overline{T}_2$.

If $\overline{T}_1 = G(\overline{T}_1'', \dots, \overline{T}_1')$, then $\overline{T}_2 = G(\overline{T}_2'', \dots, \overline{T}_2')$ otherwise $\overline{T}_1$ would not be reduced and the argument carries through by induction. $\square$

In order to relate operational and denotational semantics, we need to define the computation rules in our language. For this purpose, we say that $T_1 \overline{\mathcal{J}} T_2$ whenever $T_2$ is the result of replacing some subterms $F_j(T')$ of $T_1$ by $P_j(T')$ in $T_1$, where $P_j$ is the right-hand-side corresponding to the definition of $F_j$ in $\mathcal{J}$. Let $\frac{*}{\overline{\mathcal{J}}}$ be the transitive closure of $\overline{\mathcal{J}}$. This relation, which models Algol's copy rule, has been studied by Vuillemin [27] who showed that the set $\{T'|T \frac{*}{\overline{\mathcal{J}}} T'\}$ is a lattice, called the computation lattice of $T$ according to $\mathcal{J}$.

The relation $\frac{*}{\overline{\mathcal{J}}}$ induces an equivalence relation (See [28]) over the set of terms :

**Definition:** We say that two terms $T_7$ and $T_8$ are interconvertible : $T_1 \frac{*}{\overline{\mathcal{J}}} T_2$ with respect to $\mathcal{J}$ if there exists $T_3$ such that $T_1 \frac{*}{\overline{\mathcal{J}}} T_3$ and $T_2 \frac{*}{\overline{\mathcal{J}}} T_3$.

This syntactical notion of equivalence between terms can be used to characterize semantic equivalence in the following sense :

**Theorem 2:** For any acceptable program $\mathcal{J}$ and term $T$, the set $\{T'|\mathcal{J} \models T \equiv T'\}$ of terms semantically equivalent to $T$ coincide with the set $\{T'|T \frac{*}{\overline{\mathcal{J}}} T'\}$ of terms interconvertible to $T$ with respect to the canonical representation $\overline{\mathcal{J}}$ of $\mathcal{J}$.

**Proof:** First, we notice that $T \frac{*}{\overline{\mathcal{J}}} T_a$ where $T_a$ is obtained by replacing in $T$ the variables which are inactive in $\overline{\mathcal{J}}$. We then prove that the set $\{T'|\mathcal{J} \models T_a \equiv T'\}$ of terms equivalent to $T_a$ coincide with the computation lattice $\{T'|\overline{T}_a \frac{*}{\overline{\mathcal{J}}} T'\}$ of $\overline{T}_a$ by $\overline{\mathcal{J}}$. This imply in particular that $\overline{T}_a \frac{*}{\overline{\mathcal{J}}} T_a$.

Since $\overline{T}_a = \overline{T}$, we establish $T \frac{*}{\overline{\mathcal{J}}} T$. Since, by Lemma 9, $\mathcal{J} \models T \equiv T'$ implies $T = \overline{T}'$, we have $\overline{T} \frac{*}{\overline{\mathcal{J}}} T'$ thus $\overline{T} \frac{*}{\overline{\mathcal{J}}} T'$ for all $T'$ equivalent to $T$.

The proof that $\mathcal{J} \models T_a \equiv T'$ implies $\overline{T}_a \frac{*}{\overline{\mathcal{J}}} T'$ is by induction on the structure of $T'$ :

- if $T' = X$, then $\overline{T}_a = T_a = X$ and indeed $X \frac{*}{\overline{\mathcal{J}}} X$.

- if $T' = F_i(T_i')$ then $\overline{T}_a$ must be of the form $F_i(\overline{T}_i')$, otherwise it would not be reduced. By induction, $\overline{T}_i \frac{*}{\overline{\mathcal{J}}} T_i'$ hence $\overline{T}_a \frac{*}{\overline{\mathcal{J}}} T'$.

- if $T' = G(\overline{T}_1'', \dots, \overline{T}_p')$ then either $\overline{T}_a = G(\overline{T}_1'', \dots, \overline{T}_p')$ or $\overline{T}_a = F_i(T_i')$.

- if $\overline{T}_a = G(\overline{T}_1'', \dots, \overline{T}_p')$ the argument proceeds nicely by induction. If $\overline{T}_a = F_i(T_i')$, let $P_i = G(M_1, \dots, M_p)$ be defining right-hand-side of $\overline{T}_a$ in $\overline{\mathcal{J}}$. By definition of $\frac{*}{\overline{\mathcal{J}}}$, we have $\overline{T}_a \frac{*}{\overline{\mathcal{J}}} G(M_1\{T_i'\}, \dots, M_p\{T_i'\})$.

Since $M_i\{T_i'\}$ is reduced and $\overline{\mathcal{J}} \models M_i\{T_i'\} \equiv T_i'$ for $1 \le i \le p$, we have $M_i\{T_i'\} = \overline{T}_i'$ by Lemma 9, hence $M_i\{T_i'\} \frac{*}{\overline{\mathcal{J}}} T_i'$ and $\overline{T}_a \frac{*}{\overline{\mathcal{J}}} T'$ follows by definition of $\frac{*}{\overline{\mathcal{J}}}$ again. $\square$

## 5. A FORMAL PROOF SYSTEM AND ITS COMPLETENESS.

In this section, we describe a formal system for proving properties of programs in our language and prove its completeness. The system is a straightforward adaptation of [3] or [17].

### Description of the system

- Terms are the same as terms of the programming language, with the addition that we can take the greatest-lower-bound (g.1.b) $\min(T_1, T_2)$ of any two terms $T_1$ and $T_2$.
- A well formed formula (wff) is a conjunction of inequalities $T \leq T'$ between terms or of defining equations $F_i(X) <= P_i$ where $P_i$ is a term; $T \equiv T'$ is an abbreviation for $T \leq T'$, $T' \leq T$.

- A proof is a sequence of implications between wffs, each being obtained by application of the axioms or the rules of inference.

- The variable $F$ is bound in $\phi, F(X) <= P$ and it must be free in the wff $\phi$. The variable $\bot$ is always assumed to be bound by $\bot(X) <= \bot(X)$.

- Axioms.

(Relexivity) A1 : $\rightarrow T \leq T$

(Transitivity) A2 : $T_1 \leq T_2, T_2 \leq T_3 \rightarrow T_1 \leq T_3$

(Minimality) A3 : $\bot(X) <= \bot(X) \rightarrow \bot(T) \leq T'$.

(Monotonicity) A4 : $T_1 \leq T_2, T_3 \leq T_4 \rightarrow T_1\{T_3\} \leq T_2\{T_4\}$.

(g.1.b) A5 : $T \leq T_1, T \leq T_2 \rightarrow T \leq \underline{min}(T_1, T_2)$

A6 : $\rightarrow \underline{min}(T_1, T_2) \leq T_1$

A7 : $\rightarrow \underline{min}(T_1, T_2) \leq T_2$

(fixed point) A8 : $F(X) <= P \rightarrow T \equiv T\{P/F\}$.

A discussion regarding the introduction of $\underline{min}$ into the system can be found in [28].

- Rules of Inference

They include the usual propositional calculus rules :

(inclusion) R1 : $\frac{\Phi}{\Phi} \qquad (\Psi \text{ is a subset of } \Phi)$

(conjunction) R2 : $\frac{\Phi \rightarrow \Psi \qquad \Psi \qquad \Phi \rightarrow X}{\Phi \rightarrow \Psi, X}$

(Cut) R3 : $\frac{\Phi \rightarrow \Psi \qquad \Psi \rightarrow X}{\Phi \rightarrow X}$

together with Scott's induction rule :

(induction) R4 : $\frac{\Phi \rightarrow \Psi\{\bot/F\} \qquad \Phi, \Psi \rightarrow \Psi\{P/F\}}{\Phi, F(X) <= P \rightarrow \Psi} \qquad (F \text{ free in } \Phi \rightarrow \Psi)$

Here are some examples of theorems easily provable within the system :

(i) $F(X) <= T_1\{T_2\}, F'(X) <= T'_1\{T'_1\} \rightarrow F(X) \equiv T'_1, F'(X) \equiv T_2$

where $T'_1 = T_1\{F'/F\}$ and $T'_2 = T_2\{F'/F\}$;

(ii) $F(X) <= F(G(X)) \rightarrow F(X) \equiv \bot(X)$;

(iii) $F_1(X) <= G(X, F_1 F_1(X)), F_2(X) <= G(X, F_1 F_2(X)) \rightarrow F_1(X) \equiv F_2(X)$.

It is not quite so easy to find a proof of

(iv) $\mathcal{J}, \mathcal{J}' \rightarrow F(X) \leq F_o(X)$,

where $\mathcal{J}' = \langle F(X) \leq G(X, F_o(X), F_1(X)), F_2(X) \leq G(F_o(X), F_1(X), F_2(X)), F_2(X) \leq G(F_1(X), F_2(X), F_2F_o(X)) \rangle$

The proof of (iv) generated by the method of Theorem 3 (below) uses Scott's Induction, on the formula

$$ \Phi(f) = f \leq F_o, fF_o \leq F_1, f(\underline{min}(F_1, F_o F_o)) \leq F_2. $$

It is not known to the authors whether this particular proof (or any other for that matter) indeed requires the use of $\underline{min}$.
Completeness of the formal system.

We now prove the main result of this section :

**Theorem 3** : The formal system described above is (effectively) complete with respect to acceptable program $\mathcal{P}$, i.e, $\mathcal{P} \models T \equiv T'$ iff $\mathcal{P} \vdash T \equiv T'$.

**Proof** : Just for convenience, we restrict ourselves to acceptable programs in standard form, since there is no difficulty in extending the result to all acceptable programs. The direction $\mathcal{P} \vdash T \equiv T'$ implies $\mathcal{J}' \models T \equiv T'$ expresses the **soundness** of the system which is shown in [17] or [28]. In order to prove that $\mathcal{P} \models T \equiv T'$ implies $\mathcal{P} \vdash T \equiv T'$, we notice that, using only axiom A8, it is easy to prove that $T \models_{\mathcal{P}}^* T'$ implies $\mathcal{P} \vdash T \equiv T'$.

By Theorem 2, we know that $\overline{\mathcal{P}} \models T \equiv T'$ iff $T \models_{\mathcal{P}}^* T'$.

It follows that $\overline{\mathcal{P}} \models T \equiv T'$ iff $\overline{\mathcal{P}} \vdash T \equiv T'$ and Theorem 3 is proved for programs $\overline{\mathcal{P}}$ in canonical form. Let $\mathcal{J}' \models <F_1 \leq P_1, \dots, F_m \leq P_m>$ be an arbitrary program in standard form and $\overline{\mathcal{P}} = <\overline{F}_1 \leq \overline{F}_1, \dots, \overline{F}_m \leq \overline{F}_m>$ its canonical representation. In order to prove that $\mathcal{P} \models T \equiv T'$ implies $\mathcal{P} \vdash T \equiv T'$, it is sufficient to prove that (a) $\mathcal{J}'$, $\overline{\mathcal{J}} \models \overline{F}_1 \equiv F_1$, ..., $\overline{F}_m \equiv F_m$ : we know that $\mathcal{P} \models T \equiv T'$ iff $\overline{\mathcal{P}} \models \overline{T} \equiv \overline{T'}$ where $\overline{T} = T(\overline{F}_1/F_1, \dots, \overline{F}_m/F_m)$; we know that $\mathcal{P} \vdash \overline{T} \equiv \overline{T'}$ iff $\mathcal{P} \vdash \overline{T} \equiv \overline{T'}$ ; formula (a) implies $\mathcal{P}$, $\overline{\mathcal{P}} \vdash T \equiv T'$, $\overline{T} \equiv \overline{T'}$ thus $\mathcal{P} \models T \equiv T'$ implies $\mathcal{P} \vdash T \equiv T'$.

It is easy to show that $\mathcal{P}, \overline{\mathcal{P}} \vdash F_1 \subseteq \overline{F}_1, \dots, F_m \subseteq \overline{F}_m$ and we leave this to the reader. In order to prove the other way around ,i.e, $\mathcal{P}, \overline{\mathcal{P}} \vdash \overline{F}_1 \subseteq F_1, \dots, \overline{F}_m \subseteq F_m$, let us introduce the following notation : let $\Sigma.(M)$ represent the greatest lower bound of the finite set $\{M'|\mathcal{P} \models M' \equiv M\}$ of terms equivalent to M. For example, if $\mathcal{P} \models F_1 \equiv F_2 F_2$ is the only valid elementary formula, then $\Sigma.(F_1F_2) = \min.(F_1F_2,F_2F_2F_2,F_1F_2)$ which is just an abbreviation for $\min.(F_1F_2, \min.(F_2F_2F_2,F_1F_2))$.

For any $1 \le i \le m$ there is a unique valid formula $\mathcal{P} \models F_i \equiv F_j \dots F_k$ where $\overline{F_j}, \dots, \overline{F_k}$ are active variables in $\overline{\mathcal{P}}$. Let $w_i$ represent the wff $\overline{F_j} (\Sigma(F_j \dots F_k)) \subseteq F_i$ and $\phi$ be the conjunction $\wedge w_i$ of all $1 \le i \le m$. In order to prove (a), it is sufficient to prove (b) $\mathcal{P}, \overline{\mathcal{P}} \vdash \phi$ : if $\overline{F}_i$ is active in $\overline{\mathcal{P}}$, then $w_i$ is $\overline{F}_i \subseteq F_i$, and, since we know $\mathcal{P}, \overline{\mathcal{P}} \vdash F_i \subseteq \overline{F}_i$ proving (b) implies $\mathcal{P}, \overline{\mathcal{P}} \vdash \overline{F}_i \equiv F_i$ for all $F_i$'s which are active in $\overline{\mathcal{P}}$.

If $\overline{F}_i$ is not active in $\overline{\mathcal{P}}$ then $\overline{\mathcal{J}} \models \overline{F}_i \equiv \overline{F}_j \dots \overline{F}_k$ by A8, and $\overline{F}_j, \dots, \overline{F}_k$ are active in $\overline{\mathcal{P}}$ ; it follows from the remark that anything which is true in $\overline{\mathcal{P}}$ is provable that $\overline{\mathcal{J}} \vdash \overline{F}_j \dots \overline{F}_k \subseteq N$ for any $N \in \Sigma.(F_j \dots F_k)$, hence, by repeated use of A5 : $\overline{\mathcal{J}} \vdash \overline{F}_j \dots \overline{F}_k \subseteq \Sigma.(\overline{F}_j \dots \overline{F}_k)$.

Since we already know that $\mathcal{P}, \overline{\mathcal{P}} \vdash \overline{F}_j \equiv F_j, \dots, \overline{F}_k \equiv F_k$ we obtain, by A2 and A4

$\mathcal{P}, \overline{\mathcal{P}} \vdash \overline{F}_i \subseteq \overline{F}_j \Sigma(F_j \dots F_k)$. Assuming (b) now implies $\mathcal{P}, \overline{\mathcal{P}} \vdash w_i$, i.e, $\mathcal{P}, \overline{\mathcal{P}} \vdash \overline{F}_j(F_j \dots F_k) \subseteq F_i$ hence, by A2 again $\overline{\mathcal{P}}, \mathcal{P} \vdash \overline{F}_i \subseteq F_i$ for all $1 \le i \le m$.

Before proving (b), we need to establish the following

**Lemma** : $\mathcal{P} \models M_1 M_2 \equiv M$ and all variables in $M_1$ active in $\mathcal{P}$ implies $\mathcal{P} \vdash \overline{M_1} (\Sigma(M_2)) \subseteq M$.

The proof is by induction on $\delta(M)$.

If $\delta(M) = 0$ then $M = M_1 = M_2 = X$ and $\phi \equiv X \subseteq X$ by A1.

If $\delta(M) > 0$ then $M = F_i(M')$. Let $\models F_i \equiv F_j \dots F_k$ with $F_j, \dots, F_k$ active in $\mathcal{P}$. We consider two cases :

**Case 1** : $\delta(M_1) \ge \delta(F_j)$

In this case $\overline{M}_1 = \overline{F}_j \dots \overline{F}_k \overline{M}'_1$ and we must prove $\phi \vdash \overline{F}_j \dots \overline{F}_k \{\overline{M}'_1|\Sigma(M_2)\} \subseteq F_i(M')$.

Since $\delta(F_j \dots F_k) < \delta(F_i) \le \delta(M)$, we know by induction that $\phi \vdash \overline{F}_j \dots \overline{F}_k \subseteq N$ for any $N \in \Sigma.(F_j \dots F_k)$.
Hence, by repeated applications of A5, we obtain

$$ \phi \vdash \overline{F}_{j_2} \dots \overline{F}_{j_k} \subseteq \sum (F_{j_2} \dots F_{j_k}), \text{ hence, by A4} $$

$\phi \vdash \overline{F}_{j_1} \dots \overline{F}_{j_k} \subseteq \overline{F}_{i_1} (\sum (F_{j_2} \dots F_{j_k}))$. Since $\overline{F}_{j_1} (\sum (F_{j_2} \dots F_{j_k})) \subseteq \overline{F}_{i_1}$ belongs to $\phi$ by construction, an application of A2 gives us

$$ \phi \vdash \overline{F}_{j_1} \dots \overline{F}_{j_k} \subseteq \overline{F}_{i_1} $$

By induction again, we know that $\phi \vdash \overline{M}_1' \{\sum (M_2)\} \subseteq M'$ and one application of A4 allows to conclude
$\phi \vdash \overline{M}_1 \{\sum (M_2)\} \subseteq M$.

**Case 2 :** $\delta(M_1) < \delta(F_i)$

Then $\overline{M}_1 = \overline{F}_{j_1} \dots \overline{F}_{j_k}$ with $n < k$ and $\vdash M_2 \equiv \overline{F}_{j_{n+1}} \dots \overline{F}_{j_k} M'$.

It is clear by definition of $\sum$ and repeated applications of A6 and A7 that

$$ \sum (M_2) \subseteq \sum (\overline{F}_{j_{n+1}} \dots \overline{F}_{j_k}) \{\sum (M')\} \text{ hence, by A4 } \phi \vdash \overline{M}_1 \{\sum (M_2)\} \subseteq \overline{M}_1 \{\sum (\overline{F}_{j_{n+1}} \dots \overline{F}_{j_k}) \{\sum (M')\}\} $$

By induction, $\phi \vdash \overline{F}_{j_2} \dots \overline{F}_{j_n} \sum (\overline{F}_{j_{n+1}} \dots \overline{F}_{j_k}) \subseteq N$ for any $N \in \sum (\overline{F}_{j_2} \dots \overline{F}_{j_k})$. Hence, by repeated applications of A5 : $\phi \vdash \overline{F}_{j_2} \dots \overline{F}_{j_n} \{\sum (\overline{F}_{j_{n+1}} \dots \overline{F}_{j_k})\} \subseteq \sum (\overline{F}_{j_2} \dots \overline{F}_{j_k})$. Using the same proof as in case 1, we then obtain $\phi \vdash \overline{M}_1 \{\sum (\overline{F}_{j_{n+1}} \dots \overline{F}_{j_k})\} \subseteq \overline{F}_{i_1}$. Since $\sum (M') \subseteq M'$ by A6 and A7, we can combine every thing into $\phi \vdash \overline{M}_1 \{\sum (M_2)\} \subseteq \overline{F}_{i_1} (M')$. $\square$

We are now ready to prove (b), i.e, $\mathcal{P}, \mathcal{P}' \vdash \phi$ by Scott induction on $\mathcal{P} \vdash \phi$. We shall use the "parallel" version of rule R4 but it is shown in [27] that R4 would do just as well in the way it is stated.

- base We must prove $\mathcal{P} \vdash \phi \{\overline{\mathcal{P}} / \overline{F}_j\}$ for all $\overline{F}_j$ active in $\overline{\mathcal{P}}$.

This is easy using A3.

- Induction Assuming $\mathcal{P}, \phi$, we must prove $\phi \{\overline{P}_j / \overline{F}_j\}$ for all $\overline{F}_j$ active in $\overline{\mathcal{P}}$, i.e, that $\overline{P}_j \{\overline{\sum} (\overline{F}_{j_1} \dots \overline{F}_{j_k})\} \subseteq \overline{F}_{i_1}$ for all $1 \le i \le m$. Let $P_i = G(M_1, \dots, M_p)$; using A8, we show $\mathcal{P} \vdash P_i \equiv \overline{F}_{i_1}$ thus it will be sufficient to prove that $\phi \vdash \overline{P}_j \{\overline{\sum} (\overline{F}_{j_1} \dots \overline{F}_{j_k})\} \subseteq P_i$. The term $P_i$ can only be of the form $\overline{P}_j = G(\overline{M}_1, \dots, \overline{M}_p)$ and thus, all we need to prove is $\phi \vdash \overline{M}_k \{\overline{\sum} (\overline{F}_{j_2} \dots \overline{F}_{j_k})\} \subseteq \overline{M}_k$ for all $1 \le k \le p$. Since we know from the preceding Lemma that this is the case, we can regroup everything using A4 and the proof of Theorem 3 is completed. $\square$

## 6. CONCLUSION

There are many directions in which this type of study could be generalized.

1. Are the main results obtained here still valid without the restriction that $\delta(F_i(X)) \neq \infty$?

In terms of languages, this means being able to decide the equivalence of simple language over infinite as well as finite words. The corresponding problem for regular languages is solved in [7].

2. Is equivalence between polyadic programs decidable ?

An answer to this question would imply some new results about context-free languages.

In [28], Theorem 1 is proved in the polyadic case without restriction and equivalence between linear polyadic programs is shown to be decidable. A general answer to 1 or 2 is still unknown to the authors.

3. Do similar results exist about the typed $\lambda$-calculus and $\lambda$-calculus ? Is Milner's LCF [17] complete if we remove conditionals ?
4. Can one prove Theorem 3 without introducing *min* or, (as the authors conjecture), show that *min* is necessary ?

5. Is it possible to study "real life" languages such as Fortran, Algol or LISP in this manner. The groudwork for such a study of LISP has been laid by Gordon [9], but no such work exists yet for Fortran or Algol, to the authors'knowledge.

## ACKNOWLEDGMENTS

We wish to express our gratitude to Gilles Kahn for his collaboration to this work, and to Robin Milner and Maurice Nivat for many stimulating discussions on the subject.

## REFERENCES

[1] E.A. Ashcroft, Z. Manna, "Formalization of Properties of Parallel Program" Memo Stanford AIM 110 (1970).

[2] E.A. Ashcroft, Z. Manna, A. Pnueli, "Decidable Properties of Monadic Functional Schemas" in Theory of Machines and Computations Kohavi and Paz, Eds. Academic Press, pp 3-18 (1971).

[3] J.W. de Bakker, "Recursive Procedures", Mathematical Center Tracts n°24, Amsterdam. (1971).

[4] J.W. de Bakker, W.P. de Roever, "A Calculus for Recursive Program Schemes", Proceedings of IRIA Colloquium, North-Holland (1972).

[5] J.W. de Bakker, D. Scott, "A Theory of Programs", unpublished (1969).

[6] B. Courcelle, "Grammaires Canoniques des Langages Simples Déterministes", RAIRO n°1 Paris (1974).

[7] B. Courcelle, G. Kahn, J.Vuillemin, "Algorithmes d'Equivalence pour des Equations Récursives Simples", Rapport Laboria n°37, IRIA, (1973).

[8] B. Courcelle, J. Vuillemin, "Compléture d'un Système Formel pour l'Equivalence de Certains Schémas Récursifs Monadiques", To appear in Compte-rendu du Colloque de Paris (Avril 1974).

[9] M. Gordon, "Evaluation and Denotation of pure LISP Programs : a Worked Example in Semantics", Thesis, Edinburgh (1973).

[10] M.S. Paterson, C. Hewitt, "Comparative Schematology", in Record of Project MAC Conference on Parallel Computation, ACM, New York (1970).

[11] P. Hitchcock, D. Park, "Induction Rules and Proofs of Termination" Proceedings of IRIA Colloquium, North Holland (1972).

[12] J.E. Hopcroft, A.J. Korenjak, "Simple Deterministic Languages", 7th SWAT (1966), pp 36-46.

[13] Y.I. Ianov, "The Logical Schemes of Algorithms", Problems in Cybernetics, vol 1, Pergamon Press. (1960).

[14] G. Kahn, "A Preliminary Theory of Parallel Programs", Rapport Laboria n°6, IRIA (1973).

[15] D. Luckham, D. Park, M.S. Paterson, "On Formalized Computer Programs", JCSS vol 4, n°3, pp 220-249, (1970).

[16] Z. Manna, S. Ness, J. Vuillemin, "Inductive Methods for Proving Properties of Programs", CACM vol 16, n°8 (1973).

[17] R. Milner, "Models of LCF", AIM-186/CS-332, Stanford University (1973).
[18] R. Milner, "Processes : a model of computing agents", University of Edinburgh. Unpublished memo. (1973).

[19] R. Milner, R. Weyrauch, "Proving Compiler Correctness in a Mechanized Logic", Machine Intelligence 7, Edinburgh University Press. (1972).

[20] M. Nivat, "Sur l'Interprétation des Schémas de Programmes Monadiques", Rapport Laboria n°1, IRIA (1972).

[21] M. Newey, Ph.D. thesis, Computer Science Department, Stanford (1973).

[22] M. Paterson, "Program Schemata", in MI 3, Edinburgh University (1968).

[23] D. Scott, "Outline of a Mathematical Theory of Computation", Oxford mono., PRG-2, Oxford University (1970).

[24] D. Scott, "Continuous Lattices", Oxford mon. PRG-7 (1972).

[25] D. Scott, C. Strachey, "Towards a Mathematical Semantics for Computer Languages", Oxford mono., PRG-6, Oxford University (1972).

[26] J. Vuillemin, "Proof Techniques for Recursive Programs", Ph.D. Thesis, Stanford University (1973).

[27] J. Vuillemin, "Correct and Optimal Implementations of Recursion in a Simple Programming Language ". Proceeding of the fifth ACM Symposium on Theory of Computing, pp 224-239 (1973).

[28] J. Vuillemin, "Syntaxe, Sémantique et Axiomatique d'un Langage de Programmation Simple", These d'Etat (To appear).