/ - Diff - Linear Arithmetic - Forge du Centre Blaise Pascal

Révision 141

     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}$.
     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}.
     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.
     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}.
     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}.
     %with an approach in previous work where we characterised $\ptime$ in a \emph{linear logic}, also extracting BC programs %\cite{BaillotDas16}.
     \subsection{Extraction at ground type}
     As we did for previous work \cite{BaillotDas16}, we will rely on the \emph{witness function method} for extracting functions at bounded type.
     As we did in \cite{BaillotDas16}, we will rely on the \emph{witness function method} for extracting functions at bounded type.
     This was pioneered by Buss, although independently used by Mints beforehand. The idea is as follows:
     \begin{enumerate}
     	\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.
-...
     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$.
     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.
     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}.
     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
     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.
     % since we cannot externally certify the complexity of the predicate when unbounded quantifiers abound.
     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.

Formats disponibles : Unified diff

Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

Révision 141