# Recursive function theory

### From HaskellWiki

EndreyMark (Talk | contribs) (Connection between two separate things: (1) defining zero(x)=0 in terms of the ,,pure'' 0 approach (2) allowing 0-arity cases in composition) |
EndreyMark (Talk | contribs) (Formulating and explaining the definition of ,,special'' property') |
||

Line 79: | Line 79: | ||

See the definition of being ''special'' <nowiki>[Mon:MathLog, 45]</nowiki>. 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'' <nowiki>[Mon:MathLog, 45]</nowiki>. 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. | ||

+ | :<math>\mathbf{speciel}^m f \equiv \forall x_0, \dots, x_{m-1} \in \mathbb N\;\;\exists y \in \mathbb N\;\;f x_0 \dots x_{m-1} y = 0</math> | ||

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

Line 86: | Line 88: | ||

:<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 x_0 \dots x_{m-1} = \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]. | ||

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

+ | :<math>\forall x_0, \dots, x_{m-1} \in \mathbb N\;\;\exists y \in \mathbb N\;\;f x_0 \dots x_{m-1} y = 0</math> | ||

== Partial recursive functions == | == Partial recursive functions == |

## Revision as of 03:06, 24 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?

Are these approaches equivalent? Is the latter (more simple) one as powerful as the former one? Could we define a using the approach? Let us try:

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.

where
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?

#### 3.2.2 Successor 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.

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

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

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