# Recursive function theory

### From HaskellWiki

EndreyMark (Talk | contribs) (New notations introduced, and simplifications made (zero-arity generalizations are presupposed). Plans for incarnating recursion theory concepts as a programming laguage. Ref: Monk: Mathematical Logic) |
EndreyMark (Talk | contribs) (Categorizing under Category:Theoretical foundations. And some minor rephrasings.) |
||

Line 43: | Line 43: | ||

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

This resembles to the <math>\mathbf\Phi^n_m</math> combinator of [[Combinatory logic]] (as described in <nowiki>[HasFeyCr:CombLog1, 171]</nowiki>). | This resembles to the <math>\mathbf\Phi^n_m</math> combinator of [[Combinatory logic]] (as described in <nowiki>[HasFeyCr:CombLog1, 171]</nowiki>). | ||

− | If we prefer avoiding the notion of tuple, and use a | + | If we prefer avoiding the notion of the nested tuple, and use a more homogenous style (somewhat resembling to currying): |

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

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

Line 100: | Line 100: | ||

;<nowiki>[Mon:MathLog]</nowiki> | ;<nowiki>[Mon:MathLog]</nowiki> | ||

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

+ | |||

+ | [[Category:Theoretical foundations]] |

## Revision as of 17:11, 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.

### 2.1 Primitive recursive functions

#### 2.1.1 Type system

#### 2.1.2 Base functions

##### 2.1.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?

##### 2.1.2.2 Succesor function

##### 2.1.2.3 Projection functions

For all :

#### 2.1.3 Operations

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

##### 2.1.3.2 Primitive recursion

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

### 2.2 General recursive functions

Everything seen above, and the new concepts:

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

#### 2.2.2 Operations

##### 2.2.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].

### 2.3 Partial recursive functions

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

#### 2.3.1 Type system

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

#### 2.3.2 Operations

Their definitions are straightforward.

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