# Threshold evaluation and the semantics of call by value, assignment and generic procedures

Bernard Lang

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

## To cite this version:

Bernard Lang. Threshold evaluation and the semantics of call by value, assignment and generic procedures. [Research Report] IRIA-RR-211, IRIA. 1977, pp.12. hal-04716475

HAL Id: hal-04716475

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

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
Tw= 02661

RR211

IRIA

laboria

Institut de Recherche
d'Informatique
et d'Automatique

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

laboratoire de recherche
en informatique
et automatique

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

THRESHOLD EVALUATION
AND THE SEMANTICS OF CALL
BY VALUE, ASSIGNMENT
AND GENERIC PROCEDURES

Bernard LANG

Rapport de Recherche N° 211

Janvier 1977

12p
THRESHOLD EVALUATION AND THE SEMANTICS OF CALL BY VALUE,
ASSIGNMENT AND GENERIC PROCEDURES

B. Lang

Abstract :

We use the concept of evaluation up to a given threshold of information to generalize the seman-
tics of call by value and assignment to non-discrete domains, and to define a formal semantics
for generic procedures. We then prove the correctness of McCarthy's transformation of iterative
programs into recursive ones provided the same threshold is used for assignment and parameter
passing.

Résumé :

Nous définissons un concept d'évaluation des expressions limitant cette évaluation par un seuil donné d'information. Ce concept est utilisé pour généraliser aux domaines de calcul non-discret la sémantique de l'appel par valeur et de l'affectation, et pour définir une sémantique formelle des procédures génériques. Nous montrons que la transformation de McCarthy, transformant les programmes itératifs en programmes récursifs, est fortement correcte à condition que le même seuil soit utilisé pour l'affectation et le passage de paramètres.

* Presented at the Fourth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages.
Los Angelès (Cal), January 1977.
# Threshold evaluation and the semantics of call by value, assignment and generic procedures

Bernard Lang

IRIA, LABORIA

78150 - Rocquencourt

FRANCE

## Abstract

We use the concept of evaluation up to a given threshold of information to generalize the semantics of call by value and assignment to non-discrete domains, and to define a formal semantics for generic procedures. We then prove the correctness of McCarthy's transformation of iterative programs into recursive ones provided the same threshold is used for assignment and parameter passing.

## 0. MOTIVATION AND PREVIOUS WORK

### 0.1 McCarthy's Transformation.
The original purpose of this work was to establish in a precise way when the McCarthy transformation of an iterative program into a recursive one [1] is strongly correct (i.e. the two programs are strongly equivalent).

A characteristic of this transformation is that it changes assignment into parameter passing. Since assignment requires evaluation of the expression assigned, the parameter passing mechanism has to do the same with the expression passed. This usually corresponds to the concept of call by value.

So a key concept in our work is that of an evaluation. By considering the partial evaluation of an expression up to a given threshold of information, we will generalize the usual concepts of assignment and call by value. We will then establish the correctness of McCarthy's transformation provided the same threshold is used to evaluate actual parameters and assigned expressions.

Previous work on McCarthy's transformation, using call by value, was done by Strong [2]. However Strong's syntactic approach is limited to discrete interpretations, i.e. interpretations in which values are either completely defined or completely undefined. By non-discrete interpretations we mean domains with partially defined values (e.g. a pair having only one component defined). It is not clear how Strong's approach could be generalized to this case.

More recently Courcelle [3] proved the correctness of the transformation without using call by value, but for a class of interpretations so restricted as to be of limited practical interest.

### 0.2 Semantics of Call by Value.
We follow here only the fixed point approach to the semantics of programs as introduced by Scott [4] and developed

by many authors [5,6,7]. However the most natural use of this type of semantics for recursive equations imply the use of call by name as parameter passing mechanism.

The semantics of call by value has so far been approached in two different ways :

a) The first approach is due to Park [8] and represents functions by their graphs. This leads to a fixed point semantics of call by value as naturally as the more direct approach leads to call by name. However this representation of functions seems impractical to this author, and defining call by name in this manner is rather complicated (de Roever [9]). Furthermore this semantics allows only for discrete domains.

b) The second approach is to define call by value by some extension of the usual call by name approach. This was done by de Bakker [10] and Boudol [11], but only for discrete domains.

### 0.3 Non-discrete Domains.
Although the data domains used in most programming languages are discrete, recent developments in programming research lead more and more to the consideration of non-discrete domains :

a) Higher order languages (Lisp, Algol 68, EL1, POP-2 [12,13,14,15]) use functional domains that are not discrete. In fact, call by value as defined by Landin for lambda-calculus [16] has been given a mathematical semantics by Plotkin [17]. This work, done for ω-order functional domains, seems compatible with ours which is limited to first order but considers arbitrary domains.

b) Recent work extending the delay rule of Wadsworth [18] and Vuillemin [6] has led to new "lazy" interpreters [19,20]. Typically these interpreters can deal with data structures that are only partially defined, thus belonging to a non-discrete domain.

c) Coroutines as defined by Kahn and MacQueen [21] use non-discrete domains which are sets of possible histories for the communication channels. In Wiedmer [22], a mechanism for computing on real numbers with arbitrary precision is based on the same principles. Finally, the model theory of the programming language LUCID [23] deals with infinite cartesian products of discrete domains, hence with non-discrete domains.
Without resorting to those more advanced concepts, we have simple examples of interesting use of non-discrete domains, such as passing a pair by value for its first component and by name for its second one.

## 1. PRELIMINARIES

**1.1 General notations.** If A is a set, we note

$$A^0 = \emptyset, A^1 = A, \forall n > |A^n| = A^{n-1} \times A, \text{ and } A^* = \bigcup_{n \ge 0} A^n.$$

The cardinality of A is noted $|A|$. The function $\iota_A$ is the identity map on A. The set of functions from A to B is noted $(A+B)$. We note $[n] = \{i \in N | 1 \le i \le n\}$.

If $X = \{x_i | i \in N^+\}$, then $X_n = \{x_i | i \in [n]\}$. If $f$ is a function or a function symbol, then $\rho(f)$ or simply of is the arity of $f$ (number of arguments). We note the composition of relations. If $\to$ is a relation

$$\begin{align*} \text{on } A, \text{ then we note } \stackrel{0}{\underset{\to}{\iota}}_A = \iota_A, \forall n > 0 \stackrel{0}{\underset{\to}{n}} = n - 1 \stackrel{0}{\underset{\to}{o}}, \\ \text{and } \stackrel{0}{\underset{\to}{\iota}}_A = \iota_A \text{, and } \stackrel{0}{\underset{\to}{o}}_A = o. \end{align*}$$

In the following F will generally denote a finite or denumerable set of function symbols $f_i$, and X a denumerable set of variable symbols :

$$X = \{x_i | i \in N^+\}$$

**1.2 Vector notation.** Let A be a set. We denote by $\vec{a}$ an element of $A^*$. If $\vec{a} \in A^n$, we note $a_i$, its i-th component, and $\vec{a} = \langle a_1, \dots, a_n \rangle$. If $f$ denotes a function or a function symbol, then $f(\vec{a})$ is an abbreviation for $f(a_1, \dots, a_p)$. If K is a unary function, then $K(\vec{a})$ is an abbreviation for $\langle K(a_1), \dots, K(a_n) \rangle$. Similarly, the order relation $\prec$ in a c.p.o. $<D, \prec, \perp>$ is extended as :

$$\forall d, d' \in D^q \quad \begin{array}{l} \vec{d} \prec d' \quad \text{iff} \quad (\forall i \in [q] \ \vec{d}_i \in D_i^+) \\ \vec{d} \prec d' \quad \text{iff} \quad (\forall i \in [q] \ \vec{d}_i \in D_i^+) \end{array}$$

However, a "derivation" relation $\to$ on A is extended to $A^q$ differently :

$$\begin{align*} \forall a, a' \in A^q \quad & \begin{array}{l} \vec{a} \to \vec{a}' \quad \text{iff} \quad \exists i \in [q] \text{ such that } a_i + a_i' \\ \text{and } \forall j \in [q] - \{i\} \quad a_j = a_j' \end{array} \\ \text{By } \vec{a} \stackrel{k}{\to} \vec{a}' \text{ we denote the } k\text{-transitive closure} \end{align*}$$

(as defined in 1.1) of the vector relation $\vec{a} \to \vec{a}'$, and not the vector extension of the derivation relation $\stackrel{k}{\leftarrow}$ between single elements of A.

The substitution $[t_1/x_1, \dots, t_q/x_q]$ (see below) is noted $[t_1/t]$.

**1.3 Orders.** A partial order is a couple $<D, \prec>$ where $\prec$ is an order relation (reflexive, antisymmetric, transitive) on the set D. Let A be a subset of D, an upperbound of A is an element $d$ of D such that $\forall a \in A \ a \prec d$. Two elements $d$ and $d'$ of D are incompatible (noted $d \ne d'$) iff {$d, d'$} has no upperbound. If A has a least upperbound it is noted $UA$, or dud' when $A=\{d, d'\}$.

A partial order $<D, \prec>$ is conditionally complete iff every upper-bounded subset of D has a least upperbound. A subset $A \subseteq D$ is directed iff i) $A \ne \emptyset$

and ii) $\forall a, a' \in A \ {a, a'}$ has an upperbound in A.

A partial order $<D, \prec>$ is inductive iff i) there is a least element, noted $\perp$, in D such that $\forall d \in D \ \perp d$, and ii) every directed subset of D has a least upperbound. The inductive partial order is noted $<D, \prec, \perp>$. An element $d \in D$ is isolated iff for every directed subset $S \subseteq D$, $US \supseteq d$ implies $\exists s \in S, s \supseteq d$. We call complete partial order (in short c.p.o.) a partial order that is both conditionally complete and inductive.

Let $<D, \prec>$ and $<D', \prec>$ be two partial orders. A function $f \in (D \to D')$ is monotonic iff

$$\forall d_1, d_2 \in D \quad d_1 \prec d_2 \Rightarrow f(d_1) \prec f(d_2).$$

When the two orders are inductive, $f$ is continuous iff for every directed subset $A \subseteq D$ i) the image $f(A)$ of A by $f$ is a directed subset of $D'$, and ii) $f(UA) = Uf(A)$. The set of continuous function from D to $D'$ is noted $[D \to D']$. Continuity implies monotony.

An order $<D, \prec>$ is discrete iff i) there is a least element $\perp$ in D and ii) $\forall d, d' \in D - \{\perp\} \ d \ne \bar{d}' \Rightarrow d \ne \bar{d}'$. A discrete order is a c.p.o.

A special role will be played in this paper by the c.p.o. $O = \{\perp, \tau, \prec, \perp\}$.

**Lemma 1.1**

Let $<D, \prec, \perp>$ be a c.p.o. and for every subset $A \subseteq D$ note $S_A$ the function in $(D \to O)$ defined by

$$S_A = \lambda x \cdot \begin{array}{l} \perp \text{ if } \exists a \in A \ a \in x \\ \perp \text{ otherwise} \end{array}$$

If A is a set of isolated elements of D then $S_A$ is continuous.

**1.4 F-algebras** (or F-magmas). Let $F = \{f_i | i \in [n]\}$ be a finite set of function symbols. Let D be a set and I a mapping in $(F \to (D^* \to D))$ that preserves arities. We call I an interpretation of F on D. We note $F_I=I(f)$ and $F_I = \{f_I | f \in F\}$. The couple $<D, F_I>$ is called an F-algebra.

A morphism of F-algebras, from $<D, F_I>$ to $<D', F_I>$, is a mapping $\mu \in (D \to D')$ which preserves the functions $f_I$, i.e.

$$\forall f \in F, \forall d \in D^p \quad \mu(f_I(d)) = f_I(\mu(d)).$$

The free F-algebra $M(F,A)$ on a set A is the set of well formed (with respect to arities) terms on F and A. It is such that for any F-algebra $<D, F_I>$, any mapping $\nu \in (A \to D)$ extends uniquely to a morphism, noted $<I, \nu>$, in $(M(F,A) \to D)$. We call $\nu$ a valuation and $<I, \nu>$ a valuated interpretation. The valuated interpretation $<I, \nu>$ associates an element of D to every term in $M(F,A)$ as follows :

$$\forall t \in M(F, A)$$

$$i) \quad t = a \in A \quad \Rightarrow \quad <I, \nu>(a) = \nu(a)$$

$$ii) \quad t = f(\vec{t}) \quad \Rightarrow \quad <I, \nu>(t) = f_I(\overrightarrow{<I, \nu>(\vec{t})})$$

We allow any vector $g = \langle g_1, \dots, g_p | F \rangle$ of functions in $(D^* \to D)$ (resp. $\vec{g} = \langle d_1, \dots, d_p | A \rangle$ of elements in D) to be considered as an interpretation (resp. a valuation) of $M(F, A)$.
**Lemma 1.2**

Let D be a c.p.o. and t∈M(F,A), then
λ⁺g⁺d⁺<sub>F</sub>g⁺d⁺(t) is a continuous functional from
[D⁺→D]F|×D|A| to D.

A substitution σ is a morphism between two
free F-algebras M(F,A) and M(F,B) ; since σ is ful-
ly determined by its value on A, we note

σ = [σ(a₁)/a₁, ..., σ(aᵢ)/aᵢ, ...] allowing the omission of those elements in A for which σ is the identity.

The height ||t|| of a term t∈M(F,A) is defined
by :

i) t=a∈A or t=f with ρ(f)=0 ⇒ ||t||=1,

ii) t=f(t⁺) ⇒ ||t||=1+max{||tᵢ|| | i∈[ρf]}.

1.5 Compatible derivation relations. A "derivation" relation —→ over a free algebra M(F,D) is compatible iff ∀f∈F, ∀t, t'∈M(F,D)pf t→t' ⇒ f(t')→f(t).

Lemma :

If the relation $\xrightarrow{k}$ is compatible then
i) the relations $\xrightarrow{\phantom{k}, +}$, $\xrightarrow{+}$ and $\xrightarrow{\phantom{k}, -}$ are too,
ii) $\forall \tau \in M(F,DUX_q) \quad \forall \vec{t}, \vec{t}' \in M(F,D)^q \quad \vec{t} \xrightarrow{\phantom{k}, +} \vec{t}' \Rightarrow [\vec{t}/\vec{x}]_\tau \xrightarrow{\phantom{k}, -} [\vec{t}'/\vec{x}]_\tau$

2. GENERIC SCHEMES AND PROGRAMS

In order to have a uniform treatment of simpli-
fication and rewriting rules in our operational se-
mantics (see [6]), we are led to consider a more
general concept than that of recursive procedures,
namely that of *generic* procedures. These are recur-
sive procedures with many bodies, the choice of the
body at each call depending on some predicate over
the parameters, usually involving their type (e.g.
+ can be integer addition, boolean disjunction or
set union depending on arguments types). This con-
cepts was introduced in programming languages such
as Basel, Algol 68, EL1 [24,13,14] and is discus-
sed by Schuman in [25].

Independently, Burstall and Darlington [26]
have developed for their program transformation
system a new representation of recursive programs
that is similar to the concept of generic program
presented here.

Our calling mechanism for a generic procedure
includes a set of threshold points in the arguments
domain. This set is partitioned into subsets, each
corresponding to a different procedure body. Actual
arguments have to be evaluated up to some thres-
hold point before the procedure is called. The body
chosen is then the one corresponding to the parti-
tion that contains the threshold point reached by
the partially evaluated arguments.

2.1 Generic Rewriting Systems.

The concept of generic system introduced here
will be used later to define the operational seman-

tics of generic programs.

Generic systems are a refinement of term rewri-
ting systems [7]. For every rewriting rule there is
an applicability condition "val", depending on the
arguments of the rewritten function symbol (this
will correspond to the parameter-passing mechanism,
e.g. by name, by value...). Furthermore the replace-
ment term of a rule is also dependant on those ar-
guments (this will correspond to the generic aspect
of the programs we want to define).

This section is devoted to the definition of ge-
neric systems and the proof of their Church-Rosser
property (slightly generalized). The proof techni-
que is inspired from Tait's [27] and consists in
defining a notion of parallel derivation, showing
it to have the same transitive closure as the usual
derivation, and proving the Church-Rosser property
for parallel derivation.

2.1.1 Definitions.

a) **Generic Systems.** Let D be a set, F a finite set of function symbols, X a denumerable set of variable symbols X = {x_i | i ∈ N^+}.

We define a generic rewriting system as a couple
Γ = <val, T> where

i) val<sub>f</sub>(F→(M(F,D)<sup>*</sup>→0))

ii) T ∈ (F → (M(F, D) → M(F, DUx))),

and such that the axioms AΓ₁ and AΓ₂ given below
are satisfied.

For all f in F we abbreviate
- val(f) as val<sub>f</sub> ∈ (M(F,D)<sup>pf</sup>→0)
- T(f) as τ<sub>f</sub> ∈ (M(F,D)<sup>pf</sup>→M(F,DUx<sub>pf</sub>))

We call val and T respectively threshold and re-
writing functions.

b) **Derivation.** Given the above generic system Γ,
and A∈F, we define over M(F,D) the relation
"derive by A into", noted "A", as the smal-

lest compatible relation such that :

$$
\forall f \in A, \forall \vec{t} \in M(F,D)^{\rho f}, \text{ val}_f(\vec{t}) = \tau \Rightarrow f(\vec{t}) \xrightarrow{A} [\vec{t}/\vec{x}] \tau_f(\vec{t})
$$

c) **Axioms.** The generic system axioms can now be expressed as : $\forall f \in F, \forall \vec{t}, \vec{t}' \in M(F,D)^{\rho f}$

$$
\left.
\begin{array}{rcl}
\mathbf{A}\Gamma_1 : \vec{t} \xrightarrow{\phantom{=}F \xrightarrow{\phantom{=}} \vec{t}'} & \Rightarrow & \mathrm{val}_f(\vec{t}) \equiv \mathrm{val}_f(\vec{t}') \\[1em]
\mathbf{A}\Gamma_2 : \vec{t} \xrightarrow{\phantom{=}F \xrightarrow{\phantom{=}F} \vec{t}'} & \Rightarrow & \tau_f(\vec{t}) = \tau_f(\vec{t}') \\[1em]
& \Rightarrow & \mathrm{val}_f(\vec{t}) = \tau
\end{array}
\right\} \quad \Rightarrow \quad \tau_f(\vec{t}) = \tau_f(\vec{t}')
$$

Those axioms insure that "no possible derivation
will be disabled by performing first an inner
derivation".

d) **Parallel derivation.** Given the generic system Γ and A∈F, we define over M(F,D) the relation "derive in parallel by A into", noted "A", as the smallest relation such that :

$$
AP_1 : \forall d \in D \quad d \xrightarrow{\parallel A} d
$$
$$
\begin{align*}
\mathrm{AP}_2: & \forall f \in \mathcal{F}, \forall \vec{t}, \vec{t}' \in \mathcal{M}(\mathcal{F}, \mathcal{D})^{\mathrm{pf}} \\
& (\forall i \in [\rho f] \ t_i \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} \vec{t}_i) \Rightarrow f(\vec{t}) \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} f(\vec{t}')
\end{align*}
$$

$$
\begin{align*}
\mathrm{AP}_3: & \quad \forall f \in \mathcal{A}, \forall \vec{t}, \vec{t}' \in \mathcal{M}(\mathcal{F}, \mathcal{D})^{\mathrm{pf}} \\
& \quad \forall i \in [\rho f] \left. \begin{array}{l} \vec{t}_i \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} \vec{t}'_i \\ \text{val}_f(\vec{t}) = \tau \end{array} \right\} \Rightarrow f(\vec{t}) \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} [\vec{t}'/\vec{x}] \tau_f(\vec{t})
\end{align*}
$$

Notation

When $A=F$ we note respectively $\dashv$ and $\dashv\dashv$ for
$\rightarrow^{\rightarrow}$ and $\rightarrow^{\rightarrow\rightarrow}$.

**2.1.2 Properties.**

We now give a few technical lemmas relating
$\overrightarrow{A}$ and $\overrightarrow{\overline{\overline{A}}}$.
The main results are corollaries 2.4
and 2.7, which are used here to prove the Church-
Rosser property for generic systems (theorem 2.8),
and in section 2.4 to study the need for simplifica-
tion rules.

In the following, a generic system Γ = <val, T>
over <D, F, X> is understood.

**Lemma 2.1**

$$
\begin{align*}
\forall \tau \in \mathcal{M}(\mathcal{F}, \mathrm{DUX}_q), \quad \forall \vec{t}, \vec{t}' \in \mathcal{M}(\mathcal{F}, \mathcal{D})^q \\
(\forall j \in [q] \ t_j \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} \vec{t}_j) &\Rightarrow [\vec{t}/\vec{x}] \tau \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} [\vec{t}'/\vec{x}] \tau \\
\text{(proof by induction on } \|\tau\|) &\text{.}
\end{align*}
$$

(proof by induction on $||\tau||$).

**Lemma 2.2**

$$
\forall t, t' \in \mathcal{M}(\mathcal{F}, \mathcal{D}) \ t \xrightarrow[\mathcal{A}]{0,1} t' \Rightarrow t \xrightarrow[\mathcal{A}]{\parallel} t'
$$

(proof by induction on $||t||$).

**Lemma 2.3**

$$
\forall t, t' \in \mathcal{M}(\mathcal{F}, \mathcal{D}) \ t \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} t' \Rightarrow t \underset{A}{\stackrel{*}{\rightarrow}} t'
$$

(proof by induction on the length of the proof of
$t \overrightarrow{\parallel A} t'$ from the axioms of parallel derivation).

**Corollary 2.4**

$$
\forall t, t' \in \mathcal{M}(\mathcal{F}, \mathcal{D}) \ t \xrightarrow{\parallel A} t' \Leftrightarrow t \xrightarrow{*} t'
$$

**Lemma 2.5**

Extension of the axioms to parallel derivation.

$$
\forall f \in \mathcal{F}, \forall \vec{t}, \vec{t}' \in \mathcal{M}(\mathcal{F}, \mathcal{D})^{\mathrm{pf}}
$$

$$
1) \quad \vec{t}^* \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} \vec{t}' \quad \Rightarrow \quad \mathrm{val}_f(\vec{t}) \equiv \mathrm{val}_f(\vec{t}')
$$

$$
2) \quad \left. \begin{array}{l} \vec{t}^* \underset{\parallel A}{\stackrel{\parallel}{\rightarrow}} \vec{t}' \\ \text{val}_f(\vec{t}) = \tau \end{array} \right\} \Rightarrow \tau_f(\vec{t}) = \tau_f(\vec{t}')
$$

(proof by induction on the length k of the deriva-
tion $\vec{t} \xrightarrow{k} \vec{t}'$).

**Lemma 2.6**

$$
\begin{array}{l@{\quad}c@{\quad}c@{\quad}c@{\quad}c}
\forall A, B \in \mathcal{F} & \forall t, t', t'' \in \mathcal{M}(\mathcal{F}, \mathcal{D}) &
\multicolumn{1}{c}{\left.\vphantom{\begin{array}{@{}c@{}}\strut\\\strut\end{array}}\right\}} &
\multicolumn{1}{c}{\left.\vphantom{\begin{array}{@{}c@{}}\strut\\\strut\end{array}}\right\}} &
\multicolumn{1}{c}{\left.\vphantom{\begin{array}{@{}c@{}}\strut\\\strut\end{array}}\right\}} \\
\multicolumn{1}{c}{\begin{array}{@{}c@{}}\begin{array}{@{}c@{}}\parallel\hphantom{A}\\\parallel\hphantom{A}\end{array}\\
\begin{array}{@{}c@{}}\parallel\hphantom{A}\\\parallel\hphantom{A}\end{array}\end{array}} &
\multicolumn{1}{c}{\begin{array}{@{}c@{}}\rightarrow\\\rightarrow\end{array}} &
\multicolumn{1}{c}{\begin{array}{@{}c@{}}\rightarrow^*\\\rightarrow^*\end{array}} &
\multicolumn{1}{c}{\begin{array}{@{}c@{}}\rightarrow^*\\\rightarrow^*\end{array}} &
\multicolumn{1}{c}{\begin{array}{@{}c@{}}\rightarrow^*\\\rightarrow^*\end{array}}
\end{array}
$$

(proof by induction on the sum of the length of the
proofs of $t \overrightarrow{\parallel A} t'$ and $t \overrightarrow{\parallel B} t'$).

**Corollary 2.7**

$$
\begin{array}{c}
\forall A, B \in \mathcal{F} \\
\left.
\begin{array}{l}
t \xrightarrow[\parallel A]{i} t' \\
t \xrightarrow[\parallel B]{j} t''
\end{array}
\right\} \Rightarrow \exists \theta \in \mathcal{M}(\mathcal{F}, \mathcal{D})
\end{array}
\quad
\left[
\begin{array}{l}
t' \xrightarrow{j} \theta \\
t'' \xrightarrow{\parallel A} \theta
\end{array}
\right.
$$

(proof by induction on $i+j$).

**Theorem 2.8**

Generic systems are "Church-Rosser".

$$
\forall t, t', t'' \in \mathcal{M}(\mathcal{F}, \mathcal{D})
\left[
\begin{array}{l}
t \xrightarrow{*} t' \\
t \xrightarrow{*} t''
\end{array}
\right]
\Rightarrow \exists \theta \in \mathcal{M}(\mathcal{F}, \mathcal{D}),
\left[
\begin{array}{l}
t' \xrightarrow{*} \theta \\
t'' \xrightarrow{*} \theta
\end{array}
\right]
$$

(proof by corollaries 2.4 and 2.7).

**2.2 Generic Programs.**

**2.2.1 Syntax**

Let $\Phi = \{\phi_i | i \in [n]\}$ be a set of unknown function
symbols,

$X = \{x_i | i \in N\}$ be a set of (dummy) variable
symbols,

F be a finite set of base function symbols,

Q be a finite set of threshold function
symbols.

A generic scheme G on <F, Q, Φ, X> is a set of n
equations of the form :

$$
\phi_i(\vec{x}) \leftarrow \begin{array}{@{}c@{\quad}l@{}}
  & p_{i,1} : e_{i,1} \\
  \cdot & \cdot \\
  \cdot & \cdot \\
  p_{i,q(i)} : e_{i,q(i)}
\end{array} \quad 1 \le i \le n.
$$

where $- p_{i,j} \in \mathcal{M}(Q, \emptyset)$
note that at least one nullary function
symbol is needed in Q.

$$
- e_{i,j} \in \mathcal{M}(\mathrm{Fu}\Phi, X_p(\phi_i))
$$

The terms $p_i$ and $e_i$ will be interpreted res-
pectively as the $i$-th threshold partition and body
of the $i$-th generic procedure defined.

**2.2.2 Interpretation.**

Let <D, E, I> be a c.p.o. .

Let S = 2<sup>D</sup>* be the set of sets of sequences in D.

Let I be a mapping in (F→[D*→D])∪(Q→(S*→S)).

We note $F_I = I(F)$ and $Q_I = I(Q)$. The restrictions
$I_F$ and $I_Q$ of I to F and Q are extended into mor-
phisms $I_F \in (M(F,D) \dasharrow \langle D, F_I \rangle)$ and $I_Q \in (M(Q, \emptyset) \dasharrow \langle S, Q_I \rangle)$.

We define I to be an interpretation for a ge-
neric scheme on <F, Q, Φ, X> iff the following two
axioms hold :

AI₁: ∀i∈[n], ∀j∈[q(i)] I(pᵢ, j) is a set of isolated ρ(φᵢ)-tuples in D<sup>ρ</sup>ᵢ

AI₂: ∀i∈[n], ∀j, j'∈[q(i)] j≠j' implies
∀a∈I(pᵢ, j), ∃a'∈I(pᵢ, j') a≠a'.

The functions in F<sub>I</sub> and Q<sub>I</sub> are respectively called base and threshold functions.

A generic program is a couple <G,I> where G and I are respectively a generic scheme and an interpretation. To the generic program <G,I> we now associate two mappings noted val and T.

For i∈[n] we define the indexing function

$$
J(i) = \lambda_{\vec{x}}^{\cdot} \in j \in [q(i)] \cdot \exists \vec{d} \in I(p_{i,j}) \cdot \vec{d} \neq \vec{x}
$$

where $\in j.P$ means "the unique j such that P holds,
if it exists, and $\perp$ otherwise".

Note that the uniqueness of j is guaranteed by
axiom AI₂.

The function J(i) is in (D<sup>ρ</sup><sub>i</sub>→[q(i)]∪{⊥}).

The functions val<sub>Φ</sub>(Φ→(D<sup>*</sup>→O)) and
T<sub>Φ</sub>(Φ→(D<sup>*</sup>→M(FuΦ,X))) are defined as follows :

$$
\mathrm{val}_{\phi_i}(\lambda_{\vec{x}}^{\cdot}) \quad \begin{cases} \tau & \text{if } J(i, \vec{x}) \in [q(i)] \\ \perp & \text{if } J(i, \vec{x}) = \perp \end{cases}
$$

$$
T(\phi_i) = \lambda_{\vec{x}}^{\cdot} \mid \begin{cases} e_i, J(i, \vec{x}) & \text{if } J(i, \vec{x}) \in [q(i)] \\ \perp, J(i, \vec{x}) = \perp & \text{if } J(i, \vec{x}) = \perp \end{cases}
$$

We note again val<sub>Φ</sub> and τ<sub>Φ</sub> for val(Φ) and T(Φ).

**Lemma 2.9**

$$
\forall \phi \in \Phi
$$

a) $\forall \phi \in [D^{\rho\phi} \to O]$ (continuity of $val_{\phi}$)

b) $\forall \vec{d}, \vec{d}' \in D^{\rho\phi} \quad \left. \begin{array}{l} \vec{d} \sqsubseteq \vec{d}' \\ val_{\phi}(\vec{d}) = \tau \end{array} \right\} \Rightarrow \tau_{\phi}(\vec{d}) = \tau_{\phi}(\vec{d}')$

proof : Axiom AI₁ and lemma 1.1 imply that J(i) is
a continuous function from D<sup>ρ</sup><sub>i</sub> to the discrete
c.p.o. <N∪{⊥}, <sub>≤</sub>, ⊥>. Lemma 2.9 is an immediate co-
rollary. |

Intuitively, in order to evaluate φᵢ(↔ε) in the
interpretation (where ↔ε is a vector of expressions
passed as arguments), ε has to be first evaluated up
to the threshold defined by the points in

I(pᵢ, j), i.e. until we have an approximation ⃗
of the value of the arguments such that
val(φᵢ)(d) = τ. We then choose the body eᵢ, j iff the
threshold has been passed at a point ⃗a belonging
to the threshold set I(pᵢ, j).

From now on, we assume given a generic pro-
gram <G,I> where G is a generic scheme on <F,Q,Φ,X>

and I is an interpretation on the c.p.o. <D,<sub>≤</sub>,⊥>.
Actually we will only use the associated mappings
val and T, without referring anymore to the syntac-
tic definition of G.

We will define for <G, I> :

- a notion of operational semantics (§2.3), and

- a notion of denotational semantics (§2.5).

We will then prove their equivalence (§2.6).

2.3 Operational semantics.

To the generic program <G, I> we will associate
a generic system Γ = <val, T> on <D, FuΦ, X>, thus de-
fining a notion of computation of a term t∈M(FuΦ, D)
by mean of the derivations in Γ. For every function
symbol ψ in FuΦ, val<sub>ψ</sub> and τ<sub>ψ</sub> will be first defined
on D<sup>ρ</sup>, then extended to M(FuΦ, D)<sup>ρ</sup>.

The mappings val and T are built from two
parts :

a) the first part corresponds to the base functions
in F<sub>I</sub>. It is not constructed from <G,I>, but is
a "wired-in machinery" that is provided together
with I in order to compute on schemes interpre-
ted by I. This machinery is composed of two map-
pings : val<sub>f</sub>(F→[D<sup>*</sup>→O]) and T<sub>f</sub>(F→(D<sup>*</sup>→M(F,X))).

There is of course a requirement that this machi-
nery be coherent with I, expressed by the fol-
lowing axiom AS :

$$
\begin{array}{l}
\text{AS : } \forall f \in \mathcal{F}, \quad \forall \vec{d} \in D^{\rho f} \\
\qquad \text{val}_{f}(\vec{d}) = \tau \quad \Rightarrow \quad f_{I}(\vec{d}) = \langle I, \vec{d} \rangle (\tau_{f}(\vec{d}))
\end{array}
$$

b) the second part is "programmed". It is the mappings val and T associated to the generic program <G,I>, as defined in §2.2.2.

Those two parts are merged into one mapping
val<sub>f</sub>(F↓<sub>Φ</sub>→[D<sup>*</sup>→O]) and one mapping
T<sub>f</sub>(F↓<sub>Φ</sub>→(D<sup>*</sup>→M(F↓<sub>Φ</sub>, X))).

In order to get the promised generic system Γ,
we must now extend val<sub>ψ</sub> and τ<sub>ψ</sub> (for every ψ in FuΦ)
to M(FuΦ,D)<sup>ρ</sup>. To this end, we introduce the concept
of direct approximant (Wadsworth [18]).

The direct approximant α(t) of a term
t∈M(FuΦ,D) is the best approximation of the evalua-
tion of t in the interpretation I when the generic
scheme G is ignored. Formally it is the valued
interpretation α = <I<sub>F</sub>U<sub>⊥</sub><sub>Φ</sub>, I<sub>D</sub>>, where ⊥<sub>Φ</sub> denotes the
function λ<sub>⊥</sub><sup>·</sup> in [D<sup>ρ</sup><sub>⊥</sub>→D], and I<sub>Φ</sub> = <⊥<sub>Φ</sub>, ..., ⊥<sub>n</sub> >.
(Recall that I<sub>Φ</sub> may be considered as a mapping from
Φ to {⊥<sub>Φ</sub>|Φ∈Φ}). We will often note at for α(t).

The generic system Γ associated to <G,I> is
now defined as Γ = <val,T> where val and T are the
above defined mappings, extended as follows :

$$
\forall \psi \in \mathrm{Fu}\Phi, \quad \forall t \in \mathrm{M}(\mathrm{Fu}\Phi, \mathrm{D})^{\rho\psi} \\
\mathrm{val}_{\psi}(\vec{t}) = \mathrm{val}_{\psi}(\vec{a}(\vec{t})) \qquad \tau_{\psi}(\vec{t}) = \tau_{\psi}(\vec{a}(\vec{t})).
$$
We still have to verify that the axioms $A_1$ and $A_2$ are satisfied. This is a consequence of lemma 2.9 and the following lemma 2.10 :

**Lemma 2.10**

$$ 
\begin{array}{l}
\forall t, t' \in M(Fu\Phi, D) \\
\quad \text{a)} t \underset{\Phi}{\dashv} t' \Rightarrow \alpha \equiv \alpha' \\
\quad \text{b)} t \underset{F}{\dashv} t' \Rightarrow \alpha = \alpha'
\end{array}
$$

(proof by induction on $||t||$, using axiom AS).

We now proceed to define the operational semantics $O$ of the generic program $<G, I>$.

**Definition :**

$$ \forall t \in M(Fu\Phi, D) \quad A(t) = \{\alpha' | t \stackrel{*}{\dashv} t'\} $$

**Lemma 2.11**

$\forall t \in M(Fu\Phi, D) \quad A(t)$ is directed.

(proof immediate from lemma 2.10 and the Church-Rosser property of generic systems).

Therefore, for every term $t$ in $M(Fu\Phi, D)$ we can define the value $O[t] = \mathbb{U}A(t)$.

For every $\tau \in M(Fu\Phi, DuX_q)$ we define
$$ O[\tau] = \lambda \dot{d} . O[\dot{[d]} / \dot{x}]_\tau \in (D^q \to D). $$

Finally, we associate to every $\phi \in \Phi$ the function $O[\phi] = O[\phi(x_1, \dots, x_{D\phi})]$.

The operational value $O[t]$ of a term $t$ is thus defined as the limit (i.e. least upperbound) of a directed set $A(t)$. Unless this limit is trivial (i.e. contained in $A(t)$), no finite computation will ever reach it. Thus, in some sense, we are considering infinite computations.

This is one way to deal with such machines as lazy interpreters that compute possibly infinite values by computing increasingly more information about them (e.g. the successive elements of a list) without ever producing them fully when they are infinite (e.g. infinite lists). Finite values correspond to isolated points (which can only be trivial limits) of the domain and are thus always computed in finite time.

In particular, thresholds are finite values and are always reached in finite time, if at all.

**2.4 Simplifications.**

The derivation of a term $f(t)$ such that $f \in F$ is called *simplification*. Simplifications are interesting because they correspond to the operation of an actual computing machine for base functions. A similar concept can be found in [6,7,28].

One reason to introduce the generic concept is that it can deal with simplifications, i.e. computation of base functions, as well as with rewriting rules corresponding to the evaluation of recursive programs. For example, the most common base function *if* corresponds to the following simplification :

$$ 
\begin{array}{l}
\text{true} \equiv t_1 \Rightarrow \underset{\text{if}}{\dashv} (t_1, t_2, t_3) \dashv t_2 \\
\text{false} \equiv t_1 \Rightarrow \underset{\text{if}}{\dashv} (t_1, t_2, t_3) \dashv t_3
\end{array}
$$

and we have : $\text{val}_{\underset{\text{if}}{\dashv}}(t) = \tau$ iff $t_1 \in \{\text{true}, \text{false}\}$

$$ \tau_{\underset{\text{if}}{\dashv}}(\text{true}, t_2, t_3) = x_2 \quad \text{and} \quad \tau_{\underset{\text{if}}{\dashv}}(\text{false}, t_2, t_3) = x_3 $$

However the use of simplifications that are given in addition to the interpretation, rather than being constructed from it, is not very satisfactory. We will now show that simplifications are not necessary.

**Corollary 2.12 (of lemma 2.10)**

$$ 
\begin{array}{l}
\forall t, t' \in M(Fu\Phi, D) \\
\quad \text{a)} \quad t \underset{Fu\Phi}{\stackrel{*}{\dashv}} t' \Rightarrow \alpha \equiv \alpha' \\
\quad \text{b)} \quad t \underset{F}{\stackrel{*}{\dashv}} t' \Rightarrow \alpha = \alpha'
\end{array}
$$

**Lemma 2.13**

$$ 
\forall t, t', t'' \in M(Fu\Phi, D) \\
t \underset{F}{\dashv} t' \underset{\Phi}{\dashv} t'' \Rightarrow \exists \theta', \theta'' \in M(Fu\Phi, D) \left\{ 
\begin{array}{l}
t \underset{\Phi}{\dashv} \theta' \underset{F}{\dashv} \theta'' \\
t'' \underset{\Phi}{\dashv} \theta''
\end{array} 
\right.
$$

(proof by induction on the sum of the length of the two parallel derivation proofs).

**Lemma 2.14**

$$ 
\forall t, t', t'' \in M(Fu\Phi, D) \\
t \underset{F}{\stackrel{*}{\dashv}} t' \underset{\Phi}{\stackrel{*}{\dashv}} t'' \Rightarrow \exists \theta', \theta'' \in M(Fu\Phi, D) \left\{ 
\begin{array}{l}
t \underset{\Phi}{\stackrel{*}{\dashv}} \theta' \underset{F}{\stackrel{*}{\dashv}} \theta'' \\
t'' \underset{\Phi}{\stackrel{*}{\dashv}} \theta''
\end{array} 
\right.
$$

(proof by induction on $k$, using lemma 2.13 and corollary 2.7).

**Lemma 2.15**

$$ 
\forall t, t' \in M(Fu\Phi, D) \\
t \underset{Fu\Phi}{\stackrel{*}{\dashv}} t' \Rightarrow \exists \theta', \theta'' \in M(Fu\Phi, D) \left\{ 
\begin{array}{l}
t \underset{\Phi}{\stackrel{*}{\dashv}} \theta' \underset{F}{\stackrel{*}{\dashv}} \theta'' \\
t' \underset{\Phi}{\stackrel{*}{\dashv}} \theta''
\end{array} 
\right.
$$

(proof by induction on the length $k$ of the derivation $t \underset{\parallel}{\stackrel{k}{\dashv}} t'$, lemma 2.14 and corollary 2.7).

**Theorem 2.16**

$$ 
\forall t, t' \in M(Fu\Phi, D) \\
t \underset{Fu\Phi}{\stackrel{*}{\dashv}} t' \Rightarrow \exists \theta'' \in M(Fu\Phi, D) \left\{ 
\begin{array}{l}
t \underset{\Phi}{\stackrel{*}{\dashv}} \theta'' \\
\alpha' \equiv \alpha''
\end{array} 
\right.
$$

(proof by lemma 2.15 and corollaries 2.4 and 2.12).

For every term $t$ in $M(Fu\Phi, D)$ we define

$$ A_{\Phi}(t) = \{\alpha' | t \underset{\Phi}{\stackrel{*}{\dashv}} t'\}. $$

From theorem 2.16 we see that :

$$ \forall t \in M(Fu\Phi, D) \quad \mathbb{U}A(t) = \mathbb{U}A_{\Phi}(t). $$
Therefore the operational semantics could have been equivalently defined without simplifications, using only derivation on unknown function symbols.

Intuitively, simplifications are redundant with the use of direct approximants (see lemma 2.10). However the elimination of direct approximants in favor of simplifications would not work. Without elaborating, let us say that direct approximants are "more powerful" because they allow us to consider incremental increases of information during computation, and thus to "compute" infinite values as limits of finite ones.

## 2.5 Denotational Semantics.

We will now use fixed-point techniques to define a denotational semantics for generic programs. We refer the reader to [4,5] for more details about fixed-points and fixed-point semantics. This type of semantics is usually more tractable in proofs about programs.

Let $\vec{\phi}$ be the vector $<\phi_1, \dots, \phi_n>$. Given a vector $\vec{g}$ of functions in $[D^* \to D]$ such that $\vec{\phi}(\vec{g}) = \vec{\phi}(\phi)$, and a vector $\vec{d} \in D^P$, since the interpretation I on $<D, \mathbb{1}, \vec{\iota}>$ is fixed, we can define in a standard way a valued interpretation $\mu = <I \cup g, I_D \cup d>$ for the terms in $M(Fu\Phi, DuX_p)$. We will often abbreviate to $\mu = <\vec{g}, \vec{d}>$, or even $\mu = <\vec{g}>$ when $X_p = \emptyset$.

To every $\phi_i$ in $\Phi$ we associate the functional $\sigma_i \in ([D^* \to D]^n \to (D \to D))$ defined by:

$$ \sigma_i = \lambda \vec{g} \vec{d} \cdot \text{ if } \text{val}_{\phi_i}(d) = \bot \text{ then } <\vec{g}, \vec{d}> (\tau_{\phi_i}(\vec{d})) \text{ else } \top $$

### Lemma 2.17

$\forall i \in [n] \ \sigma_i$ is continuous (the proof relies on lemmas 2.9 and 1.2).

We note $\vec{\sigma} = \sigma_1, \dots, \sigma_n$. By lemma 2.17 we have $\vec{\sigma} \in [[D^* \to D]^n \to [D^* \to D]^n]$. Thus $\vec{\sigma}$ has a least fixed-point, noted $Y\vec{\sigma}$, in $[D^*]^n$.

The denotational semantics $D[\phi_i]$ of a function symbol $\phi_i \in \Phi$ is then defined as the i-th component of $Y\vec{\sigma}$:

$$ \forall i \in [n] \quad D[\phi_i] = (Y\vec{\sigma})_i $$

For every term $t$ in $M(Fu\Phi, D)$ we define:

$$ D[t] = <I U Y \vec{\sigma}, I_D>(t). $$

## 2.6 Adequation.

We now prove the adequation theorem establishing the equivalence of operational and denotational semantics.

### Lemma 2.18

$$ \forall t, t' \in M(Fu\Phi, D), \quad \forall k \in N \\ \xrightarrow{k} t' \Rightarrow <\vec{\sigma}^k(\vec{I}_\Phi)>(t') \subseteq <\vec{\sigma}^{k+1}(\vec{I}_\Phi)>(t) \\ \text{(proof by induction on } \|t\| \text{)}. $$

### Lemma 2.19

$$ \begin{array}{l} \forall t, t' \in M(Fu\Phi, D), \quad \forall k \in N \\ \xrightarrow{k} t' \Rightarrow <\vec{I}_\Phi>(t') \subseteq <\vec{\sigma}^k(\vec{I}_\Phi)>(t) \\ \text{(proof by induction on } k \text{ and lemma 2.18)}. \end{array} $$

### Lemma 2.20

$$ \begin{array}{l} \forall \phi \in \Phi \quad O[\phi] \subseteq D[\phi] \\ \text{(proof by lemma 2.19 and continuity of } \vec{\sigma}). \end{array} $$

### Lemma 2.21

$$ \begin{array}{l} \forall \tau \in M(Fu\Phi, DuX_p^q), \quad \forall \vec{t} \in M(Fu\Phi, D)^q, \quad \forall k \in N \\ [\vec{\sigma}[\vec{t}]/\vec{x}]_{\tau} \xrightarrow{k} \emptyset \Rightarrow \\ \Rightarrow \exists \tau' \in M(Fu\Phi, DuX_p^q) \cdot \exists \vec{t}' \in M(Fu\Phi, D)^q \\ \left\{ \begin{array}{l} \theta = [\vec{\sigma}[\vec{t}]/\vec{x}]_{\tau'} \\ \vec{t}' \xrightarrow{\sigma} \vec{t}' \\ \forall \vec{\theta}' \in M(Fu\Phi, D)^q \\ \alpha \vec{t}' \subseteq \alpha \vec{\theta}' \Rightarrow [\vec{\theta}'/\vec{x}]_{\tau} \xrightarrow{k} [\vec{\theta}'/\vec{x}]_{\tau'} \end{array} \right. \\ \text{(proof by induction on } <k, \|\tau\|> \text{)} \end{array} $$

Remark: this crucial lemma is better understood in the light of the comments at the end of §2.3.

### Lemma 2.22

$$ \begin{array}{l} \forall \tau \in M(Fu\Phi, DuX_p^q), \quad \forall \vec{t} \in M(Fu\Phi, D)^q \\ O[\vec{\sigma}[\vec{t}]/\vec{x}]_{\tau} \subseteq O[\vec{t}/\vec{x}]_{\tau} \end{array} $$

### Lemma 2.23

$$ \begin{array}{l} \forall \vec{g} \in [D^* \to D]^* \quad \text{such that } \vec{\sigma}(\vec{g}) = \vec{\sigma}(\phi) \\ \vec{g} \subseteq \vec{\sigma}[\vec{\phi}] \Rightarrow \forall t \in M(Fu\Phi, D) \quad <\vec{g}>(t) \subseteq O[t] \\ \text{(proof by induction on } \|t\| \text{)}. \end{array} $$

### Lemma 2.24

$$ \begin{array}{l} \forall k \in N \quad \vec{\sigma}^k(\vec{\iota}_\Phi) \subseteq \vec{\sigma}[\vec{\Phi}] \\ \text{(proof by induction on } k \text{)} \end{array} $$

### Corollary 2.25

$$ \vec{\sigma}[\vec{\Phi}] \subseteq \vec{\sigma}[\vec{\Phi}] $$

### Theorem 2.26 (Adequation)

$$ \vec{\sigma}[\vec{\Phi}] = \vec{\sigma}[\vec{\Phi}] $$

## 2.7 Applications

a. If a function has only one body $e_{i,1}$ and $I(p_i) = \{\bot\}$, then it is a usual recursive function with call by name.

b. If $\phi_i$ has one body $e_{i,1}$ and $I(p_i)$ is the set of $\rho(\phi_i)$-tuples of maximal elements in D, then we have a recursive function with the usual call by value.

c. We can consider intermediate cases :
- some parameters can be called by name, and
others by value.

- a parameter can be called partially by value, i.e. be required to be evaluated up to some non-maximal point in D. For example we can have an array argument, and require only the first two elements to be evaluated before passing the actual array.

d. With appropriate interpretations (see e.) we a semantics for generic procedure, with the possibility of calling the parameters by name for some bodies, and by value for others (a problem left open in [24]). In the case of generic + considered earlier we may wish it to call its arguments by name when it is the boolean disjunction, and by value when it is the integer addition.

e. To enable the threshold mechanism to perform type checking we can include types in the domain of interpretation, e.g. :

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

**Example :**

We consider an interpretation I in the above domain. The interpretation of the threshold function symbol *value* is a function I(value)(S) is the set of isolated maximal points greater than some point in S. Then

$$ \text{foo}(x) \leftarrow \begin{cases} \text{integer} : e_1(x) \\ \text{value}(\text{boolean}) : e_2(x) \\ \text{cons}(\text{value}(\text{list}), \text{list}) : e_3(x) \end{cases} $$

is interpreted as a generic function where the body $e_1$ gets its argument almost by name (almost because we require it to be at least an integer), $e_2$ gets its argument by value, and $e_3$ requires its argument to be a non-atomic list in which only the first succlist must have been evaluated.

### 3. FLOWCHARTS AND McCARTHY'S TRANSFORMATION

In §3.1 we use threshold evaluation to generalize the concept of assignment in flowcharts as we did call by value in recursive programs. The correctness of McCarthy's transformation is then established in §3.2.

#### 3.1 Flowchart programs.

The flowcharts defined here are composed of assignment and branching statements, and of exit statements returning the results of computations. Sequencing is done exclusively through labels (it is never implicit).

We will define in a standard way the interpretation and the operational semantics of a flowchart program. The original aspect is that the interpretation

specifies a set $\Theta$ of isolated threshold points in the domain D of interpretation. Assignments can be performed only when the assigned expression has been evaluated up to some threshold point in $\Theta$.

The threshold set $\Theta$ actually determines the semantics of assignment. If $\Theta$ is the set of isolated maximal points in D, we have the usual concept of assignment (thus corresponding to call by value) which requires the assigned expression to be completely evaluated. For other thresholds $\Theta$, the assigned expression is not always required to be completely evaluated when the assignment is executed. In particular, when $\Theta = \{1\}$ we have an "assignment by name" as we might want it in a lazy interpreter [19,20]. This assignment by name is very similar to the port assignment used in [21] to build coroutine networks.

Note that we simplify the following presentation by considering just one flowchart rather than a set of flowchart procedures calling each other recursively. Thus expressions (or rather terms) are built only from base functions without recursive calls to other procedures.

#### 3.1.1 Flowchart schemes.

Let $L, X_p$ and $F$ be three finite sets whose elements are respectively noted $\beta_i$, $1 \le i \le n$, $x_i$, $1 \le i \le p$ and $f_i$, $1 \le i \le |F|$, and are called *labels*, *registers* and *base function symbols*.

We define the following sets :

i) $As(L, X_p, F) = X_p \times M(F, X_p) \times L$ is the set of assignments, noted $\langle x_i \to t; \beta_i \rangle$.

ii) $Br(L, X_p, F) = M(F, X_p) \times L \times L$ is the set of branchings, noted $\langle t \to \beta', \beta'' \rangle$.

iii) $Ex(X_p, F) = M(F, X_p)$ is the set of exits noted $\langle \text{return } t \rangle$.

iv) $St(L, X_p, F) = As(L, X_p, F) \cup Br(L, X_p, F) \cup Ex(X_p, F)$ is the set of statements.

In the above definitions, $t$ denotes some element of $M(D, X_p)$.

We define a flowchart scheme on $\langle L, X_p, F \rangle$ as a mapping $\delta \in (L \to St(L, X_p, F))$.

#### 3.1.2 Interpretations.

Let $\langle D, \mathcal{E}, \mathcal{I} \rangle$ be a c.p.o. containing three distinguished elements, noted $tt$, $ff$ and $\emptyset$, that are isolated and maximal. Those elements stand respectively for the boolean values true and false, and a special value corresponding to error messages in real computations.

Let I be a mapping in $(F \to [D^* \cup D])$ preserving arities, and $\Theta$ a set of isolated elements of D.

We define the couple $\langle I, \Theta \rangle$ to be an interpretation for flowchart schemes on $\langle L, X_p, F \rangle$. The set $\Theta$
is called the threshold set.

To the set $\Theta$ we associate a continuous mapping $val_{\Theta} \in [D \to O]$ defined by :

$$val_{\Theta} = \lambda x . \text{if } \exists d \in \Theta . d \notin x \text{ then } \tau \text{ else } \uparrow$$

### 3.1.3 Operational Semantics.

From now on we implicitly consider a flowchart program $<\delta, \langle I, \Theta \rangle>$, composed of a flowchart scheme $\delta$ on $\langle L, X_p, F \rangle$ and an interpretation $\langle I, \Theta \rangle$ on the domain $\langle D, \Sigma, \perp \rangle$, with the function $val_{\Theta}$ as defined above.

A state is a couple $n=\langle v, \beta \rangle$ where $v$ is a valuation of the registers in $X_p$, i.e. a mapping in $(X_p \to D)$, or equivalently (up to isomorphism) a vector $\tilde{d} \in D^p$, and $\beta$ is a label called *program counter* in this context.
Let $S = D^p \times L$ be the set of states.

A register valuation $v$ together with $I$ defines a valuated-interpretation $\langle I, v \rangle$ of the terms in $M(F, X_p)$.

A *derivation relation*, noted $\dashv\vdash$, is defined between states as follows :

i) if $\delta(\beta) = \langle x_i + t, \beta' \rangle$ then
$$ \begin{array}{l} val_{\Theta}(\langle I, v \rangle(t)) = \tau \Rightarrow \langle v, \beta \rangle \dashv\vdash \langle v', \beta' \rangle \\ \text{where } v' = \langle \langle I, v \rangle(t) / x_i \rangle_v \end{array} $$
i.e. $v'$ is equal to $v$ except for the i-th register which has taken the value $\langle I, v \rangle(t)$.

ii) if $\delta(\beta) = \langle t \to \beta', \beta'' \rangle$ then
$$ \begin{array}{l} \langle I, v \rangle(t) = \text{tt} \Rightarrow \langle v, \beta \rangle \dashv\vdash \langle v, \beta' \rangle \\ \langle I, v \rangle(t) = \text{ff} \Rightarrow \langle v, \beta \rangle \dashv\vdash \langle v, \beta'' \rangle \end{array} $$

Remark that for every state $n$ there is at most one state $n'$ such that $n \dashv\vdash n'$. We have deterministic computations.

We now define a mapping $\alpha \in (S \to D)$, called *direct result*, as follows :

$$ \alpha(\langle v, \beta \rangle) = \begin{cases} \langle I, v \rangle(t) & \text{if } \delta(\beta) = \langle \text{return } t \rangle \\ \emptyset & \text{if } \delta(\beta) = \langle t \to \beta', \beta'' \rangle \\ \perp & \text{otherwise.} \end{cases} $$

Note that if a state $n$ is derivable, then $\alpha(n) = \perp$. The result is $\emptyset$, meaning error, when a branching test is applied to a non-boolean value.

For every state $n \in S$, let $A(n)$ be the set $A(n) = \{\alpha(n') | n' \dashv\vdash n'\}$.

By the above remarks on derivations we see that $A(n)$ contains at most one element not equal to $\perp$.

So we can define the value computed by the flowchart program for some initial state $n$ as :

$$O[n] = \mathbb{U}A(n).$$

Note that this limit is always trivial, which means that only finite elements of $D$ can be computed (assuming finite initialisation of the registers in $n$, and that base functions give a finite

result for finite arguments). If the result is not $\perp$ (non termination), it is obtained after a finite number of computation (derivation) steps.

Finally our operational semantics associates to every label $\beta$ in $L$ a function in $[D^P \to D]$ as follows :

$$\forall \beta \in L \quad O[\beta] = \lambda d \cdot O[\tilde{d}, \beta]$$

Defining a fixed-point semantics for flowchart programs (see for example [29]) and giving an adequation theorem would be much easier than for generic programs, but without real interest for the present work.

### 3.2 McCarthy's Transformation.

We now study the transformation due to McCarthy's [1] that transforms a flowchart program into an equivalent recursive one, or generic one here.

We will have to consider only generic functions with a unique body ; thus we will ignore the threshold feature that generalizes call by value. Consequently we will abbreviate the notation of generic equations, in schemes, by writing simply $\phi_i(\tilde{x}) \leftarrow p_i : e_i$ (i.e. without the second index corresponding to different possible bodies).

The essential point in our presentation of the transformation is that it uses the same threshold for the flowchart program and its generic transform. With the usual semantics of assignment, this amounts to requiring the use of call by value for the transform.

In this section, $\tilde{x}$ will always denote the vector $\langle x_1, \dots, x_p \rangle$.

#### 3.2.1 The transformation.

Given the flowchart program $<\delta, \langle I, \Theta \rangle>$ as defined in §3.1, we build a generic program as follows.

i) Let $\Phi = \{\phi_i | 1 \le i \le n = |L|\}$ be the set of unknown function symbols,

ii) Let $F' = \text{Fu}(\underline{\text{if}})$ be the set of base function symbols,

iii) Let $Q$ be the set of threshold function symbols containing only the symbol $\pi$, with the arity $\rho(\pi) = 0$.

iv) Let the generic scheme $G$ on $\langle F', Q, \Phi, X \rangle$ be the set of equations

$$\phi_i(\tilde{x}) \leftarrow \pi : e_i \quad 1 \le i \le n.$$

such that :

$$a) \delta(\beta_i) = \langle x_j + t; \beta_k \rangle \Rightarrow e_i = [t/x_j](\phi_k(\tilde{x}))$$

$$b) \delta(\beta_i) = \langle t \to \beta_j; \beta_k \rangle \Rightarrow e_i = \underline{\text{if}}(t, \phi_j(\tilde{x}), \phi_k(\tilde{x}))$$

$$c) \delta(\beta_i) = \langle \text{return } t \rangle \Rightarrow e_i = t$$

Note that the threshold term is the same (i.e. $\pi$) for all equations.

v) Let $I$ be the mapping on $F' \cup Q$ defined by

$$a) \forall f \in F \quad I'(f) = I(f)$$
$$
\begin{array}{l}
b) I'(\underline{i}f) = \lambda x_1 x_2 x_3' \left|
\begin{array}{l}
x_2 \text{ if } x_1 = tt \\
x_3 \text{ if } x_1 = ff \\
\emptyset \text{ if } x_1 \neq tt \text{ and } x_1 \neq ff \\
\perp \text{ otherwise}
\end{array}
\right.
\end{array}
$$

c) $I'(\pi) = \theta^P$

We define the generic program <G, I'> to be
the McCarthy transform of the flowchart program
<δ, <I, Θ>>.

3.2.2 Correctness.

An operational semantics O is defined for
both the flowchart program <δ, <I, Θ>> and its gene-
ric McCarthy transform <G, I'>, that associates func-
tions in [DP→D] to every label β∈L or unknown func-
tion symbol φ∈Φ. Strong correctness of the trans-
formation can thus be expressed by :

$$
\forall i \in [n], \quad O[\beta_i] = O[\phi_i]
$$

However we will not be able to completely
achieve this goal. Indeed, for any $\phi_i \in \Phi$ and $\tilde{d} \in DP$,
if there is an index $j \in [p]$ such that $val_{\Theta}(d_j) = \perp$,
then we have $val_{\phi_i}(\tilde{d}) = \perp$ and $O[\phi_i(\tilde{d})] = \perp$. But the
same hypothesis do not generally imply that
$O[\langle \tilde{d}, \beta_i \rangle] = \perp$, i.e. the non-termination of the flow-
chart $^1$-computation.

The reason for this discrepancy is that a
generic function in the transform always requires
its actual arguments to be above the threshold,
whereas the flowchart does not have this require-
ment for the initial content of registers.

We could deal with this problem by duplica-
ting 2<sup>P</sup> times each unknown function φ<sub>i</sub>, with a dif-
ferent threshold for each copy, to meet all initial
cases of arguments above or below the threshold.
This would in general require n·2<sup>P</sup> unknown function
symbols in the generic transform, instead of n. In
practice, we may consider that the flowchart is the
body of some procedure which is called only if its
arguments (i.e. the initial values of the registers)
are above the threshold.

Hence we will restrict our strong correct-
ness requirement to the domain $D_\Theta = \{d \in D | val_\Theta(d) = \tau\}$.

The following lemmas 3.1 and 3.2 show that
the flowchart and its generic transform can simulate
each other. The correctness theorem 3.3 follows im-
mediately.

**Lemma 3.1**

$$
\forall \tilde{d} \in D_{\Theta}^{P}, \quad \forall \phi_i \in \Phi, \quad \forall k \in N
$$

$$
\phi_i(\tilde{d}) \xrightarrow{k} t' \text{ implies}
$$

- either $t' = \phi_i(\tilde{t}')$ with $\tilde{t}' \in M(F', D_\Theta)^P$, and
  $\langle \tilde{d}, \beta_i \rangle \xrightarrow{k} \langle \overleftarrow{I}, \iota_D \rangle (\tilde{t}'), \beta_j$

- or
  $t' \in M(F', D_\Theta)$ and
  $O[\langle \tilde{d}, \beta_i \rangle] = \langle I', \iota_D \rangle(t)$

(proof by induction on k)

**Lemma 3.2**

$$
\forall \tilde{d} \in D_{\Theta}^{P} \quad \forall \beta_{i} \in L
$$

$$
a) \langle \tilde{d}, \beta_i \rangle \xrightarrow{k} \langle \tilde{d}', \beta_j \rangle \implies \phi_i(\tilde{d}) \xrightarrow{k} \phi_j(\tilde{t}') \\
\text{with } \tilde{t}' \in \mathcal{M}(F', D_{\Theta})^{\mathcal{P}} \text{ and } \overleftarrow{I'}, \iota_D \xrightarrow{\tilde{t}'} (\tilde{t}') = \tilde{d}'
$$

$$
b) \alpha(\langle \tilde{d}, \beta_i \rangle) = d \implies \phi_i(\tilde{d}) \xrightarrow{t} \\
\text{with } t \in \mathcal{M}(F', D_{\Theta}) \text{ and } \overleftarrow{I'}, \iota_D \xrightarrow{t} (\tilde{t}) = d \\
(\text{proof of a) is done by induction on } k).
$$

**Theorem 3.3** *Strong Correctness on D<sub>θ</sub>*

$$
\forall i \in [n], \quad \forall \tilde{d} \in D_{\Theta}^{P} \quad O[\phi_i(\tilde{d})] = O[\langle \tilde{d}, \beta_i \rangle]
$$

4. SUMMARY

We have defined a concept of threshold evalua-
tion in non-discrete domains, and applied it to the
following points :

1) Uniform treatment of call by value and call by name, generalizing both into a continuum from one to the other.

2) Similar generalization of assignment resulting also in a continuum from the usual assignment to an assignment by name.

3) Analysis of McCarthy's transformation that relates assignment and parameter passing. We showed in particular that, as originally described, it is only weakly correct when applied to the flowchart body of a procedure calling its arguments by name.

4) Formalization of the concept of generic procedure.

5) Uniform treatment, using the "generic mechanism",
of recursive rewriting rules and of simplifications
of base functions in the operational semantics of
recursive (here generic) programs.

The proofs of the lemmas and theorems enou-
ced in this paper will be published in [30].

Acknowledgements

I wish to thank my friends G. Berry, G. Huet,
G. Kahn and D. MacQueen for many helpful discus-
sions, J.J. Levy for constant technical and moral
support and C. Le Moal for her speedy typing.

**References**

[1] J.McCarthy. A basis for a mathematical theory of computation. In *Computer Programming and Formal Systems*, Braffort and Hirschberg Ed., North Holland, Amsterdam, (1963).

[2] R. Strong. Translating recursion equations into flow charts. *Journal of Computer and System Sciences*, Vol.5, N°3. (June 1971).

[3] B. Courcelle. Personal communication. To appear in book form.
[4] D. Scott. Outline of a mathematical theory of computation. *Programming Research Group Monograph N°.2*, Oxford University (1970).

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

[6] J. Vuillemin. Syntax, semantique et axiomatique d'un language de programmation simple. *These de Doctorat es-sciences Mathematiques*, Université de Paris VII, Paris, (1974).
see also
Implementation of recursion in a simple programming language. *Proc. 5th Annual ACM Symposium on Computing*, (1973).

[7] M. Nivat. On the interpretation of recursive program schemes. *Symposia Mathematica*, Vol. XV, Instituto Nationale di Alta Matematica, Italy, pp. 255-281, (1975).

[8] D. Park. Fixpoint induction and proofs of program properties. *Machine Intelligence 8* (eds. B. Meltzer and D. Michie), Edinburgh: Edinburgh University Press, pp.59-77 (1969).

[9] W.P. de Roever. Recursion and parameter-mechanisms : an axiomatic approach. In *Automata, Languages and Programming* (ed. J. Loeckz), pp.34-65, Lecture Notes in Computer Science Vol. 14, Springer-Verlag, Berlin, etc., (1974).

[10] J.W. de Bakker. Least fixed points revisited. *Proc. of Symposium on λ-Calculus and Computer Science Theory*, Roma, pp.1-35, (1975).

[11] G. Boudol. *Langages polédiques algébriques. Théorie des schemas de programmes : semantique de l'appel par valeur*. Thèse 3e cycle, Université Paris VII, (1975).

[12] J. McCarthy et al. *LISP 1.5 Programmer's Manual*, MIT Press, Cambridge, Mass., (1962).

[13] A. van Wijngaarden et al. Revised report on the algorithmic language ALGOL 68. *Acta Informatica*, Vol.5, Fasc.1-3, (1975).

[14] B. Wegbreit et al. *The ECL Programmer's Manual*. Harvard University, Center for Research in Computing Technology, 21-72, (1972).

[15] R.M. Burstall, J.S. Collins and R.J. Popplestone. *Programming in POP-2*. Edinburgh : Edinburgh University Press, (1971).

[16] P.J. Landin. The mechanical evaluation of expressions. *Computer Journal*, Vol.6 N°4.

[17] G.D. Plotkin. Call-by-name, call-by-value and the λ-calculus. *J. Theoret. Comp.Sci.*, 1, 125-159, (1975).

[18] C.P. Wadsworth. Semantics and pragmatics of the lambda-calculus. *Ph.D. thesis*, University of Oxford, (1971).

[19] P. Henderson and J. Morris, Jr. A lazy evaluator. *3rd ACM Symp.on Prin. of Prog. Lang.*, pp. 95-103.

[20] D.P. Friedman and D.S. Wise. CONS should not evaluate its arguments. *Proc. of 3rd Coll. on Automata, Languages and Programming*. Edinburgh, (1976).

[21] G. Kahn and D. MacQueen. Coroutines and networks of parallel processes. Submitted for publication.

[22] E. Wiedmer. *Exaktes Rechnen mit reellen Zahlen*. Eidgenössische Technische Hochschule, Zürich. Bericht nr.20, (1976).

[23] E.A. Ashcroft and W. Wadge. Proving programs without tears. *Proc. Symp. on Proving and improving Programs*, IRIA, Rocquencourt, Huet and Kahn Ed., (1975).

[24] Ph. Jorrands. Contributions au développement des langages extensibles. *Thèse d'Etat*, Université Scientifique et Médicale de Grenoble, (1975).

[25] S.A. Schuman. On generic functions. In *New Directions in Algorithmic Languages* 75 (ed.S.A. Schuman) IRIA, (1976).

[26] R. Burstall and J. Darlington. Some transformations for developing recursive programs. *Proc. of Internat. Conf. on Reliable Software*, Los Angeles, Cal., (1975).

[27] H.P. Barendregt. Some extensional term models for combinatory logics and λ-calculi. *Ph.D. thesis*, University of Utrecht, (1971).

[28] J.M. Cadiou. Recursive definitions of partial functions and their computations. *Ph.D. thesis*, Stanford Un., (1972).

[29] R. Bird. On transformations of programs. *J. Comput. System Sci.*, 8, 22-35, (1974).

[30] B. Lang. Transformations Schematiques. Thèse 3e cycle, Université Paris VII, Paris, (to appear).