Elementary recursive algorithms${\,}^{\ast}$

My understanding of the algorithm defined by $E(\vec{\textup{{x}}})$ in a $\Phi$-structure A is that it calls for solving in A the system of recursive equations in the body of $E(\vec{\textup{{x}}})$ (within the braces $\{\cdots\}$) and then plugging the solutions in its head $E_{0}(\vec{\textup{{x}}})$ to compute $\textup{den}({\textup{{A}}},E(\vec{x}))$, the value of the partial function computed by $E(\vec{\textup{{x}}})$ on the input $\vec{x}$; how we find the canonical (least) solutions of this system is not specified in this view by the algorithm from the primitives of A defined by $E(\vec{\textup{{x}}})$.

This “lack of specificity” of elementary recursive algorithms is surely a weakness of the view I have adopted, especially as it leads to some difficult problems.

To compute $\textup{den}({\textup{{A}}},E(\vec{x}))$ for $\vec{x}\in A^{n}$, we might use the method outlined in the proof of the Fixed Point Lemma LABEL:lfp or the recursive machine defined in Section LABEL:cmodels of ARIC, or any one of several well known and much studied implementations of recursion. These are iterative algorithms defined on structures which are (typically) richer than A and they must satisfy additional properties relating them to $E(\vec{\textup{{x}}})$—we would not call any iterative algorithm from any primitives which happens to compute the same partial function on $A$ as $E(\vec{\textup{{x}}})$ an implementation of it; so to specify the implementations of a recursive program is an important (and difficult) part of this approach to the foundations of the theory of algorithms, cf.  [ynmsicily] and (especially) [ynmpaschalis2008] which proposes a precise definition and establishes some basic results about it.

On the other hand, the standard view has some problems of its own:

Iterators are defined rigorously in ARIC and Theorem LABEL:itrecthmA gives a strong, precise version of the slogan

$$\textit{iteration can be reduced to recursion};$$

(1-5)

on every structure A, if $f:A^{n}\rightharpoonup A_{s}$ is computed by an A-explicit iterator, then $f$ is also computed by an A-recursive program. The converse of (1-5) is not true however: there are structures where some A-recursive relation is not tail recursive, i.e., it cannot be decided by an iterator which is explicit in A—it is necessary to add primitives and/or to enlarge the universe of A. Classical examples include [patterson-hewitt1970] (Theorem LABEL:pathewhm in ARIC), [lynch-blum1979] and (the most interesting) [tiuryn1989].³³3See also [jones1999, jones2001] and [bhaskar2017int, bhaskar2017ext]. The last Chapter LABEL:algebra of ARIC discusses a (basic) problem from algebraic complexity theory, a very rich and active research area in which the recursive representation of algorithms is essential.

It is sometimes argued that the main difference between recursion and iteration is a matter of “programming style”, at least for the structures which are mostly studied in complexity theory in which every recursive partial function is tail recursive, i.e., computed by some A-explicit iterator. This is not quite true: consider, for example the classical merge-sort algorithm (Section LABEL:algexamples of ARIC) which sorts strings from the primitives of the Lisp structure

$${\textup{{L}}^{\ast}}=(L^{\ast},\textup{nil},{\textup{eq}}_{\textup{nil}},\textup{head},\textup{tail},\textup{cons})$$

over an ordered set $L$, (LABEL:stringstr) in ARIC; it is certainly implemented by some ${\textup{{L}}^{\ast}}$-explicit iterator (as is every recursive algorithm of ${\textup{{L}}^{\ast}}$), but which one of these is the merge-sort? It seems that we can understand this classic algorithm and reason about it better by looking at Proposition LABEL:mergelemma of ARIC rather than focussing on choosing some specific implementation of it.⁴⁴4See also Theorem LABEL:sortinglb of ARIC for a precise formulation and proof of the basic optimality property of the merge-sort.

In Proposition LABEL:mergesortprop of ARIC, we claimed the correctness of the merge-sort—that it sorts—by just saying that

The sort function satisfies the equation …

whose proof was too trivial to deserve more than the single sentence

The validity of (LABEL:mergesort) is immediate, by induction on $|u|$.

To prove the correctness of an iterator that “expresses the merge-sort”, you must first design a specific one and then explain how you can extract from all the “housekeeping” details necessary for the specification of iterators a proof that what is actually being computed is the sorting function; most likely you will trust that a formal version of (LABEL:mergesort) of ARIC is implemented correctly by some compiler or interpreter of whatever higher-level language you are using, as we did for the recursive machine.

Simply put, whether correct or not, the view that algorithms are faithfully expressed by systems of recursive equations typically separates proofs of their correctness and their basic complexity properties which involve only purely mathematical facts from the relevant subject and standard results of fixed-point-theory, from proofs of implementation correctness for programming languages which are ultimately necessary but have a very different flavor.

Finally, it may be useful to review here briefly what it means to define algorithms according to a general (and widely accepted, I think) naive view of what it means to define mathematical objects. This is discussed more fully in Section 3 of [ynmsicily].

One standard example is the “definition” (or “construction”) of real numbers using (canonically) convergent sequences of rational numbers: we set first

$$x\in\textup{Cauchy}(\mathbb{Q})\iff x:\mathbb{N}\to\mathbb{Q}\\ {~{}\&~{}}(\forall k)(\exists n)(\forall i,j)\Big{[}i,j\geq n\implies|x(i)-x(j)|<\frac{1}{k+1}\Big{]},$$

next we put for $x,y\in\textup{Cauchy}(\mathbb{Q})$

$$x\sim y\iff(\forall k)(\exists n)(\forall i>n)|x(i)-y(i)|<\frac{1}{k+1},$$

and finally we declare that $x,y\in\textup{Cauchy}(\mathbb{Q})$ represent the same real number if $x\sim y$.

In general, a representation in set theory of a mathematical notion $P$ is a pair of a set (or class) $\mathcal{C}_{P}$ of set-theoretic objects which represent the objects that fall under $P$ and an equivalence condition $\sim_{P}$ on $\mathcal{C}_{P}$ which models the identity relation on them; and the representation is faithful—and can be viewed as a definition of $P$ in set theory—to the extent that the relations on $P$-objects that we want to study are those which are equivalent to the $\sim_{P}$-invariant properties of the objects in $\mathcal{C}_{P}$.

Now, number theorists could not care less about such “definitions” of real numbers and they were happily investigating the existence and properties of rational, algebraic and transcedental numbers for more than two thousand years before they were given in the 1870s. Part of the reason for giving them was to argue for adopting set theory as a “foundation” (a “universal language”) for all of mathematics and to apply set theoretic methods to algebraic number theory;⁵⁵5Most spectacular of these was Cantor’s proof that transcedental numbers exist by a counting argument much simpler than Liouville’s original proof—the first “killer application” of set theory. but this is not the main point—some people would use category theory today and argue for its superiority over set theory as both a foundation and a tool for applications. The main point of looking for such “definitions” is to identify the fundamental, characteristic properties of a mathematical notion, which, to repeat, should be the $\sim_{P}$-invariant properties of the set-theoretic objects that model the notion.

Another, fundamental (and much more sophisticated) example of this process of constructing faithful modelings of mathematical notions is the identification in [kolmogorov1933] of real-valued random variables with measurable functions $X:\Omega\to\mathbb{R}$ on a probability space, under various equivalence relations.\ynmequal, equal almost surely, or equal in distribution

The (pure, explicit) $\Phi^{2}$-terms are defined by the structural recursion

$$F:\equiv{\textup{t\hskip-1.7ptt}}\mid{\textup{ff}}\mid\textup{{v}}_{i}\mid\textup{{p}}^{s,n}(F_{1},\ldots,F_{n})\\ \mid\phi(F_{1},\ldots,F_{\textup{arity}(\phi)})\mid\textup{if }F_{0}~{}\textup{then }F_{1}~{}\textup{else }F_{2},$$

where $\textup{{v}}_{0},\textup{{v}}_{1},\ldots$ is a fixed list of individual variables; for each $s\in\{{\texttt{ind}},{\texttt{boole}}\}$ and each $n\in\mathbb{N}$, $\textup{{p}}^{s,n}_{0},\textup{{p}}^{s,n}_{1},\ldots$ is a fixed list of (partial) function variables of sort $s$ and arity $n$; each term is assigned a sort in the natural way; and a Parsing Lemma (like Problem x1E.1 of ARIC) justifies the standard method of defining functions on these terms by structural recursion.⁶⁶6See Problem x2.1 for a detailed statement and proof of this. We just write $\phi$ for $\phi(~{})$ when $\textup{arity}(\phi)=0$, $\textup{{p}}^{s,0}$ for $\textup{{p}}^{s,0}(~{})$ and we do not allow variables over the set $\mathbb{B}=\{{\textup{ff}},{\textup{t\hskip-1.7ptt}}\}$ of truth values, cf. footnote 9 on p. 37 of ARIC.

A $\Phi$-term is a $\Phi^{2}$-term which has no function variables and a $\Phi\cup\{\textup{{p}}_{1},\ldots,\textup{{p}}_{K}\}$-term is a $\Phi^{2}$-term whose function variables are all in the list $\textup{{p}}_{1},\ldots,\textup{{p}}_{K}$; these terms are naturally interpreted in expansions $({\textup{{A}}},p_{1},\ldots,p_{K})$ of $\Phi$-structures which interpret each $\textup{{p}}_{i}$ by some $p_{i}$ of the correct sort and arity.

An extended $\Phi^{2}$-term is a pair

$$(F,\vec{\textup{{x}}})\equiv F(\vec{\textup{{x}}})\equiv F(\textup{{x}}_{1},\ldots,\textup{{x}}_{n})$$

of a $\Phi^{2}$-term $F$ and a finite list of distinct individual variables which includes all the individual variables that occur in $F$. The notation provides a simple way to deal with substitutions,

$$F(E_{1},\ldots,E_{n}):\equiv F\{\textup{{x}}_{1}:\equiv E_{1},\ldots,\textup{{x}}_{n}:\equiv E_{n}\}\\ (F(\vec{\textup{{x}}})\text{ an extended term, $E_{1},\ldots,E_{n}$ terms of sort ${\texttt{ind}}$}).$$

The denotation (or value) $\textup{den}(({\textup{{A}}},\vec{p}),F(\vec{x}))$ in a $\Phi$-structure A of each extended $\Phi\cup\{\vec{\textup{{p}}}\}$-term $F(\vec{\textup{{x}}})$ for given values $\vec{p},\vec{x}$ of its variables is defined by the usual (compositional) structural recursion on the definition of terms: skipping the $({\textup{{A}}},\vec{p})$ part (which remains constant),

	$$\displaystyle\textup{den}({\textup{t\hskip-1.7ptt}}(\vec{x}))={\textup{t\hskip-1.7ptt}},~{}~{}\textup{den}({\textup{ff}}(\vec{x}))={\textup{ff}},~{}~{}\textup{den}(\textup{{x}}_{i}(\vec{x}))=x_{i},$$
	$$\displaystyle\textup{den}(\textup{{p}}_{i}(F_{1},\ldots,F_{n})(\vec{x}))=p_{i}(\textup{den}(F_{1}(\vec{x})),\ldots,\textup{den}(F_{n}(\vec{x}))),$$
	$$\displaystyle\textup{den}(\phi(F_{1},\ldots,F_{\textup{arity}(\phi)})(\vec{x}))=\phi^{\textup{{A}}}(\textup{den}(F_{1}(\vec{x})),\ldots,\textup{den}(F_{\textup{arity}(\phi)}(\vec{x}))),$$
	$$\displaystyle\textup{den}(\textup{if }F_{0}~{}\textup{then }F_{1}~{}\textup{else }F_{2}(\vec{x}))=\textup{if }\textup{den}(F_{0}(\vec{x}))~{}\textup{then }\textup{den}(F_{1}(\vec{x}))~{}\textup{else }\textup{den}(F_{2}(\vec{x}));$$

and we will also use standard model-theoretic notation,

	$\displaystyle({\textup{{A}}},\vec{p})\models F(\vec{x})=G(\vec{x})$	$\displaystyle\iff\kern-6.49994pt_{\mathrm{df}}~{}\textup{den}(({\textup{{A}}},\vec{p}),F(\vec{x}))=\textup{den}(({\textup{{A}}},\vec{p}),G(\vec{x})),$
	$\displaystyle{\textup{{A}}}\models F(\vec{\textup{{x}}})=G(\vec{\textup{{x}}})$	$\displaystyle\iff\kern-6.49994pt_{\mathrm{df}}~{}(\forall\vec{p},\vec{x})\Big{(}({\textup{{A}}},\vec{p})\models F(\vec{x})=G(\vec{x}\Big{)}$
	$\displaystyle\models F(\vec{\textup{{x}}})=G(\vec{\textup{{x}}})$	$\displaystyle\iff\kern-6.49994pt_{\mathrm{df}}~{}(\forall{\textup{{A}}})\Big{(}{\textup{{A}}}\models F(\vec{\textup{{x}}})=G(\vec{\textup{{x}}})\Big{)}.$

Every (deterministic) extended recursive $\Phi$-program

$$E(\vec{\textup{{x}}})\equiv E_{0}(\vec{\textup{{x}}}){\sf~{}where~{}}\Big{\{}\textup{{p}}_{1}(\vec{\textup{{x}}}_{1})=E_{1},\ldots,\textup{{p}}_{K}(\vec{\textup{{x}}}_{K})=E_{K}\Big{\}}$$

(as in (1-4)) with dimension $K$, arity $n$ and sort $s$ defines naturally on each $\Phi$-structure A the continuous pure recursor on $A$ of sort $s$ and arity $n$

$$\mathfrak{r}({\textup{{A}}},E(\vec{\textup{{x}}}))=(\alpha_{0},\alpha_{1},\ldots,\alpha_{K}):A^{n}\rightsquigarrow A_{s},$$

(3-4)

where

$$\begin{array}[]{rcl}\alpha_{0}(\vec{x},\vec{p})&=&\textup{den}(({\textup{{A}}},\vec{p}),E_{0}(\vec{x})),\\ \alpha_{i}(\vec{x}_{i},\vec{p})&=&\textup{den}(({\textup{{A}}},\vec{p}),E_{i}(\vec{x}_{i}))\quad(1\leq i\leq K)\end{array}$$

(3-5)

or, with the notation in (3-3),

$$\mathfrak{r}({\textup{{A}}},E(\vec{x}))=\textup{den}(({\textup{{A}}},\vec{p}),E_{0}(\vec{x}))\\ \textit{ where }\Big{\{}p_{1}(\vec{x}_{1})=\textup{den}(({\textup{{A}}},\vec{p}),E_{1}(\vec{x}_{1})),\\ \ldots,p_{K}(\vec{x}_{K})=\textup{den}(({\textup{{A}}},\vec{p}),E_{K}(\vec{x}_{K}))\Big{\}}.$$

(3-6)

\ynm

Our understanding of the algorithm expressed by a recursor $\alpha$ in (3-3) is that it calls for solving the system of recursive equations in its body and then plugging the solutions in the head functional to compute the value $\overline{\alpha}(x)=\alpha_{0}(x,\overline{p}_{1},\ldots,\overline{p}_{K})$. How we find the canonical solutions of this system is not specified by $\alpha$: we might use the method outlined in the proof of the Fixed Point Lemma LABEL:lfp, or the recursive machine defined in Section LABEL:cmodels if $\alpha=\mathfrak{r}({\textup{{A}}},E(\vec{\textup{{x}}}))$ is the recursor of an extended program in a structure, or any one of several well-known and much studied implementations of recursion. What the implementations of pure recursors are is an important part of this approach to the foundations of the theory of algorithms, cf.  [ynmsicily] and (especially) [ynmpaschalis2008] which includes a precise definition and some basic results. We will not go into this here, except for a few additional comments on page 4.

The solutions of the system of recursive equations in the body of a recursor $\alpha$ as in (3-3) do not depend on the order in which these equations are listed and the known methods for computing them also do not depend on that order in any important way; so it is natural to identify recursors which differ only in the order in which their bodies are enumerated, so that, for example

$$\alpha_{0}(x,p_{1},p_{2},p_{3})\textit{ where }\Big{\{}p_{1}(y_{1})=\alpha_{1}(y_{1},p_{1},p_{2},p_{3}),\\ \hskip 56.9055ptp_{2}(y_{2})=\alpha_{2}(y_{2},p_{1},p_{2},p_{3}),~{}~{}p_{3}(y_{3})=\alpha_{3}(y_{3},p_{1},p_{2},p_{3})\Big{\}}\\ =\alpha_{0}(x,p_{1},p_{2},p_{3})\textit{ where }\Big{\{}p_{3}(y_{3})=\alpha_{3}(y_{3},p_{1},p_{2},p_{3}),\\ \hskip 28.45274ptp_{1}(y_{1})=\alpha_{1}(y_{1},p_{1},p_{2},p_{3}),~{}~{}p_{2}(y_{2})=\alpha_{2}(y_{2},p_{1},p_{2},p_{3})\Big{\}}.$$

\ynm

Detail for the example We need $q_{1}=p_{3},q_{2}=p_{1},q_{3}=p_{2}$, so take $\pi(1)=3,\pi(2)=1,\pi(3)=2$, with the inverse being $\rho(3)=1,\rho(1)=2,\rho(2)=3$. This then requires the equations

	$\displaystyle\beta_{0}(x,q_{1},q_{2},q_{3})$	$\displaystyle=\alpha_{0}(x,p_{1},p_{2},p_{3})=\alpha_{0}(x,q_{\rho(1)},q_{\rho(2)},q_{\rho(3)})$
	$\displaystyle\beta_{1}(y_{3},q_{1},q_{2},q_{3})$	$\displaystyle=\alpha_{3}(y_{3},p_{1},p_{2},p_{3})=\alpha_{3}(y_{3},q_{\rho(1)},q_{\rho(2)},q_{\rho(3)})$

For these we need to have

$$Y^{\beta}_{1}=Y^{\alpha}_{3}=Y^{\alpha}_{\pi(1)},Y^{\beta}_{2}=Y^{\alpha}_{1}=Y^{\alpha}_{\pi(2)},Y^{\beta}_{3}=Y^{\alpha}_{2}=Y^{\alpha}_{\pi(3)}$$

so

$$q_{i}:Y^{\beta}_{i}=Y^{\alpha}_{\pi(i)}\rightharpoonup W^{\alpha}_{\pi(i)}=W^{\beta}_{i},\text{ so }q_{\rho(i)}:Y^{\alpha}_{i}\rightharpoonup W^{\alpha}_{i}.$$

The precise definition of this equivalence relation is a bit messy in the general case: two recursors $\alpha,\beta:X\rightsquigarrow W$ on the same input and output sets are strongly isomorphic—or just equal—if they have the same dimension $K$ and there is a permutation $\pi:\{1,\ldots,K\}\mbox{\,$\rightarrowtail\kern-8.00003pt\rightarrow$\,}\{1,\ldots,K\}$ with inverse $\rho=\pi^{-1}$ such that

$$\begin{array}[]{c}Y^{\beta}_{i}=Y^{\alpha}_{\pi(i)},\quad W^{\beta}_{i}=W^{\alpha}_{\pi(i)}\quad(i=1,\ldots,K),\\ \beta_{0}(x,q_{1},\ldots,q_{K})=\alpha_{0}(x,q_{\rho(1)},\ldots,q_{\rho(K)}),\\ \beta_{i}(y_{\pi(i)},q_{1},\ldots,q_{K})=\alpha_{\pi(i)}(y_{\pi(i)},q_{\rho(1)},\ldots,q_{\rho(K)}),~{}(1\leq i\leq K).\end{array}$$

(3-8)

Directly from the definitions, strongly isomorphic recursors $\alpha,\beta:X\rightsquigarrow W$ compute the same partial function $\overline{\alpha}=\overline{\beta}:X\rightharpoonup W$; the idea, of course, is that strongly isomorphic recursors model the same algorithm, and so we will simply write $\alpha=\beta$ to indicate that $\alpha$ and $\beta$ are strongly isomorphic. This view is discussed in several of the articles cited above and we will not go into it here.⁸⁸8This finest relation of recursor equivalence was introduced (for monotone recursors) in [ynmbotik], and more general, weaker notions were considered in [ynmsicily, ynmeng] and in [ynmpaschalis2008].

For the recursors defined by recursive programs, this definition takes the following form, where for any $\Phi^{2}$-term $F$ and sequences of distinct function and individual variables $\vec{\textup{{q}}},\vec{\textup{{p}}},\vec{\textup{{y}}},\vec{\textup{{x}}}$ (satisfying the obvious sort and arity conditions),

$$F\{\vec{\textup{{q}}}:\equiv\vec{\textup{{p}}},\vec{\textup{{y}}}:\equiv\vec{\textup{{x}}}\}\\ :\equiv\text{the result of replacing in $F$ every $\textup{{q}}_{i}$ by $\textup{{p}}_{i}$ and every $\textup{{y}}_{j}$ by $\textup{{x}}_{j}$}.$$

(3-9)

{proofplain}

[The proof] is an exercise in managing messy notations and we leave it for Problem x3.1.

Two programs $E$ and $F$ are congruent if $F$ can be constructed from $E$ by an alphabetic change (renaming) of the bound individual and function variables in its parts (as in (3-9)) and a permutation of the equations in the body of $E$. Congruence is obviously an equivalence relation on programs, congruent programs have the same free variables and we write

	$\displaystyle E\equiv_{c}F$	$\displaystyle\iff\kern-6.49994pt_{\mathrm{df}}~{}\text{ $E$ and $F$ are congruent},$
	$\displaystyle E(\vec{\textup{{x}}})\equiv_{c}F(\vec{\textup{{y}}})$	$\displaystyle\iff\kern-6.49994pt_{\mathrm{df}}~{}\vec{\textup{{x}}}\equiv\vec{\textup{{y}}}\text{ and }E\equiv_{c}F.$

By Lemma 3.1, congruent extended programs define equal recursors in every structure A, i.e., for every extended program $E(\vec{\textup{{x}}})$ and every program $F$,

$$E\equiv_{c}F\implies(\forall{\textup{{A}}})[\mathfrak{r}({\textup{{A}}},E(\vec{\textup{{x}}}))=\mathfrak{r}({\textup{{A}}},F(\vec{\textup{{x}}}))],$$

(3-12)

but the converse fails, cf.  Problem x3.2.

The definition of recursors we gave is basically the one in [ynmbotik], except that we allowed there the parts $\alpha_{i}$ of $\alpha$ to be (monotone but) not continuous and to depend on the input set $X$, i.e.,

$$\alpha=(\alpha_{0},\alpha_{1},\ldots,\alpha_{K}):X\rightsquigarrow W,$$

($\star$)

such that for suitable sets $Y^{\alpha}_{1},W^{\alpha}_{1},\ldots,Y^{\alpha}_{K},W^{\alpha}_{K}$,

	$\displaystyle\alpha_{0}:(Y^{\alpha}_{1}\rightharpoonup W^{\alpha}_{1})\times\cdots\times(Y^{\alpha}_{K}\rightharpoonup W^{\alpha}_{K})\times X$	$\displaystyle\rightharpoonup W,\text{ and}$
	$\displaystyle\alpha_{i}:Y^{\alpha}_{i}\times(Y^{\alpha}_{1}\rightharpoonup W^{\alpha}_{1})\times\cdots\times(Y^{\alpha}_{K}\rightharpoonup W^{\alpha}_{K})\times X$	$\displaystyle\rightharpoonup W^{\alpha}_{i}\quad(1\leq i\leq K).$

Allowing the parts to be discontinuous is necessary for the theory of higher-type recursion which was the topic of [ynmflr, ynmbotik], but their dependence on the input set $X$ is not: the simpler, present notion is easier to work with and it includes the more general objects if we identify $\alpha$ in ($\star$ ‣ 3) with

$$\alpha^{\prime}=(\alpha^{\prime}_{0},\alpha^{\prime}_{1},\ldots,\alpha^{\prime}_{K}):X\rightsquigarrow W$$

on the sets $Y^{\prime}_{i}=X\times Y_{i},W^{\prime}_{i}=W_{i}$ ($1\leq i\leq K$) with

	$\displaystyle\alpha^{\prime}_{0}(x,p_{1},\ldots,p_{K})$	$\displaystyle=\alpha_{0}(\lambda y_{1}p(x,y_{1}),\ldots,\lambda y_{K}p(x,y_{K}),x),$
	$\displaystyle\alpha^{\prime}_{i}(x,y_{i},p_{1},\ldots,p_{K})$	$\displaystyle=\alpha_{i}(\lambda y_{1}p(x,y_{1}),\ldots,\lambda y_{K}p(x,y_{K}),x)\quad(1\leq i\leq K).$

Substantially more general notions of (monotone and continuous) recursors whose solution spaces are products of arbitrary complete posets were introduced in [ynmsicily, ynmeng] and (in greater detail) in [ynmpaschalis2008]; and it is routine to define nondeterministic algorithms along the same lines, using the fixpoint semantics of nondeterministic programs on page LABEL:ndfpsemantics of ARIC.

For the syntactic work we will do in this Section we need to enrich and simplify the notation of ARIC summarized in Section 2.

We introduce two function symbols $\textsf{cond}_{s}$ of arity $3$ and sort $s$ ($\equiv{\texttt{ind}}$ or boole) and the abbreviations

$$\textsf{cond}_{s}(F_{0},F_{1},F_{2}):\equiv\textup{if }F_{0}~{}\textup{then }F_{1}~{}\textup{else }F_{2};$$

this is semantically inappropriate because the conditionals do not define (strict) partial functions, but it simplifies considerably the definition of pure, explicit $\Phi^{2}$-terms on page 2 which now takes the form

$$F:\equiv{\textup{t\hskip-1.7ptt}}\mid{\textup{ff}}\mid\textup{{v}}_{i}\mid\textup{{c}}(F_{1},\ldots,F_{n}),$$

(Pure explicit terms)

where c is any $n$-ary function symbol $\phi$ in the vocabulary $\Phi$, or an $n$-ary function variable $\textup{{p}}^{s,n}_{i}$ or $\textsf{cond}_{s}$ (and $n=3$).

With each extended $\Phi$-program $E(\vec{\textup{{x}}})$ as in (4-1), we associate its set representation

$$\textup{set}(E(\vec{\textup{{x}}}))=\Big{\{}E_{0}(\vec{\textup{{x}}}),~{}~{}\textup{{p}}_{1}(\vec{\textup{{x}}}_{1})=E_{1},\ldots,~{}~{}\textup{{p}}_{K}(\vec{\textup{{x}}}_{K})=E_{K}\Big{\}}.$$

(4-2)

Notice that $\textup{set}(E(\vec{\textup{{x}}}))$ determines $E_{0}(\vec{\textup{{x}}})$, its only member which is not an equation, and by the definition of the congruence relation on page 3,

$$\textup{set}(E(\vec{\textup{{x}}}))=\textup{set}(F(\vec{\textup{{x}}}))\implies E\equiv_{c}F;$$

the converse implication fails, but the algorithm which computes canonical forms naturally operates on these set representations of extended terms, so having a notation for them simplifies greatly its specification.

A term $I$ is immediate if it is an individual variable or a direct call to a recursive variable applied to individual variables,\ynmChecked this out in detail.

$$I:\equiv\textup{{v}}_{i}\mid\textup{{p}}^{s,0}\mid\textup{{p}}^{n,s}_{i}(\textup{{u}}_{1},\ldots,\textup{{u}}_{n});$$

(Immediate terms)

and a term $F$ is irreducible if it is immediate, a Boolean constant, or of the form $\textup{{c}}(I_{1},\ldots,I_{l})$ with immediate $I_{1},\ldots,I_{n}$,⁹⁹9There are natural sort restrictions in these definitions and assignments of sorts to immediate and irreducible terms that we will suppress in the notation, cf. Problem x4.1.

$$F:\equiv I\mid{\textup{t\hskip-1.7ptt}}\mid{\textup{ff}}\mid\textup{{c}}(I_{1},\ldots,I_{n})$$

(Irreducible terms)

For example, $\textup{{u}},\textup{{p}}(\textup{{u}}_{1},\textup{{u}}_{2},\textup{{u}}_{1})$ are immediate, $\phi(\textup{{u}})$ and $\textup{{p}}(\textup{{u}},\textup{{q}}(\textup{{v}}),\textup{{r}}(\textup{{u}}))$ are irreducible but not immediate, and $\textup{{p}}(u,\phi(\textup{{v}}))$ is reducible.