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

Révision 240

     \end{figure}
     In order to carry out witness extraction for proofs of $\arith^i$, it will be useful to work with a \emph{sequent calculus} representation of proofs.
     Such systems exhibit strong normal forms, notably `free-cut free' proofs, and so are widely used for the `witness function method' for extracting programs from proofs.
     We introduce the required technical material here only briefly, due to space constraints.
     Such systems exhibit strong normal forms, notably `free-cut free' proofs, and so are widely used for the `witness function method' for extracting programs from proofs \cite{Buss86book,Buss98:intro-proof-theory}.
     We state the required technical material here only briefly, due to space constraints.
     A \emph{sequent} is an expression $\Gamma \seqar \Delta$ where $\Gamma$ and $\Delta$ are multisets of formulas.
     The inference rules of the sequent calculus $\LK$ are displayed in Fig.~\ref{fig:sequentcalculus}.
-...
     %As an example any axiom can be represented by such a nonlogical rule $(R)$, with no premise ($I=\emptyset$), $\Delta'$ equal to the axiom and $\Gamma=\Sigma'=\Pi$.
     We extend this purely logical calculus with certain non-logical rules and initial sequents corresponding to our theories $\arith^i$.
      For instance the axiom $\pind$ of Def. \ref{def:polynomialinduction} is represented by the following rule:
      For instance the axiom $\pind$ of Dfn.~\ref{def:polynomialinduction} is represented by the following rule:
     \begin{equation}
     \label{eqn:ind-rule}
     \small
     \vliinf{\pind}{}{ \normal(t) , \Gamma , A(0) \seqar A(t), \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{0} a) , \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{1} a) , \Delta  }
     \end{equation}
     where $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent.
     where $t$ varies over terms and the eigenvariable $a$ does not occur in the lower sequent.
+    %
     Similarly the $\rais$ inference rule of Dfn.~\ref{def:ariththeory} is represented by the nonlogical rule,
      \[
-...
         \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \exists  y^\normal .  A }{  \normal(t_1), \dots, \normal(t_k) \seqar \exists  y^\safe .  A}
     \end{array}
     \]
+    %
     %\patrick{In fact, I think we rather need the following nonlogical rule, which implies the previous one but is I guess more general:
     %\[
     % \begin{array}{cc}
-...
     %\]
     %}
+    %
     and the $\basic$ axioms are represented by designated initial sequents.
     $\basic$ axioms are represented by designated initial sequents.
     For instance here are some initial sequents corresponding to some of the $\basic$ axioms:
     \[
     \small
-...
     \end{array}
     \]
     The sequent system for $\arith^i$ extends $\LK$ by the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.
      Naturally, by completeness, we have that $\arith^i \proves A$ if and only if there is a sequent proof of $\seqar A$.
     The sequent system for $\arith^i$ extends $\LK$ by the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ rules.
      Naturally, by completeness, we have that $\arith^i \proves A$ if and only if there is a sequent proof of $\seqar A$ in the corresponding system.
      In fact, by \emph{free-cut elimination} results \cite{Takeuti87,Cook:2010:LFP:1734064} we may actually say something much stronger.
      Let us say that a sorting $(\vec u ; \vec x)$ of the variables $\vec u , \vec x$ is \emph{compatible} with a formula $A$ if each variable of $\vec x$ occurs hereditarily safe with respect to the $\bc$-typing of terms, i.e.\ never under $\smsh, |\cdot|$ and to the right of $\times$.
-...
     Strictly speaking, we must alter some of the sequent rules a little to arrive at this normal form. For instance the $\pind$ rule would have $\normal(\vec u)$ in its lower sequent rather than $\normal (t(\vec u))$. The latter is a consequence of the former already in $\basic$.
     The proof of this result also relies on a heavy use of the structural rules, contraction and weakening, to ensure that we always have a complete and compatible sorting of variables on the LHS of a sequent. This is similar to what is done in \cite{OstrinWainer05} where they use a $G3$ style calculus to manage such structural manipulations.
     As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae immediately below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.
     As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae `immediately' below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.
     Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:
     \[
-...
     \[
     \vlinf{\lefrul{|\forall|}}{}{\normal (\vec u ) , \safe (\vec x) , s(\vec u) \leq |t(\vec u)| , \forall u^\normal \leq |t(\vec u)| . A(u) , \Gamma \seqar \Delta }{\normal (\vec u ) , \safe (\vec x) , A(s(\vec u)  ) , \Gamma \seqar \Delta  }
     \]
     where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.
     with the usual side conditions and where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.

Formats disponibles : Unified diff

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

Révision 240