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

\documentclass[a4paper,UKenglish]{lipics-v2016}

%This is a template for producing LIPIcs articles. 

%See lipics-manual.pdf for further information.

%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"

%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"

% for section-numbered lemmas etc., use "numberwithinsect"

\usepackage{microtype}%if unwanted, comment out or use option "draft"

%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory

\bibliographystyle{plainurl}% the recommended bibstyle

% Author macros::begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Free-cut elimination in linear logic: an application to implicit complexity}

%\titlerunning{A Sample LIPIcs Article} %optional, in case that the title is too long; the running title should fit into the top page column

%% Please provide for each author the \author and \affil macro, even when authors have the same affiliation, i.e. for each author there needs to be the  \author and \affil macros

\author[1]{Patrick Baillot}

\author[2]{Anupam Das}

\affil[1]{Dummy University Computing Laboratory, Address/City, Country\\

  \texttt{open@dummyuniversity.org}}

\affil[2]{Department of Informatics, Dummy College, Address/City, Country\\

  \texttt{access@dummycollege.org}}

\authorrunning{J.\,Q. Open and J.\,R. Access} %mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et. al.'

\Copyright{John Q. Open and Joan R. Access}%mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

\subjclass{Dummy classification -- please refer to \url{http://www.acm.org/about/class/ccs98-html}}% mandatory: Please choose ACM 1998 classifications from http://www.acm.org/about/class/ccs98-html . E.g., cite as "F.1.1 Models of Computation". 

\keywords{Dummy keyword -- please provide 1--5 keywords}% mandatory: Please provide 1-5 keywords

% Author macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\EventEditors{John Q. Open and Joan R. Acces}

\EventNoEds{2}

\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}

\EventShortTitle{CVIT 2016}

\EventAcronym{CVIT}

\EventYear{2016}

\EventDate{December 24--27, 2016}

\EventLocation{Little Whinging, United Kingdom}

\EventLogo{}

\SeriesVolume{42}

\ArticleNo{23}

% Editor-only macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\usepackage[lutzsyntax]{virginialake}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{amsthm}

\usepackage{times}

%\usepackage{sans}

\usepackage{cmll}

%\newtheorem{theorem}{Theorem}

%\newtheorem{maintheorem}[theorem]{Main Theorem}

%\newtheorem{observation}[theorem]{Observation}

%\newtheorem{corollary}[theorem]{Corollary}

%\newtheorem{lemma}[theorem]{Lemma}

\newtheorem{proposition}[theorem]{Proposition}

%\newtheorem{conjecture}[theorem]{Conjecture}

%

%\theoremstyle{definition}

%\newtheorem{definition}[theorem]{Definition}

%\newtheorem{example}[theorem]{Example}

%\newtheorem{notation}[theorem]{Notation}

%\newtheorem{convention}[theorem]{Convention}

%\newtheorem{remark}[theorem]{Remark}

%\newtheorem{discussion}[theorem]{Discussion}

\newcommand{\todo}[1]{{\color{red}{\textbf{Todo:} #1}}}

\newcommand{\anupam}[1]{{\color{orange}{\textbf{Anupam:} #1}}}

\newcommand{\patrick}[1]{{\color{blue}{\textbf{Patrick:} #1}}}

\newcommand{\defined}{:=}

\begin{document}

	\newcommand{\LL}{\it{LL}}

	\vllineartrue

	\newcommand{\FV}{\mathit{FV}}

	%terms

	\renewcommand{\succ}{s}

	\renewcommand{\epsilon}{\varepsilon}

	% linear connectives

	\newcommand{\limp}{\multimap}

	\renewcommand{\land}{\otimes}

	\newcommand{\laand}{\&}

	\newcommand{\laor}{\oplus}

	\renewcommand{\lor}{\vlpa}

	\renewcommand{\lnot}[1]{{#1^{\perp}}}

	\newcommand{\lnotnot}[1]{#1^{\perp \perp}}

	% classical connectives

	\newcommand{\cimp}{\supset}

	\newcommand{\cand}{\wedge}

	\newcommand{\cor}{\vee}

	\newcommand{\cnot}{\neg}

	\newcommand{\Ax}{\mathit{(Ax)}}

	\newcommand{\Rl}{\mathit{(Rl)}}

	\newcommand{\MELL}{\mathit{MELL}}

	\newcommand{\MEAL}{\mathit{MELLW}}

	\newcommand{\MELLW}{\mathit{MELL(W)}}

	\newcommand{\Aonetwo}{\mathcal{A}^1_2}

	\newcommand{\logic}{\mathit{L}_{\mathcal A} }

	% predicates

	\newcommand{\nat}{N}

	\newcommand{\Nat}{\mathbb{N}}

	%axioms

	\newcommand{\wk}{\mathit{wk}}

	\newcommand{\impl}{\cimp\text{-}\mathit{l}}

	\newcommand{\impcomm}{\mathit{com}}

	\newcommand{\conint}{\cand\text{-}\mathit{i}}

	\newcommand{\conel}{\cand\text{-}\mathit{e}}

	\newcommand{\negclass}{\cnot}

	%rules

	\renewcommand{\mp}{\mathit{mp}}

	\newcommand{\gen}{\mathit{gen}}

	\newcommand{\inst}{\mathit{ins}}

	\newcommand{\id}{\it{id}}

	\newcommand{\cut}{\it{cut}}

	\newcommand{\multicut}{\it{mcut}}

	\newcommand{\indr}{\mathit{IND}}

	\newcommand{\nec}{\mathit{nec}}

	\newcommand{\tax}{\mathit{T}}

	\newcommand{\four}{\mathit{4}}

	\newcommand{\kax}{\mathit{K}}

	\newcommand{\cntr}{\mathit{cntr}}

	\newcommand{\lefrul}[1]{#1\text{-}\mathit{l}}

	\newcommand{\rigrul}[1]{#1\text{-}\mathit{r}}

	%consequence relations

	\newcommand{\admits}{\vDash}

	\newcommand{\seqar}{\vdash}

	\newcommand{\proves}{\vdash}

	%induction

	\newcommand{\ind}{\mathit{IND}}

	\newcommand{\pind}{\mathit{PIND}}

	\newcommand{\cax}[2]{#1\text{-}#2}

\maketitle

\begin{abstract}

We prove a general form of free-cut elimination for first-order theories in linear logic. We consider a version of Peano Arithmetic in linear logic and prove a witnessing theorem via the Buss and Mints \emph{witness function method}, characterising polytime as the provably total functions.

 \end{abstract}

\section{Introduction}

\section{Preliminaries}

\todo{consider removing and just have a section on linear logic, including free-cut elimination.}

\subsection{Linear logic}

\subsection{Deduction theorem}

[cite Avron:`semantics and proof theory of linear logic']

We will make much use of the deduction theorem, allowing us to argue informally within a theory for hypotheses that have been promoted.

\begin{theorem}

	[Deduction]

	If $\mathcal T , A \proves B$ then $\mathcal{T} \proves !A \limp B$.

\end{theorem}

\todo{need that $A$ above is closed! Check for rules to axioms.}

\subsection{Converting axioms to rules in $\MELLW$}

\begin{proposition}

	An axiom $\Ax$ of the form,

	\[

	A_1 \limp \vldots \limp A_m \limp !B_1 \limp \vldots \limp !B_n \limp C

	\]

	is equivalent (over propositional $\LL$) to the rule $\Rl$:

	\[

	\vliiinf{\Rl}{}{ !\Gamma , A_1 , \dots , A_m \seqar C , ? \Delta  }{ !\Gamma \seqar B_1 , ?\Delta }{\vldots }{ !\Gamma \seqar B_n , ?\Delta}

	\]

\end{proposition}

\begin{proof}

	Let us first assume $\Ax$ and derive $\Rl$. From the axiom and Currying, we have a proof of:

	\begin{equation}\label{eqn:curried-axiom}

	A_1 , \dots , A_m , !B_1 , \dots , !B_n \seqar C

	\end{equation}

	This can simply be cut against each of the premisses of $\Rl$, applying appropriate contractions and necessitations, to derive it:

	\[

	\vlderivation{

		\vliq{c}{}{!\Gamma , A_1 , \dots , A_m \seqar C , ?\Delta }{

			\vliin{\cut}{}{!\Gamma, \dots , !\Gamma , A_1 , \dots , A_m \seqar C , ?\Delta, \dots , ?\Delta }{

				\vlin{!}{}{!\Gamma \seqar !B_n, ?\Delta }{\vlhy{!\Gamma \seqar B_n , ?\Delta }}

			}{

			\vliin{\cut}{}{\qquad \qquad \qquad \qquad  \vlvdots \qquad \qquad \qquad \qquad }{

				\vlin{!}{}{!\Gamma \seqar !B_1 , ?\Delta}{\vlhy{!\Gamma \seqar B_1, ?\Delta }}

			}{\vlhy{ A_1 , \dots , A_m , !B_1 , \dots , !B_n \seqar C } }

		}

	}

}

\]

Now let us prove $\Ax$ (again in the form of \eqref{eqn:curried-axiom}) by using $\Rl$ as follows:

\[

\vliiinf{\Rl}{}{ A_1 , \dots , A_m , !B_1 , \dots , !B_n \seqar C }{  \vlderivation{

		\vlin{w}{}{ !B_1 , \dots , !B_n \seqar B_1 }{

			\vlin{!}{}{!B_1 \seqar B_1 }{

				\vlin{\id}{}{B_1 \seqar B_1 }{\vlhy{}}

			}

		}

	}  }{\vldots}{

	\vlderivation{

		\vlin{w}{}{ !B_1 , \dots , !B_n \seqar B_n }{

			\vlin{!}{}{!B_n \seqar B_n }{

				\vlin{\id}{}{B_n \seqar B_n }{\vlhy{}}

			}

		}

	}

}

\]

\end{proof}

\textbf{NB:} The proof does not strictly require side formulae $? \Delta$ on the right of the sequent arrow $\seqar$, it would work without them, e.g.\ for the intuitionistic case. In a one-sided setting there is no difference.

\begin{corollary}

	The induction axiom of $A^1_2$ is equivalent to the rule:

	\[

	\vliinf{}{(x \notin \FV(\Gamma, \Delta))}{ !\Gamma , A(\epsilon) \seqar A(t) , ?\Delta }{ !\Gamma , A(x) \seqar A(s_0 x ), ?\Delta }{ !\Gamma, A(x) \seqar A( s_1 x ) , ?\Delta}

	\]

\end{corollary}

\begin{proof}

	By proposition above, generalisation and Currying.

\end{proof}

\subsection{Prenexing}

%In the presence of weakening we have a prenex normal form due to the following:

%

%\[

%\vlderivation{

%	\vlin{}{}{\exists x . A \lor B \seqar \exists x . (A(x) \lor B) }{

%		

%		}

%	}

%\]

Cannot derive prenexing operations, e.g.\ a problem with $\exists x . A \lor B \seqar \exists x . (A(x) \lor B)$. Can safely add prenexing rules? Or not a problem due to Witness predicate?

\section{Free-cut elimination in linear logic}

\section{Some variants of arithmetic in linear logic}

For pretty much all variants discussed we will actually work in the \emph{affine} variant of linear logic, which validates weakening: $(A \land B )\limp A$. There are many reasons for this; essentially it has not much effect on complexity while also creating a more robust proof theory. For example it induces the following equivalence:

\[

!(A\land B) \equiv (!A \land !B)

\]

(The right-left direction is already valid in usual linear logic, but the left-right direction requires weakening).

We define a variant of arithmetic inspired by Bellantoni and Hofmann's $A^1_2$. We describe later some connections to bounded arithmetic.

\subsection{Based on Bellantoni-Hoffmann, Leivant, etc.}

\newcommand{\natcntr}{\nat\mathit{cntr}}

\newcommand{\geneps}{\nat_{\epsilon}}

\newcommand{\genzer}{\nat_{0}}

\newcommand{\genone}{\nat_{1}}

\newcommand{\sepeps}{\epsilon}

\newcommand{\sepzer}{\succ_{0}}

\newcommand{\sepone}{\succ_{1}}

\newcommand{\inj}{\mathit{inj}}

\newcommand{\surj}{\mathit{surj}}

\begin{definition}

[Arithmetic]

We have the following axioms:

\[

\begin{array}{rl}

\natcntr & \forall x^N . (N(x) \land N(x)) \\

\geneps & \nat(\epsilon) \\

\genzer & \forall x^N . N(\succ_0 x) \\

\genone & \forall x^N . N(\succ_1 x) \\

\sepeps & \forall x^N . (\epsilon \neq \succ_0 x \land \epsilon \neq \succ_1 x) \\

\sepzer & \forall x^N , y^N. ( \succ_0 x = \succ_0 y \limp x=y ) \\

\sepone & \forall x^N , y^N. ( \succ_1 x = \succ_1 y \limp x=y ) \\

\inj & \forall x^N . \succ_0 x \neq \succ_1 x \\

\surj & \forall x^N . (x = \epsilon \lor \exists y^N . x = \succ_0 y \lor \exists y^N . x = \succ_1 y ) \\

\noalign{\bigskip}

\ind & todo

\end{array}

\]

Induction rule should be the following, to take account of relativised quantifiers?

\[

\vliinf{\ind}{}{ !N(t) , !\Gamma , A(\epsilon) \seqar A(t), ?\Delta }{ !N(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta }{ !N(a) , !\Gamma, A(a) \seqar A(\succ_0 a) , ?\Delta  }

\]

\todo{in existential above, is there a prenexing problem?}

\todo{what about $\leq$? Introducing this could solve prenexing problem, e.g.\ by induction?}

\end{definition}

\subsection{$\nat$-hierarchy}

\begin{definition}

\todo{replace N with nat.}

	Let us define the quantifiers $\exists x^N . A$ and $\forall x^N . A$ as $\exists x . (N(x) \land A)$ and $\forall x . (N(x) \limp A) $ respectively.

	We define $\Sigma^N_0 = \Pi^N_0 $ as the class of formulae that are free of quantifiers. For $i\geq 0$ we define:

	\begin{itemize}

		\item $\Sigma^N_{i+1}$ is the class of formulae $\exists x^N . A$ where $A \in \Pi^N_i$.

		\item $\Pi^N_{i+1}$ is the class of formulae $\forall x^N . A$ where $A \in \Sigma^N_i$.

		\item ($\Delta^N_i$ is the class $\Sigma^N_i \cap \Pi^N_i$.)

	\end{itemize}

\end{definition}

\todo{allow closure under positive Boolean operations?}

\todo{What about prenexing rules? Should not change provably total functions!}

\subsection{Equivalent rule systems}

For the quantifiers $\exists x^N $ and $\forall x^N$ we introduce the following rules, which are compatible with free-cut elimination:

\[

\begin{array}{cc}

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

\quad & \quad

\vlinf{}{}{\Gamma, N(t),\forall x^N A(x) \seqar \Delta}{\Gamma,  A(t) \seqar \Delta}

\\

\noalign{\bigskip}

\vlinf{}{}{\Gamma , \exists x^N A(x) \seqar \Delta}{\Gamma, N(a), A(a) \seqar \Delta}

\quad &\quad 

\vlinf{}{}{\Gamma, N(t) \seqar \Delta , \exists x^N . A(x)}{\Gamma  \seqar \Delta, A(t)}

\end{array}

\]

CHECK THESE!

\todo{Also include rules for contraction and weakening.}

\section{Convergence of Bellantoni-Cook programs}

\subsection{Bellantoni-Cook programs}

We first recall the notion of safe recursion on notation from BC. TODO

\subsection{Convergence in arithmetic}

\begin{theorem}

	[Convergence]

	If $\Phi(f)$ is an equational specification corresponding to a BC-program defining $f()$, then $\cax{\Sigma^N_1}{\pind} \proves  \ !\Phi(f) \limp \forall \vec{x}^{!N} . N(f(\vec x))$.

\end{theorem}

\begin{proof}

	We show by induction on the structure of a BC-program for $f(\vec x ; \vec y)$ that:

	\begin{equation}

	\Phi(f) , \cax{\Sigma^N_1}{\pind} \proves \ \forall \vec{x}^{!N} . \forall \vec{y}^N . N(f(\vec x ; \vec y))

	\end{equation}

	We give some key cases in what follows.

	Suppose $f$ is defined by PRN by:

	\[

	\begin{array}{rcl}

	f(0,\vec x ; \vec y) & = & g(\vec x ; \vec y) \\

	f(\succ_i x , \vec x ; \vec y) & = & h_i (x, \vec x ; \vec y , f(x , \vec x ; \vec y))

	\end{array}

	\]

	By the inductive hypothesis we already have that $g, h_0, h_1$ are provably convergent, so let us suppose that $N(\vec x)$ and prove,

	\begin{equation}

	\forall x^{!N} . ( N(\vec y) \limp N(f(x , \vec x ; \vec y)  )

	\end{equation}

	by $\cax{\Sigma^N_1}{\pind}$ on $x$.

	In the base case we have the following proof:

	\[

	\vlderivation{

		\vliin{}{}{N(\vec y) \limp N(f(0, \vec x ; \vec y))}{

			\vltr{IH}{N(\vec y) \limp N(g(\vec x ; \vec y))}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

		}{

		\vlin{}{}{N(g (\vec x ; \vec y) ) \limp N(f(0, \vec x ; \vec y)) }{

			\vlin{}{}{g(\vec x ; \vec y) = f(0 , \vec x ; \vec y)}{\vlhy{}}

		}

	}

}

\]

For the inductive step, we need to show that,

\[

\forall x^{!N} . (( N(\vec y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N(\vec y) \limp N(f(\succ_i x , \vec x ; \vec y) )   )

\]

so let us suppose that $N(x)$ and we give the following proof:

\[

\vlderivation{

	\vlin{N\cntr}{}{N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y)  ) }{

		\vliin{}{}{N(y) \limp N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y)  ) }{

			\vliin{}{}{ N(y) \limp N(y) \limp ( N(y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N( h_i (x , \vec x ; \vec y , f(x , \vec x ; \vec y) ) ) }{

				\vltr{MLL}{( N(\vec y) \limp (N (\vec y) \limp N(f(x, \vec x ; \vec y) )) \limp N(f(x, \vec x ; \vec y)) }{\vlhy{\quad }}{\vlhy{\ }}{\vlhy{\quad }}

			}{

			\vlhy{2}

		}

	}{

	\vlhy{3}

}

}

}

\]

TOFINISH

\end{proof}

\section{Witness function method}

\todo{negation normal form}

\newcommand{\type}{\mathtt{t}}

\newcommand{\norm}{\nu}

\newcommand{\safe}{\sigma}

\subsection{Typing}

\begin{definition}

	[Types]

	To each formula we associate a type as follows:

	\[

	\begin{array}{rcll}

	\type (\nat (t)) & := & \Nat_\safe & \\

	\type(s = t) & := & \Nat_\safe & \\

	\type (A \star B)  & : = & \type (A) \times \type (B) & \text{for $\star \in \{ \lor, \land, \laor, \laand \} $.} \\

	\type (! A) & : = & \type_\norm (A) & \text{for $\lambda \in \{ !, ? \}$.}\\

	\type (\exists x^N . A) & := & \Nat_\norm \times \type (A) & \\

	\type (\forall x^N . A) & := & \Nat_\norm \to \type(A)

	\end{array}

	\]

	\end{definition}

	\todo{does this need to be compatible with safety etc.?}

	\newcommand{\witness}[2]{\mathit{Witness}^{#1}_{#2}}

	\begin{definition}

		[Witness predicate]

		We define the following formula:

		\[

		\begin{array}{rcll}

		\witness{\vec a}{A} (w, \vec a) & := & A(\vec a) & \text{for $A$ quantifier-free.} \\

		\witness{\vec a}{\exists x . A} (w, \vec w , \vec a) & := & \witness{\vec{a}, a}{A(a)}(\vec w , \vec a, w ) & \\

		\witness{\vec a}{A \star B} ( \vec w^1 , \vec w^2 ) & := &  \witness{\vec a}{A} (\vec w^1) \star \witness{\vec a}{B} (\vec w^2) & \text{for $\star \in \{ \land, \lor, \laand , \laor\}$.} \\

		\end{array}

		\]

	\end{definition}

	\todo{problem: what about complexity of checking equality? }

	\todo{What about $\nat (t)$? What does it mean? Replace with true?}

	\todo{either use the witness predicate above, or use realizability predicate at meta-level and a model theory, like BH.}

	\subsection{The translation}

	Need witness predicate so that we know what is being preserved.

\begin{definition}

	[Translation]

	We give a translation of proofs $\pi$ of sequents $\Gamma(\vec a) \seqar \Delta(\vec a)$ to BC-programs for a vector of functions $\vec f^\pi : \type(\bigotimes\Gamma) \times \Nat^{|\vec a|} \to \type(\bigparr\Delta)$ such that:

	\[

	\witness{\vec a}{\bigotimes \Gamma} (\vec w , \vec a) \implies \witness{\vec a}{\bigparr \Delta } (\vec f(\vec w , \vec a), \vec a)

	\]

	We will be explicit about normal and safe inputs when necessary, for the most part we will simply rearrange inputs into lists $(\vec x; \vec a)$ as in BC framework.

	We often suppress the parameters $\vec a$ when it is not important.	

	\anupam{Is this implication provable in Bellantoni's version of PV based on BC?}

	\anupam{for moment try ignore decoration on right? what about negation?}

	\anupam{just do it and see what happens!}

	\[

	\vlderivation{

		\vliin{\land}{}{ \Gamma, \Sigma \seqar \Delta, \Pi, A\land B }{

			\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

			}{

			\vltr{\pi_2}{ \Sigma \seqar \Pi, B }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

			}

		}

	\]

	So we have $\vec f^{1} (\vec x ; \vec a)$ and $\vec f^2 (\vec y ; \vec b)$ for $\pi_1 $ and $\pi_2$ respectively, by the inductive hypothesis. We simply construct $\vec f^\pi$ by rearranging these functions:

	\[

	\vec f^\pi (\vec x , \vec y ; \vec a , \vec b) \quad := \quad ( f^1_1 (\vec x ; \vec a) , \dots , f^1_{|\Delta|} (\vec x ; \vec a) , f^2_1 (\vec y; \vec b) , \dots , f^2_{|\Pi|} (\vec y ; \vec b) , f^1_{|\Delta|+1} (\vec x ; \vec a ) , f^2_{|\Pi|+1} (\vec y ; \vec b)

	\] 

	\anupam{bad notation since need to include free variables of sequent too. (also of theory.) Reconsider.}

	\[

	\vlderivation{

		\vlin{\lefrul{\cntr}}{}{ !A , \Gamma \seqar \Delta }{

			\vltr{\pi'}{  !A, !A , \Gamma \seqar \Delta}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

			}

		}

	\]

	Have $\vec f' (x_1 , x_2 , \vec y ; \vec a)$ for $\pi'$. Define

	\[

	\vec f (x_1 , \vec y ; \vec a) \quad := \quad \vec f'(x_1 , x_1 , \vec y ; \vec a)

	\]

	\[

	\vlderivation{

	\vlin{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, ?A}{

	\vltr{\pi'}{  \Gamma \seqar \Delta, ?A, ?A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

	}

	}

	\]

	(need test function against witness predicate?)

	\anupam{problem: how to test even equality of two terms? Maybe treat $?$ as $!$ on left?}

	\anupam{Not a problem by free-cut elimination! Can assume there are no $?$ in the proof! Is this equivalent to treaing $?$ as $!$ on left?}

	\anupam{Yes I think so. We can work in a left-sided calculus. only problem is for induction. But this can never be a problem for modalities since induction formulae are modality-free.}

	\anupam{this is actually the main point.}

	\[

	\vlderivation{

	\vliin{\rigrul{\laand}}{}{\Gamma \seqar \Delta, A \laand B}{

	\vltr{\pi_1}{  \Gamma \seqar \Delta, A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

	}{

	\vltr{\pi_2}{  \Gamma \seqar \Delta, B}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

	}

	}

	\]

	Suppose we have $\vec f^i (\vec x , \vec a ; \vec y , \vec b)$ from $\pi_i$.

	\anupam{problem: does this require many tests, just like for contraction? Can we isolate a different complexity class? e.g.\ PH or Grzegorzyck?}

	\anupam{skip this case and consider later.}

\[

\vlderivation{

\vliin{\cut}{}{\Gamma , \Sigma \seqar \Delta , \Pi}{

\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}{

\vltr{\pi_2}{\Sigma , A \seqar \Pi}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

	\]

We can assume that $A$ in the conclusion of $\pi_2$ is free of modalities, since one of the $A$s must be directly descended from an induction formula, and so consists of only safe inputs. Therefore we have functions $\vec f^1 (\vec w; \vec x)$ and $\vec f^2 (\vec y ; \vec z , \vec u)$ for $\pi_1$ and $\pi_2 $ respectively (free variable parameters are suppressed), with $\vec u$ corresponding to the (safe) inputs for $A$. 

Let us write:

\[

\begin{array}{rcl}

\vec f^1 & = & ( \vec f^1_i )^{|\Delta|+1}_{i=1} \\

\vec f^2 & = & ( \vec f^2_i )^{|\Pi|}_{i=1}

\end{array}

\]

to denote the parts of $\vec f^i$ corresponding to formulae in their sequents.

We define:

\[

\vec f (\vec w , \vec y ; \vec x , \vec z)

\quad := \quad

(

( \vec f^1_i (\vec w ; \vec x) )_{i \leq |\Delta|}

,

\vec f^2 ( \vec y ; \vec z , \vec f^1_{|\Delta| +1 } (\vec w ; \vec x) )

)

\]

Notice that all safe inputs are hereditarily right of a $;$, and so these terms are definable by safe composition and projection.

\todo{left todo below.}

Right existential:

\[

\vlderivation{

\vlin{\rigrul{\exists}}{}{ \Gamma, \nat(t) \seqar \Delta , \exists x^\nat . A(x) }{

\vltr{\pi'}{ \Gamma \seqar \Delta , A(t) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

Left existential:

\[

\vlderivation{

\vlin{\lefrul{\exists}}{}{ \Gamma, \exists x^N . A(x) \seqar \Delta }{

\vltr{\pi'}{ \Gamma, A(a) ,  N(a) \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

!:

\[

\vlderivation{

\vlin{!}{}{\Gamma, !A \seqar \Delta}{

\vltr{\pi'}{ \Gamma , A \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

\anupam{Again, use free-cut elimination to get rid of this case. We know $!$-ed formulae in advance, so just fix those as normal inputs in advance.}

Induction: (can assume no side-formulae on right for same reason as no contraction.)

\[

\vlderivation{

\vliin{\ind}{}{ !\Gamma , !\nat (t) ,  A(0) \seqar A(t) }{

\vltr{\pi_0}{ !\Gamma , !\nat(a) , A(a) \seqar A(\succ_0 a)}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}{

\vltr{\pi_1}{ !\Gamma , !\nat(a), A(a)\seqar A(\succ_1 a) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

}

}

\]

Suppose we have functions $\vec f^i (\vec x , y ; \vec u)$ from proofs $\pi_i$ where $\vec x $ corresponds to $!\Gamma$, $y$ corresponds to $!N(a)$ and $\vec u$ corresponds to $A(a)$.

\anupam{role of $!N(a)$ versus having $a$ as a parameter to function. To consider!}

Define the function $f_k$ (for $k = 1 , \dots , |\vec u|$) by PRN:

\[

\begin{array}{rcl}

f_k(\epsilon, \vec x , y ; \vec u) & := & u_k \\

f_k (\succ_i w , \vec x , y ; \vec u) & : = & f^i_k ( \vec x ,  y ; \vec f ( w, \vec x , y ; \vec u ) )

\end{array}

\]

\anupam{check this, esp use of parameters, cf.\ above.}

\anupam{Is this not using a simultaneous version of PRN? Might need concatenation of words/basic coding to deal with this.}

\end{definition}

\section{Further work}

Say something about minimisation and the polynomial hierarchy. Could be achieved by controlling contraction/additives, since this requires a notion of tests.

\section{Conclusions}

\end{document}