Révision 216

CSL17/preliminaries.tex (revision 216)
199 199 
  $$ \size{f(\vec u; \vec x)} \leq q(\size{u_1} , \dots , \size{u_k}) + \max_j \size{x_j}.$$
200 200 
 \end{definition}
201 201
202 
 We define the function $\mode$ by $u\mode x:= u \mod 2^{\size{x}}$.
202 
 We define the function $\mode$ by $u\mode x:= u \mod 2^{\size{x}}$. Note that this means that as a binary string $u\mode x$ is the suffix of $u$ of length $\size{x}$.
203 203 
 \begin{definition}
204 204 
 A function $f(\vec u; \vec x)$ is a \textit{polynomial checking function} on $\vec u$ if there exists a polynomial $q$
205 205 
 such that, for any $\vec u$, $\vec x$, $y$ and $z$ such that $\size{y} \geq q(\size{\vec u})+ \size{z}$ we have:
CSL17/arithmetic.tex (revision 216)
144 144 
                                                                                                   & \cor( \exists^{\safe}z.(x=\succ{1}z) \cand (y=y_1)))\
145 145 
\end{array}
146 146 
$$
147 
\item Addition:
148 
$\forall^{\safe} x, y,  \exists^{\safe} z. z=x+y$.
147 149 
\end{itemize}
148 150 

  		





  149
  151
  
    

  		












  

    
      CSL17/completeness.tex	(revision 216)
    
  






  10
  10
  
    
The rest of this section is devoted to a proof of this theorem.


  		





  11
  11
  
    
We proceed by structural induction on a $\mubc^{i-1} $ program, dealing with each case in the proceeding paragraphs.


  		





  12
  12
  
    

  		





  13
  
  
    
 The property is easily verified for the class of initial functions of  $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional. \patrick{Maybe we can refer here to Sect. \ref{sect:graphsbasicfunctions}.} Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition. 


  		





  
  13
  
    
 The property is easily verified for the class of initial functions of  $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional, as already shown in Sect. \ref{sect:graphsbasicfunctions}. Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition. 


  		





  14
  14
  
    
\paragraph*{Predicative minimisation}


  		





  15
  15
  
    
Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$. 


  		





  16
  16
  
    
By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,


  		












Formats disponibles :
  Unified diff