Difference between revisions of "Recursive function theory"
EndreyMark (talk | contribs) m (Headline hierarchy is simpified -- a ,,singleton'' level eliminated) |
EndreyMark (talk | contribs) m (Typos and typesettings (italics)) |
||
Line 21: | Line 21: | ||
:<math>\mathbf 0 = 0</math> |
:<math>\mathbf 0 = 0</math> |
||
− | Question: is the well-known <math>\mathbf{zero}(x)=0</math> approach superfluous? Can we avoid it and use the more simple and indirect <math>\mathbf{0} = 0</math> approach, if we generalize operations (especially composition) to deal with zero-arity cases in an |
+ | Question: is the well-known <math>\mathbf{zero}(x)=0</math> approach superfluous? Can we avoid it and use the more simple and indirect <math>\mathbf{0} = 0</math> approach, if we generalize operations (especially composition) to deal with zero-arity cases in an appropriate way? |
E.g., <math>\underline\mathbf\dot K^0_1\mathbf0\left\langle\right\rangle = n</math> and <math>\underline\mathbf K^0_1\mathbf0 = n</math>, too? |
E.g., <math>\underline\mathbf\dot K^0_1\mathbf0\left\langle\right\rangle = n</math> and <math>\underline\mathbf K^0_1\mathbf0 = n</math>, too? |
||
− | Does it take a generalization to allow, or can it be inferred? |
+ | Does it take a generalization to allow such cases, or can it be inferred? |
− | ==== |
+ | ==== Successor function ==== |
:<math>\mathbf s : \left\lfloor1\right\rfloor</math> |
:<math>\mathbf s : \left\lfloor1\right\rfloor</math> |
||
Line 67: | Line 67: | ||
:<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> |
||
− | 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. |
Line 76: | Line 76: | ||
:<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 == |
Revision as of 17:40, 23 April 2006
Introduction
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.
Primitive recursive functions
Type system
Base functions
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 appropriate way? E.g., and , too? Does it take a generalization to allow such cases, or can it be inferred?
Successor function
Projection functions
For all :
Operations
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
Primitive recursion
The last equation resembles to the combinator of Combinatory logic (as described in [HasFeyCr:CombLog1, 169]):
General recursive functions
Everything seen above, and the new concepts:
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.
Operations
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].
Partial recursive functions
Everything seen above, but new constructs are provided, too.
Type system
Question: is there any sense to define in another way than simply ? Partial constants?
Operations
Their definitions are straightforward.
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.