Recursive function theory

Introduction

PlanetMath article

Plans towards a programming language

Well-known concepts are taken from [Mon:MatLog], but several new notations (only notations, not concepts) are introduced to reflect all concepts described in [Mon:MatLog], and some simplification are made (by allowing zero-arity generalizations). These are plans to achive formalizations that can allow us in the future to incarnate the main concepts of recursive function theory in a programming language.

Primitive recursive functions

Type system

$\left\lfloor 0\right\rfloor =\mathbb {N}$

${\begin{matrix}\left\lfloor n+1\right\rfloor =\underbrace {\mathbb {N} \times \dots \times \mathbb {N} } \to \mathbb {N} \\\;\;\;\;\;\;\;\;n+1\end{matrix}}$

Base functions

Constant

$\mathbf {0} :\left\lfloor 0\right\rfloor$

$\mathbf {0} =0$

Question: is the well-known $\mathbf {zero} \;x=0$ approach superfluous? Can we avoid it and use the more simple and indirect $\mathbf {0} =0$ approach?

Are these approaches equivalent? Is the latter (more simple) one as powerful as the former one? Could we define a $\mathbf {zero} \;x=0$ using the $\mathbf {0} =0$ approach? Let us try:

$\mathbf {zero} ={\underline {\mathbf {K} }}_{1}^{0}\mathbf {0}$

This looks like working, but raises new questions: what about generalizing operations (here composition) to deal with zero-arity cases in an appropriate way? E.g.

${\underline {\mathbf {\dot {K}} }}_{n}^{0}c\left\langle \right\rangle$

${\underline {\mathbf {K} }}_{n}^{0}c$

where $c:\left\lfloor 0\right\rfloor ,n\in \mathbb {N}$ can be regarded as $n$-ary functions throwing all their $n$ arguments away and returning $c$.

Does it take a generalization to allow such cases, or can it be inferred?

Successor function

$\mathbf {s} :\left\lfloor 1\right\rfloor$

$\mathbf {s} =\lambda x.x+1$

Projection functions

For all $0\leq i<m$:

$\mathbf {U} _{i}^{m}:\left\lfloor m\right\rfloor$

$\mathbf {U} _{i}^{m}x_{0}\dots x_{i}\dots x_{m-1}=x_{i}$

Operations

Composition

${\underline {\mathbf {\dot {K}} }}_{n}^{m}:\left\lfloor m\right\rfloor \times \left\lfloor n\right\rfloor ^{m}\to \left\lfloor n\right\rfloor$

${\underline {\mathbf {\dot {K}} }}_{n}^{m}f\left\langle g_{0},\dots ,g_{m-1}\right\rangle x_{0}\dots x_{n-1}=f\left(g_{0}x_{0}\dots x_{n-1}\right)\dots \left(g_{m-1}x_{0}\dots x_{n-1}\right)$

This resembles to the $\mathbf {\Phi } _{m}^{n}$ combinator of Combinatory logic (as described in [HasFeyCr:CombLog1, 171]). If we prefer avoiding the notion of the nested tuple, and use a more homogenous style (somewhat resembling to currying):

${\begin{matrix}{\underline {\mathbf {K} }}_{n}^{m}:\left\lfloor m\right\rfloor \times \underbrace {\left\lfloor n\right\rfloor \times \dots \times \left\lfloor n\right\rfloor } \to \left\lfloor n\right\rfloor \\\;\;\;\;\;\;\;\;\;\;m\end{matrix}}$

Let underbrace not mislead us -- it does not mean any bracing.

${\underline {\mathbf {K} }}_{n}^{m}fg_{0}\dots g_{m-1}x_{0}\dots x_{n-1}=f\left(g_{0}x_{0}\dots x_{n-1}\right)\dots \left(g_{m-1}x_{0}\dots x_{n-1}\right)$

remembering us to

${\underline {\mathbf {K} }}_{n}^{m}fg_{0}\dots g_{m-1}x_{0}\dots x_{n-1}=\mathbf {\Phi } _{m}^{n}fg_{0}\dots g_{m-1}x_{0}\dots x_{n-1}$

Primitive recursion

${\underline {\mathbf {R} }}^{m}:\left\lfloor m\right\rfloor \times \left\lfloor m+2\right\rfloor \to \left\lfloor m+1\right\rfloor$

${\underline {\mathbf {R} }}^{m}fh=g\;\mathrm {where}$

$gx_{0}\dots x_{m-1}0=fx_{0}\dots x_{m-1}$

$gx_{0}\dots x_{m-1}\left(\mathbf {s} y\right)=hx_{0}\dots x_{m-1}y\left(gx_{0}\dots x_{m-1}y\right)$

The last equation resembles to the $\mathbf {S} _{n}$ combinator of Combinatory logic (as described in [HasFeyCr:CombLog1, 169]):

$gx_{0}\dots x_{m-1}\left(\mathbf {s} y\right)=\mathbf {S} _{m+1}hgx_{0}\dots x_{m-1}y$

General recursive functions

Everything seen above, and the new concepts:

Type system

${\widehat {\,m\,}}=\left\{f:\left\lfloor m+1\right\rfloor \;\vert \;f\mathrm {\ is\ special} \right\}$

See the definition of being special [Mon:MathLog, 45]. This property ensures, that minimalization does not lead us out of the world of total functions. Its definition is the rather straightforward formalization of this expectation.

$\mathbf {special} ^{m}f\equiv \forall x_{0},\dots ,x_{m-1}\in \mathbb {N} \;\;\exists y\in \mathbb {N} \;\;fx_{0}\dots x_{m-1}y=0$

It resembles to the concept of inverse -- more exactly, to the existence part.

Operations

Minimalization

${\underline {\mu }}^{m}:{\widehat {m}}\to \left\lfloor m\right\rfloor$

${\underline {\mu }}^{m}fx_{0}\dots x_{m-1}=\min \left\{y\in \mathbb {N} \;\vert \;fx_{0}\dots x_{m-1}y=0\right\}$

Minimalization does not lead us out of the word of total functions, if we use it only for special functions -- the property of being special is defined exactly for this purpose [Mon:MatLog, 45]. As we can see, minimalization is a concept resembling somehow to the concept of inverse.

Existence of the required minimum value of the set -- a sufficient and satisfactory condition for this is that the set is never empty. And this is equivalent to the statement

$\forall x_{0},\dots ,x_{m-1}\in \mathbb {N} \;\;\exists y\in \mathbb {N} \;\;fx_{0}\dots x_{m-1}y=0$

Partial recursive functions

Everything seen above, but new constructs are provided, too.

Type system

${\begin{matrix}\left\lceil n+1\right\rceil =\underbrace {\mathbb {N} \times \dots \times \mathbb {N} } \supset \!\to \mathbb {N} \\\;\;\;\;\;\;n+1\end{matrix}}$

Question: is there any sense to define $\left\lceil 0\right\rceil$ in another way than simply $\left\lceil 0\right\rceil =\left\lfloor 0\right\rfloor =\mathbb {N}$? Partial constants?

Operations

${\overline {\mathbf {\dot {K}} }}_{n}^{m}:\left\lceil m\right\rceil \times \left\lceil n\right\rceil ^{m}\to \left\lceil n\right\rceil$

${\overline {\mathbf {R} }}^{m}:\left\lceil m\right\rceil \times \left\lceil m+2\right\rceil \to \left\lceil m+1\right\rceil$

${\overline {\mu }}^{m}:\left\lceil m+1\right\rceil \to \left\lceil m\right\rceil$

Their definitions are straightforward.

Bibliography

[HasFeyCr:CombLog1]

Curry, Haskell B; Feys, Robert; Craig, William: Combinatory Logic. Volume I. North-Holland Publishing Company, Amsterdam, 1958.

[Mon:MathLog]

Monk, J. Donald: Mathematical Logic. Springer-Verlag, New York * Heidelberg * Berlin, 1976.