# Recursive function theory

(Difference between revisions)
 Revision as of 17:17, 23 April 2006 (edit)m (Headline hierarchy is simpified -- a ,,singleton'' level eliminated)← Previous diff Revision as of 17:40, 23 April 2006 (edit) (undo)m (Typos and typesettings (italics))Next diff → Line 21: Line 21: :$\mathbf 0 = 0$ :$\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? + 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 appropriate way? E.g., $\underline\mathbf\dot K^0_1\mathbf0\left\langle\right\rangle = n$ and $\underline\mathbf K^0_1\mathbf0 = n$, too? E.g., $\underline\mathbf\dot K^0_1\mathbf0\left\langle\right\rangle = n$ and $\underline\mathbf K^0_1\mathbf0 = n$, too? - Does it take a generalization to allow, or can it be inferred? + Does it take a generalization to allow such cases, or can it be inferred? - ==== Succesor function ==== + ==== Successor function ==== :$\mathbf s : \left\lfloor1\right\rfloor$ :$\mathbf s : \left\lfloor1\right\rfloor$ Line 67: Line 67: :$\widehat{\,m\,} = \left\{ f : \left\lfloor m+1\right\rfloor\;\vert\;f \mathrm{\ is\ special}\right\}$ :$\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. + 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. Line 76: Line 76: :$\underline\mu^m : \widehat m \to \left\lfloor m\right\rfloor$ :$\underline\mu^m : \widehat m \to \left\lfloor m\right\rfloor$ :$\underline\mu^m f = \min \left\{y\in\mathbb N\;\vert\;f x_0 \dots x_{m-1} y = 0\right\}$ :$\underline\mu^m f = \min \left\{y\in\mathbb N\;\vert\;f x_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]. + 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 == == Partial recursive functions ==

## 2 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.

## 3 Primitive recursive functions

### 3.1 Type system

$\left\lfloor0\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}$

### 3.2 Base functions

#### 3.2.1 Constant

$\mathbf 0 : \left\lfloor0\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 appropriate way? E.g., $\underline\mathbf\dot K^0_1\mathbf0\left\langle\right\rangle = n$ and $\underline\mathbf K^0_1\mathbf0 = n$, too? Does it take a generalization to allow such cases, or can it be inferred?

#### 3.2.2 Successor function

$\mathbf s : \left\lfloor1\right\rfloor$
$\mathbf s = \lambda x . x + 1$

#### 3.2.3 Projection functions

For all $0\leq i:

$\mathbf U^m_i : \left\lfloor m\right\rfloor$
$\mathbf U^m_i x_0\dots x_i \dots x_{m-1} = x_i$

### 3.3 Operations

#### 3.3.1 Composition

$\underline\mathbf\dot K^m_n : \left\lfloor m\right\rfloor \times \left\lfloor n\right\rfloor^m \to \left\lfloor n\right\rfloor$
$\underline\mathbf\dot K^m_n 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^n_m$ 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^m_n : \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^m_n f g_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^m_n f g_0\dots g_{m-1} x_0 \dots x_{n-1} = \mathbf \Phi^n_m f g_0 \dots g_{m-1} x_0 \dots x_{n-1}$

#### 3.3.2 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 f h = g\;\mathrm{where}$
$g x_0 \dots x_{m-1} 0 = f x_0 \dots x_{m-1}$
$g x_0 \dots x_{m-1} \left(\mathbf s y\right) = h x_0 \dots x_{m-1} y \left(g x_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]):

$g x_0 \dots x_{m-1} \left(\mathbf s y\right) = \mathbf S_{m+1} h g x_0 \dots x_{m-1} y$

## 4 General recursive functions

Everything seen above, and the new concepts:

### 4.1 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.

### 4.2 Operations

#### 4.2.1 Minimalization

$\underline\mu^m : \widehat m \to \left\lfloor m\right\rfloor$
$\underline\mu^m f = \min \left\{y\in\mathbb N\;\vert\;f x_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].

## 5 Partial recursive functions

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

### 5.1 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\lceil0\right\rceil$ in another way than simply $\left\lceil0\right\rceil = \left\lfloor0\right\rfloor = \mathbb N$? Partial constants?

### 5.2 Operations

$\overline\mathbf\dot K^m_n : \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.

## 6 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.