Révision 252 CSL17/preliminaries.tex

preliminaries.tex (revision 252)
142 142 

  		





  143
  143
  
    
%\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)$. }


  		





  144
  144
  
    

  		





  
  145
  
    
We denote $|x|=\ulcorner \log(x+1) \urcorner.$


  		





  145
  146
  
    
\begin{example}


  		





  146
  147
  
    
	[Some simple functions]


  		





  147
  148
  
    
	\label{ex:simple-bc-fns}


  		





  ......




  153
  154
  
    
	%\item $\bit(l;x)$ returns the $\mode l$th bit of $x$.


  		





  154
  155
  
    
	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1101)=0$.


  		





  155
  156
  
    
	


  		





  156
  
  
    
	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|+1$ prefix of $x$, as follows:


  		





  
  157
  
    
	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:


  		





  157
  158
  
    
	\begin{eqnarray*}


  		





  158
  159
  
    
	\shorten(0;x) &=&x\\


  		





  159
  
  
    
	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x))


  		





  
  160
  
    
	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x)) \mbox{ if $l\neq 0$.}


  		





  160
  161
  
    
	\end{eqnarray*}


  		





  161
  162
  
    
	Then we define $\bit(l;x)$  as follows:


  		





  162
  163
  
    
	$$\bit(l;x)=C(;\shorten(l;x),0,1).$$ 


  		












Formats disponibles :
  Unified diff