Révision 235

CSL17/conclusions.tex (revision 235)
1 1 
\section{Conclusions}
2 2 
\label{sect:conclusion}
3 3 

  		





  4
  
  
    
 We have presented a ramified arithmetic parameterized by the number of alternations of safe (unbounded) quantifiers allowed in induction formulae. We have proved that the system $\arith^i$ with 


  		





  5
  
  
    
$\Sigma_i^{\safe}$-induction corresponds to the $i$th level $\fphi{i}$ of the polynomial hierarchy. This result brings an implicit complexity analogue of Buss' bounded arithmetic in which $S_2^i$ captures  $\fphi{i}$, and suggests that implicit arithmetics can provide fine-grained characterizations of hierarchies of complexity classes.


  		





  
  4
  
    
 We have presented a ramified arithmetic parameterized by the number of alternations of safe (unbounded) quantifiers allowed in induction formulae. We have proved that the system $\arith^i$, with 


  		





  
  5
  
    
$\Sigma_i^{\safe}$-induction, corresponds to $\fphi{i}$. This result brings an implicit complexity analogue of Buss' bounded arithmetic in which $S_2^i$ captures  $\fphi{i}$, and suggests that implicit arithmetics can provide fine-grained characterizations of hierarchies of complexity classes.


  		





  6
  6
  
    
 


  		





  7
  7
  
    
We have used a two-level ramified logic, but we believe that this approach could be implemented with a modal logic, setting $\normal = \Box \safe$, as in \cite{BelHof:02}. The exposition would be more complicated due to the lack of a developed proof theory for first-order modal logic, but arguably more elegant.


  		





  8
  8
  
    
At the same time, we could consider \emph{second-order} theories that characterise $\fph$, analogous to the bounded arithmetic theories $V^i$ from \cite{Cook:2010:LFP:1734064}, since the treatment of sequence (de)coding might be more natural, using function symbols. However it seems that delineating the levels of $\fph$ might be more difficult in such a setting.


  		












  

    
      CSL17/completeness.tex	(revision 235)
    
  






  12
  12
  
    
 


  		





  13
  13
  
    
 For predicative recursion, the basic idea is to follow the classical simulation of primitive recursion in arithmetic, adapted to recursion on notation, by encoding the sequence of recursive calls as an integer $w$. 


  		





  14
  14
  
    
 The main technical difficulty is the representation of (de)coding functions $\beta (k, x)$ (``the $k$th element of the sequence $x$'') and $\langle x,y \rangle$ (``the pair $(x,y)$'').


  		





  15
  
  
    
 For this we represent instead the length-bounded variants of these functions given towards the end of Sect.~\ref{sect:prelims}, relying on the bounded minimisation and polychecking results, Lemmas~\ref{lem:bounded-minimisation} and \ref{lem:bounded-minimisation}, to find appropriate length bounds.


  		





  
  15
  
    
 For this we represent instead the length-bounded variants of these functions given towards the end of Sect.~\ref{sect:prelims}, relying on the bounded minimisation and polychecking results, Lemmas~\ref{lem:bounded-minimisation} and \ref{lem:polychecking}, to find appropriate length bounds.


  		





  16
  16
  
    
%  which is sorted in a suitable way so that the formula $A_f$  is in the same class $\Sigma^{\safe}_i$ as $A_g$,  $A_{h_0}$ and $A_{h_1}$.  This can be obtained by defining  the predicate $\beta (k, w, y)$ with $k$ in $\normal$ and $w$, $y$ in $\safe$.


  		





  17
  17
  
    

  		





  18
  18
  
    
 


  		





  ......




  33
  33
  
    
\end{array}


  		





  34
  34
  
    
\]


  		





  35
  35
  
    
As for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a \emph{minimisation} principle for $\Sigma^\safe_{i-1}$ formulas, allowing us to extract the \emph{least} witness of a safe existential, which we apply to $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From here we are able to readily prove the totality of $A_f(\vec u ; \vec x , z)$, notably relying crucially on classical reasoning.


  		





  36
  
  
    

  		





  37
  36
  
    
\end{proof}


  		





  38
  37
  
    

  		





  39
  38
  
    

  		












  

    
      CSL17/soundness.tex	(revision 235)
    
  






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


  		





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


  		





  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
  
  
    
Notice that, while we write $p(l)$ below, we really mean a polynomial in the \emph{length} of $l$, as a slight abuse of notation.


  		





  
  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}


  		





  ......




  138
  138
  
    
	\[


  		





  139
  139
  
    
%	\vec a^\nu = \vec u ,


  		





  140
  140
  
    
%	\vec b^\sigma = \vec u, 


  		





  141
  
  
    
	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1


  		





  142
  
  
    
	\ \implies \


  		





  143
  
  
    
	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1


  		





  
  141
  
    
%	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1


  		





  
  142
  
    
%	\ \implies \


  		





  
  143
  
    
%	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1


  		





  
  144
  
    
	\begin{array}{rl}


  		





  
  145
  
    
&	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A \mode b_A(l)) =1 \\


  		





  
  146
  
    
\noalign{\medskip}


  		





  
  147
  
    
\implies & 	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1


  		





  
  148
  
    
	\end{array}


  		





  144
  149
  
    
	\]


  		





  145
  150
  
    
	for some polynomial $p$.


  		





  146
  151
  
    
%	\anupam{Need $\vec w \mode p(l)$ for some $p$.}


  		












Formats disponibles :
  Unified diff