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

@article{GaboardiMarionRonchi12,

  author    = {Marco Gaboardi and

               Jean{-}Yves Marion and

In this work we improve the situation by using implicit methods in first-order theories to characterise $\ph$.

To achieve this we work with a function algebra of Bellantoni from \cite{BellantoniThesis} in which to extract programs, and use the \emph{witness function method} of Buss to extract programs at ground type and preserve quantifier information, necessary to delineate the levels of $\ph$.

%One particular feature of this work that helps make this possible is to break one of the aforementioned correlations: while we use implicit constraints, our witness extraction methods will use only functions of bounded type level. In this way we can naturally appeal to function algebras, which are of ground type in nature, which implicitly characterise $\ph$, namely via \emph{predicative minimisation} \cite{BellantoniThesis}.

%In order to remain in this class of programs and not get lost with higher types, we appeal to the \emph{witness function method} of extracting programs from proofs, a technique developed by Buss \cite{Buss86book} \cite{Buss:95:wfm-arith}, which is ideal for extracting ground programs directly from classical proofs in weak theories.

%This extends work presented in \cite{BaillotDas16}. %at \emph{CSL '16}.

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}

We rely on the \emph{witness function method} for extracting functions at bounded type.

%This was pioneered by Buss, although independently used by Mints beforehand. 

	\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.

	\item\label{item:free-cut} Conduct a \emph{free-cut elimination} on the proof, resulting in a proof whose formulae are restricted to

	essentially just subformulae of the conclusion, axioms and nonlogical steps.

	\end{enumerate}

	\ref{item:de-morgan} ensures that our extraction works at ground type, rather than higher types which are typically necessary when negation has larger scope.