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

\documentclass{amsart}

\usepackage{amsthm}

\input{macros}

\begin{document}

	\section{Logical operations as programs}

	Any polynomial-time predicate can be conservatively added to BC with only safe inputs.

	Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments.

	\section{Soundness}

	We show that any provably convergent function of $I\Sigma^{N}_i$ is in $\Box_i$.

	\subsection{Interpreting $\Pi_{i-1}$ formulae as programs}

	Each $\Pi_{i-1}$ formula is directly interpreted, as in usual WFM, as a descriptive program evaluating whether it is true or not.

	We define it by induction on formula structure:

	\[

	\begin{array}{rcl}

	\wit{s,t}{s=t} (;x) & \dfn & =(;s,t) \\

	\smallskip

	\wit{t}{N(t)} (;x) & \dfn & =(;x,t)\\

	\smallskip

	\wit{t}{\Box N(t)} (u;) & \dfn & =(;u,t) \\

	\smallskip

	\wit{\vec t}{A\star B} (;x) & \dfn & \star (; \wit{\vec t}{A} (;x), \wit{\vec t}{B} (;x) ) \\

	\smallskip

	\wit{\vec t}{\exists x^N . A(x)} (;x) & \dfn & \begin{cases}

	1 & \exists a^N . \wit{a , \vec t}{A(a)} (;x) = 1 \\

	0 & \text{otherwise}

	\end{cases} \\

	\smallskip

	\wit{\vec t}{\forall x^N . A(x)} (;x) & \dfn &

	\begin{cases}

	0 & \exists a^N. \wit{a, \vec t}{ A(a)} (;x) = 0 \\

	1 & \text{otherwise}

	\end{cases}

	\end{array}

	\]

	(Notice that, by free-cut elimination, $\Box$-formulae are always of the form $\Box N(t)$, so any composite formulae can be assumed to have only safe arguments.

	We can also assume that they always occur on the LHS of a sequent.)

	\subsection{Witness predicate for $\Sigma_i$ formulae}

%	We give the witness predicate for $\Sigma_i$ formulae assumed to be in prenex form.

	When $A,B$ are $\Sigma_{i}$ we define:

		\[

		\begin{array}{rcl}

		\wit{\vec t}{A\star B} (;\vec x , \vec y) & \dfn & \star (; \wit{\vec t}{A} (;\vec x), \wit{\vec t}{B} (;\vec y) ) \\

		\smallskip

		\wit{\vec t}{\exists  x . A( x)} (; x, \vec x) & \dfn & \wit{a, \vec t}{A( a)}(;\vec x) \left[ x^N /  a\right]

		\end{array}

		\]

	(Notice that this covers all $\Sigma_i$ formulae).

	\subsection{Witness extraction invariant}

%	We will show the following result:

	We will show that, if there is a proof $\pi$ of $\Gamma \seqar \Delta$, then there are programs $\vec f$ such that:

	\[

	\wit{\vec t}{\bigwedge \Gamma} (; \vec x)

	\quad \implies \quad

	\wit{\vec t}{\bigvee \Delta } (; \vec f (; \vec x) )

	\]

	\subsection{Defining the programs}

	We define the extracted programs inductively on a free-cut free proof.

	\begin{itemize}

	\item $\forall$ right case. Auxiliary formula $A$ must be $\Pi_{i-1}$ by free-cut elimination.

		\[

		\dfrac{N(a), \Gamma \seqar \Delta , A(a)}{\Gamma \seqar \Delta , \forall x^N. A(x)}

		\]

		By the inductive hypothesis we have functions $\vec f^\Delta , \vec f^A$ such that:

		\[

		\wit{a , \vec t}{N(a)} (;x)

		\wedge

		\wit{a , \vec t}{\bigwedge \Gamma} (\vec u; \vec x)

		\implies

		\wit{a , \vec t}{\bigvee \Delta}{ (; \vec f^\Delta (\vec u ; x , \vec x))}

		\vee

		\wit{a , \vec t}{ A} (; \vec f^A (\vec u ; x , \vec x) )

		\]

		Since $A$ is $\Pi_{i-1}$ we can forget about $\vec f^A$.

		We define $\vec g^\Delta , \vec g^{\forall x^N . A}$ as follows:

		\[

		\begin{array}{rcl}

		\vec g^{\forall x^N . A} (\vec u ; \vec x) & \dfn & 0 \\

		\vec g^\Delta (\vec u ; \vec x) & \dfn &

		\vec f^\Delta ( \vec u ;  \mu a^N . ( \wit{a , \vec t}{A} (;0) = 0 ) , \vec x )

		\end{array}

		\]

		(Notice that the minimisation program has the same complexity as the witness predicate for $\forall x^N . A(x)$, i.e.\ $\Pi_{i-1}$.)

	\item Contraction right case. Need to test the witness predicate using conditional. (No need for $\mu$s.).

	Given such a step,

	\[

	\dfrac{\Gamma \seqar \Delta , A , A}{\Gamma \seqar \Delta , A}

	\]

	by the inductive hypothesis we have programs $\vec f^\Delta , \vec f^0 , \vec f^1$ such that:

	\[

	\wit{\vec t}{\bigwedge \Gamma} (\vec u ; \vec x)

	\implies

	\wit{\vec t}{\bigvee \Delta} (; \vec f^\Delta (\vec u ; \vec x) )

	\vee

	\wit{\vec t}{A} (;\vec f^0 (\vec u ; \vec x))

	\vee

	\wit{\vec t}{A} (; \vec f^1 (\vec u ; \vec x))

	\]

	Construct the programs $\vec g^\Delta, \vec g^A$ as follows:

	\[

	\begin{array}{rcl}

	\vec g^\Delta (\vec u ; \vec x) & \dfn & \vec f^\Delta (\vec u ; \vec x) \\

	\vec g^A (\vec u; \vec x) & \dfn &

	\begin{cases}

	\vec f^0 (\vec u ; \vec x) & \wit{\vec t}{A} (;\vec f^0(\vec u ; \vec x) =1 ) \\

	\vec f^1 (\vec u ; \vec x) & \text{otherwise}

	\end{cases}

	\end{array}

	\]

	\item Induction. NB: Can assume no side-formulae on the right!!

	\[

	\dfrac{\Box N(a), \Gamma, A(a) \seqar A(s_i a)}{\Box N(s), \Gamma , A(0) \seqar A(s)}

	\]

	We need to keep track of all the terms in the witness predicate.

	\[

%	\begin{array}{rl}

%	&\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)

%	\\

%	\implies &

%	\wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^A (u , \vec u ; \vec x , \vec y)  )

%	\vee

%	\wit{a , t(a), t(s_i a), \vec t}{\bigvee \Delta} (; \vec f^\Delta (u , \vec u ; \vec x , \vec y)  )

%	\end{array}

\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)

\implies

\wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^i (u , \vec u ; \vec x , \vec y)  )

	\]

	Define $\vec g$ by safe recursion as follows:

	\[

	\begin{array}{rcl}

	\vec g (0 , \vec u ; \vec x , \vec y) & \dfn & \vec y \\

	\vec g (s_i u, \vec u ; \vec x , \vec y) & \dfn & \vec f^i ( u, \vec u; \vec x, \vec g (u, \vec u ; \vec x , \vec y) )

	\end{array}

	\]

	\end{itemize}

	\subsection{Proof of correctness}

\end{document}