# Recursive function theory

### From HaskellWiki

EndreyMark (Talk | contribs) (Categorizing under Category:Theoretical foundations. And some minor rephrasings.) |
EndreyMark (Talk | contribs) m (Headline hierarchy is simpified -- a ,,singleton'' level eliminated) |
||

Line 7: | Line 7: | ||

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. | 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 === | |

:<math>\left\lfloor0\right\rfloor = \mathbb N</math> | :<math>\left\lfloor0\right\rfloor = \mathbb N</math> | ||

:<math>\begin{matrix}\left\lfloor n + 1\right\rfloor = \underbrace{\mathbb N\times\dots\times\mathbb N}\to\mathbb N\\\;\;\;\;\;\;\;\;n+1\end{matrix}</math> | :<math>\begin{matrix}\left\lfloor n + 1\right\rfloor = \underbrace{\mathbb N\times\dots\times\mathbb N}\to\mathbb N\\\;\;\;\;\;\;\;\;n+1\end{matrix}</math> | ||

− | + | === Base functions === | |

− | + | ==== Constant ==== | |

:<math>\mathbf 0 : \left\lfloor0\right\rfloor</math> | :<math>\mathbf 0 : \left\lfloor0\right\rfloor</math> | ||

Line 25: | Line 25: | ||

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

− | + | ==== Succesor function ==== | |

:<math>\mathbf s : \left\lfloor1\right\rfloor</math> | :<math>\mathbf s : \left\lfloor1\right\rfloor</math> | ||

:<math>\mathbf s = \lambda x . x + 1</math> | :<math>\mathbf s = \lambda x . x + 1</math> | ||

− | + | ==== Projection functions ==== | |

For all <math>0\leq i<m</math>: | For all <math>0\leq i<m</math>: | ||

Line 36: | Line 36: | ||

:<math>\mathbf U^m_i x_0\dots x_i \dots x_{m-1} = x_i</math> | :<math>\mathbf U^m_i x_0\dots x_i \dots x_{m-1} = x_i</math> | ||

− | + | === Operations === | |

− | + | ==== Composition ==== | |

:<math>\underline\mathbf\dot K^m_n : \left\lfloor m\right\rfloor \times \left\lfloor n\right\rfloor^m \to \left\lfloor n\right\rfloor</math> | :<math>\underline\mathbf\dot K^m_n : \left\lfloor m\right\rfloor \times \left\lfloor n\right\rfloor^m \to \left\lfloor n\right\rfloor</math> | ||

Line 50: | Line 50: | ||

:<math>\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}</math> | :<math>\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}</math> | ||

− | + | ==== Primitive recursion ==== | |

:<math>\underline\mathbf R^m : \left\lfloor m\right\rfloor \times \left\lfloor m+2\right\rfloor \to \left\lfloor m+1\right\rfloor</math> | :<math>\underline\mathbf R^m : \left\lfloor m\right\rfloor \times \left\lfloor m+2\right\rfloor \to \left\lfloor m+1\right\rfloor</math> | ||

Line 59: | Line 59: | ||

:<math>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</math> | :<math>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</math> | ||

− | + | == General recursive functions == | |

Everything seen above, and the new concepts: | Everything seen above, and the new concepts: | ||

− | + | === Type system === | |

:<math> \widehat{\,m\,} = \left\{ f : \left\lfloor m+1\right\rfloor\;\vert\;f \mathrm{\ is\ special}\right\}</math> | :<math> \widehat{\,m\,} = \left\{ f : \left\lfloor m+1\right\rfloor\;\vert\;f \mathrm{\ is\ special}\right\}</math> | ||

Line 70: | Line 70: | ||

− | + | === Operations === | |

− | + | ==== Minimalization ==== | |

:<math>\underline\mu^m : \widehat m \to \left\lfloor m\right\rfloor</math> | :<math>\underline\mu^m : \widehat m \to \left\lfloor m\right\rfloor</math> | ||

:<math>\underline\mu^m f = \min \left\{y\in\mathbb N\;\vert\;f x_0 \dots x_{m-1} y = 0\right\}</math> | :<math>\underline\mu^m f = \min \left\{y\in\mathbb N\;\vert\;f x_0 \dots x_{m-1} y = 0\right\}</math> | ||

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 == | ||

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

− | + | === Type system === | |

:<math>\begin{matrix}\left\lceil n + 1\right\rceil = \underbrace{\mathbb N\times\dots\times\mathbb N}\supset\!\to\mathbb N\\\;\;\;\;\;\;n+1\end{matrix}</math> | :<math>\begin{matrix}\left\lceil n + 1\right\rceil = \underbrace{\mathbb N\times\dots\times\mathbb N}\supset\!\to\mathbb N\\\;\;\;\;\;\;n+1\end{matrix}</math> | ||

Line 88: | Line 89: | ||

<math>\left\lceil0\right\rceil</math> in another way than simply <math>\left\lceil0\right\rceil = \left\lfloor0\right\rfloor = \mathbb N</math>? Partial constants? | <math>\left\lceil0\right\rceil</math> in another way than simply <math>\left\lceil0\right\rceil = \left\lfloor0\right\rfloor = \mathbb N</math>? Partial constants? | ||

− | + | === Operations === | |

+ | |||

:<math>\overline\mathbf\dot K^m_n : \left\lceil m\right\rceil \times \left\lceil n\right\rceil^m \to \left\lceil n\right\rceil</math> | :<math>\overline\mathbf\dot K^m_n : \left\lceil m\right\rceil \times \left\lceil n\right\rceil^m \to \left\lceil n\right\rceil</math> | ||

:<math>\overline\mathbf R^m : \left\lceil m\right\rceil \times \left\lceil m+2\right\rceil \to \left\lceil m+1\right\rceil</math> | :<math>\overline\mathbf R^m : \left\lceil m\right\rceil \times \left\lceil m+2\right\rceil \to \left\lceil m+1\right\rceil</math> | ||

Line 96: | Line 98: | ||

== Bibliography == | == Bibliography == | ||

+ | |||

;<nowiki>[HasFeyCr:CombLog1]</nowiki> | ;<nowiki>[HasFeyCr:CombLog1]</nowiki> | ||

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

## Revision as of 17:17, 23 April 2006

## Contents |

## 1 Introduction

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

### 3.2 Base functions

#### 3.2.1 Constant

Question: is the well-known approach superfluous? Can we avoid it and use the more simple and indirect approach, if we generalize operations (especially composition) to deal with zero-arity cases in an approprate way? E.g., and , too? Does it take a generalization to allow, or can it be inferred?

#### 3.2.2 Succesor function

#### 3.2.3 Projection functions

For all :

### 3.3 Operations

#### 3.3.1 Composition

This resembles to the 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):

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

remembering us to

#### 3.3.2 Primitive recursion

The last equation resembles to the combinator of Combinatory logic (as described in [HasFeyCr:CombLog1, 169]):

## 4 General recursive functions

Everything seen above, and the new concepts:

### 4.1 Type system

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

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

Question: is there any sense to define in another way than simply ? Partial constants?

### 5.2 Operations

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.