Personal tools

Recursive function theory

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (Typographic corrections and clearer choice of words)
(Adding link to Dr Matt Fairtlough's lecture notes, as they contain theoretical texts, implementations written in Haskell, and further useful links. Using also his term ,,initial functions'')

Revision as of 13:20, 30 April 2006


1 Introduction

2 Designed languages

  • Dr Matt Fairtlough's Minimal Programming Language (MIN) is not exactly a recursive function theory language, but it is based on natural numbers, too and its equivalent power with partal recursive functions is shown in its description.

3 Implementations

In Haskell, among other implementations (e.g. written in Java) in Dr Matt Fairtlough's lecture notes (see the bottom of the page).

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

5 Primitive recursive functions

5.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}

5.2 Initial functions

5.2.1 Constant

\mathbf 0 : \left\lfloor0\right\rfloor
\mathbf 0 = 0

This allows us to deal with a concept of zero in recursive function theory. In the literature (in [Mon:MathLog], too) this aim is achieved in another way: a

\mathbf{zero} : \left\lfloor1\right\rfloor
\mathbf{zero}\;x = 0

is defined instead. Is this approach superfluously overcomplicated? Can we avoid it and use the more simple and indirect looking

\mathbf 0 : \left\lfloor0\right\rfloor
\mathbf 0 = 0


Are these approaches equivalent? Is the latter (more simple looking) one as powerful as the former one? Could we define a \mathbf{zero} using the

\mathbf 0 : \left\lfloor0\right\rfloor
\mathbf 0 = 0

approach? Let us try:

\mathbf{zero} = \underline\mathbf K^0_1 \mathbf0

(see the definition of \underline\mathbf K^m_n somewhat below). 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.

\underline\mathbf\dot K^0_n c\left\langle\right\rangle
\underline\mathbf K^0_n c

where c : \left\lfloor0\right\rfloor, n \in \mathbb N 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 they be inferred? A practical approach to solve such questions: let us write a Haskell program which implements (at least partially) recursive function theory. Then we can see clearly which things have to be defined and things which are consequences. I think the \underline\mathbf K^0_n c construct is a rather straighforward thing.

Why all this can be important: it may be exactly \underline\mathbf K^0_n c that saves us from defining the concept of zero in recursive function theory as

\mathbf{zero} : \left\lfloor1\right\rfloor
\mathbf{zero}\;x = 0

-- it may be superfluous: if we need functions that throw away (some or all) of their arguments and return a constant, then we can combine them from \underline\mathbf K^m_n, \mathbf s and \mathbf 0, if we allow concepts like \underline\mathbf K^0_m.

5.2.2 Successor function

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

5.2.3 Projection functions

For all 0\leq i<m:

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

5.3 Operations

5.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}

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

6 General recursive functions

Everything seen above, and the new concepts:

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

\mathbf{special}^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

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

6.2 Operations

6.2.1 Minimalization

\underline\mu^m : \widehat m \to \left\lfloor m\right\rfloor
\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\}

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

\forall x_0, \dots, x_{m-1} \in \mathbb N\;\;\exists y \in \mathbb N\;\;f x_0 \dots x_{m-1} y = 0

7 Partial recursive functions

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

7.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 constant? Is

\left\lceil0\right\rceil = \mathbb N


\left\lceil0\right\rceil = \mathbb N\;\cup\;\left\{\bot\right\}?

7.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 extension of the corresponding total function based definitions.

Remark: these operations take partial functions as arguments, but they are total operations themselves in the sense that they always yield a result -- at worst an empty function (as an ultimate partial function).

8 Bibliography

Curry, Haskell B; Feys, Robert; Craig, William: Combinatory Logic. Volume I. North-Holland Publishing Company, Amsterdam, 1958.
Monk, J. Donald: Mathematical Logic. Springer-Verlag, New York * Heidelberg * Berlin, 1976.