Recursive function theory
From HaskellWiki
EndreyMark (Talk  contribs) m (typographic correction) 
EndreyMark (Talk  contribs) (→Constant: : Arguing for another choice of base functions) 

Line 21:  Line 21:  
:<math>\mathbf 0 = 0</math> 
:<math>\mathbf 0 = 0</math> 

−  Question: is the wellknown <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? 
+  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 

+  :<math>\mathbf{zero} : \left\lfloor1\right\rfloor</math> 

+  :<math>\mathbf{zero}\;x = 0</math> 

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

+  :<math>\mathbf 0 : \left\lfloor0\right\rfloor</math> 

+  :<math>\mathbf 0 = 0</math> 

+  approach? 

−  Are these approaches equivalent? Is the latter (more simple) one as powerful as the former one? Could we define a <math>\mathbf{zero}\;x = 0</math> using the <math>\mathbf{0} = 0</math> approach? 
+  Are these approaches equivalent? Is the latter (more simple looking) one as powerful as the former one? Could we define a <math>\mathbf{zero}</math> using the 
+  :<math>\mathbf 0 : \left\lfloor0\right\rfloor</math> 

+  :<math>\mathbf 0 = 0</math> 

+  approach? 

Let us try: 
Let us try: 

:<math>\mathbf{zero} = \underline\mathbf K^0_1 \mathbf0</math> 
:<math>\mathbf{zero} = \underline\mathbf K^0_1 \mathbf0</math> 

−  +  (see the definition of <math>\underline\mathbf K^m_n</math> somewhat below). 

−  This looks like working, but raises new questions: what about generalizing operations (here composition) to deal with zeroarity cases in an appropriate way? 
+  This looks like working, but raises new questions: what about generalizing operations (here: composition) to deal with zeroarity cases in an appropriate way? 
E.g. 
E.g. 

:<math>\underline\mathbf\dot K^0_n c\left\langle\right\rangle</math> 
:<math>\underline\mathbf\dot K^0_n c\left\langle\right\rangle</math> 

Line 35:  Line 35:  
Does it take a generalization to allow such cases, or can it be inferred? 
Does it take a generalization to allow such cases, or can it be inferred? 

+  A practical approach to slve 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 <math>\underline\mathbf K^0_n c</math> construct is a rather straighforward thing. 

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

+  :<math>\mathbf{zero} : \left\lfloor1\right\rfloor</math> 

+  :<math>\mathbf{zero}\;x = 0</math> 

+   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 <math>\underline\mathbf K^m_n</math>, <math>\mathbf s</math> and <math>\mathbf 0</math>, if we allow concepts like <math>\underline\mathbf K^0_m</math>. 

==== Successor function ==== 
==== Successor function ==== 
Revision as of 09:30, 30 April 2006
Contents 
1 Introduction
2 Plans towards a programming language
Wellknown 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 zeroarity 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
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
is defined instead. Is this approach superfluous? Can we avoid it and use the more simple and indirect looking
approach?
Are these approaches equivalent? Is the latter (more simple looking) one as powerful as the former one? Could we define a using the
approach? Let us try:
(see the definition of somewhat below). This looks like working, but raises new questions: what about generalizing operations (here: composition) to deal with zeroarity cases in an appropriate way? E.g.
where can be regarded as nary functions throwing all their n arguments away and returning c.
Does it take a generalization to allow such cases, or can it be inferred? A practical approach to slve 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 construct is a rather straighforward thing.
Why all this can be important: it may be exactly that saves us from defining the concept of zero in recursive function theory as
 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 , and , if we allow concepts like .
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 constant? Is
or
 ?
5.2 Operations
Their definitions are straightforward extension of the corresponding total function based definitions.
Remark: these operations take partial functions as arguments, but they are total operation themselves in the sense that they always yield a result  at worst an empty function.
6 Bibliography
 [HasFeyCr:CombLog1]
 Curry, Haskell B; Feys, Robert; Craig, William: Combinatory Logic. Volume I. NorthHolland Publishing Company, Amsterdam, 1958.
 [Mon:MathLog]
 Monk, J. Donald: Mathematical Logic. SpringerVerlag, New York * Heidelberg * Berlin, 1976.