Personal tools

Recursive function theory

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(Categorizing under Category:Theoretical foundations. And some minor rephrasings.)
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 ===
+
== Primitive recursive functions ==
-
==== Type system ====
+
=== 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 ====
+
=== Base functions ===
-
===== Constant =====
+
==== 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 =====
+
==== 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 =====
+
==== 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 ====
+
=== Operations ===
-
===== Composition =====
+
==== 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 =====
+
==== 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 ===
+
== General recursive functions ==
Everything seen above, and the new concepts:
Everything seen above, and the new concepts:
-
==== Type system ====
+
=== 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 ====
+
=== Operations ===
-
===== Minimalization =====
+
==== 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 ===
+
 
 +
== Partial recursive functions ==
Everything seen above, but new constructs are provided, too.
Everything seen above, but new constructs are provided, too.
-
==== Type system ====
+
=== 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 ====
+
=== 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

PlanetMath article

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 approprate 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, or can it be inferred?

3.2.2 Succesor function

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

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

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.
Retrieved from "http://www.haskell.org/haskellwiki/Recursive_function_theory"

Category: Theoretical foundations