Révision 141 CharacterizingPH/draft.tex

draft.tex (revision 141)
172 172 
In fact, two predicates will suffice and their relationship is entirely governed by the equation $N_1 (x) \iff \square N_0 (x)$, under the laws of the modal logic $\mathit{S4}$.
173 173 
The distinction between the two predicates corresponds to the distinction between safe and normal variables in BC-like programs, which was an observation from previous work \cite{BaillotDas16}.
174 174 
A similar phenomenon occurs in Cantini's work \cite{Cantini02}, which presents a characterisation of $\ptime$ in an \emph{applicative theory}, in order to extract BC programs.
175 
While he allows arbitrary alternation of unbounded quantifiers, note that his induction is \emph{positive}, and so universal quantifiers cannot vary over certified natural numbers, i.e.\ individuals in $N$. In fact this sort of unbounded quantification is also compatible with an approach in previous work where we characterised $\ptime$ in a \emph{linear logic}, also extracting BC programs \cite{BaillotDas16}.
175 
While he allows arbitrary alternation of unbounded quantifiers, note that his induction is \emph{positive}, and so universal quantifiers cannot vary over certified natural numbers, i.e.\ individuals in $N$. In fact this sort of unbounded quantification is also compatible with our approach of \cite{BaillotDas16}.
176 
%with an approach in previous work where we characterised $\ptime$ in a \emph{linear logic}, also extracting BC programs %\cite{BaillotDas16}.
176 177 

  		





  177
  178
  
    

  		





  178
  179
  
    

  		





  179
  180
  
    
\subsection{Extraction at ground type}


  		





  180
  
  
    
As we did for previous work \cite{BaillotDas16}, we will rely on the \emph{witness function method} for extracting functions at bounded type.


  		





  
  181
  
    
As we did in \cite{BaillotDas16}, we will rely on the \emph{witness function method} for extracting functions at bounded type.


  		





  181
  182
  
    
This was pioneered by Buss, although independently used by Mints beforehand. The idea is as follows:


  		





  182
  183
  
    
\begin{enumerate}


  		





  183
  184
  
    
	\item\label{item:de-morgan} Reduce a proof to \emph{De Morgan} normal form, with formulae over the basis $\{ \bot, \top, \vee , \wedge , \exists, \wedge \}$ and negation restricted to atoms.


  		





  ......




  196
  197
  
    
Indeed this could have been possible in our previous work \cite{BaillotDas16}, as Cantini did in his work \cite{Cantini02}, for a characterisation of $\ptime$.


  		





  197
  198
  
    
However, in this case, since the quantifiers are unbounded the realisability argument is apparently not readily formalised, and it is therefore quite natural to pursue a \emph{bona fide} proof interpretation.


  		





  198
  199
  
    
For this, it seems we need to go one level higher than type 1 functions to verify semantic properties of witnesses of first-order formulae, themselves considered as genuine type 1 functions. Intuitively this is simply an inlining of \emph{Skolemisation}, although the idea of extending `witness predicates' to type 1 objects resembles methods from second-order bounded arithmetic, e.g.\ \cite{Cook:2010:LFP:1734064}. 


  		





  199
  
  
    
Unlike in the bounded arithmetic setting, due to the apparent unboundedness of programs in the $\mu$BC framework, we will need a formal witness predicate implemented itself as a BC-like program, hence the need for a proof interpretation rather than a realisability approach


  		





  
  200
  
    
Unlike in the bounded arithmetic setting, due to the apparent unboundedness of programs in the $\mu$BC framework, we will need a formal witness predicate implemented itself as a BC-like program, hence the need for a proof interpretation rather than a realisability approach.


  		





  200
  201
  
    
% since we cannot externally certify the complexity of the predicate when unbounded quantifiers abound.


  		





  201
  202
  
    
Fortunately, we believe that it suffices to consider $\mu$BC-programs with \emph{holes}, rather than a full characterisation of type 2 $\ph$, but verifying that such an approach could work represents the outstanding technical component of this work-in-progress.


  		





  202
  203
  
    
	


  		












Formats disponibles :
  Unified diff