Dw: 03638 RR262

IRIA
laboria

Institut de Recherche
d'Informatique
et d'Automatique

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

laboratoire de recherche
en informatique
et automatique

NON DETERMINISTIC
RECURSIVE
PROGRAM SCHEMES

A. ARNOLD
M. NIVAT

Rapport de Recherche N° 262

Novembre 1977

12p.
NON DETERMINISTIC RECURSIVE PROGRAM SCHEMES

A. Arnold*, M. Nivat**

Résumé :

On étend aux schémas de programme récursifs non déterministes les méthodes et résultats qui permettent de définir dans le cas déterministe la sémantique de ces schémas. On montre que sous certaines hypothèses naturelles l'ensemble des arbres finis et infinis engendrés est le plus grand point fixe de la fonctionnelle habituellement attachée au schéma.

Abstract :

One extends to non deterministic recursive program schemes the methods and results which permit to define the semantics of such schemes in the deterministic case. Under natural hypotheses the set of finite and infinite trees generated by a scheme is proved to be the greatest fixed point of the functional usually attached to the scheme.

<footnote>* Université de Lille I</footnote>

<footnote>** Université de Paris VII (Lab. 248 Informatique Théorique et Programmation) et IRIA.</footnote>
NON DETERMINISTIC RECURSIVE PROGRAM SCHEMES

A. Arnold* and M. Nivat**

A number of recent papers [4,13,14] have demonstrated the interest of attaching to the recursive program scheme S : $\phi_1(x_1, ..., x_{n_1}) = t_i ; i=1, ..., N$ the infinite tree which it computes when freely interpreted in the complete free ordered magma $M^{\infty}(F, V)$. Indeed the computed function, for any interpretation I, is a morphic image of this infinite tree, $T(S, \phi_1(x_1, ..., x_{n_1}))$. The well known equivalence between operational and denotational semantics comes from the fact that $T(S, \phi, (x_1, ..., x_{n_1}))$ is both

- the 1.u.b. of the tree language generated by S considered as an algebraic tree grammar, this language being directed

- the first component of the least fixed point of the mapping $\hat{S}$ of $M^{\infty}(F, V)^N$ into itself which is canonically attached to S.

In the non deterministic case i.e. when each equation in S may have several right hand members (which we separate by the symbol *or*) one is tempted to intend the same construction in order to define the semantics. But then at least two problems arise :

1. Freely interpreted in $M^{\infty}(F, V)$ the non deterministic program S does not compute one but a set of infinite trees. The language generated by S, as an algebraic grammar, is no longer directed and the computed infinite trees are 1.u.b.'s of increasing subsequences but not all 1.u.b. of an increasing subsequence correspond to an actual computation of S.

2. As pointed by Hennessy-Ashcroft [7] there is no hope to get this set of infinite trees as the least fixed point of $\hat{S}$ for any order defined on $(M^{\infty}(F, V))^N$. We prove on the contrary that under some weak and natural hypothesis the same set is the first component of the greatest fixed point of the same $\hat{S}$ in $(\hat{M}^{\infty}(F, V))^N$ simply ordered by inclusion.

<footnote>* Université de Lille I</footnote>

<footnote>** Université Paris VII (LA 248 Informatique Théorique et Programmation) et IRIA</footnote>
# I. DEFINITIONS and NOTATIONS

We recall here some definitions and notations from [4].

F is a set of function symbols, each $f \in F$ given with an arity $\rho(f) \in \mathbb{N}$.

$V = \{x_1, \dots, x_k\}$ is a finite set of variables disjoint from F.

$M(F,V)$ is the free $F$-magma generated by $V$: its elements will be called finite $F$-trees or simply finite trees.

If $\Omega$ does not belong to $F \cup V$, $M(F \cup \{\Omega\}, V)$ also written $M_{\Omega}(F, V)$, where $\rho(\Omega) = 0$, is ordered by the syntactic order $\prec$. It can then be completed by the standard "completion by ideals" to get $M_{\Omega}^{\infty}(F, V)$ which can be viewed as $M_{\Omega}(F, V)$ with added infinite trees which are the least upper bounds of the directed subsets of $M_{\Omega}(F, V)$. From now on we shall denote by a small letter $t$, $t'$, $t_i$, $u$, $v$, ... a finite tree and by a capital letter $T$, $T'$, $T_i$, $U$, $V$, ... a finite or infinite tree.

# II. NON DETERMINISTIC RECURSIVE PROGRAM SCHEME

Let $\Phi = \{\phi_1, \dots, \phi_N\}$ be a set of unknown function symbols disjoint from $F \cup V$. The arity of $\phi_i$ is denoted by $n_i$. A non deterministic recursive program scheme (abbreviated ndrps) is a system of equations of the form

$$ S \left\{ \begin{array}{l} \phi_i(x_1, \dots, x_{n_i}) = t_i \\ i = 1, \dots, N \end{array} \right. $$

where $t_i \in M(F \cup \Phi \cup \{\text{or}\}, \{x, \dots, x_{n_i}\})$ for all $i \in [N]$.

The special symbol *or* has arity 2.

We first define a computation sequence of $S$. This notion is similar to the notion of computation sequence for an ordinary (deterministic) recursive program scheme : the role of *or* is to express a possibility of choice.

To be precise a computation sequence is a possibly infinite sequence $u_1, u_2, \dots, u_n, \dots$ of elements of $M(F \cup \Phi \cup \{\text{or}\}, V)$ where for all $i$, $u_i \to_S u_{i+1}$.
which means that either $u_i = \alpha\phi_j(v_1, \dots, v_{n_j})\beta$ and $u_{i+1} = \alpha t_j[v_1/x_1, \dots, v_{n_i}/x_{n_i}]\beta$
or $n_i = \alpha \underline{or}(v_1, v_2)\beta$ and $u_{i+1} = \alpha v_1\beta$ or $\alpha v_2\beta$.

In fact what we define here is the most general notion of computation sequence which corresponds to "call by name". A more restricted notion corresponds to "call by value" which in the non deterministic case leads to completely different re-results, see [1], and will not be treated here. An treatment of call by value analogous to our present treatment of call by name is better carried of in the framework of the theory of magmoïds, see [2], and will be given elsewhere by the authors.

What is clear from the definition is that there is a whole set of finite and infinite computation sequence of S from $t = u_1$. We now define what is the result of a computation sequence. A computation sequence $u_1, \dots, u_n$ terminates at n with result $u_n$ if and only if there does not exist v such that $u_n \to v$ that is if and only if there is no occurrence of *or* nor of any $\phi_i$ in $u_n$. Thus the result $u_n$ of a finite terminating computation sequence belongs to $M(F,V)$. The set of results of terminating computing sequences from t is denoted $\text{Res}_S(t)$.

In order to define the result of non terminating (or infinite) computation sequences we need a definition and lemma.

Define the $F$-morphisme $\omega$ of $M(F \cup \Phi \cup \underline{\{or\}}, V)$ into $M_\Omega(F, V)$ by the induction

$$ - \omega(x) = x $$

$$ - \rho(f) = 0 \implies \omega(f) = f $$

$$ - \omega(f(u_1, \dots, u_{\rho(f)})) = f(\omega(u_1), \dots, \omega(u_{\rho(f)})) $$

$$ - \omega(\phi_j(u_1, \dots, u_{n_j})) = \Omega $$

$$ - \omega(\underline{or}(u_1, u_2)) = \Omega. $$

**Lemma 1** : For all $u, v \in M(F \cup \Phi \cup \underline{\{or\}}, V)$ $u \to v$ implies $\omega(u) < \omega(v)$.

From this lemma we get that for all infinite computation sequence $u_1, u_2, \dots, u_n, \dots$ the sequence $\omega(u_1), \omega(u_2), \dots, \omega(u_n), \dots$ is increasing in $M_\Omega(F, V)$ ordered by $\prec$ and thus has a least upper bound $\text{Sup}_i \omega(u_i) \in M_\Omega^\infty(F, V)$. But in fact we are only interested in results belonging to $M^\infty(F, V)$ whence the definition.

**Definition** : The infinite computation sequence $u_1, \dots, u_n, \dots$ is terminal iff one of
the three equivalent conditions holds.

1. $\sup_i \omega(u_i) \in M^\infty(F, V)$

$2. \text{ For all } v \in M_{\Omega}^{\infty}(F, V) \\ (\forall i \in N : \omega(u_i) < v) \Longrightarrow v = \sup_i \omega(u_i)$

$3. \quad \bigcap_i \{v \in M_{\Omega}^{\infty}(F, V) \mid \rho(\omega_i) < v\} = \{\sup_i \omega(u_i)\}$

The result of the infinite terminal computation sequence $u_1, \dots, u_n, \dots$ is then defined as $\sup_i \omega(u_i)$ and we denote by $\text{Res}_S^\infty(t)$ the set of results of all infinite terminal computation sequences from $t$. These definitions of computation sequences and their results correspond exactly to our intuitive idea of what can be computed by $S$, as a program operating on the domain $M^\infty(F, V)$. Especially one should remark that $\Omega$ acts as an auxiliary symbol needed for the definition of the result and must not appear in the result itself. This definition also covers the deterministic case and is equivalent to the definition of the computed tree given in that case [4,14].

### Examples

$$1. \quad S_1 : \phi(x) = x \text{ or } s(\phi(x))$$

(we also use `or` as an infix operator, in the most usual way). $\text{Res}_S^\infty(\phi(x))$ is clearly $\{s^n(x) \mid n \in \mathbb{N}\}$ since all the terminating finite computation sequences are of the form $\phi(x) \to s(\phi(x)) \to s^2(\phi(x)) \to \dots \to s^n(\phi(x)) \to s^n(x)$. Clearly also the only possible infinite computation sequence is $\phi(x) \to s(\phi(x)) \to \dots \to s^n(\phi(x)) \to s^{n+1}(\phi(x)) \to \dots$ and is terminal since $\sup_i s^n(\Omega) = \sup_i \in M^\infty(\{s\}, \{x\})$. Whence $\text{Res}_S^\infty(\phi(x)) = \{s^\infty\}$.

$$2. \quad S_2 : \phi(x) = x \text{ or } \phi(s(x))$$

We have $\text{Res}_{S_2}(\phi(x)) = \text{Res}_{S_1}(\phi(x))$. But the only infinite computation sequence of $S_2$ from $\phi(x)$ is $\phi(x) \to \phi(s^1(x)) \to \phi(s^2(x)) \to \dots \to \phi(s^n(x)) \to \dots$ and is not terminal ($\omega(\phi(s^n(x))) = \Omega$ for all $n$) whence $\text{Res}_{S_2}^\infty(\phi(x)) = \emptyset$.

The operational semantics of ndrps now defines the function computed by $S$ as the mapping $\text{val } S$ of $M^\infty(F, V)^{n_1}$ into $\mathcal{P}(M^\infty(F, V))$ given by
$$ \text{val } S(U_1, \dots, U_{n_1}) = \{T[U_1/x_1, \dots, U_{n_1}/x_{n_1}] \mid T \in \text{Res}_S(\phi_1(x_1, \dots, x_{n_1})) \\ \phantom{\text{val } S(U_1, \dots, U_{n_1}) = \{T[U_1/x_1, \dots, U_{n_1}/x_{n_1}] \mid} \text{ u } \text{Res}_S^\infty(\phi_1(x_1, \dots, x_{n_1})) \} $$
The substitution $T[U_1/x_1, \dots, U_{n_1}/x_{n_1}]$ is defined by
$$ \sup \{t[u_1/x_1, \dots, u_{n_1}/x_{n_1}] \mid t \prec T, u_i \prec U_i\}. $$

There is no difficulty in verifying that this set is directed.

### III. DENOTATIONAL SEMANTICS

In this section we try to give an alternative equivalent definition of the computed function val S, for a ndrps $\hat{S}$. Since this new definition amounts to define val S as the component of the fixed point of some functional $\hat{S}$ attached to S we shall call this semantics denotational as in [12]. We first notice that val S is a one many-function of $M^\infty(F,V)^{\mathbb{N}}$ into $M^\infty(F,V)$ has the very special property of being represented by a subset of $M^\infty(F,V)$. Reciprocally if A is a subset of $M^\infty(F,V)$ it defines the one many function $g_A(U_1, \dots, U_K) = \{T[U_1/x_1, \dots, U_K/x_K] \mid T \in A\}$. Since our aim is to retrieve val S as some fixed point of some functional $\hat{S}$ we can look for $\hat{S}$ being a mapping of $(\mathcal{F}(M^\infty(F,V)))^N$ into itself.

In a natural way we are thus lead to consider $\hat{S}$ given by
$$ \hat{S}(\langle A_1, \dots, A_N \rangle) = \langle t_1[A_1/\phi_1, \dots, A_N/\phi_N], \dots, t_N[A_1/\phi_1, \dots, A_N/\phi_N] \rangle \text{ where the substitution } \sigma = t \rightsquigarrow t[A_1/\phi_1, \dots, A_N/\phi_N] \text{ is inductively defined by} $$

$$ - \sigma(x) = \{x\} $$

$$ - \sigma(f(u_1, \dots, u_{\rho(f)}) ) = \{f(v_1, \dots, v_{\rho(f)}) \mid v_i \in \sigma(u_i)\} $$

$$ - \sigma(\underline{or}(u_1, u_2)) = \sigma(u_1) \cup \sigma(u_2) $$

$$ - \sigma(\phi_i(u_1, \dots, u_{n_i})) = \bigcup_{T \in A_i} T[\sigma(u_1)/x_1, \dots, \sigma(u_{n_i})/x_{n_i}] $$

We use the notion of OI-substitution [6] (also called "greffe complete" [3]) to define

$$ T[B_1/x_1, \dots, B_n/x_n] \text{ when T is finite.} $$

Let $\tau$ be the mapping $T \rightsquigarrow T[B_1/x_1, \dots, B_n/x_n]$, $\tau$ is given by

$$ - \tau(x_i) = B_i \quad i=1, \dots, n $$

$$ - \tau(x_j) = \{x_j\} \quad j>n $$

$$ - \tau(f(u_1, \dots, u_S(f))) = \{f(v_1, \dots, v_S(f)) \mid v_i \in \tau(u_i)\} $$

And this substitution is extended to infinite trees using the continuity. Namely
$W \in \tau(T)$ if and only if there exists an increasing sequence $w_1, \dots, w_n, \dots$ and an increasing sequence $t_1, \dots, t_m, \dots$ such that $\text{Sup}\{t_m\} = T$, $\text{Sup}\{w_n\} = W$ and for all $i \in \mathbb{N}$, $w_i \in \tau(t_i)$.

One should remark that $\hat{S}$ maps $(\mathcal{A}^N(M(F, V)))^N$ into itself. Thus restricted to finite trees, $\hat{S}$ is the mapping which allows to define algebraic tree languages as least fixed points and we can rephrase the theorem of algebricity of [9].

**Theorem 1 :** The $N$-vector of subsets of $M(F, V)$

$\text{Res}_S = \langle \text{Res}_S \phi_1(v_1, \dots, v_{n_1}), \dots, \text{Res}_S \phi_N(v_1, \dots, v_{n_N}) \rangle$ is the least fixed point of $\hat{S}$ in $(\mathcal{A}^N(M(F, V)))^N$. $\text{Res}_S$ is also the least fixed point of $\hat{S}$ in $(\mathcal{A}^N(M^{\infty}(F, V)))^N$.

The mapping $\hat{S}$ can be easily proved to be an increasing mapping of $(\mathcal{A}^N(M^{\infty}(F, V)))^N$ ordered by inclusion into itself. It is also weakly $U$-continuous which means that $\hat{S}(\bigcup_{i \in N} A_i) = \bigcup_{i \in N} \hat{S}(A_i)$ when $A_i$ is an increasing sequence. But it is not $\cap$-continuous nor weakly $\cap$-continuous.

Since $(\mathcal{A}^N(M^{\infty}(F, V)))^N$ is a complete lattice $\hat{S}$ has a largest fixed point [3] namely

$$v(\hat{S}) = \bigcup \{A \mid A \subset \hat{S}(A)\}$$

One could be tempted to believe that $v(\hat{S})$ is equal to

$$\lambda(\hat{S}) = \bigcap_{i \in N} \hat{S}^i((\mathcal{A}^N(M^{\infty}(F, V)))^N)$$

but this cannot be proved in general, since $\hat{S}$ is not weakly $\cap$-continuous. The following properties give a sufficient condition in order that $v(\hat{S}) = \lambda(\hat{S})$.

First define $\text{Res}_S^\infty$ in the same way as $\text{Res}_S$.

**Property 1 :** $\text{Res}_S \cup \text{Res}_S^\infty \subset \hat{S}(\text{Res}_S \cup \text{Res}_S^\infty)$.

This follows immediately from

**Lemma 2 :** Let $u_1, \dots, u_n, \dots$ be a terminal infinite computation sequence with result U. Then

$$U \in u_1[\text{Res}_S \cup \text{Res}_S^\infty/\emptyset]$$
### Sketch of proof

The main argument, hard to prove formally, is that from every infinite terminal computation sequence $\gamma$ from $\phi_i(v_1, ..., v_{n_i})$ one can extract a finite terminating or infinite terminal computation sequence from $\phi_i(x_1, ..., x_{n_i})$ with result T such that $\text{Res}(\gamma)$ is obtained from T by substituting to every occurrence of $x_i$ in T the result of some finite terminating or infinite terminal computation sequence from $v_i$.

**Property 2 :** $A \subset \hat{S}(A)$ implies $A \subset \lambda(S)$.

The proof is obvious from the fact that $\hat{S}$ is increasing.

**Property 3 :** $\hat{S}(\lambda(S)) \subset \lambda(S)$.

This comes from the fact that

$$ \hat{S}(\bigcap_{i \in N} A_i) \subset \bigcap_{i \in N} \hat{S}(A_i) $$

From Property 1-2-3 follows

**Theorem 2 :** If $\text{Res}_S$ u $\text{Res}_S^\infty$ contrins $\lambda(S)$ then

$$ v(\hat{S}) = \lambda(\hat{S}) = \text{Res}_S u \text{Res}_S^\infty $$

## IV. GREIBACH SCHEMES

This section contains our main theorem which concerns a class of schemes satisfying a condition which is very natural in the theory of languages : the Greibach condition on S amounts to say that each occurrence of an unknown function symbol is included in a sub-expression headed by a basic function symbol. It ensures that every balanced infinite computation sequence is terminal, where balanced means that all the branches of the tree are computed (this is the case of the Kleene's sequence or the sequence obtained by parallel outermost computation).

**Definition :** The set of contracting elements in $M(F \cup \Phi \cup \text{\textit{or}}, V)$ is defined as the smallest subset $C$ such that

$$ V \subset C $$

$$ \rho(f) = 0 \implies f \in C $$
$$ \forall t_1, \dots, t_{\rho(f)} \in M(F \cup \Phi \cup \{\underline{or}\}, V) $$

$$ f(t_1, \dots, t_{\rho(f)}) \in C $$

$$ \forall t_1, t_2 \in C, \quad t_1 \underline{\text{or}} t_2 \in C $$

The ndrps $S : \phi_i(x_1, \dots, x_{n_i}) = t_i$, $i=1, \dots, N$, is a Greibach scheme if and only if $t_i$ is contracting for all $i \in [N]$.

**Example:** The above example $S_1 : \phi(x) = x \underline{\text{or}} s(\phi(x))$ is a Greibach scheme and $S_2 : \phi(x) = x \underline{\text{or}} \phi(s(x))$ is not.

**Theorem 3:** If $S$ is a Greibach scheme, $\text{Res}_S \cup \text{Res}_S^\infty$ is the largest fixed point of $\hat{S}$ equal to

$$ \bigcap_i \hat{S}^i((\mathcal{H}^{\infty}(F, V)))^N $$

**Sketch of proof**

From theorem 2 it suffices to show that

$$ \lambda(\hat{S}) \in \text{Res}_S \cup \text{Res}_S^\infty $$

Consider $\lambda(S)_k$, the $k^{th}$ component of $\lambda(\hat{S})$ and $U \in \lambda(\hat{S})_k$. Then for all $i \in N$

$$ U \in \hat{S}^i((\mathcal{H}^{\infty}(F, V)))^N_k $$

It is rather easy to deduce that there exists for all $i$ an element $w_i$ such that

$$ - \phi_k(x_1, \dots, x_{n_k}) \stackrel{*}{\to} w_i $$

$$ - \omega(w_i) \in \hat{S}^i(\Omega) $$

$$ - \omega(w_i) \prec U $$

Using all these finite computation sequences from $\phi_k(x_1, \dots, x_k)$ to $w_i$ we have to build an infinite computation sequence with result $U$. This is the crucial step for which the main tool is Koenig's lemma which we take in the following form :
**Lemma 3** : Let {$A_i$}$_{i \in N}$ be a sequence of finite non empty subsets of the infinite set E. Let R be a relation on E, $R \subset E \times E$, such that

$$V_i \in N, V a \in A_{i+1} \quad \exists b \in A_i \ (b,a) \in R$$

Then there exists an infinite sequence {$a_i$}$_{i \in N}$ such that for all $i \in N$, $a_i \in A_i$ and $(a_i, a_{i+1}) \in R$.

Applying lemma 3 we now obtain an infinite computation sequence
$v_1 = \phi_k(x_1, \dots, x_{n_k})$, $v_2, \dots, v_n, \dots$ such that there exists a sequence $j_1, j_2, \dots, j_m$
of integers satisfying

$$\omega(v_{j_i}) \in \hat{S}^i(\Omega) \text{ and } \omega(v_{j_i}) < U$$

The Greibach condition on S implies that this sequence is terminal whence
$U = \text{Sup } \omega(v_{j_i}) = \text{Sup } \omega(v_j)$ and the result is proved.

An entirely similar proof is given for infinite words generated by an
algebraic grammar in [10].

## Conclusion

The difficulties encountered in trying to extend the classical least fixed
point construction of the function computed by a recursive program from the
deterministic to the non deterministic case has pointed out by several authors
[5,7,12]. We have proved that in the Herbrand interpretation $M^\infty(F,V)$ the computed
function is the largest fixed point for a wide class of schemes. For a general
interpretation I the same result holds provided that some conditions of a topolo-
gical nature are satisfied by I. This study will be the object of a forthcoming
paper of the two authors.

***

## REFERENCES

[1] A.ARNOLD. Systèmes d'équations dans le magmoïde. Ensembles rationnels et algébriques d'arbres. Thèse d'Etat, Lille (1977).

[2] A.ARNOLD et M.DAUCHET. Théorie des magmoïdes. Publication du laboratoire de Calcul, Lille (1977).
[3] G.BOUDOL. Langages polyadiques algébriques. Théorie des schémas de programme : sémantique de l'appel par valeur. Thèse 3ᵉ cycle, Paris (1975).

[4] B.COURCELLE and M.NIVAT. Algebraic families of interpretations. 17th Symp. on Foundations of Computer Science (1976).

[5] H.EGLI. A mathematical model for non-deterministic computations. Zürich (1975).

[6] J.ENGELFRIET and E.M.SCHMIDT. 10 and 01. Daimi Report PB 47, University of Aarhus, Danemark (1975).

[7] M.HENNESSY and E.A. ASHCROFT. The semantics of non determinism. In "Automata, Languages and Programming" 3rd Internat. Colloquium, Edinburgh (1976).

[8] P.HITCHCOCK and D.PARK. Induction rules and termination proofs. In "Automata, Languages and Programming" 1st Internat. Colloquium, Paris (1972).

[9] M.NIVAT. On the interpretation of Polyadic Recursive Program Schemes. Symp. Mathematica 15 (1975).

[10] M.NIVAT. Mots infinis engendrés par une grammaire algébrique. To appear in RAIRO Informatique Théorique.

[11] G.D.PLOTKIN. Powerdomain Constructions. SIAM J. on Comput. (1976) 452-486.

[12] D.SCCOT. Outline of a mathematical theory of computation. Memo Oxford (1972).

[13] J.W.THATCHER, J.A.GOGUEN, E.G.WAGNER and J.B.WRIGHT. Initial Algebra Semantics and Continuous Algebra. J. Assoc. Comput. Mach. 24 (1977) 68-95.

[14] J.VUILLEMIN. Syntaxe, Sémantique et Axiomatique d'un Langage de Programmation Simple. Thèse d'Etat, Paris (1974).