Révision 236 CSL17/soundness.tex

soundness.tex (revision 236)
1 1 
\section{Soundness}
2 2 
\label{sect:soundness}
3 
In this section we show that the representable functions of our theories $\arith^i$ are in $\fphi i$ (`soundness').
4 
The main result is the following:
3 5 

  		





  4
  
  
    
The main result of this section is the following:


  		





  5
  
  
    

  		





  6
  6
  
    
\begin{theorem}


  		





  7
  7
  
    
	\label{thm:soundness}


  		





  8
  8
  
    
	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.


  		





  ......




  10
  10
  
    

  		





  11
  11
  
    

  		





  12
  12
  
    

  		





  13
  
  
    
The main problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions. 


  		





  14
  
  
    
For this we will use length-bounded witnessing, borrowing a similar idea from Bellantoni's previous work \cite{Bellantoni95}.


  		





  
  13
  
    
The problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions, Lemma~\ref{lem:polychecking}. 


  		





  
  14
  
    
For this we will use \emph{length-bounded} witnessing argument, borrowing a similar idea from Bellantoni's work \cite{Bellantoni95}.


  		





  15
  15
  
    

  		





  16
  16
  
    

  		





  17
  17
  
    
\begin{definition}


  		












Formats disponibles :
  Unified diff