数理解析研究所講究録
918 巻 1995 年 224-237

224

Non-Standard Recursion Theory
Tohru NAOI
Faculty of Engineering, Gifu University
Yanagido, Gifu-shi, JAPANemail: naoi@info.gifu-u.ac.jp
Abstract. This paper investigates a new approach to the recursive function theory, which is suitable for dealing with computational models based on term-rewriting. The set of natural numby adding parbers is completed into a countable algebraic
tial numbers and . Primitive recursion is interpreted as a way
to define continuous functions on this “non-standard” structureof numerals. It is shown that recursive functions can be formaland quasi-primitiveized as functions definable by the constantrecursion, a slightly generalized version of primitive recursion.
Also, computability of those functions is discussed through anorder-theoretic semantics of term rewriting systems. Finally, therelation between quasi-primitive and primitive recursion is investigated.
$\mathrm{c}\mathrm{p}o$$\infty$$\infty$

1

Introduction

As shown by Herbrand, G\"odel and Kleene [5], partial recursive functions canbe defined by first-order equations. Once mathematical objects are describedin such a formal way, the description itself generally admits non-standard
interpretations. Namely, equations which are originally intended to definefunctions over the set $N$ of natural numbers can be viewed as a descriptionof functions over a set other than $N$ . A non-standard interpretation of thiskind has been proposed and studied by the authors’ previous paper [9]. The
present paper describes some new results on this framework.
An advantage of the new interpretation is that it allows the ordinary
inference by equational axioms. For example, suppose that the conditional
functionis defined as $if(\mathrm{O}, x, y)=x$ and $\dot{i}f(s(x), y, z)=z$ by primitive
recursion. Then, an equation
derived from the first axiom
is valid for any terms and in our interpretation. On the other hand, inthe conventional interpretation, it is valid only if the value of is defined.
This inconvenience arises because one interprets $if$ as a partial function.
To compute these partial functions, we are forced to adopt eager evaluation
strategies. That is, before we reduce
to , we should evaluate thesubterm
to assurebeing defined. This does not seem to be a natural
policy to computation.
Scott’s mathematical tools for program semantics [11] enables us to formalize computable numerical functions without referring to evaluation or inference strategies. Our new interpretation, mainly based on Scott’s approach,$\dot{i}f$$\dot{i}f(\mathrm{O}, t_{1}, t_{2})=t_{1}$$t_{1}$$t_{2}$$t_{2}$$\dot{i}f(\mathrm{O}, t_{1}, t_{2})$$t_{2}$$t_{2}$$t_{1}$

225

claims that recursive functions described by equations are not partial functions over $N$ but continuous functions over a superset of $N$ , a complete partial. This framework generalizes the conventional one because
order named
partial functions can be treated as a special case of continuous functions.
,consists of total natural numbers
The complete partial order$s(s(\perp)),$, and infinity ,, partial natural numbers
the state that a program does not termiwhere the least
nate and produces no outputs.
Partial natural numbers appear since we obey a premise $\perp\neq s(\perp)$ .
au
arThese two elements should be distinguished with each other
that
it
is
at least gives information
ries entirely no information but
not equal to . In fact, the sign function defined by $S\dot{i}gn(0)=0$ and
as $S\dot{i}gn(\perp)=\perp$
sign $(S(x))=s(0)$ detects the difference, where the latter is obtained from the second axiom
but
on sign.1 Those partial numbers require the existence of for the orderis the unique (and least) upper bound of theto be complete: The infinity, and the unique (and least) fixed point of .
We remark that this order structure is more complicated than the flat
lattice discussed in Scott [11]: One can obtain a similar flat order fromby forcing $\perp=s(\perp)$ since it implies $\perp=s(\perp)=s(s(\perp))=\cdots=\infty$ .
However, such a flat order is not suitable for our purpose since $\perp=s(\perp)$, an infeasible equality.
also
Recall that bounded-minimization can be defined with primitive recur-minimization works as minision. It is natural to conjecture thatis used as the bound of search. To prove this, we need tomization when
consider a slightly generalized version of primitive recursion, quasi-primitive
recursion. It will also be shown that the descriptive powers of quasi-primitiveand primitive recursions are the same in the conventional interpretation,
while they differ in our interpretation.
Now, the following summarizes the contents of the present paper. Section
2 introduces basic definitions. In Section 3, we shall first illustrate the conand several properties on continuous functions over this set.
struction ofThen, quasi-primitive recursive functions are formalized and studied. Finally,
the notion of recursive functions are defined in the way discussed above. In
Section 4, we shall study the computational aspect of recursive functions using the notion of infinite term-rewriting. In Section 5, the descriptive powersof quasi-primitive and primitive recursions are compared.
$N_{\infty}$$0,$$N_{\infty}$$s(s(\mathrm{O})),$$\perp,$$\ldots$$s(\perp),$$s(\mathrm{O})$$\infty$$\ldots$$\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}\perp \mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{S}$$\mathrm{b}\mathrm{e}c$$s\mathrm{e}\perp c$$s(\perp)$$0$$\mathrm{b}\mathrm{e}\mathrm{t}\mathrm{w}\mathrm{e}\mathrm{e}\mathrm{n}\perp \mathrm{a}\mathrm{n}\mathrm{d}s(\perp)$$S\dot{i}gn(S(\perp))=s(\mathrm{O})$$\infty$$N_{\infty}$$\infty$$c\mathrm{h}\mathrm{a}\mathrm{i}\mathrm{n}\perp\subseteq s(\perp)\subseteq s(s(\perp))\subseteq\cdots$$s$$N_{\infty}$$\mathrm{i}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{i}\mathrm{e}\mathrm{s}\perp=S\dot{i}gn(\perp)=sign(s(\perp))=s(0)$$\mathrm{b}\mathrm{o}\dot{u}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{d}$$\infty$$N_{\infty}$

1Another equality sign$(\perp)=\perp \mathrm{a}\mathrm{l}\mathrm{w}\mathrm{a}\mathrm{y}_{\mathrm{S}}$holds in our interpretation.

226

2

Preliminary Definitions

2.1

CPOs and Continuous Functions

We introduce preliminary notions on CPOs an continuous functions. For
more details of these subjects, see e.g., a tutorial in [1].
be a partial order. An -ary function on $D$ is aid to beLetfor any
impliesmonotone if$D$ is$d_{n}\inD$
and. A subset of
directed if it is nonempty
and.
and $d_{2}\in S$ , there exists $d\in S$ such thatand for any
such that there is
A complete partial order $(CPO)$ is a partial order$D$$D$a least element in , and every directed subset of has its l.u.b. denotedby US.
be a CPO. A function
on $D$ is aid continuous if for any
Let,of $D,$
holds.
directed subsets
It is known that every continuous function is monotone and that continuousfunctions are closed under composition.
is compact if for every directed subset
An element of a CPO
for some $s\in S$ . Let be the set of all compact
impliesof $D,$
is an algebraic $CPO$ (with baseelements in $D$ . We say that the CPO$\{c|C\nic\subseteqd\}$$C)$ if for any$D,$is directed and $d=\mathrm{u}\{c|C\ni c\subseteq d\}$inholds.
$\mathrm{d}$$n$$\langle D, \subseteq\rangle$$c_{n}\subseteq d_{n}$$c_{1}\subseteq d_{1},$$\ldots,$$c_{1},$$\ldots,$$d_{1},$$c_{n}$$s$$\varphi$$\varphi(c_{1}, \ldots, C_{\mathcal{R}})\subseteq\varphi(d_{1}, \ldots , d_{n})$$S$$\ldots,$$d_{2}\subseteq d$$d_{1}\subseteq d$$d_{1}$$\langle D, \subseteq\rangle$$S$$\langle D, \subseteq\rangle$$s$$\varphi$$S_{1},$$\ldots$$\varphi(\mathrm{u}S_{1}, \ldots, \mathrm{u}S_{n})=\mathrm{u}\varphi(s_{1}, \ldots, S_{n})$$S_{n}$$S$$\langle D, \subseteq\rangle$

$c$

$C$

$c\subseteq s$$c\subseteq \mathrm{u}S$$\langle D, \subseteq\rangle$

$d$

2.2

Terms and Infinite Trees

In this section we informally introduce the notion of infinite trees. A preciset,reatment of the notion is found in, e.g., [2].
Let $F,$ $B$ , and $X$ be the set of unknown function symbols, base function
symbols, and variable symbols, respectively. These three sets are countablean mutually disjoint. Each symbols are associated with a natural number
alled arity, and a variable symbol always has arity .
-tree is a finite or infinite tree such that every node isAnlabeled with a symbol in $F\cup B\cup X$ , and for any node, the mber of thechildren nodes is equal to the arity of the label on the node. We denote the setof-trees by $T_{\infty}(F\cup B, X)$ , and the set of finite-trees
by $T(F\cup B, X)$ . A finite-tree is identified with a well-formed
term.
be a tree. We write NodeLet
for the set of nodes of . For in$T(p)$ is the label ofNodeand $T\lceil parrow T’$ ] denotes the tree obtainedby replacing the subtree of with root by another tree $T’$ . We define an$p\leq q$ iff
order on Nodeas follows: For all and in Node
is an
$P$
$\min(P)$ denotes the set of minimal
ancestor of . For a subset of Node$P$
nodes in w.r.t.
above.
denotes the set of variable symbols occur in
For a tree $T,$aslabels.
$\mathrm{d}$

$0$

$c$

$\langle F\cup B, X\rangle$$\mathrm{n}u$$\langle F\cup B, X\rangle$$\langle F\cup B, X\rangle$$\langle F\cup B, X\rangle$

$T$

$T$

$(\tau)$$(\tau),$

$p$

$p$

$T$

$(\tau)$$\leq$

$p$

$p$

$q$

$(\tau),$$p$$(\tau),$$q$$\leq$$\mathrm{V}\mathrm{a}\mathrm{r}(T)$

$T$

227

We now define the denotation of a term as a continuous function on a
(on $D$ ) is a
. For a subset of $F\cup B$ , an interpretation ofCPO
map $I:G arrow\bigcup_{n}\{D^{n}arrow D\}$ such that for any in with arity $I(g)$ is an-ary function on $D$ . We often write for $I(g)$ . A continuous interpretation
is an interpretation such that every $I(g)$ is continuous.
and a term in $T(G, X)$ . For disbe an interpretation ofLet, a function
such thattinct variable symbols$D^{n}arrowD$
is defined inductively by:
:
$G$

$G$

$\langle D, \subseteq\rangle$

$G$

$g$

$n$

$n,$

$g_{I}$

$I$

$G$

$I$

$x_{1},$$\ldots,$$t$$\mathrm{v}_{\mathrm{a}\mathrm{r}}(t)\subseteq\{x_{1}, \ldots, x_{n}\}$$x_{n}$$t_{I}^{x_{1},\ldots,x_{n}}$1. If $t=x_{i}$ for some , then for$d_{n}$$d_{1},$$\dot{i}$$\ldots,$

in $D$ ,$t_{I}^{x_{1},\ldots,x}n(d_{1}, \ldots, d_{n})=di$

2. If $t=g(t_{1}, \ldots, t_{m})$ for some$g$and some.

$t_{m}$$t_{1},$$\ldots,$,$t_{I}^{x_{1},\ldots,x_{n}}(d_{1}, \ldots, dn)=g_{I}(c_{1}, \ldots, c_{m})$where$c_{i}=(t_{i})^{x_{1}}I’\ldots,x_{n}(d_{1}, \ldots, d_{n})$for each .
$\dot{i}$Since continuous functions are closed under composition, we get:). For any contin uous interpretation I of
Proposition 2.2.1 (Niva$T(G,\{X_{1},\ldots,X_{n}\})$
is contin uous.
, a function
inand any$t[\mathit{1}\mathit{0}]$$t\mathrm{e}rmt$$G$$t_{I}^{x_{1},\ldots,x_{n}}$3Recursive Functions

3.1

Completion of Natural Numbers

mentioned in Section 1.
We shall now construct the ordered set
Let $N$ be the set of natural numbers, and let$\langle N_{\infty}, \subseteq\rangle$$N_{\infty}$$\{\{n\}|n\in N\}$$=$$\cup\{\{k|n\leq k\in N\}|n\in N\}$$\cup\{\emptyset\}$

.

. A
in
for andiffby:on
We define an order
will be identified with and a set $\{k|n\leq k\}$ is denoted bysingleton; the latter is called a partial natural number. The set $\{n\uparrow|n\in N\}$ of allforand. We also
partial natural mbers is written as
write
conventions,
an
we
these
. Under$\subseteq$$d\subseteq d’$$N_{\infty}$$\{n\}$$d\supseteq d’$

$d$

$d’$

$N_{\infty}$$n$$n\uparrow$$N\uparrow$$\mathrm{n}u$$\mathrm{w}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{e}\perp \mathrm{f}\mathrm{o}\mathrm{r}\mathrm{o}\dagger$$\infty$$c$$\emptyset$$N_{\infty}=N\cup N\uparrow\cup\{\infty\}$and draw Fig. 1 to illustrate the order.
.
, and
iff
Note that $n\leq m$ iff
is intuitively explained as follows. Consider a
The construction ofloop program to search a number that satisfies a certain condition and$n\uparrow\underline{[:}m$$n\uparrow\subseteq m\uparrow$$N_{\infty}$$x$$\infty=\mathrm{U}\{n\uparrow|n\dagger\in N\uparrow\}$

228

suppose that at the n-th iteration, the program tests as a andidate ofis successful, an answer that $x\in\{n\}$ , or $x=n$ is. If the test for
failed for $n-1$
obtained. On the other hand, the state that the test has$n\uparrow=\{k|n\leq
k\}$
which
claimsthatifthe number,byis represented
exists, then must be in $\{k|n\leq k\}$ , or at this moment, which gives no information about ,. The least element
in
state
that
the search starts, and all the states oftheinitialcorresponds to.
this successful execution will form an increasing chain
Contrastively, if there are no numbers that pas the test, the “result” of theor $x=\infty$ . Thus,is the l.u.b. of an infinite
non-terminating search is, which is the ”limit” of the chain and tually,chain
the program can not reach it by finite repetition.
$n$

$c$

$n$

$x$

$\mathrm{j}us\mathrm{t}$$x$$x=n\uparrow \mathrm{h}\mathrm{o}\mathrm{l}\mathrm{d}s$$x$$\perp=0\uparrow$$N_{\infty}$$x$$0\uparrow\subseteq 1\uparrow\subseteq\cdots\underline{\subset \mathrm{I}}7l\uparrow\subseteq n$$s$$x\in\emptyset$$\infty$$0\uparrow\subseteq 1\uparrow\subseteq\cdots\subseteq n\uparrow\subseteq\cdots$

Theorem 3.1.1.
elemen$\langle N_{\infty}, \subseteq\rangle$$\mathrm{a}c$is an algebraic $CPO$ with base$N\cup N\uparrow \mathrm{a}nd$

least$t\perp$-,:
Corollary 3.1.2 Let
is continuous iff
monotone.
$N_{\infty}$$\varphi$$\tau l_{len},$$N_{\infty}$

be a function such that$\varphi|_{N\cup N\lceil}$is$\varphi$$\varphi(\infty)=\mathrm{u}\mathrm{t}\varphi(n\uparrow)|n\dagger\in N\uparrow\}$.

is stable if $\varphi(N, \ldots, N)\subseteq N$ :We say that an -ary function on
This notion corresponds to the totality of functions on $N$ in the conventional framework. As well, is said strict $w.r.t$ . the -th argument if for any
impliesin. An -ary function isstrict if it is strict w.r.t. every argument. Also, in the conventional framework, if one of the argument to a function is undefined, then so is the valueof the function. Remark that we can treat this sit ation by considering strict
functions.
$n$$N_{\infty}$$\varphi$$i$$\varphi$$d_{1},$$d_{n}$$N_{\infty},$$\ldots,$$\varphi(d_{1}, \ldots , d_{n})=\perp$$d_{i}\not\in N$

$n$

$u$

.

.

$\underline{9}$$.\cdot$$\nwarrow$1$\nearrow$$2\uparrow$$\nearrow$$\nwarrow$$0$$1\uparrow$$\nearrow$$\nwarrow$$\perp$Figure 1:$\langle N_{\infty}, \subseteq\rangle$$\infty$229

We shall now define the successor function$s$$s(n)$$=$$n+1$$s(n\uparrow)$$=$$(n+1)\uparrow$$s(\infty)$$=$$\infty$on$N_{\infty}$

as follow :$s$.

is partitioned into two well-founded -chains, $N$ andis the unique fixedpoint of .
. Clearly,
one singleton
Note that$s$$N_{\infty}$$\{\infty\}$

Lemma 3.1.3$Tl_{l}e$

, and

$s$

$\infty$successor function is stable, continuous, and not strict.
$s$

The strict version of can be obtained as the composition ofcertain function that will be introduced later.
$s$

3.2

$N\uparrow$

and a

$s$

Quasi-Primitive Recursion

In this subsection, we shall formulate quasi-primitive recursion, together withprimitive recursion, in a more formal way than the conventional framework.
of terms in $T(F\cup B, X)$ ,An equation (on $T(F\cup B,$ $X)$ ) is a pair$E$of equations, we denote, bywhich will be written as $t=u$ . For a set$(E)$ationsthat occur insymbolsbasefunction, the set of unknown or
Funof . For an interpretation of Fun $(E)$ , we say that I satisfies $E$ if for any.
holds with
$t=u$ in $E,$
$B$
of
zero
and
succ
with
the
set
consists
From now on, we suppose that, the standard interpretation
arities and 1, respectively. We denote, by$B$ that maps zero toand succ to .
of$\langle t, u\rangle$$\mathrm{e}\mathrm{q}u$

$E$

$I$

$\{x_{1}, \ldots, x_{n}\}=\mathrm{v}_{\mathrm{a}\mathrm{r}}(t)\cup \mathrm{v}_{\mathrm{a}\mathrm{r}}(u)$$t_{I}^{x_{1}}’\ldots,x_{\eta}=u_{I}^{x_{1},\ldots,x_{n}}$$0$$\triangle_{B}$

$0$

$s$

Definition 3.2.1 A quasi-primitive recursive definition (QPRD) is a set of
equations on $T(F\cup B, X)$ defined inductively as follows.

1. An empty set is

$a$

QPRD.

be
. Also let
2. Letbe a QPRD andmutually distinct variable symbols.
a function symbol andand one of the following systems of equations
Then, the union ofis a QPRD.
$f\not\in G_{0}$$G_{0}=\mathrm{F}\mathrm{u}\mathrm{n}(E_{0})\cup B$$E_{0}$$x_{1},$$E$$\ldots,$$x_{n}$$E_{0}$(2a) Constant functions.
$f(x_{1}, \ldots, X_{n})=t\in T(B, \emptyset)$(2b) Projection Functions. For some$\dot{i}\geq 0$,$f(x_{1,\ldots,n}X)=x_{i}$(2c) Function Composition. For some

$g,$

.

.

$h_{1},$$\ldots,$$h_{m}\in G_{0}$,$f(x_{1,\ldots,n}x)=g(h_{1}(x_{1}, \ldots, Xn), \ldots, h_{m}(X_{1}, \ldots, x_{n}))$

.

230

(2d) Quasi-Primitive Recursion. For some $g,$$h,$ $k_{2},$in$k_{n}$$\ldots,$$G_{0}$,,$f(Zero, X_{2,\ldots,n}X)$$=$$g(x_{2\cdot\cdot n},., x)$$f(suCC(X_{1}), x_{2}, \ldots, x_{n})$$=$$h(f(x_{1}, k2(X_{2}),$ $\ldots$, $k_{n}(X_{n})),$ $X1,$$\ldots,$$X)n$

A primitive recursive definition $(PRD)$ is a QPRD such that whenever thecase (2d) is applied,,
are the identity function.
$k_{2},$$\ldots$$k_{n}$

Lemma 3.2.2 Let
be a set of two equations given inabove,aset of function symbols such th at
and
, and
a
continuous in terpretation ofon. Then, a continuous interpretationof $G_{0}\cup\{f\}$ th at satisfies the following conditions uniquely exists.
$E_{1}$$(\mathit{2}d)$$g,$ $h,$ $k_{2},$$f\not\in G_{0}$$G_{0}$

1. I extends$I_{0}$and sa tisfies$\ldots,$$G_{0}$$k_{n}\in G_{0}$$I_{0}$$I$$N_{\infty}$$E_{1}$, and,

2. $f_{I}(\perp, d_{2}, \ldots, d_{n})=\perp holds$ for any$d_{2},$$d_{n}$$\ldots,$in$N_{\infty}$.

This lemma can be shown by induction on $N$ and on, and Tar
fixedpoint theorem. It helps $us$ to formulate an interpretation specified by a
QPRD:

$s\mathrm{k}\mathrm{i}’ s$$N\uparrow$

Definition 3.2.3 For a QPRD $E$ , the denotational interpretation of $E$ , de, is an interpretation of Fun $(E)\cup B$ defined inductively as below.
noted by$\triangle_{E}$1. If $E=\phi$ , then$\triangle_{E}=\triangle_{B}$.

2. Otherwise, there are a partitionof and a function symbol
such thatis a QPRD, andis one of the sets ofations fromin Definition 3.2.1:$\{E_{0}, E_{1}\}$$f\not\in \mathrm{F}\mathrm{u}\mathrm{n}(E_{0})\cup B$$E_{0}$$E_{1}$$(2\mathrm{a}-2\mathrm{d})$$\mathrm{e}\mathrm{q}u$$(2\mathrm{a}-2\mathrm{c})\triangle_{E}=\triangle_{E_{0}}\cup\{frightarrow t_{\Delta_{E}0}^{x_{1},\ldots,x_{n}}\}$

(2d)

$E$

$\triangle_{E}$

is

$I$

, where $E_{1}=\{f(x_{1,\ldots,n}X)=t\}$

in Lemma 3.2.2 with

$G_{0}=\mathrm{F}u\mathrm{n}(E_{0})\cup B$

and$I_{0}=\triangle_{E_{0}}$Theorem 3.2.4 For any QPRD $E$ , the denotational in terpretation
isfies .

$\triangle_{E}$

.

sat-

$E$

Definition 3.2.5 An -ary function on
is quasi-primitive recursive if it
is definable by some QPRD , that is, it belgongs to the range of.
$n$$N_{\infty}$$E$$\triangle_{E}$Theorem 3.2.6 Every quasi-primitive recursive function is
tinuous.

$st\mathrm{a}ble$and con-Let us see some examples of quasi-primitive recursive functions which willplay important roles in the later of this paper. For notational simplicity, we
shall leave each QPRDs anonymous and often identify a function symbol (say$f)$ with its interpretation (say).
$f_{\triangle_{E}}$

.

231

to
Projection. From now on, we call the -th projection fromdefined by (2b) as . This function is, of course, not strict.
The strict “projection”, e.g., , can be defined by primitive recursion as:$i$$(N_{\infty})^{n}$$N_{\infty}$$u_{i}^{n}$$\tilde{u}_{2}^{2}$$=$$x_{2}$$\tilde{u}_{2}^{2}(sucC(x_{1}), X_{2})$$=$$\tilde{u}_{2}^{2}(x_{1}, x_{2})$(zero,

Lemma 3.2.7 The functioninandfor any$N_{\infty},$$d_{2}$$d_{1}$,)$\tilde{u}_{2}^{2}$$\tilde{u}_{2}^{2}$$d_{1}\not\in N$$x_{2}$.

is strict $w.r.t$ . the first argument. That is,.
implies$\tilde{u}_{2}^{2}(d_{1}, d_{2})=\perp$

Degeneration. The degeneration function defined below maps every $n\in N$. This function will project any functions on
to and every
to the conventional world.
$N^{\infty}$$d\not\in N\mathrm{t}\mathrm{o}\perp$$n$degen $(X)=\tilde{u}_{2}^{2}(X, X)$ .

Conditional. The following defines the conditional function with true represented by an false represented by any $d\in N_{\infty}-\{0, \perp\}$ .
$0$$\mathrm{d}$$\dot{i}f(zero, x1, x2)$$=$

$x_{1}$$\dot{i}f(succ(x), x1, X2)$$=$

$x_{2}$,.

be $(k+1)$ -ary functions on
andBounded minimization. Let. We ayinis the bounded-tuplefor aand write,inminimization with respect to if for any $n\in N$ an$k$$\overline{m}$$N_{\infty}$$\beta$$\pi$$N^{k}$$\langle m_{1}, \ldots, m_{k}\rangle$

$\pi$

if

$\min\{i\in N|\pi(\dot{i},\overline{m})=0\}$$\beta(n,\overline{m})=\{$$s$$\mathrm{d}\overline{m}$$7\ulcorner(i,\overline{m})=0$$\beta$$N^{k}$

for some$\dot{i}\leq n$,$n+1$ otherwise.

where $\min$ denotes the minimum with respect to the usual order on $N$ .

Lemma 3.2.8 If is quasi-primitive recursive, then so is the bounded $\min-$. : If is represented by a function symbol $p(i.e.,$
imiza tion
for some $E$ ), then represented by a symbol is $obt$ ained by the following
equa tion :$\pi$$\beta_{W.r.t}$

$T$

$\pi$

$\pi=p\triangle_{E}$$b$$\beta$$\mathrm{s}$$b’(zero,\overline{x}, Z)$, zero, succ $(Zero))$ ,, zero, succ $(b’(y,\overline{x}, Succ(z))))$ ,$=$$\dot{i}f(p(z,\overline{X})$$b’(Succ(y),\overline{x}, z)$$=$$if(p(z,\overline{X})$$b(y,\overline{x})$$=$$b’(y,\overline{X}, Zero)$.

Suppose that there is such thatis “false” (i.e., in $N_{\infty}-\{0,$). We therefore obtainfor all . Then, for any. (See Corollary 3.1.2). The left-hand side virtually expresses
search and the right-hand side mean the failure of the search.
Note that the equational system in the lemma above is not a PRD but a
QPRD. Although we can define bounded minimization by PRDs, the above
definition is crucial for the result in the next section, where we shall see theminimization operation can be replaced by bounded minimiz.
$\overline{d}$$n\uparrow,$$\dot{i}$$\pi(\dot{i},\overline{d})$$\perp\}$$\beta(n\dagger,\overline{d})=(n+1)\uparrow$$\beta(\infty,\overline{d})=\infty$”$\zeta(\mathrm{u}\mathrm{n}\mathrm{b}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{d}$$s$$a\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}+\infty$

232

Minimization and Recursive Functions

3.3

In this section, we extend the class of functions dealt with in order to obtain
the general class of computable functions. In the conventional framework, one
introduces the operation of minimization for this purpose. In our framework,
we do not require the operation as discussed below.
First we remark that in QPRDs there is no way to express
since weonly have zero as an constant symbol and quasi-primitive recursive functions(including ) are stable. Thus, we now extend our language by adding
new constant symbol inf to the set $B$ of base function symbols: We let$B_{inf}=B\cup\{\dot{i}nf\}$ and define the standard interpretationofby.
$\infty$$s$$a$$\triangle_{B_{\inf}}$$B_{inf}$$\triangle_{B_{\inf}}=\triangle_{B}\cup\{inf\vdash\Rightarrow\infty\}$

Definition 3.3.1 A recursive definition $(RD)$ is a setof equations on$T(F\cup B_{\inf}, X)$ , which is defined in the same way as SPRDs except thatis used instead of . For an RD , the denotational interpretationofis also defined similarly. An -ary function on
is said to be recursive if
it belongs to the range offor some RD .
$E$

$B_{\inf}$

$B$

$E$

$\triangle_{E}$

$n$

$E$

$N_{\infty}$$E$$\triangle_{E}$Theorem 3.3.2 For any $RDE$ , the interpretation$\triangle_{E}$satisfies $E$ .

Theorem 3.3.3 Every recursive function is continuous.
In general, recursive functions are not stable, and then, not quasi-primitive
recursive: The following defines a representation undef, which is a nonstable constant.
undef $=degen(\dot{i}nf)$ .
$\mathrm{o}\mathrm{f}\perp$

Using undef an inf, every element in
is now representable by a term.
Let be a $(k+1)$ -ary function on. A minimization with respect tois a -ary function that atisfies: For any,$\mathrm{d}$$N_{\infty}$$N_{\infty}$

$\pi$

$k$

$\mu$

$\mu(\overline{m})=\min\{\dot{i}\in N|\pi(\dot{i},\overline{m})=0\}$$\{$$\mu(\overline{m})\not\in N$$\pi$$\overline{m}\in N^{k}$

$s$

if

for some $i\in N$ ,$\pi(i,\overline{m})=0$

otherwise.

Theorem 3.3.4 For any recursive function , there is a recursive minimization w.r.t : The followin equation gives it.
$\pi$

$\pi$

$g$

$m(x_{1}, \ldots, x_{k})=b(\inf, x_{1}, \ldots, x_{k})$

where

$b$

,

is defined as in Lemma 3.2.8

We note that, to show the theorem above, bounded minimization definedby a QPRD is used. As we discuss in Section 5, the closure property will not
be held if bounded minimization is defined by a PRD.

233

4Computability of Recursive Functions
In this section we discuss how our recursive functions are computed. The
model of computation we use is term rewriting systems, which generalizes
string rewriting systems and then, Turing machines.

Term Rewriting Systems

4.1

We briefly introduce some definitions and notations on term rewriting systems. See e.g. [4] for more details.
of terms in $T(F\cup B_{inf}, X)$ such that
A rewrite rule is a pair
. A term. We write $tarrow u$ for a rewrite ruleandrewriting system $(TRS)R$ is a set of rewrite rules. A term is called a redexof if for some $tarrow u$ in $R,$ matches . We denote the reduction relation, and the reflexive-transitive closure(on $T(F\cup B_{inf},$ $X)$ )in.
in , no variable symbol
is said left-linear if for
A TRS
occurs in twice or more. is non-overlapping (non-ambiguous) if for every$tarrow u$ and $t’arrow u’$ in $R,$
does not unify with any non-variable subterm ofand $t’=s$ .
except the trivial case where$t\not\in X$$\langle t, u\rangle$$\langle t, u\rangle$$\mathrm{v}_{\mathrm{a}\mathrm{r}}(t)\supseteq \mathrm{v}_{\mathrm{a}\mathrm{r}}(u)$

$s$

$R$

$t$

$R$

$\mathrm{b}\mathrm{y}arrow R$$s$$\mathrm{o}\mathrm{f}arrow R$$\mathrm{b}\mathrm{y}arrow^{*}R$$R$$\mathrm{e}\mathrm{a}c\mathrm{h}tarrow u$

$R$

$R$

$t$

$s$

$t$

$t’$

$\langle tarrow u\rangle=\langle t’arrow u’\rangle$

4.2

Algebraic Semantics of TRSs

To see that recursive functions are computable, we first introduce the algebraic semantics of left-linear and non-overlapping TRSs [6-8], which generalizes that of recursive program schemes originated by Nivat [10]. It willappear in a simpler form than the literature [6-8] since RDs have a quite
restricted form as a TRS.
is called a constructor system on
be a subset of $F$ . A TRSLet$R,$$tarrowu$$t=f(t_{1}.’\ldots,t_{k})$
holds for some $f\in F-C$ andin
if for all$.7’ t_{k}\in T(C, X)$ . A constructor system
is perfect if for every in$f(t_{1},..-, t_{k})$ isredex of .
inand every
F.unIn$(R)-c$$E$ as a TRS and let $E_{inf}=E\cup\{\dot{i}nfarrow$
what follows, we regard an RD$suCc( \inf)\}$ .
$R$

$C$

$C$

$R$

$t_{1},$$f$$,$$t_{1},$$T(C, \emptyset),$$t_{k}$$\ldots,$

$R$

$a$

is a left-linear and non-overlappin$gTRS$ .
Lemma 4.2.1 For any $RDE,$
Moreover, it is a perfect constructor system on $B$ .
$E_{\inf}$, we
To formalize the computational semantics of $E$ using a TRS
be a new constantagain extend the set of base function symbols. Letsymbol, $B_{\Omega}=B\cup\{\Omega\}$ and $B_{\Omega,\inf}=B\cup$ { , inf}. Let us define an$T=U[parrow\Omega|$
by: $T\preceq U$ iff for someon
$p \in\min(P)]$ . This ordering is due to [10].
$E_{\inf}$$\Omega$$\Omega$$T^{\infty}(F\cup B_{\Omega,inf})$$P\subseteq \mathrm{N}\mathrm{o}\mathrm{d}\mathrm{e}(U),$Proposition 4.2.2
CPOs with bases
the le as element is a term$\langle T^{\infty}(F\cup B_{\Omega,\inf}), \preceq\rangle$$T(F\cup B_{\Omega,\inf})$$t$$\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\preceq$$\Omega$

.

and

and

$T(B_{\Omega})$

are algebraic
In both as $es$ ,$\langle T^{\infty}(B_{\Omega}), \preceq\rangle$, respectively.

$c$

234

Define a function$t \in T(F\cup B\Omega,\inf)$from $T(F\cup B_{\Omega,\inf})$ to$\omega_{E_{:}nf}$$T(B_{\Omega})$$\omega_{E_{nf}}.\cdot(t)=t[parrow\Omega|p\in\min(P)]$

where

.

$P= \{p\in \mathrm{N}\mathrm{o}\mathrm{d}\mathrm{e}(t)|t(p)\in F\cup\{\inf\}\}^{2}$

an approximate normal form of .
Next, we define the symbolic value of inIf,$tarrow^{*}E_{*nf}.u$, then, we call$t$$\omega_{E_{n}}(:Ju)$

$t$

by:

as below: For each,$E_{\inf}$, denoted by$\mathrm{V}\mathrm{a}1_{EtnJ}(t)$,.

$\mathrm{V}\mathrm{a}1_{E_{\inf}}(t)=\mathrm{u}\{\omega_{E_{\inf}}(u)|tarrow^{*}E_{\inf}u\}$

We can show thatis total monotone function from $T(F\cup B_{\inf,\Omega})$. This function defines the evaluator for a program, i.e., a termto$T(F\cup
B_{\inf,\Omega})$in. Approximate normal forms are “partial” outputs from theevaluator running and their l.u.b. is the “eventual” output as the limit.
$a$$\mathrm{V}\mathrm{a}1_{E_{nf}}.\cdot$$T^{\infty}(B_{\Omega})$

4.3

Computational Interpretation of RDs

Using the function$\mathrm{R}\mathrm{D}s$$\mathrm{V}\mathrm{a}1_{E_{\inf}}$, we formulate the functions on$N_{\infty}$

computed by.

The CPOis considered as the output domain of our evaluator. It is easy to see that the CPO is isomorphic to; We letbethe unique continuous bijection fromto.
Next, we shall construct the input domain. Remark that$\langle T_{\infty}(B_{\Omega}), \preceq\rangle$$\langle N_{\infty}, \subseteq\rangle$$\gamma_{\mathit{0}}$$\langle N_{\infty}, \subseteq\rangle$$\langle T_{\infty}(B_{\Omega}), \preceq\rangle$$\mathrm{V}\mathrm{a}1_{E}(\inf T(B_{\Omega})\cup\{\inf\})=T_{\infty}(B_{\Omega})$holds for every RD $E$ . Let us define a preorder
on $T(B_{\Omega}) \cup\{\inf\}$
by:iff. Then, it an easily be shown thatis a CPO isomorphic to; We denote, by ,the unique continuous bijection fromto.
$\subset$$\sim E_{\inf}$$\mathrm{V}\mathrm{a}1_{E_{\inf}}(t)\preceq \mathrm{V}\mathrm{a}1_{E_{\inf}}(u)$$t\sim_{E_{\inf}}\subset u$$c$$\langle N_{\infty}, \subseteq\rangle$$\langle T(B_{\Omega})\cup\{\dot{i}nf\}, \sim\subset_{E_{\inf}}\rangle$$\gamma_{i}$$\langle N_{\infty}, \subseteq\rangle$$\langle T(B_{\Omega})\cup\{\inf\}, \sim\subset_{E_{\inf}}\rangle$

Definition 4.3.1 For an RD , the computational interpretation
an interpretation of Fun $(E)\cup B_{\inf}$ defined as follows: Forwith arity ,$E$$\Gamma_{E}$

of

$E$

is

$f\in \mathrm{F}u\mathrm{n}(E)\cup B_{\inf}$$n$$f_{\mathrm{r}}E(d_{1}, \ldots, d_{n})=\gamma o(\mathrm{v}_{\mathrm{a}1}E_{\inf}(f(\gamma_{i}(d_{1}), \ldots, \gamma_{i}(d_{n})))$

for$d_{1},$$d_{n}$$\ldots,$in$N_{\infty}$,.

Theorem 4.3.2 For any $RDE,$$\Gamma_{E}=\triangle_{E}$.

2It can be shown thatis exactly one appeared in [6,7,8] using the fact thatis a perfect constructor system and is in $T(F\cup B_{\Omega,inf})$ .
$\omega_{E_{inj}}$$t$$E_{inf}$235

Quasi-Primitive Recursion
Recursion

5$\mathrm{v}\mathrm{s}$. Primitive

asiIn the earlier sections, we have introduced and mainly dealt withprimitive recursion, a generalized version of primitive recursion. We shall
now investigate the relationship between these two schemes of recursion.
$\mathrm{q}u$Conventional Viewpoint

5.1

We can show that:
Theorem 5.1.1 For any n-ary quasi-primitive recursive function , there isan n-ary primitive cursive function such th at $\sigma\cap(N^{n}\cross N)=\pi\cap(N^{n}\cross N)$ .
$\sigma$$\pi$$r\mathrm{e}$That is, they have the same descriptive power from the conventional pointof view,

Detecting Bottom

5.2

Now, we shall see that quasi-primitive an primitive recursion are different.
with each other as schemes to describe functions on
We have defined recursive functions using QPRDs with . On the other.
hand, we can consider the class of functions described by PRDs with-functions (Under this convention, we should all
We all the latter as-functions). We shall show that the clas ofrecursive functions as-functions. For therecursive functions is strictly larger than that of
purpose, we introduce a property that-functions satisfy but recursivefunctions do generally not.
an order over the set of -tuples of elements
We extend the
in
: For
an
iff
for all .
$\{1,\cdots,n\}$. We also define a strict
Let be a subset of
over
if
and
as follows:$\mathrm{d}$$N_{\infty}$$\infty$$\infty$$c$$c$$\mathrm{P}\mathrm{R}_{\infty}$$s$$\mathrm{Q}\mathrm{P}\mathrm{R}_{\infty}$$\mathrm{P}\mathrm{R}_{\infty}$$\mathrm{P}\mathrm{R}_{\infty}$$n$$\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\subseteq \mathrm{i}\mathrm{n}\mathrm{t}\mathrm{o}$$\overline{d}=\langle d_{1}, \ldots, d_{n}\rangle$$N_{\infty}$$\mathrm{d}d^{\overline{\prime}}=\langle d_{1}’, \ldots, d_{n}’\rangle,\overline{d}\subseteq d^{\overline{\prime}}$$I$$d_{i}\subseteq d_{i}’$$\mathrm{o}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{r}\subset_{I}$$\overline{d}\subset_{I}d^{\overline{\prime}}$$(N_{\infty})^{n}$$\overline{d}\subseteq d^{\overline{\prime}}$

1. for all $i\in I,$$d_{i}\subset d_{i}’$2. for all$d_{i}=d_{i}’$$i\not\in I,$$\dot{i}$or$d_{i}$

is maximal, and.

Clearly, for any -ary monotone function
implies.
For a monotone function , we say is -saturated at if for all suchthat
we have. A monotone function
is said simply
monotone if, for arbitrary
andand
implies thatis -saturated at .
$\varphi,\overline{d}\subset Id^{\overline{\prime}}$$n$$\varphi$$\overline{d}\subset_{I}\overline{e}$$\varphi$$I$$\varphi(\overline{d})\subseteq\varphi(d^{\overline{\prime}})$$\overline{d}$$\overline{e}$$\varphi(\overline{d})=\varphi(\overline{e})$$\varphi$$d^{\overline{\prime}}$$\overline{d},$$\varphi$$I$$I,\overline{d}\subset_{I}d^{\overline{\prime}}$$\varphi(\overline{d})=\varphi(d^{\overline{\prime}})$$d^{\overline{\prime}}$

Theorem 5.2.1 Any$PR_{\infty}- f\mathrm{u}$nction is simply mon otone.

It can easily be shown that recursive functions are generally not simply
monotone. Thus, we have:236

Corollary 5.2.2 The class of recursive functions is strictly larger th anction .
$ofPR_{\infty}- f\mathrm{u}n$$tl_{l}\mathrm{a}t$$s$

From the theorem above, we also obtain another interesting result. First
holds for aremark that, in general, we can not decide whether, since this decision
given recursive function and arguments.
problem can be regarded as the halting problem from the following“
formulation
theconventionalinisundefined”
Although the statement”
here, the latter is equivalent tois parallel to the statement “”
where degen is the degeneration operator. Since our class“degenof recursive functions has been shown to include the class of partial recursivefunctions in the conventional framework, the decision of degenmust be unsolvable.
-functions. As we
Nevertheless, the unsolvability is not the case forshall see below, these functions enjoy a sufficient condition which ensuresthat the halting problem is solvable.
$\varphi(\overline{d})=\perp$$\overline{d}=\langle d_{1}, \ldots, d_{n}\rangle$$\varphi$$\arg_{\mathrm{U}\mathrm{n}\mathrm{u}\mathrm{e}\mathrm{n}}\mathrm{t}$$\varphi(\overline{d})$$\varphi(\overline{d})\not\in N$$(\varphi(\overline{d}))=\perp$$(\varphi(\overline{d}))=\perp$$\mathrm{P}\mathrm{R}_{\infty}$-ary function
is $lower-bound- ver\dot{i}fiable$ if for any$c\in N\cup N\uparrow$ , it is decidable whether
コ-c or not.

Definition 5.2.3 An
and any$\overline{d}\in(N_{\infty})^{n}$$n$$\varphi$$\varphi(\overline{d})$.
Note that if $c\in N$ , then, the above test is just the test offunctionsdecidable for
The condition.
andsince this condition is true iff
view,simplymonotonefunctions enjoy
pointofFrom the computationala useful property.
$\varphi(\overline{d})=c$$1\mathrm{o}\mathrm{w}\mathrm{e}\mathrm{r}-\mathrm{b}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{d}_{-}\mathrm{V}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}$$\varphi(\overline{d})=\perp \mathrm{i}\mathrm{s}$$\varphi(\overline{d})\sum s(\perp)$$\varphi(\overline{d})\sum 0$

Lemma 5.2.4 Let be a simply monotone function and suppose that the
an $dc\in$
コ-c is ecida $ble$ for “finite”
lower-bound tes. Then, is lower-bound verifia .
$\varphi$$d$$t\varphi(\overline{d})$$N\cup N\uparrow$$\overline{d}\in(N\cup N\uparrow)^{n}$$\mathrm{b}l\mathrm{e}$$\varphi$

Using Theorem 5.2.1 and the above lemma, we get:
Theorem 5.2.5 Any$PR_{\infty}$-function is

The result suggests that the device
to describe all computable functions.

6$l_{oWer}- bound-_{\mathrm{V}}e\mathrm{r}i\mathrm{f}\mathrm{i}\mathrm{a}ble$$\mathrm{P}\mathrm{R}\mathrm{D}\mathrm{s}+\infty$.

has not sufficient power

Future WorkIn our framework, the class of recursive function is proved to be closed underminimization, and clearly it includes all quasi-primitive recursive functions.
However, it has not been shown that this class is the least one among suchclasses. We conjecture the positive answer to the question becau se recursive functions are “computable” in the sense of algebraic semantics of term
and theis “recursive”
rewriting systems (the function:in the conventional sen se).
$\omega_{E_{:}nf}$$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}arrow E_{nf}$237

Acknowledgement
The author wishes to thank Prof. Muneo GOTO and Prof. Yasuyoshi INAGAKI for their encouragement, and Dr. Mizuhito OGAWA and Dr. Ken
MANO for their helpful discussions.
References[1] H.P. Barendregt, “The lambda Calculus-Its Syntax an d Semantics,”
2nd ed., North-Holland (1984).

[2] B. Courcelle, “Fundamental Properties of Infinite Trees,” TheoreticalComputer Science 25, pp. 95-169 (1983).

[3] A. Church, “The Calculi of Lambda Conversion,” Annals of Math. 6,
Princeton University Press (1941).
[4] G. Huet, “Confluent Reductions: Abstract Properties and Applications
to Term Rewriting Systems,” J. ACM 27, pp. 797-821 (1980).

Recursive Functions of Natural Numbers,” Math[5] S. Kleene,112,
pp. 727-742 (1936)
ematische Annalen$‘(\mathrm{G}\mathrm{e}\mathrm{n}\mathrm{e}\mathrm{r}a1$[6] T. Naoi and Y. Inagaki, “The Conservative Extension and Behavioral Semantics of Term Rewriting Systems,” Technical Research Report No.8604, Department of Information Science, Nagoya University(1986).
[7] T. Naoi and Y. Inagaki, “The Relation between Algebraic and Fixedpoint Semantics of Term Rewriting Systems,” Technical Report COMP8637, IEICE (1986).

[8] T. Naoi and Y. Inagaki, “Algebraic Semantics and Complexity of Term
Rewriting Systems,” Proc. of 3rd RTA89, Lecture Notes in Computer
Science 355, Springer, pp. 312-325 (1989).
[9] T. Naoi and Y. Inagaki, “Recursive Functions on a Completed Set of
Natural Numbers,” Technical Report COMP90-1, IEICE (1990).

[10] M. Nivat, “On the Interpretation of Recursive Polyadic Program Schemes,”
Symposia Mathematica 15, Rome, pp. 255-281(1975).
[11] D. Scott, “Continuous Lattices,” in: F. Lawvere, ed., “Toposes, Algebraic Geometry and Logic,” Lecture Notes in Mathematics 274, Springer,
pp. 97-136(1972).