Révision 213

CSL17/arithmetic.tex (revision 213)
21 21 
\forall u^\normal, x^\safe . \safe(u\times x) \\
22 22 
\forall u^\normal , v^\normal . \safe (u \smsh v)\\
23 23 
\forall u^\normal \safe(u) \\
24 
\forall u^\normal \safe(\hlf{u})\\
24 
\forall u^\safe \safe(\hlf{u})\\
25 25 
\forall x^\safe \safe(|x|)
26 26 
\end{array}
27 27 
\]
28 
\patrick{did I type writly the 2 last axioms?}
28 
%\patrick{did I type writly the 2 last axioms?}
29 29 

  		





  30
  30
  
    
and the list of axioms of Appendix \ref{appendix:arithmetic}, coming from \cite{Buss86book}.


  		





  31
  31
  
    

  		












  

    
      CSL17/ph-macros.tex	(revision 213)
    
  






  48
  48
  
    
\newcommand{\orfn}{\textsc{or}}


  		





  49
  49
  
    
\newcommand{\notfn}{\textsc{not}}


  		





  50
  50
  
    
\newcommand{\equivfn}{\textsc{equiv}}


  		





  
  51
  
    
\newcommand{\shorten}{\textsc{shorten}}


  		





  51
  52
  
    

  		





  
  53
  
    

  		





  52
  54
  
    
\newcommand{\zerobit}{\textsc{0bit}}


  		





  53
  55
  
    
\newcommand{\onebit}{\textsc{1bit}}


  		





  54
  56
  
    
\newcommand{\pref}{\textsc{pref}}


  		












  

    
      CSL17/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