Révision 216 CSL17/completeness.tex

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