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, if we generalize operations (especially composition) to deal with zero-arity cases in an approprate way? E.g., ${\underline {\mathbf {\dot {K}} }}_{1}^{0}\mathbf {0} \left\langle \right\rangle =n$ and ${\underline {\mathbf {K} }}_{1}^{0}\mathbf {0} =n$, too? Does it take a generalization to allow, or can it be inferred?

Succesor 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 tuple, and use a style more 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.

Operations

Minimalization

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

${\underline {\mu }}^{m}f=\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].

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.