Révision 213 CSL17/preliminaries.tex

preliminaries.tex (revision 213)
142 142 
\begin{example}
143 143 
	[Some simple functions]
144 144 
	\label{ex:simple-bc-fns}
145 
	\todo{Boolean predicates $\notfn, \andfn, \orfn, \equivfn$ .}
146 
	\todo{$\bit$}
145 
%	\todo{Boolean predicates $\notfn, \andfn, \orfn, \equivfn$ .}
146 
%	\todo{$\bit$}
147 
Observe that:
148 
	\begin{itemize}
149 
	\item The boolean predicates $\notfn (;x)$,  $\andfn(;x,y)$, $\orfn(;x,y)$, $\equivfn(;x,y)$ can all be defined on safe arguments, simply by computing by case distinction using the conditional $C(;x,y_{\epsilon}, y_0,y_1)$ function.
150 
	%\item $\bit(l;x)$ returns the $\mode l$th bit of $x$.
151 
	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1010)=0$.
147 152
148 
	$\bit(l;x)$ returns the $\mode l$th bit of $x$.
153 
	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:
154 
	\begin{eqnarray*}
155 
	\shorten(\epsilon;x) &=&x\\
156 
	\shorten(li;x) &=&p(;\shorten(l;x))
157 
	\end{eqnarray*}
158 
	Then we define $\bit(l;x)$  as follows:
159 
	$$\bit(l;x)=C(;\shorten(pl;x),\epsilon,0,1).$$
160 
	\end{itemize}
149 161 
	\end{example}
150 162 

  		





  151
  163
  
    

  		





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


  		





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


  		





  153
  165
  
    

  		





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


  		





  155
  167
  
    
\begin{definition}[$\mubc$ and $\mubc^i$ programs]


  		












Formats disponibles :
  Unified diff