Révision 201 CSL17/preliminaries.tex

preliminaries.tex (revision 201)
137 137 

  		





  138
  138
  
    
%\nb{TODO: extend with $\mu$s.}


  		





  139
  139
  
    

  		





  
  140
  
    
\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }


  		





  140
  141
  
    

  		





  
  142
  
    
\begin{example}


  		





  
  143
  
    
	[Some simple functions]


  		





  
  144
  
    
	\label{ex:simple-bc-fns}


  		





  
  145
  
    
	\todo{Boolean predicates $\notfn, \andfn, \orfn, \equivfn$ .}


  		





  
  146
  
    
	\todo{$\bit$}


  		





  
  147
  
    
	


  		





  
  148
  
    
	$\bit(l;x)$ returns the $\mode l$th bit of $x$.


  		





  
  149
  
    
	\end{example}


  		





  
  150
  
    

  		





  
  151
  
    

  		





  141
  152
  
    
\nb{Remember polymax bounded checking lemma! Quite important. Also need to bear this in mind when adding functions.}


  		





  142
  153
  
    

  		





  143
  154
  
    
Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, defined by using predicative minimization: 


  		












Formats disponibles :
  Unified diff