# On the interpretation of recursive program schemes

Maurice Nivat

► To cite this version:

Maurice Nivat. On the interpretation of recursive program schemes. [Research Report] IRIA-RR-084, IRIA. 1974, pp.33. hal-04715926

HAL Id: hal-04715926

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

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

laboratoire de recherche
en informatique
et automatique

On the interpretation
of recursive program schemes

M.Nivat

Institut de Recherche
d'Informatique
et d'Automatique

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

Rapport de Recherche n° 84

Octobre 1974
# ON THE INTERPRETATION OF RECURSIVE PROGRAM SCHEMES

M. Nivat

University of Paris VII and IRIA

A first version of this work was presented at Convegno d'Informatica Teorica, Istituto di Alta Matematica di Roma, February 1973.

The present paper has been written as the notes of lectures given at the Advanced Course on the Semantics of Programming Languages Saarbrücken, February 1974 and at the Mathematical Foundations of Computer Science Semester, Stefan Banach Mathematical Center, Warszawa, March 1974.

## Abstract :

This paper extends a previous paper [8] where we described a semantics for monadic recursive program schemes (also called Scott-de Bakker schemes). The method consists in considering program schemes as rewriting systems which generate subsets of a free magma and defining a mapping of such subsets in a proper domain of functions. In our previous paper, dealing with a simple case, the combinatorial properties on which the whole construction relies were well known or at least immediate corollaries of well-known results in the theory of context-free languages. In the present case, the rewriting systems which we are led to consider and which in a very natural way could be called algebraic rewriting systems or grammars on a free magma, have been little considered in the literature and we need establish first a number of results concerning such systems. This is done in a first part of this paper. Afterwards we establish the link between such rewriting systems and recursive program schemes, define the function computed by such a scheme under a given discrete interpretation and apply the results of part I to show the equivalence of one definition of this function with the classical definitions : the operational semantics as described for example in [3], Kleene's definition of recursive function [2], the fix-point semantics as it can be found in [5], [6] or [10].

## Résumé :

Cet article est l'extension d'un article précédent [8] où nous avons décrit une sémantique pour les schémas de programme monadiques (aussi appelés schémas de Scott-de Bakker). La méthode consiste à considérer les schémas de programmes comme des systèmes de réécriture qui engendrent des sous ensembles du magma libre et à définir une application de ces sous ensembles dans un domaine de fonctions convenablement choisi. Dans notre article précédent, consacré à un cas simple, les propriétés combinatoires sur lesquelles notre construction reposait étaient bien connues ou en tout cas étaient des corollaires immédiats de résultats bien connus dans la théorie des langages algébriques.

Dans le cas présent, les systèmes de réécriture que nous sommes conduits à considérer et qui pourraient fort naturellement être appelés des systèmes de réécriture algébriques ou des grammaires sur le magma libre, ont été peu étudiés dans la littérature et nous devons d'abord établir un certain nombre de résultats à leur sujet. C'est ce que nous faisons dans la première partie. Puis nous établissons le lien entre ces systèmes de réécriture et les schémas de programmes récursifs, définissons la fonction calculée par un tel schéma dans une interprétation discrète donnée et appliquons les résultats de la première partie pour montrer l'équivalence entre notre définition de cette fonction et les définitions classiques : la sémantique opérationnelle comme elle est décrite dans [3] par exemple, la définition des fonctions récursives selon Kleene [2], la sémantique du point fixe comme on peut la trouver dans [5], [6] ou [10].
## First part

### Rewriting systems on free magmas

#### I The free F-magma generated by V

Let $F$ be a finite set of symbols called function symbols.
With each $f \in F$ is associated a positive integer $\rho(f)$ called
the arity of $f$.

We define a $F$-magma as a set $E$ together with for each $f$ in $F$ an
application $\sigma(f)$ of $E^{\rho(f)}$ into $E$.

A morphism of the $F$-magma $(E, \sigma)$ into the $F$-magma $(E', \sigma')$ is a
mapping $\varphi$ of $E$ into $E'$ such that for all $f \in F$ and $e_1, \dots, e_{\rho(f)} \in E$

$$ \varphi(\sigma(f)(e_1, \dots, e_{\rho(f)})) = \sigma'(f)(\varphi(e_1), \dots, \varphi(e_{\rho(f)})) $$

Given a set $V$, disjoint from $F$, there exists a unique $F$-magma
containing $V$, denoted by $M(F,V)$ such that every mapping of $V$ into
an $F$-magma $(E, \sigma)$ can be extended in a morphism of $M(F,V)$ into $(E, \sigma')$.
$M(F,V)$ is called the free $F$-magma generated by $V$ and its existence
results from standard theorems in algebra.

It will suffice here how to construct this free magma.

Let $X$ be the alphabet composed of $F,V$ and the three
symbols which are the left parenthesis "(" , the right parenthesis")"
and the comma "," . $M(F,V)$ can be identified with the smallest
subset of $X^*$ which

- contains $V$

- contains $f(m_1, \dots, m_{\rho(f)})$ whenever $f \in F$ and

$m_1, \dots, m_{\rho(f)} \in M(F,V)$.

The mapping of $M(F,V)^{\rho(f)}$ into $M(F,V)$ associated with $f \in F$
is the mapping which maps $m_1, \dots, m_{\rho(f)}$ onto $f(m_1, \dots, m_{\rho(f)})$

The identification of $M(F,V)$ with this set of words will be
complete in what follows. We shall have no occasion to distinguish
between the free $F$-magma generated by $V$ and the specific
representation we built.

As a set of words in $X^*$, $M(F,V)$ has a number of interesting
properties:
Let us call factor of an element $m \in M(F,V)$ any triple $(\alpha; n; \beta)$ where $\alpha, \beta \in X^*$, $n \in M(F,V)$ and $\alpha\beta = m$. $\alpha\beta$ denotes the product of $\alpha, n, \beta$ as words in $X^*$.

The two factors $(\alpha; n; \beta)$ and $(\alpha'; n'; \beta')$ of $m \in M(F,V)$ are called disjoint iff there exist $\alpha'', \beta'' \in X^*$ such that

$$ \text{either } \alpha = \alpha' n' \alpha'' \text{ and } \beta' = \alpha'' \beta'' $$

$$ \text{or } \alpha' = \alpha n \alpha'' \text{ and } \beta = \alpha'' \beta'' $$

The factor $(\alpha; n; \beta)$ is said to be contained in the factor $(\alpha'; n'; \beta')$ iff there exist $\alpha''$, $\beta'' \in X^*$ such that

$$ \alpha = \alpha'\alpha'' , \beta = \beta''\beta' \text{ and } n' = \alpha''n\beta'' $$

**Property 1** If $(\alpha; n; \beta)$ and $(\alpha'; n'; \beta')$ are factors of an element $m \in M(F,V)$ one of the three following conditions is satisfied

1. $(\alpha; n; \beta)$ and $(\alpha'; n'; \beta')$ are disjoint

2. $(\alpha; n; \beta)$ is contained in $(\alpha'; n'; \beta')$

3. $(\alpha'; n'; \beta')$ is contained in $(\alpha; n; \beta)$

We omit the proof

**Property 2** $M(F,V)$ is the language generated by the algebraic grammar

$$ \xi = \sum_{f \in F} f(\xi, \xi, \dots, \xi) + \sum_{v \in V} v $$

and thus is an algebraic (context-free) language in $X^*$

This follows immediately from the definition of an algebraic grammar.

## II Rewriting systems on a free magma

Let $M(F,V)$ be the free $F$-magma generated by $V$.

Let $\phi$ be a finite set of symbols called unknown function symbols.

With each $\varphi \in \phi$ is associated an integer $\rho(\varphi)$ called the arity of $\varphi$. We assume that $\phi$ is disjoint from $F \cup V$.

We assume now on that $V$ is finite too and that the elements of $V$
are numbered $v_1, v_2, \dots, v_n$ and we write $\phi = \{\varphi_1, \dots, \varphi_N\}$.

A rewriting system on the free magma $M(F,V)$ is a system of equations of the following form

$$ \sum_i \left\{ \begin{array}{l} \varphi_i(v_1, \dots, v_{\rho(\varphi_i)}) \\ i = 1, \dots, N \end{array} \right\} = \tau_i $$

where for all $i = 1, \dots, N$ $\tau_i$ is a subset of $M(FU\phi, \{v_1, \dots, v_{\rho(\phi_i)}\})$.

Given two words $f$ and $f'$ in $M(FU\phi, V)$ we say that $f'$ derives immediately from $f$ in $\Sigma$ iff there exists a factor $(\alpha; n; \beta)$ of $f$ where $n = \varphi_i(m_1, \dots, m_{\rho(\varphi_i)})$ and $g \in \tau_i$ such that $f' = \alpha g(m_1/v_1, \dots, m_{\rho(\varphi_i)}/v_{\rho(\varphi_i)})^\beta$.

We denote by $g(m_1/v_1, \dots, m_{\rho(\varphi_i)}/v_{\rho(\varphi_i)})$ the result of substituting $m_j$ to every occurrence of $v_j$ in $g$, for all $j = 1, \dots, \rho(\varphi_i)$.

We write $f \xrightarrow{\Sigma} f'$ or simply, when no confusion can arise, $f \to f'$.

We denote by $\Sigma \xrightarrow{*} \Sigma$ or $\Sigma \xrightarrow{\Sigma} \Sigma$ the reflexive and transitive closure of $\Sigma \to \Sigma$ and when $f \Sigma \xrightarrow{*} f'$ we say that $f'$ derives from $f$ in $\Sigma$. From the definition we have that $f \Sigma \xrightarrow{*} f'$ iff there exists a finite sequence of words in $M(FU\phi, V)$, say $f_1, f_2, \dots, f_{k+1}$ such that $f_1 = f, f_{k+1} = f'$ and for all $h = 1, \dots, k$ $f_h \Sigma \xrightarrow{\Sigma} f_{h+1}$.
Such a sequence is called a derivation of $f$ into $f'$ in $\Sigma$.

If $d = \langle f_1, \dots, f_{k+1} \rangle$ is such a derivation let us denote by $(\alpha_h; n_h; \beta_h)$ the factor of $f_h$ such that $f_{h+1}$ is obtained by substituting some $g$ to $n$ in $f_h$.

Then $d$ is said to be a left derivation iff for all $h = 1, \dots, k-1$

$$ |\alpha_h| \le |\alpha_{h+1}| $$

($|\alpha|$ denotes the length of $\alpha$).
The following theorem was proved by Mike Fischer [1] and
will be extremely useful in the sequel.

**Theorem 1:** For all $f, f' \in M(Fu_1^\Z, V)$, $f'$ derives from $f$ in $\Sigma$
iff there exists a left derivation of $f$ into $f'$ in $\Sigma$.

**Proof:** Let $d = \langle f_1, \dots, f_{k+1} \rangle$ a derivation of $f$ into $f'$ in $\Sigma$.

Define $\Pi(d) = \text{card}\{h \in \{1, \dots, k-1\} \mid |\alpha_h| > |\alpha_{h+1}|\}$

$\Pi(d)$ measures how far is $d$ from a left derivation. Indeed we have

$$ \Pi(d) = o \iff d \text{ is a left derivation.} $$

Assuming now that $\Pi(d) > o$ we shall construct another derivation $d'$
from $f$ into $f'$ satisfying $\Pi(d') < \Pi(d)$. This is sufficient to
establish the theorem.

Let $h_o$ be the smallest $h$ such that $|\alpha_{h+1}| < |\alpha_h|$.

We can write $f_{h+1} = \alpha_h w_h \beta_h$ where

$w_h = g(m_1/v_1, \dots, m_\zeta(v_1)/v_\zeta(v_1))$ for some appropriate $g, i$ and $v$.

The condition $|\alpha_{h+1}| < |\alpha_h|$ implies that the factor $(\alpha_h; w_h; \beta_h)$ is
contained in the factor $(\bar{\alpha}_{h+1}; \bar{\gamma}_{h+1}; \beta_{h+1})$ or that these two factors
are disjoint.

If they are disjoint the construction of $d'$ is immediate : we can
write $f_h = \alpha_{h+1} n_{h+1} \alpha' n_h \beta_h$ for some $\alpha'$

$$ f_{h+1} = \alpha_{h+1} \mathfrak{A}_{h+1} \alpha' w_h \beta_h $$

$$ f_{h+2} = \alpha_{h+1} w_{h+1} \alpha' w_h \beta_h $$

Now replace in $d$ the element $f_{h+1}$ by $f'_{h+1} = \alpha_{h+1} w_{h+1} \alpha' n_h \beta_h$.

It is clear that $f_h \to f'_{h+1}$ and $f'_{h+1} \to f_{h+2}$ so that after the
replacement we indeed obtain a derivation $d'$ which satisfies
$\Pi(d') = \Pi(d)$. Suppose now $(\alpha_h; w_h; \beta_h)$ is contained in $(\alpha_{h+1}; n_{h+1}; \beta_{h+1})$

by the form of $n_{h+1} = \varphi_j(m'_1, \dots, m'_\zeta(\varphi_j))$ we know that $(\alpha_h; w_h; \beta_h)$ is
contained in the factors

$$ (\alpha_{h+1} \varphi_j(m'_1, \dots, m'_{\alpha-1}; m'_\alpha; m'_{\alpha+1}, \dots, m'_\zeta(\varphi_j)) \beta_{h+1})^\tau $$
Denote the by $\bar{\alpha}, \bar{\beta}$ the two words such that

$$m'_{e} = \bar{\alpha}w'_{h}\bar{\beta}$$

and let $m''_{e} = \bar{\alpha}n'_{h}\bar{\beta}$.

We have $f_h = \alpha_{h+1} \varphi_j(m'_1, \dots, m'_{e-1}, m''_{e}, m'_{e+1}, \dots, m'_{\varphi_j}(\varphi_j))^{\beta}_{h+1}$

Let $f'_{h+1} = \alpha_{h+1} g(m'_1/v_1, \dots, m'_{e-1}/v_{e-1}, m''_{e}/v_e, \dots, m'_{\varphi_j}(\varphi_j)/v_{\varphi_j}(\varphi_j))$

if $f_{h+2} = \alpha_{h+1} g(m'_1/v_1, \dots, m'_{e-1}/v_{e-1}, m'_{e}/v_e, \dots, m'_{\varphi_j}(\varphi_j)/v_{\varphi_j}(\varphi_j))$

It is clear that $f_h \xrightarrow{\alpha} f'_{h+1}$. To obtain $f_{h+2}$ from $f'_{h+1}$ we need replace $n_h$ by $w_h$ in each occurrence of $m''_e$ coming from an occurrence of $v_e$ in $g$. This can be done easily by a left derivation if one orders these occurrences from left to right and makes the proper replacement in the various occurrences thus ordered, one at each time. We obtain thus a left derivation $\langle f'_{h+1}, f'_{h+2}, \dots, f'_{h+s+1} \rangle$ of $f'_{h+1}$ into $f'_{h+2} = f'_{h+s+1}$ in $\Sigma$ and the sequence

$d' = \langle f_1, f_2, \dots, f_h, f'_{h+1}, f'_{h+2}, \dots, f'_{h+s}, f_{h+2}, f_{h+3}, \dots, f_{k+1} \rangle$ is a left derivation of $f$ into $f'$ in $\Sigma$ satisfying $\Pi(d') < \Pi(d)$

Q.E.D.

We can make here a few remarks

**Remark 1:** If $d = \langle f_1, f_2, \dots, f_{k+1} \rangle$ is a left derivation of $f$ into $f'$ in $\Sigma$, then for all $h = 1, \dots, k$ there exists $\alpha'_{h}(XU_{\phi})$ such that $f' = \alpha'_{h} \alpha'_{h}$

This follows immediately from the definition. As consequences we have the following

**Remark 2:** If $d = \langle f_1, \dots, f_{k+1} \rangle$ is a left derivation of $f$ into $f'$ in $\Sigma$ and $f'$ belongs to $M(F,V)$ then for all $h$ $\alpha'_{h} \in X^{*}$
**Remark 3:** Call a replaceable factor of $m$ any factor of the form $(\alpha; \varphi_j(m_1, \dots, m_\rho(\varphi_j)); \beta)$. Call a replaceable factor maximal iff it is not properly contained in another replaceable factor.

If $d = \langle f_1, \dots, f_{k+1} \rangle$ is a left derivation of $f$ into $f'$ in $\Sigma$ and $f'$ belongs to $M(F,V)$ then

for all $h$ $(\alpha_h; n_h; \beta_h)$ is a maximal replaceable factor.

A maximal replaceable factor can also be called an outermost factor so that in a left derivation $d = \langle f_1, \dots, f_{k+1} \rangle$ of $f$ into $f'$ where $f' \in M(F,V)$, $(\alpha_h; n_h; \beta_h)$ is for all $h$ the leftmost outermost replaceable factor. That is the reason why left derivations are usually called leftmost outermost though the above property holds only when $f' \in M(F,V)$.

### III An order on M(F,V)

We assume now on that $V$ contains a distinguished element $\mathcal{N}$ and we define $\langle \cdot \rangle$ as the coarsest order relation on $M(F,V)$ which is such that $\mathcal{N}\{v$ for all $v \in V$ and which is compatible with the magma structure.

(ie satisfies $\forall f \in F, m_1, \dots, m_{\mathcal{G}(f)}, m_1', \dots, m_{\mathcal{G}(f)}' \in M(F,V)$

$$m_1 \langle m_1', \dots, m_{\mathcal{G}(f)} \rangle \langle m'_{\mathcal{G}(f)} \rangle \Rightarrow f(m_1, \dots, m_{\mathcal{G}(f)}) \langle f(m_1', \dots, m'_{\mathcal{G}(f)}) \rangle$$

On proves easily that

**Property 3** $m \langle m'$ iff there exists $\alpha_1, \dots, \alpha_{t+1} \in X^*$ and $m_1, \dots, m_t \in M(F,V)$ such that

$$m = \alpha_1 \mathcal{N} \alpha_2 \mathcal{N} \dots \alpha_t \mathcal{N} \alpha_{t+1}$$

and $m' = \alpha_1 m_1 \alpha_2 m_2 \dots \alpha_t m_t \alpha_{t+1}$

In other words $m$ is less than $m'$ if one can obtain $m'$ from $m$ by replacing certain occurrences of $\mathcal{N}$ in $m$ by elements of $M(F,V)$
## IV Schematic rewriting systems

The rewriting system $Σ$ is called schematic iff for all $i = 1,...,N$ $τ_i = p_i + Ω$ where $p_i \in M(Fu_φ,V)$.

An interesting property of schematic rewriting systems is basic to our work:

**Theorem 2** If $Σ$ is a schematic rewriting system and $f \in M(Fu_φ,V)$ $f_1, f_2 \in M(F,V)$ are such that

$$f \underset{Σ}{\stackrel{*}{\to}} f_1 \quad \text{and} \quad f \stackrel{*}{\underset{Σ}{\to}} f_2$$

then there exists $f_3$ such that $f \underset{Σ}{\stackrel{*}{\to}} f_3$, $f_1 \prec f_3$ and $f_2 \prec f_3$

*Proof:* The proof is by induction on the sum of the length of the shortest derivations of $f$ into $f_1$ and of $f$ into $f_2$ in $Σ$. Call them $k$ and $e$.

If $k + e = 2$ we certainly have

$$f = α_1 φ_1(m_1, ..., m_ρ(φ_1))β \quad \text{where}$$

$$f' = α_1 p_1(m_1/v_1, ..., m_ρ(φ_1)/v_ρ(φ_1))β \in M(F,V)$$

and the four possibilities arise of

$$f_1 = α_1β$$

$$f_1 = α_1β$$

$$f_1 = f'$$

$$f_1 = f'$$

$$f_2 = α_2β$$

$$f_2 = f'$$

$$f_2 = α_2β$$

$$f_2 = f'$$

In these four cases the existence of $f_3$ is obvious.

Assume now that the theorem has been established for $k'+e' < k+e$ and consider the two left derivations

$d_1 = <g_1, ..., g_{k+1}>$ of $f$ into $f_1$ in $Σ$.

$d_2 = <h_1, ..., h_{e+1}>$ of $f$ into $f_2$ in $Σ$.

If $g_1 = h_1$ the result follows immediately for then $f_1$ and $f_2$ derive from $f' = g_1 = h_1$ by left derivations of length $k-1$ and $e-1$.

Thus we consider only the case where $h_1 \neq g_1$.
$$
\begin{align*}
\text{We can write } f &= \alpha_1 n_1 \beta_1 & g_1 &= \alpha_1 v_1 \beta_1 \\
f &= \alpha_2 n_2 \beta_2 & g_2 &= \alpha_2 v_2 \beta_2
\end{align*}
$$

and we need distinguish several cases.

1) $(\alpha_1; n_1; \beta_1)$ and $(\alpha_2; n_2; \beta_2)$ are disjoint factors of f

We can always assume $|\alpha_1| < |\alpha_2|$ and thus write

$f = \alpha_1 n_1 \gamma n_2 \beta_2$

But this is impossible since $f_2 \in M(F,V)$ and by remark 1 above
$\alpha_2 \in X^*$ which contradicts $\alpha_2 = \alpha_1 n_1 \gamma$

2) $(\alpha_1; n_1; \beta_1)$ is contained in $(\alpha_2; n_2; \beta_2)$

The same remark as in case 1 shows that this inclusion cannot
be proper so that we have (α₁; n₁; β₁) = (α₂; n₂; β₂)

Certainly then one /the words g₁,h₁ is equal to α₁∩β₁,the other
one being equal to α₁pᵢ(mᵢ/v₁, ..., mₚ(φᵢ)/vₚ(φᵢ)) β₁ if

$$
n_1 = \varphi_1(m_1, \dots, m_p(\varphi_i))
$$

There is no less of generality in assuming now on that

$$
g_1 = \alpha_1 \cap \beta_1 \quad \text{and} \quad h_1 = \gamma_1 \cap \delta_1 \quad \text{where} \quad \omega = p_1(m_1 / v_1, \dots)
$$

Since the two derivations $d_1$ and $d_2$ are left derivations we
have

$$
f_1 = \alpha \wedge \beta'_1 \quad \text{where} \quad \beta'_1 \quad \text{derives from} \quad \beta_1
$$

$$
f_2 = \alpha \omega' \beta'_2 \quad \text{where } \omega' \text{ derives from } \omega \text{ and } \beta'_2 \text{ derives from } \beta_1
$$

Certainly the lengths of the left derivations of $\beta_1$ in $\beta'_1$ and $\beta'_2$ are less respectively than k and e. By induction there exists $\beta'_3$ deriving from $\beta_1$ such that $\beta'_1 < \beta'_3$ and $\beta'_2 < \beta'_3$.

It is clear that $f_3 = \alpha\omega'\beta_3$ derives from f and satisfies $f_1' \nmid f_3$ and $f_2' \nmid f_3$.
**Remark 3:** By the above argument we can prove that there exists

$$ \alpha_1, \dots, \alpha_{t+1} \in X^*, w_1, \dots, w_t, w'_1, \dots, w'_t \in M(F,V) $$

such that
$$ f_1 = \alpha_1 w_1 \alpha_2 w_2 \dots \alpha_t w'_t \alpha_{t+1} $$
$$ f_2 = \alpha_1 w'_1 \alpha_2 w'_2 \dots \alpha_t w''_t \alpha_{t+1} $$

and for all $s = 1, \dots, t$ either $w_1$ or $w'_1$ but not both is equal to $\emptyset$. If we denote by $\bar{w}_s$ the element different from $\emptyset$ in $\{w_s, w'_s\}$

it is easy to show that $f_3 = \alpha_1 \bar{w}_1 \alpha_2 \bar{w}_2 \dots \alpha_t \bar{w}_t \alpha_{t+1}$ is a least upper bound of $f_1$ and $f_2$ and that $f_4 = \alpha_1 \cap \alpha_2 \cap \dots \cap \alpha_t \cap \alpha_{t+1}$ is a greatest lower bound of $f_1$ and $f_2$.

Since also $f \xrightarrow{\Sigma} f_3$ and $f \xrightarrow{\Sigma} f_4$ we can state:

If $\Sigma$ is a schematic system on $M(F,V)$ and $f$ an element of $M(FU_\phi,V)$ then the restriction of the order relation on $M(F,V)$ to the set

$$ L(\Sigma, f) = \{f' \in M(F,V) \mid f \xrightarrow{\Sigma} f'\} $$

is a lattice order.

## V Kleene's sequence

In this paragraph we shall exhibit for all schematic rewriting system $\Sigma$ and word $f \in M(FU_\phi,V)$ an increasing sequence

$$ f^{(0)} < f^{(1)} < \dots < f^{(k)} < \dots $$

of elements of $M(F,V)$ such that

$$ \forall f' \quad f \xrightarrow{\Sigma} f' \Rightarrow \exists k \in \mathbb{N} \quad f' < f^{(k)} $$

This sequence, used by Kleene [2] to define recursive functions, will be called the Kleene's sequence of $f$ with respect to $\Sigma$. Let $\Sigma$ be the schematic rewriting system

$$ \Sigma \left\{ \begin{array}{l} \varphi_i (v_1, \dots, v_0 (\varphi_i)) = p_i + \emptyset \\ i = 1, \dots, N \end{array} \right. $$
To $\Sigma$ we associate a mapping $\sigma$ of $M(FU\Phi,V)$ into itself recursively defined by

$$ - \sigma(v) = v $$

$$ - \sigma(\varphi_i(m_1, m_2, \dots, m_\rho(\varphi_i))) = p_i(\sigma(m_1)/v_1, \dots, \sigma(m_\rho(\varphi_i))/v_\rho(\varphi_i)) $$

$$ - \sigma(f(m_1, m_2, \dots, m_\rho(f))) = f(\sigma(m_1), \dots, \sigma(m_\rho(f))) $$

We shall denote by $\Pi$ the mapping of $M(FU\Phi,V)$ into $M(F,V)$ which sends an element $f$ on the element obtained by replacing by $\Omega$ all the maximal replaceable factors of $f$. Precisely

$$ \left\{ \begin{array}{l} - \Pi(v) = v \\ - \Pi(\varphi_i(m_1, m_2, \dots, m_\rho(\varphi_i))) = \Omega \\ - \Pi(f(m_1, m_2, \dots, m_\rho(f))) = f(\Pi(m_1), \dots, \Pi(m_\rho(f))) \end{array} \right. $$

The Kleene's sequence of $f$ with respect to $\Sigma$ is defined by

$$ f^{(k)} = \Pi \sigma^k(f) \text{ where } \sigma^0(f) = f \text{ and } \sigma^{k+1}(f) = \sigma(\sigma^k(f)) $$

**Theorem 3** If there exists a derivation of length $k$ of $f$ into $f'$ in $\Sigma$ and $f'$ belongs to $M(A,V)$ then $f' \nmid f^{(k)}$.

We need to introduce the two relations on $M(FU\Phi,V)$

$f \Rightarrow f'$ iff there exists a factor $(\alpha; n; \beta)$ of $f$ such that
$n = \varphi_i(m_1, \dots, m_\rho(\varphi_i))$ and $f' = \alpha p_i(m_1/v_1, \dots, m_\rho(v_\rho))$

$f \dashrightarrow f'$ iff there exists a factor $(\alpha; n; \beta)$ of $f$ such that
$n = \varphi_i(m_1, \dots, m_\rho(\varphi_i))$ and $f' = \alpha \wedge \beta$

We shall use also the reflexive and transitive closures of these two relations, denoted by $\underset{*}{\Rightarrow}$ and $\stackrel{*}{\Rightarrow}$.

**Lemma 1:** For all $f, f' \in M(FU\Phi, V)$

$$ f \Rightarrow f' \text{ implies } f' \underset{*}{\Rightarrow} \sigma(f) $$
**Proof** By induction on the number of occurrences in $f$ of
elements of $FU\Phi$. We denote this number by $||f||$

The result is obvious for $||f|| = 1$ which implies

$$f = \varphi_i(v_1, \dots, v_p(\varphi_i))$$

Then we consider the three cases

a - $f = f(m_1, \dots, m_p(f))$ in which case $\exists$ $e$ $1 \le e \le p(f)$

such that $m_e \Rightarrow m'_e$ and $f' = f(m_1, \dots, m_{e-1}, m'_e, \dots, m_p(f))$

b1 - $f = \varphi_i(m_1, \dots, m_p(\varphi_i))$ and as in case a $\exists$ $e$ $1 \le e \le p(\varphi_i)$

such that $m_e \Rightarrow m'_e$ and $f' = \varphi_i(m_1, \dots, m_{e-1}, m'_e, \dots, m_p(\varphi_i))$

b2 - $f = \varphi_i(m_1, \dots, m_p(\varphi_i))$ as in case b1 but

$$f' = p_i(m_1/v_1, \dots, m_p(\varphi_i) / v_p(\varphi_i))$$

In all three cases the result follows immediately by induction.

**Lemma 2:** For all $f, f' \in M(FU\Phi, V)$

$$f \Rightarrow f' \text{ implies } \sigma(f) \stackrel{*}{\Rightarrow} \sigma(f')$$

**Proof** by induction on $||f||$

$$\text{If } ||f|| = 1 \text{ then } f' = \sigma(f) \text{ and } f' \stackrel{*}{\Rightarrow} \sigma(f')$$

We consider then the same three cases as in the proof of Lemma 2.

**Lemma 3:** For all $f, f' \in M(FU\Phi, V)$

$$f \stackrel{*}{\Rightarrow} f' \text{ implies } \sigma(f) \stackrel{*}{\Rightarrow} \sigma(f')$$

**Proof** By induction on the length of the derivation of $f$ into $f'$ in $\Sigma$
It will be convenient to call strong derivation of $f$ into $f'$ a
sequence $\langle f_1, \dots, f_{k+1} \rangle$ such that $f_1 = f$, $f_{k+1} = f'$ and for

$$\text{all } j = 1, \dots, k \quad f_j \Rightarrow f_{j+1}$$

Let $k$ be the length of a strong derivation of $f$ into $f'$ in $\Sigma$.
If $k=1$ the result is lemma 2.

Otherwise we consider a strong derivation of length $k$.
By induction $\sigma(f) \stackrel{*}{\Longrightarrow} \sigma(f_k)$. But $f_k \Longrightarrow f_{k+1} = f'$ implies
by lemma 2 that $\sigma(f_k) \stackrel{*}{\Longrightarrow} \sigma(f')$.

**Lemma 4:** For all $f, f' \in M(FU\tilde{\Omega}, V)$ if there exists a strong derivation of length $k$ of $f$ into $f'$ then $f' \Longrightarrow \sigma^k(f)$

*Proof* By induction on $k$

If $k=1$ the result is lemma 1

In the general case we have by induction $f_k \stackrel{*}{\Longrightarrow} \sigma^{k-1}(f)$,
and this implies by lemma 3 $\sigma(f_k) \stackrel{*}{\Longrightarrow} \sigma(\sigma^{k-1}(f)) = \sigma^k(f)$.
But $f_k \Longrightarrow f_{k+1} = f'$ implies by lemma 1 $f' \stackrel{*}{\Longrightarrow} \sigma(f_k)$.

**Lemma 5:** If $f_1 \xrightarrow{*} f_2$ and $f_2 \Longrightarrow f_3$ then there is $f_4$
such that $f_1 \Longrightarrow f_4$ and $f_4 \xrightarrow{*} f_3$

*Proof* We first prove it when $f_1 \xrightarrow{\cdot} f_2$

We can then write

$f_1 = \alpha_1 n_1 \beta_1$ where $n_1 = \varphi_1(m_1, \dots, m_\rho(\varphi_1))$ and
$f_2 = \alpha_1 \beta_1$

and also write

$f_2 = \alpha_2 n_2 \beta_2$ where $n_2 = \varphi_j(m'_1, \dots, m'_\rho(\varphi_j))$ and
$f_3 = \alpha_2 p_j(m'_1/v_1, \dots) \beta_2$

Two cases arise:

1. $(\alpha_1; \Omega; \beta_1)$ and $(\alpha_2; n_2; \beta_2)$ are disjoint factors of $f_2$.
We can assume without loss of generality $|\alpha_1| < |\alpha_2|$.
Then $f_2 = \alpha_1 \Omega \gamma n_2 \beta_2$ and clearly $f_1 = \alpha_1 n_1 \gamma n_2 \beta_2$.
We then take $f_4 = \alpha_1 n_1 \gamma p_j(m'_1/v_1, \dots) \beta_2$.
2 - $(\alpha_1; \Lambda; \beta_1)$ is contained in $(\alpha_2; n_2; \beta_2)$.

We then have indeed $(\alpha_1; \Lambda; \beta_1)$ contained in

$$ \alpha_2 \varphi_j (m'_1, \dots, m'_{e-1} ; m'_e ; m'_{e+1}, \dots, m'_{\rho(\varphi_j)} )^{\beta_2} $$

for some $e \in \{1, \dots, \rho(\varphi_j)\}$.

There exists thus $\bar{\alpha}$ and $\bar{\beta}$ such that $m'_e = \bar{\alpha} \wedge \bar{\beta}$ and if we denote $m''_e = \bar{\alpha} \varphi_i (m'_1, \dots, m'_e, m''_e / \varphi_i)$ we have

$$ f_1 = \alpha_2 \varphi_j (m'_1, \dots, m'_{e-1}, m''_e, m'_{e+1}, \dots, m'_{\rho(\varphi_j)}) $$

$$ \text{Take now } f_4 = \alpha_2 p_j (m'_1/v_1, \dots, m'_{e-1}/v_{e-1}, m''_e/v_e, \dots, m'_{\rho(\varphi_j)}/v_{\rho(\varphi_j)}) $$

It is clear that $f_4 \xrightarrow{*} f_3$ since we need only replace $m''_e$ by $m'_e$, at each occurrence of $m''_e$ coming from an occurrence of $v_e$ in $p_j$.

In the general case we proceed by induction on the length of a derivation of $f_1$ into $f_2$. The following drawing helps

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

Q.E.D.

## Proof of the theorem

We prove that if in a derivation $d = <f_1, \dots, f_{k+1}>$ of $f$ into $f'$ in $\Sigma$:

$\Theta(d) = \text{card}\,\{j \in \{1, \dots, k\} \mid f_j \Rightarrow f_{j+1}\} = h$ then there exists a strong derivation of length less than $h$ into some $f''$ such that $f' = \Pi(f'')$.

The result is obvious if $h=0$ since then $f' = \tau(f)$.

We proceed by induction on $h$.
In the general case call j the smallest index such that
$f_j \rightarrow f_{j+1}$.

By lemma 5 there exists an element $g$ such that

$$f = f_1 \Rightarrow g \text{ and } g \xrightarrow{*} f_{j+1}$$

The derivation of $g$ into $f'$ which can be written

$$d' = g \rightarrow \dots \rightarrow f_{j+1} \rightarrow f_{j+2} \rightarrow \dots \rightarrow f' \text{ is such that}$$

$\Theta(d') = h-1$. By induction there exists a strong derivation of $g$ into some $f''$, of length less than $h-1$ such that $f' = \Pi(f'')$.
Since $f \rightarrow g$ there exists a strong derivation of length less than $h$ of $f$ into $f''$ and the result is proved.

The theorem follows from the remark that

$$f'' \Rightarrow \sigma^k(f) \text{ implies } \Pi(f'') \{ \Pi(\sigma^k(f)) \} = f^{(k)}$$

**Remark 4:** It is easy to see that the Kleene's sequence is increasing for the order $\{\cdot\}$. Q.E.D.

Theorem 2 then follows as an immediate corollary of theorem 3, but not the strengthening of theorem 2 given as remark 3. Moreover as can be seen the proof of theorem 2 given above is much easier than the proof of theorem 3.

# VI Rewriting systems as systems of equations

We shall prove in this paragraph a theorem which is needed afterwards to establish the equivalence between the semantics given by the fix point theorem and the semantics we are constructing.

This theorem 4 is very similar to a theorem of MP Schützenberger [9] for algebraic grammars.

Let $\Sigma$ be the rewriting system on $M(F,V)$

$$\Sigma \left\{ \begin{array}{l} \varphi_1(v_1, \dots, v_\rho(\varphi_1)) = \tau_1 \\ \qquad i = 1, \dots, N \end{array} \right.$$
where for all $i = 1, \dots, N$ $\tau_i \subset M(FU\phi, V)$.

We shall denote by $\mathcal{F}$ the set of n-tuples $t = \langle t_1, \dots, t_N \rangle$

where for all $i = 1, \dots, N$ $t_i \subset M(F, \{v_1, \dots, v_{\rho(\varphi_i)}\})$

And we define on $\mathcal{F}$ a canonical order relation

$$t \subset t' \quad \text{iff} \quad \text{for all } i = 1, \dots, N \quad t_i \subset t_i'$$

$t_i \subset t_i'$ means ordinary set inclusion.

It is easy to see that for this order $\mathcal{F}$ is a complete lattice. Let $t$ be an element of $\mathcal{F}$. We can define a mapping $\lambda_t$ of $M(FU\phi, V)$ into the set of subsets of $M(F, V)$ :

$$\lambda_t(v) = v \quad \text{for all } v \in V$$

$$\lambda_t(f(m_1, \dots, m_{\rho(f)}) = f(\lambda_t(m_1), \dots, \lambda_t(m_{\rho(f)}))$$

$$\lambda_t (\varphi_i(m_1, \dots, m_\rho(\varphi_i)) = \{g(\lambda_t(m_1)/v_1, \dots, \lambda_t(m_\rho(\varphi_i))/v_\rho(\varphi_i)) \mid g \in t_i\}$$

(When $n_1, \dots, n_\rho(f)$ are subsets of $M(F, V)$

$f(n_1, \dots, n_\rho(f))$ denotes the set $\{f(m_1, \dots, m_\rho(f)) \mid m_i \subset n_i\}$)

This mapping extends canonically to a mapping of the set of subsets of $M(FU\phi, V)$ into the set of subsets of $M(F, V)$ if we define

$$\lambda_t(s) = \bigcup \{\lambda_t(m) \mid m \in s\} \quad \text{for } s \subset M(F, V)$$

We can also extend it to a mapping of the set of n-tuples

$$s = \langle s_1, \dots, s_N \rangle \quad \text{where for all } i = 1, \dots, N \quad s_i \subset M(FU\phi, \{v_1, \dots, v_{\rho(i)}\})$$

$$\text{into } \mathcal{F} \text{ by defining}$$
$$\lambda_t(s) = \langle \lambda_t(s_1), \dots, \lambda_t(s_N) \rangle$$

We now associate to $\sum_i$ a mapping $\hat{\sum}$ of $\mathcal{F}$ into $\mathcal{F}$.

$$\hat{\sum}(t) = \lambda_t(t) \quad \text{where } t \text{ is the n-tuple } t = \langle \tau_1, \dots, \tau_N \rangle$$

It is clear from the definition of $\hat{\sum}$ that

$$1 - \hat{\sum} \text{ is an increasing mapping of } \mathcal{F} \text{ into } \mathcal{F}.$$
Namely $t \subset t' \Rightarrow \hat{\Sigma}(t) \subset \hat{\Sigma}(t')$

2. $\hat{\Sigma}$ satisfies the continuity condition.

For all increasing sequence $t^{(1)} \subset t^{(2)} \subset \dots \subset t^{(n)} \subset \dots$

$$ \hat{\Sigma}(\bigcup_{n \in \mathbb{N}} t^{(n)}) = \bigcup_{n \in \mathbb{N}} \hat{\Sigma}(t^{(n)}) $$

Indeed the lowest greater bound of the $t^{(n)}$ is the union, set-theoretically, of the $t^{(n)}$.

We then know from the Knaster-Tarski theorem [2] that $\Sigma$ has a minimal fix point ie that there exists an element $s = \langle s_1, \dots, s_N \rangle$ of $\mathcal{I}$ such that

$$ - \hat{\Sigma}(s) = s $$

- For all $s'$ such that $\hat{\Sigma}(s') = s'$ it is true that $s \subset s'$.

Moreover this minimal fix point is equal to

$$ \hat{\Sigma}^*(\emptyset) = \bigcup_{k \ge 0} \hat{\Sigma}^k(\emptyset) $$
where $\emptyset$ is the n-tuple whose n-components are the empty subset of $M(F,V)$.

This minimal fix point is what it is natural to call the solution of $\Sigma$ considered as a system of equations to be solved in the set of subsets of $M(F,V)$. The method to compute the solution which consists in finding the limit of $\hat{\Sigma}^k(\emptyset)$ is nothing else than the well-known Goursat's method of approximation.

We can now state the theorem

**Theorem 4:** The minimal fix point of $\hat{\Sigma}$ is equal to the n-tuple of subsets of $M(F,V)$, $L = \langle L(\Sigma, \varphi_1), \dots, L(\Sigma, \varphi_N) \rangle$

We abbreviate in $L(\Sigma, \varphi_i)$ the name of the set

$$ L(\Sigma, \varphi_1(v_1, \dots, v_{\rho(\varphi_1)}) = \{f \in M(F,V) | \varphi_1(v_1, \dots, v_{\rho(\varphi_1)}) \stackrel{*}{\rightarrow} f\} $$

We need two lemmas to prove theorem 4.

**Lemma 6:** For all $g \in M(F \cup \Phi, V)$, $g' \in \lambda_L(g)$

$$ g \xrightarrow{\Sigma} g' $$

*Proof* By induction on $||g||$

There is nothing to prove if $||g|| = 0$
Otherwise take $g = f(m_1, \dots, m_{\rho(f)}橋)$.

There exist $m_i' \in \lambda_L m_1, \dots, m_{\rho(f)}$ such that
$g' = f(m_1', \dots, m_{\rho(f)}')$.

Since for all $i$ $||m_i|| < ||g||$ one has by induction $m_i \xrightarrow{*} m_i'$
and thus $g \xrightarrow{\Sigma} g'$.

Take now $g = \varphi_i(m_1, \dots, m_{\rho(\varphi_i)})$. There exists an $h \in \tau_i$
such that $g' \in h(\lambda_L m_1 / v_1, \dots, \lambda_L m_{\rho(\varphi_i)} / v_{\rho(\varphi_i)})$

Call $g$ the word $h(m_1/v_1, \dots, m_{\rho(\varphi_i)}/v_{\rho(\varphi_i)})$

It is clear that $g \xrightarrow{\Sigma} g'$ and that $g'$ is obtained by replacing
in $g'$ the various occurrences of $m_i$, for all $i$, by words in
$\lambda_L m_i$ which derive from $m_i$ by the above remark.

The following lemma was suggested to me by David Park [7] and
allowed me to simplify to a considerable extent a previous proof
of theorem 4.

**Lemma 7:** Let $\hat{\Sigma}(t) = \hat{\Sigma}(t)vt$
and $\hat{\Sigma}^*(t) = \bigcup_{k>0} \hat{\Sigma}^k(t)$

For all $g,g' \in M(FU_{\Phi},V)$

$$
g \xrightarrow{\Sigma} g' \Rightarrow \lambda_t(g') \subset \lambda \hat{\Sigma}^*(t) g
$$

**Proof** We need only prove

$$
g \xrightarrow{\Sigma} g' \Longrightarrow \lambda_t(g') \subset \lambda \hat{\Sigma}(t) g
$$

since the lemma follows from this implication by transitive closure.
This comes from two facts which are both easily verified

1. Let $v_o$ be a variable such that $g \subset M(FU_{\Phi,V} \setminus \{v_o\})$.
If $(\alpha; n; \beta)$ is a factor of $g$

$$
\lambda_t g = \lambda_t (\alpha v_o \beta) (\lambda_t n / v_o)
$$

In words $\lambda_t g$ is obtained by replacing all occurrences of $v_o$ in
$\lambda_t (\alpha v_o \beta)$ by $\lambda_t n$
2. If $g = \alpha n\beta$, $n = \varphi_i(m_1, \dots, m_p(\varphi_i))$
and $g' = \alpha w\beta$, $w = h(m_1/v_1, \dots, m_p(\varphi_i)/v_p(\varphi_i))$

for some $h \in \tau_i$

$$
\lambda_t(g') = \lambda_t(\alpha v_o \beta) (\lambda_t w / v_o)
$$

$$
\lambda \hat{\Sigma}(t) (g) = \lambda \hat{\Sigma}(t) (\alpha v_o \beta) (\lambda \hat{\Sigma}(t) n / v_o)
$$

Now one has immediately $\lambda_t(\alpha v_o \beta) \subset \lambda \hat{\Sigma}(t) (\alpha v_o \beta)$ since
$t \subset \hat{\Sigma}(t)$. And one has also

$\lambda_t w \subset \lambda \hat{\Sigma}(t)^n$ by the very definition where

$$
\lambda \hat{\Sigma}(t) \varphi_i(m_1, \dots, m_p(\varphi_i)) = \{h' (\lambda \hat{\Sigma} (t)^{m_1} / v_1, \dots, \lambda \hat{\Sigma} (t)^{m_p} / v_p(\varphi_i))\} \quad |h' \in \hat{\Sigma}(t)|
$$
since $h \in \tau_i$ implies $\lambda_t(h) \subset \lambda_t(\tau)$

and $\lambda_t w = \{h'' (\lambda_t (m_1)/v_1, \dots, \lambda_t m_p(\varphi_i)/v_p(\varphi_i)) \mid h'' \in \lambda_t(h)\}$

Q.E.D.

We go back to the proof of theorem 4.

Apply lemma 7 to $g = \varphi_i(v_1, \dots, v_p(\varphi_i))$, $g' \in M(F,V)$ and $t = \emptyset$.

$$
\lambda' \emptyset g' = g' \in \lambda \hat{\Sigma}^*(\emptyset) g = (\hat{\Sigma}^*(\emptyset))^t
$$

But a straightforward computation shows that

$$
\hat{\Sigma}^h(\emptyset) = \hat{\Sigma}^k(\emptyset) \quad \text{and consequently} \quad \hat{\Sigma}^{*}(\emptyset) = \hat{\Sigma}^{*}(\emptyset) = s
$$

We have thus proved $L \subset s$.

To prove that $s \subset L$, since $s$ is the smallest fix point of $\hat{\Sigma}$ we
need only prove that $L$ is a fix point of $\hat{\Sigma}$ namely

$L = \hat{\Sigma} (L)$

Lemma 6 proves the inclusion $\hat{\Sigma}(L) \subset L$
To prove that $L \subset \hat{\Sigma}(L)$ apply lemma 7 again with $g \in \tau_1$
$g' \in M(F,V)$, $g \xrightarrow{*} g'$ and $t = L$
$\lambda_L g' = g' \in \lambda_L \hat{\Sigma}^*(L) g$

But $\hat{\Sigma}_{(L)} \subset L$ implies $\hat{\hat{\Sigma}}_{(L)} \subset L$ and $\hat{\Sigma}^*_{(L)} \subset L$. Thus we have
$g' \in \lambda_L g \subset \lambda_L(\tau_1) = (\hat{\Sigma}(L))_1$

Q.E.D.
Second Part: Recursive program schemes and their interpretation

I. Recursive program schemes

The recursive program schemes are recursive programs in which
the basic functions used are unspecified and appear in the pro-
gram as mere symbols. One may always go from a program to a
program scheme by replacing actual functions by arbitrary func-
tion symbols and vice versa if one has a program scheme he gets
a program by replacing function symbols by actual functions de-
fined on some domain.

Let us take an example:

$$
\begin{cases}
\varphi_1(x,y) = & \text{if } x = 0 \text{ then } y \text{ else if } y = 0 \text{ then } x \text{ else } \varphi_1(y, \varphi_2(x,y)) \\
\varphi_2(x,y) = & \text{if } x < y \text{ then } x \text{ else } \varphi_2(x-y,y)
\end{cases}
$$

is a recursive program P

$$
\begin{cases}
\varphi_1(x,y) = h(x,y,h(y,x,\varphi_1(y,\varphi_2(x,y))))) \\
\varphi_2(x,y) = g(x,y,\varphi_2(k(x,y),y))
\end{cases}
$$

is a recursive program scheme $\Sigma$

It is clear that P is obtained from Σ by replacing the function
symbols h,g,k by the actual functions defined on N by

h_I(m,n,p) = if m = 0 then n else p

g_I(m,n,p) = if m < n then m else p

k_I(m,n) = m - n

**Definitions:** A recursive program scheme (deterministic) is a rewriting system on some free magma M(F,V), say

$$
\sum_i \begin{cases} \varphi_i(v_1, \dots, v_{\rho(\varphi_i)}) = \tau_i \\ i = 1, \dots, N \end{cases}
$$

where for all i = 1, ..., N τᵢ ∈ M(F, {v₁, ..., vρ(φᵢ)})

An interpretation I of a recursive program scheme as M(F,V) is
given by

- a non empty domain D_I

- for all f ∈ F a partial mapping f_I : D_I^p(f) → D
We shall call program the pair <Σ,I> of a recursive program scheme Σ and an interpretation I.

As every program <Σ,I> is intended to compute a certain function which we shall denote by $val_I^Σ$ (this function corresponding to $\varphi_1$). The aim of this paper is to give a definition for this computed function: a semantics of recursive program schemes is a way of specifying for all pair <Σ,I> a function $val_I^Σ$. In this respect we describe in this paper a semantics of recursive program schemes: it is certainly not the first to be described nor the last one. We shall also prove the equivalence of our semantics and the most well known two other semantics: the "naive" operational one and the so-called fixpoint as it may be found in the works of semantics D. Scott [10], D. Park [5] A. Mazurkiewicz [5]. A good account of it is in [4].

## II. Discrete domains and discrete interpretations

As it is very awkward to deal with partial mappings we shall do the following given an interpretation I

- extend $D_I$ into $\hat{D}_I$ by adding an element $\omega$ called undefined

- extend the mappings $f_I$ into total mappings $\hat{f}_I$

We need first a definition.

Say that $d_{i_1}, \dots, d_{i_k}$ where $d_{i_1}, \dots, d_{i_k} \in D_I^{\wedge}$, $1 \le i_1 < i_2 < \dots < i_k \le \rho(f)$ determine a value of $f_I$ iff

$$ \forall d_1, \dots, d_\rho(f), d'_1, \dots, d'_\rho(f) \in D: $$

$$ d_{i_1} = d'_{i_1}, \dots, d_{i_k} = d'_{i_k} \Rightarrow $$

$$ \text{either } f(d_1, \dots, d_\rho(f)) = f(d'_1, \dots, d'_\rho(f)) $$

or both $f(d_1, \dots, d_\rho(f))$ and $f(d'_1, \dots, d'_\rho(f))$ are undefined

Denote by $f(\underline{d}_{i_1}, \underline{d}_{i_2}, \dots, \underline{d}_{i_k})$ the value determined by $d_{i_1}, \dots, d_{i_k}$ and set

$$ f(\underline{d}_{i_1}, \dots, \underline{d}_{i_k}) = \begin{cases} \text{the common value of } f(d'_1, \dots, d'_\rho(f)) & \text{for all} \\ d'_1, \dots, d'_\rho(f) & \text{such that } d_{i_1} = d'_1, \dots, d_{i_k} = d'_k \\ \text{if such a value exists} \\ = \omega & \text{if none of the } f(d'_1, \dots, d'_\rho(f)) \text{ is defined.} \end{cases} $$
We then define $\hat{f}_I$ in the following way

$$ \forall d_1, \dots, d_\rho(f) \in D_I : \hat{f}_I(d_1, \dots, d_\rho(f)) = \begin{cases} f_I(d_1, \dots, d_\rho(f)) & \text{if this is defined} \\ \omega & \text{otherwise} \end{cases} $$

$$ \forall 1 \le i_1 < i_2 < \dots < i_k \le \rho(f) \ d_{i_1}, \dots, d_{i_k} \in D_I $$

$$ \hat{f}_I(\omega, \dots, \omega, d_{i_1}, \omega, \dots, \omega, d_{i_2}, \omega, \dots) = \begin{cases} f_I(d_{i_1}, d_{i_2}, \dots, d_{i_k}) & \text{if } d_{i_1}, \dots, d_{i_k} \text{ determine a value of } f_I \\ \omega & \text{otherwise.} \end{cases} $$

**Example:**

For the interpretation I above we shall take

$$ \hat{O}_I = \mathbb{N} \cup \{\omega\} $$

$$ \hat{f}_I (m,n,p) = \begin{cases} f(m,n,p) & \text{if } m = 0 \text{ then } n \text{ else } p \text{ for all } m,n,p \in \mathbb{N} \\ \omega & \text{otherwise} \end{cases} $$

$$ \hat{f}_I (0, n, \omega) = n \text{ for all } n \in \mathbb{N} $$

$$ \hat{f}_I (m, \omega, p) = p \text{ for all } m \in \mathbb{N}^+ , p \in \mathbb{N} $$

$$ \hat{f}_I (m, n, p) = \omega \text{ in all other cases} $$

$$ \hat{g}_I (m,n,p) = \begin{cases} g(m,n,p) & \text{if } m<n \text{ then } m \text{ else } p \text{ for all } m,n,p \in \mathbb{N} \\ \omega & \text{otherwise} \end{cases} $$

$$ \hat{g}_I (m,n,p) = \omega \text{ in all other cases} $$

$$ \hat{k}_I (m,n) = \begin{cases} m-n & \text{if } m \ge n \\ \omega & \text{otherwise.} \end{cases} $$

Let us introduce on $\hat{D}_I$ the partial order $\leq$ by

$$ \forall \delta, \delta' \in \hat{D}_I \quad \delta \le \delta' \iff \delta = \omega \text{ or } \delta = \delta' $$

This order induces an order on $\hat{D}_I^n$ :

$$ \forall <\delta_1, \dots, \delta_n>, <\delta'_1, \dots, \delta'_n> \in \hat{D}_I^n \\ <\delta_1, \dots, \delta_n> \le <\delta'_1, \dots, \delta'_n> \iff \forall i=1, \dots, n \ \delta_i \le \delta'_i . $$
We say that a mapping $\varphi$ of $\hat{D}_I^n$ into $\hat{D}_I$ is increasing iff

$$<\delta_1, \dots, \delta_n> \subseteq <\delta'_1, \dots, \delta'_n> \Rightarrow \varphi(\delta_1, \dots, \delta_n) \subseteq \varphi(\delta'_1, \dots, \delta'_n)$$

One can easily check that the extensions $\hat{f}_I$ of the mappings $f_I$ are increasing mappings. We are thus led to the definition.

A discrete interpretation I of a recursive program scheme on $M(F,V)$ is given by

- a domain $D_I$ containing $\omega$ and ordered by $\subseteq$ in such a way that $\forall \delta, \delta' \in D_I \ \delta \subseteq \delta' \Leftrightarrow \delta = \omega$ or $\delta = \delta'$

- for each $f \in F$ an increasing mapping $f_I$ of $D_I^\rho(f)$ into $D_I$.

### III. Construction of $Val_I \Sigma$

We first describe a mapping of $M(F,\{v_1,\dots,v_n\})$ into $D_I$ associated with an interpretation I and a valuation $v$ where a valuation $v$ is a mapping of $v_1,\dots,v_n$ into $D_I$.

We write $v_i$ for $v(v_i)$.

This mapping is the mapping used by all mathematicians, even unconsciously, to give a value to an expression.

- $(I,v)(\Omega) = \omega$

- $(I,v)(v_i) = v_i$

- $(I,v)(f(m_1, \dots, m_\rho(f))) = f_I((I,v)m_1, \dots, (I,v)m_\rho(f))$.

This mapping $(I,v)$ has the following important property.

**Property:** For all $m, m' \in M(F, \{v_1, \dots, v_n\})$
$$m<m' \Rightarrow (I,v)(m) \subseteq (I,v)(m')$$

**Proof.** It comes easily from the condition imposed on the mapping $f_I$.
We make an induction on $\|m\|$.

If $\|m\| = 0$ then $m = v \in V$ and either $m = \Omega$, $m'$ can be any element of $M(F, \{v_1, \dots, v_n\})$

- $(I,v)(m) = \omega \subseteq d$ whatever is $d \in D_I$

- either $m = v_i \neq \Omega$ and $m' = v_i$ too.
In the general case $m = f(m_1, \dots, m_{\rho(f)})$

and $m' = f(m'_1, \dots, m'_{\rho(f)})$ where for all $i = 1, \dots, \rho(f)$

$$m_i < m'_i$$

since for all $i = 1, \dots, \rho(f)$ $\|m_i\| < \|m\|$ by induction
$(I, \nu)(m_i) \subseteq (I, \nu)(m'_i)$

and
$(I, \nu)(m) = f_I((I, \nu)m_1, \dots, (I, \nu)m_{\rho(f)}) \subseteq$

$$(I, \nu)(m') = f_I((I, \nu)m'_1, \dots, (I, \nu)m'_{\rho(f)})$$

since $f_I$ is increasing.

Let us now associate with the program scheme $\Sigma$

$$\Sigma \left\{ \begin{array}{l} \varphi_i(v_1, \dots, v_{\rho(\varphi i)}) = \tau_i \\ i = 1, \dots, N \end{array} \right. = \tau$$

the schematic rewriting system $\bar{\Sigma}$

$$\bar{\Sigma} \left\{ \begin{array}{l} \varphi_i(v_1, \dots, v_{\rho(\varphi i)}) = \tau_i + \Omega \\ i = 1, \dots, N \end{array} \right. = \tau$$

We can define a mapping of $L(\bar{\Sigma}, \varphi_1)$ into $D_I$, corresponding to an
interpretation $I$ and a valuation $\nu : v_1, \dots, v_{\rho(\varphi_1)} \to D$ by using
theorem 2. Indeed if $m, m' \in L(\bar{\Sigma}, \varphi_1)$

$$(I, \nu)(m) \neq \omega \text{ and } (I, \nu)(m') = \omega$$

$$(I, \nu)(m) = (I, \nu)(m').$$

For there exists $m'' \in L(\bar{\Sigma}, \varphi_1)$ such that $m<m''$ and $m'<m''$:

from property 1 we get $(I, \nu)(m) \subseteq (I, \nu)(m'')$ and

$$(I, \nu)(m') \subseteq (I, \nu)(m'') \text{ but this means}$$

$$(I, \nu)(m) = (I, \nu)(m'') \text{ and } (I, \nu)(m') = (I, \nu)(m'').$$

This gives us a semantics if we state:

**Definition:** The function computed by $\Sigma$ under interpretation $I$ is
$\text{val}_I(\Sigma)(\nu) = \text{the common value of } (I, \nu)(m), \text{ for all } m \in L(\bar{\Sigma}, \varphi_1)$
such that $(I, \nu)(m) \neq \omega$ if such an $m$ exists
$= \omega$ otherwise.

We shall refer to the semantics thus defined as the "language semantics".
#### IV. Operational semantics

The usual naive way in which $val_I(\Sigma)$ is defined goes that way. One builds a sequence of expressions $\epsilon M(F \cup \Phi, D)$

$$e_0, e_1, \dots, e_n, \dots \\ \text{where } e_0 = \varphi_1 (v_1, \dots, v_\rho (\varphi))$$

and for all n we have one of the two following relations between $e_n$ and $e_{n+1}$:

1. There exists a factor $(\alpha; n; \beta)$ of $e_n$ such that

$$n = \varphi_i(m_1, \dots, m_\rho(\varphi_i)) \text{ and}$$

$$e_{n+1} = \alpha \tau_i \left( \frac{m_1}{v_1}, \dots, \frac{m_\rho(\varphi_i)}{v_\rho(\varphi_i)} \right)^{\beta}.$$

We denote this relation by $\Rightarrow$ and we then say that $e_{n+1}$ follows $e_n$ by rewriting.

2. There exists a factor $(\alpha; n; \beta)$ of $e_n$ such that

$$n = f(m_1, \dots, m_\rho(f))$$

- there exists a sequence of indices $1 \le i_1 < i_2 < \dots < i_k \le \rho(f)$ such that $m_{i_1}, m_{i_2}, \dots, m_{i_k} \in D_I$ and $m_{i_1}, \dots, m_{i_k}$ determine a value of $f_I$

$$e_{n+1} = \alpha f_I (\underline{m}_{i_1}, \underline{m}_{i_2}, \dots, \underline{m}_{i_k})$$

We denote this relation by $\leftrightarrow$ and we then say that $e_{n+1}$ follows $e_n$ by reduction.

A sequence $e_0, e_1, \dots, e_n, \dots$ is called a computation sequence of $\Sigma$ under I at point v. It is said to terminate iff there exists an n such that $e_n \in D_I$ (indeed then no $e_{n+1}$ can follow $e_n$), and in case it terminates in $e_n$, $e_n$ is called the result of the computation.

In order to define the computed function we need first establish the theorem.

**Theorem 5.** The results of two terminating computation sequences of $\Sigma$ under I at point v, when they are both defined are equal. We leave the proof for some time and rather define:
**Definition:** The value of the function computed by Σ at a point v is according to the operational semantics equal to the common result of all terminating computation sequences of Σ under I at point v which give a defined result if any and is undefined otherwise.

We have then

**Theorem 6.** The language semantics and the operational semantics are equivalent, in other words they define the same function $val_I(Σ)$ given Σ and I.

*Proof* We need two lemmas

**Lemma 8** For all $e_1, e_2, e_3 \in \mathcal{M}(F \cup \Phi, D_I)$

if $e_1 \stackrel{*}{\to} e_2$ and $e_2 \to e_3$ then there exists $e_4$ such that $e_1 \to e_4$ and $e_4 \stackrel{*}{\to} e_3$.

The proof of this lemma is identical to the proof of lemma 5.

**Lemma 9** For every terminating computation sequence of Σ under I at point v there exists a word $m \in L(\bar{\Sigma}, \phi_1)$ such that the result of this terminating computation sequence is $(I, v)(m)$.

*Proof* By induction from lemma 8 we can prove that if

$e_0, e_1, \dots, e_n$ is a terminating computation sequence, then there exists

$e'_0, e'_1, \dots, e'_h, e'_{h+1}, \dots, e'_n$, where

for all $i=0, \dots, h-1$ $e'_i \to e'_{i+1}$

for all $i=h, \dots, n'-1$ $e'_i \to e'_{i+1}$

$e_0 = e'_0 \qquad e_n = e'_n$

Indeed h is the exact number of rewrites in the original computation sequence.

Now consider $\epsilon_0 = \phi_1(v_1, \dots, v_\rho(\phi_1))$.

Clearly $e_0 = \epsilon_0(v'_1/v_1, \dots, v'_\rho(\phi_1)/v_\rho(\phi_1))$.
It is extremely easy to show that one can build a sequence

$\epsilon_0, \epsilon_1, \dots, \epsilon_h$ such that for all $i = 0, \dots, h-1$ $\epsilon_i \to \bar{\epsilon}_{i+1}$

and

$e'_i = \epsilon_i (v_1/v_1, \dots, v_{\rho(\varphi 1)}/v_{\rho(\varphi 1)}) .$

Consider then $m = \pi(\epsilon_h)$ where $\pi$ is the mapping which replaces all replaceable factors by $\Omega$, already used in the proof of theorem 3.

We have $(I, \nu)(m) = e_n$ for we can apply to

$m(v_1/v_1, \dots, v_{\rho(\varphi 1)}/v_{\rho(\varphi 1)})$ exactly the same sequence of reduction that applied to $e'_h$ leads to the result $e_n$. q.e.d.

**Remark:** In the literature the word operational semantics is generally used in connection with a computational rule: such a rule determines uniquely a computation sequence starting with a given $e_0 = \varphi_1(v_1, \dots, v_{\rho(\varphi 1)})$ by specifying at each step which reduction or rewriting should be applied. The value $val_I^\Sigma(\nu)$ is then taken as the result of this computation sequence if it terminates or as $\omega$ if it does not terminate.

Obviously we have the result that the function computed by $\Sigma$ under $I$ according to a computation rule $R$, denote it by $val_I^R \Sigma$, satisfies

$$val_I^R \Sigma \subseteq val_I \Sigma \text{ (cf Cadiou [11])}.$$

We warn here the reader that the so called "leftmost outermost" or "call by name" computation rule is not sufficient to compute $val_I \Sigma$ in all cases. For example we may have

$$\varphi(x,y) = h(\varphi(x,y), k(x,y),y)$$

and the interpretation $h_I(m,n,p) = \text{if } n = 0 \text{ then } p \text{ else } m$ for all $m,n,p \in \mathbb{N}$ $u\{\omega\}$

$$k_I(m,n) = m-n.$$

Then the leftmost outermost computation sequence starting with $\varphi(2,2)$ does not terminate

$$\varphi(2,2), h(\varphi(2,2), k(2,2),2), h(h(\varphi(2,2), k(2,2),2), k(2,2),2)$$
Nevertheless this computation rule is easily shown to lead to
the result $\text{val}_I \Sigma(v)$ if this exists if the interpretation satisfies

$$ \forall v \in \mathcal{F} \quad \begin{array}{l} d_{i_1}, \dots, d_{i_k} \text{ determine a value of } f_I \text{ iff} \\ i_1 = 1, i_2 = 2, \dots, i_k = k. \end{array} $$

This follows easily from th 1 and lemma 9. An important case is
when the only non total function $f_I$ is the function *if then else*.
On the contrary a computation rule always leads to the resulting
value $\text{val}_I \Sigma$ if this exists: this is the rule which constructs
as a computation sequence the analogous of the Kleene's sequence.

At step 2n we substitute $\tau_i$ for $\varphi_i$ in all replaceable factors
to get $e_{2n+1}$ and then we make all possible reductions to get
$e_{2n+2}$ from $e_{2n+1}$. The fact that this sequence always leads to
the result $\text{val}_I \Sigma(v)$ follows easily from theorem 3 and lemma 9.

As a corollary we get that $\text{val}_I \Sigma$ is also the function computed by
$\Sigma$ under I according to Kleene's definition of recursive functions
[2].

## V. Fix-point semantics

We need in order to define it a number of definitions.

We first denote by $\Delta$ the set of all increasing mappings of
$\hat{D}_I^n$ into $D_I$, and we canonically extend the order $\le$ to $\Delta$ by:

For all $\varphi, \psi \in \Delta$

$$ \varphi \le \psi \text{ iff } \begin{array}{l} 1. \varphi \text{ and } \psi \text{ have the same arity } n = \rho(\varphi) = \rho(\psi) \\ 2. \forall \delta_1, \dots, \delta_n \in \hat{D}_I \ \varphi(\delta_1, \dots, \delta_n) \le \psi(\delta_1, \dots, \delta_n) . \end{array} $$

Let us consider a directed subset $\Delta'$ of $\Delta$. A directed subset $\Delta'$
is a subset which satisfies:

For all $\varphi, \psi \in \Delta'$ there exists $\theta \in \Delta'$ such that $\varphi \le \theta$ and $\psi \le \theta$
We can easily prove that $\Delta'$ has a least upper bound in $\Delta$ if
that there exists a function $\llbracket \phi | \phi \in \Delta' \rrbracket$ with the two pro-
perties that

$$
1. \ \forall \phi \in \Delta' \quad \phi \in \llbracket \phi | \phi \in \Delta' \rrbracket
$$

$$
2. \ \forall \theta [\forall \varphi : \varphi \leq \theta \rightarrow \bigwedge \{\varphi | \varphi \in \Delta'\} \leq \theta]
$$

We repeat the argument which led to the definition of val$_I$Σ
above:

just take Θ(δ₁, ..., δₙ) = the common value of φ(δ₁, ..., δₙ) for
which φ(δ₁, ..., δₙ) ≠ ω if any such
exists
= ω otherwise.

A partially ordered set in which all directed subsets have a
least upper bound is called a complete partially ordered set
(abbreviated cpo).

Similar definitions and properties hold obviously for $\Delta^N$.

We now associate with the recursive program scheme Σ and the
discrete interpretation I a mapping $\hat{\Sigma}_I$ of $\Delta^N$ into itself.

This mapping is described by

$$
\hat{\Sigma}_I (\phi_1, \dots, \phi_N) (v_1, \dots, v_p(\phi_1)) = \langle (I, v) \pi(\tau_1), \dots, (I, v) \pi(\tau_N) \rangle
$$

where (I, v) and π are the mappings described above.

This mapping $\hat{\Sigma}_I$ is continuous which means that:

For every directed subset $\Delta'$ of $\Delta^N$

$$
\begin{align*}
\hat{\Sigma}_I (\llbracket \{\langle \phi_1, \dots, \phi_N \rangle \mid \langle \phi_1, \dots, \phi_N \rangle \in \Delta' \} \rrbracket) \\
&= \llbracket \hat{\Sigma}_I (\phi_1, \dots, \phi_N) \mid \langle \phi_1, \dots, \phi_N \rangle \in \Delta' \rrbracket
\end{align*}
$$

the right hand side being well defined since $\hat{\Sigma}_I$ is increasing
and this maps a directed subset on a directed subset.
This continuity follows easily from the definition of the lub
we gave.

Now we know that any continuous mapping of a cpo into itself
has a least fix point. The least fix point of $\hat{\Sigma}_I$ is given by

$$s_I = \bigsqcup_{k \ge 1} \hat{\Sigma}_I^k (\omega)$$

where $\omega$ is the n-tuple of functions whose components are all the
constant function equal to $\omega$. Since $\hat{\Sigma}_I$ is increasing the set
$\{\hat{\Sigma}_I^k(\omega) | k \ge 1\}$ is a chain and a fortiori a directed subset so
that the lub is well defined.

The fix point semantics takes $(s_I)_1$ as the definition for the
function computed by $\Sigma$ under I. And we can state

**Theorem 7:** The fix point semantics and the language semantics
are equivalent. In other words $s_I = \text{val}_I \Sigma$.

*Proof* We rely mainly on theorem 4.

If A is a directed subset of M(F,V) for the order < we have seen
how to define $A_I$ which is the function given by

$A_I(v_1, \dots, v_n) =$ the common value of $(I,v)m$, for all $m \in A$
such that $(I,v)m * \omega$ if any such $m$ exists
$= \omega$ otherwise.

The two following facts are true and both easily verified.

1. If $t$ is a directed subset of $\mathcal{C}$ (see the definition above in § VI of Part I) then $\hat{\Sigma}(t)$ is directed (both for $<$).

2. $(\hat{\Sigma}(t))_I = \hat{\Sigma}_I(t_I)$

It follows that $\bigsqcup_{k \ge 1} \hat{\Sigma}^k(\Omega)_I = \bigsqcup_{k \ge 1} \hat{\Sigma}_I^k(\omega)$

On the right hand side one has $s_I$. On the left hand side one
has $L_I$. But we know from theorem 4 that $(L_I)_1 = \text{val}_I \Sigma$. q.e.d.
**Remark:** It is interesting at this point to see that the mapping I which maps directed subsets of $\mathcal{L}$ into $\Delta$ is order preserving when the set of subsets of $\mathcal{L}$ is ordered by inclusion and $\Delta^N$ by $\subseteq$.

This is not sufficient however to induce from the fact that $L$ is the smallest fix point of $\hat{\Sigma}$ the fact that $L_I$ is the smallest fixpoint of $\hat{\Sigma}_I$. This however is true for we have

If $\langle\varphi_1, \dots, \varphi_N\rangle \in \Delta^N$ is such that for some directed subset of $\mathcal{L}$

$$ \langle\varphi_1, \dots, \varphi_N\rangle = t_I \text{ then } \hat{\Sigma}_I(\varphi_1, \dots, \varphi_N) = \hat{\Sigma}(t)_I. $$
Bibliography

[1] M. Fischer, *Grammars with macro-like instructions*, Thesis, Harvard (1969)

[2] S. Kleene, *Introduction to metamathematics*, McGraw Hill, New York (1952)

[3] J. McCarthy, *A basis for a mathematical theory of computation*, in Computer Programming and Formal Systems, North-Holland, Amsterdam (1963)

[4] Z. Manna and J. Vuillemin, *Fix point approach to the theory of computation*, Communication of the ACM 15 (1972), 528-536

[5] A. Mazurkiewicz, *Proving algorithms by tail functions*, Information and Control 18 (1971), 220-226

[6] D. Park, *Fix point induction and proof of program semantics* in Machine Intelligence, Vol. 5, Edinburgh (1969)

[7] D. Park, *Personal communication* (1973)

[8] M. Nivat, *Langages algébriques sur le magma libre et sémantique des schémas de programmes*, in Automata, Languages and Programming, North-Holland, Amsterdam (1972)

[9] M.P. Schützenberger, *Pushdown automata and context-free languages*, Information and Control 6 (1963), 246-264

[10] D. Scott, *The lattice of flow diagrams*, Technical Monograph PRG 3, Oxford Univ., Computation Lab. (1970)

[11] J.M. Cadiou, *Doctoral thesis* (1972)