Révision 247 CSL17/soundness.tex

soundness.tex (revision 247)
48 48 

  		





  49
  49
  
    

  		





  50
  50
  
    
\begin{proposition}


  		





  51
  
  
    
Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i-1}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.


  		





  
  51
  
    
Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.


  		





  52
  52
  
    
\end{proposition}


  		





  53
  53
  
    

  		





  54
  54
  
    

  		





  55
  55
  
    
We will use the programs $\charfn{}{}$ in the witness functions we define below.


  		





  56
  
  
    
Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Pi^\safe_{i-1}$.


  		





  
  56
  
    
Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Sigma^\safe_{i}$.


  		





  57
  57
  
    
For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'.


  		





  58
  58
  
    
Notice that, while we refer to $b_A(l), p(l)$ etc.\ below as a `polynomial', we really mean a \emph{quasipolynomial} (which may also contain $\smsh$), i.e.\ a polynomial in the \emph{length} of $l$, as a slight abuse of notation.


  		





  59
  59
  
    

  		





  60
  60
  
    

  		





  61
  61
  
    
\begin{definition}


  		





  62
  62
  
    
	[Length bounded witness function]


  		





  63
  
  
    
	For a $\Sigma^\safe_{i}$ formula $A$ with a compatible sorting $(\vec u ; \vec x)$, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ in $\bc (\charfn{}{i})$ and its \emph{bounding polynomial} $b_A (l)$ as follows:


  		





  
  63
  
    
	For a $\Sigma^\safe_{i}$ formula $A$ with a compatible sorting $(\vec u ; \vec x)$, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ in $\bc (\charfn{}{i-1})$ and its \emph{bounding polynomial} $b_A (l)$ as follows:


  		





  64
  64
  
    
	\begin{itemize}


  		





  65
  65
  
    
		\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$ and we set $b_A (l) = 1$.


  		





  66
  66
  
    
		\item If $A$ is $B \cor C$ then we may set $b_A = O(b_B + b_C)$ and define $		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) \dfn		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )$.


  		












Formats disponibles :
  Unified diff