Révision 236

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


  		












  

    
      CSL17/arithmetic.tex	(revision 236)
    
  






  1
  1
  
    
\section{An arithmetic for the polynomial hierarchy}\label{sect:arithmetic}


  		





  2
  2
  
    
%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$. 


  		





  3
  3
  
    
Our base language consists of constant and function symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and predicate symbols 


  		





  4
  
  
    
 $\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $\smash(x,y)$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.


  		





  
  4
  
    
 $\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $x\smsh y$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.


  		





  5
  5
  
    
 We may write $\succ{0}(x)$ for $2\cdot x$, $\succ{1}(x)$ for $\succ{}(2\cdot x)$, and $\pred (x)$ for $\hlf{x}$, to better relate to the $\bc$ setting.


  		





  6
  6
  
    
 


  		





  7
  7
  
    
We consider formulas of classical first-order logic, over $\neg$, $\cand$, $\cor$, $\forall$, $\exists$, along with usual shorthands and abbreviations. 


  		












Formats disponibles :
  Unified diff