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

\section{A two-sorted arithmetic for the polynomial hierarchy}

(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)

\newcommand{\nb}[1]{{\color{red} NB: #1}}

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

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

\newtheorem{proposition}[theorem]{Proposition}

\newcommand{\Word}{\mathbb{W}}

\newcommand{\pred}{p}

\renewcommand{\succ}[1]{s_i}

\section{Introduction and motivation}

\anupam{Copied below from DICE submission}

Today, there are countless approaches towards characterising complexity classes via logic.

Foremost amongst these lies the proof-theoretic approach, characterising classes as the `representable' functions of some logic or theory.

Examples include bounded arithmetic \cite{Buss86book} \cite{Krajicek:1996:BAP:225488} \cite{Cook:2010:LFP:1734064}, applicative theories \cite{Cantini02} \cite{KahOit:13:ph-levels}, intrinsic and ramified theories \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, fragments of linear logic \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.

To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.

Perhaps a more important (and somewhat orthogonal) distinction for the \textsc{Dice-Fopara} community is whether the constraints on the logic or theory are \emph{implicit} or \emph{explicit}. The former includes constraints such as ramification, type level and substructural considerations, while the latter includes bounded quantification, bounded modalities etc. This distinction is also naturally exhibited in associated function algebras, e.g. Cobham's \emph{limited} recursion on notation \cite{Cobham} vs.\ Bellantoni and Cook's \emph{predicative} recursion on notation \cite{BellantoniCook92}.

Some correlations abound: explicit bounds are typically far more useful for more fine-grained characterisations of complexity classes, e.g.\ levels of the polynomial or arithmetical hierarchies, and often admit witness extraction methods that remain in a ground type programming language, e.g.\ via recursion theoretic characterisations. Implicit bounds, however, are more often associated with higher-typed programming languages, which are arguably more useful for achieving witness extraction at all for powerful theories such as arithmetic and set theory, cf.~\cite{avigad1998godel}, \cite{troelstra1998realizability}. Complexity bounds are harder to obtain, but the framework is nonetheless somewhat more desirable since no bounds occur in the characterisation itself \emph{per se}.

In this line of work we attempt to ameliorate the situation by using implicit methods to delineate fine-grained hierarchies of feasible complexity classes, namely the \emph{polynomial hierarchy}, $\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}.

\subsection{State of the art}

As we have already argued, it is natural to expect that characterisations of hierarchies such as $\ph$ are more readily established by using ground or bounded type witness extraction procedures, due to the correspondence between logical searches in a program and the quantification over objects of ground type in a theory.

As justification for this position, consider the following table of examples of known characterisations:\footnote{All classes can be taken in their functional variations.}

%, distinguished by the type level of programs extracted:

\bigskip

\begin{tabular}{c|c|c}

	Class &	Ground & Higher order\\

	\hline

	%	quantifiers  & type-level\\

	$\nc^i$    & $\mathit{TNC}^i$ \cite{CloTak:1995:nc-ac}, $\mathit{VNC}^i$ \cite{Cook:2010:LFP:1734064} & - \\

	$\ptime$  &  $S^1_2$ \cite{Buss86book}, \cite{Strahm03}, $V^1$ \cite{Zambella96} \cite{Cook:2010:LFP:1734064} & $\mathit{LLL}$ \cite{Girard94:lll}, $\mathit{SLL}$ \cite{Lafont04} \\

	$\Box_i$  & $S^i_2$ \cite{Buss86book}, \cite{KahOit:13:ph-levels} & -  \\

	$\ph$& $S_2$ & - \\

	$\pspace$& $U^1_2$ \cite{Buss86book} & $\mathit{STA}_B$ \cite{GaboardiMarionRonchi12} \\

	%	$k$-$\exptime$ & -  & $\mathit{ELL}(k)$ \\

	Elementary & $I\Delta_0 + \exp$  & $\mathit{ELL}\;  \cite{Girard94:lll}$

\end{tabular}

\bigskip

\noindent

Thus, if we want an implicit characterisation of $\ph$ in a logical theory, we should break the apparent (although not universal) link between `implicit' and `higher type'. 

%If we restrict to the ground setting, where extracted programs do not make use of higher types, we have the following picture.

%

% Now, if we restrict to the ground setting, where extracted programs do not make use of higher types, there are still several 

Now, if we zoom in on the ground setting, where extracted programs do not make use of higher types, there are still several parameters by which the characterisations can vary, in particular:

\begin{itemize}

	\item How are programs specified in the language of the theory? By a formula, as in Peano arithmetic, by a first-order equational program, or by an applicative term in the style of combinatory algebra;

	\item What type of programs are extracted from proofs of the theory? A program of a bounded recursion class, e.g.\ of Cobham's algebra, or of a tiered recursion class, e.g.\ of Bellantoni and Cook's algebra.

\end{itemize}

We classify some known characterisations from the literature according to these two parameters in  the following table:

\bigskip

\begin{tabular}{c|c|c}

	{

		%\small model of comp. $\backslash$ extracted program 

	} & bounded rec. programs & tiered rec. programs \\

	\hline &&\\

	formula & $\ph$, $\square_i$ (Buss \cite{Buss86book})&\\

	%	& bounded induction (Buss \cite{Buss86book}) &\\

	\hline &&\\

	equational && $\ptime$\\

	&& (Leivant \cite{Leivant94:intrinsic-theories}) \\

	\hline &&\\

	applicative & $\ptime$ (Strahm \cite{Strahm03})  & $\ptime$ \\

	&$\ph$ (Kahle-Oitavem \cite{KahOit:13:ph-levels})& (Cantini \cite{Cantini02})

\end{tabular}

%TODO: improve table to make clear columns and rows, explicit and implicit columns.

%

%\begin{tabular}{c|c|c|c}

%	{

%		%\small model of comp. $\backslash$ extracted program 

%		} & Cobham & mon. constraints & BC-like \\

%	\hline &&\\

%	formula & PH, $\square_i$&&\\

%	& bounded induction (Buss) &&\\

%	\hline &&\\

%	equational &&& P\\

%	&&& (Leivant) \\

%	\hline &&\\

%	applicative &&PH & P \\

%	&&(Kahle-Oitavem)& (Cantini)

%\end{tabular}

\bigskip

\noindent

Our goal is to extend the approach using extraction of programs of a tiered recursion class (second column), using the equational style of specification (second row), to the whole of the polynomial hierarchy, i.e.\  $\ph$ and its levels $\square_i$.

%Our goal is to extend the implicit approach, via variations of Bellantoni-Cook (BC) programs, to the whole of the polynomial hierarchy.

@article{GaboardiMarionRonchi12,

  author    = {Marco Gaboardi and

               Jean{-}Yves Marion and

               Simona Ronchi Della Rocca},

  title     = {An Implicit Characterization of {PSPACE}},

  journal   = {{ACM} Trans. Comput. Log.},

  volume    = {13},

  number    = {2},

  pages     = {18:1--18:36},

  year      = {2012},

  url       = {http://doi.acm.org/10.1145/2159531.2159540},

  doi       = {10.1145/2159531.2159540},

  timestamp = {Mon, 09 Jan 2017 14:08:26 +0100},

  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tocl/GaboardiMR12},

  bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{Baelde12,

  author    = {David Baelde},

  title     = {Least and Greatest Fixed Points in Linear Logic},

  journal   = {{ACM} Trans. Comput. Log.},

  volume    = {13},

  number    = {1},

  pages     = {2},

  year      = {2012}

  }

@inproceedings{BaillotDas16,

  author    = {Patrick Baillot and

               Anupam Das},

  title     = {Free-Cut Elimination in Linear Logic and an Application to a Feasible

               Arithmetic},

  booktitle = {Proceedings of CSL 2016},

  pages     = {40:1--40:18},

    series    = {LIPIcs},

  volume    = {62},

  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},

  year      = {2016}

 }

@article{BellantoniCook92,

  author    = {Stephen Bellantoni and

               Stephen A. Cook},

  title     = {A New Recursion-Theoretic Characterization of the Polytime Functions},

  journal   = {Computational Complexity},

  volume    = {2},

  pages     = {97--110},

  year      = {1992}

 }

@inproceedings{Cobham,

	author = {Cobham, A.},

	title = {On the intrinsic computational difficulty of functions},

	booktitle={Proc. of the 1964 International Congress for Logic, Methodology, and the Philosophy

	of Science},

	year = {1964},

	issn = {0001-0782},

	pages = {24--30},

		publisher = {North Holland, Amsterdam}

} 

@article{Dershowitz:1979:PTM:359138.359142,

	author = {Dershowitz, Nachum and Manna, Zohar},

	title = {Proving Termination with Multiset Orderings},

	journal = {Commun. ACM},

	issue_date = {Aug. 1979},

	volume = {22},

	number = {8},

	month = aug,

	year = {1979},

	issn = {0001-0782},

	pages = {465--476},

	numpages = {12},

	doi = {10.1145/359138.359142},

	acmid = {359142},

	publisher = {ACM},

	address = {New York, NY, USA},

	keywords = {bags, multisets, production systems, program correctness, program termination, program verification, reduction rules, term rewriting systems, tree replacement systems, well-founded orderings, well-founded sets},

} 

@article{Beckmann11,

  author    = {Arnold Beckmann and

               Samuel R. Buss},

  title     = {Corrected upper bounds for free-cut elimination},

  journal   = {Theor. Comput. Sci.},

  volume    = {412},

  number    = {39},

  pages     = {5433--5445},

  year      = {2011}

}

@Phdthesis{BellantoniThesis,

author={Stephen J. Bellantoni},

title={Predicative Recursion and Computational Complexity},

school={University of Toronto},

year={1992}

}

@article{BelHof:02,

  author    = {Stephen Bellantoni and

               Martin Hofmann},

  title     = {A New "Feasible" Arithmetic},

  journal   = {J. Symb. Log.},

  volume    = {67},

  number    = {1},

  pages     = {104--116},

  year      = {2002}

 }

@article{Girard98,

  author    = {Jean{-}Yves Girard},

  title     = {Light Linear Logic},

  journal   = {Inf. Comput.},

  volume    = {143},

  number    = {2},

  pages     = {175--204},

  year      = {1998}

 }

@article{Hofmann00,

  author    = {Martin Hofmann},

  title     = {Safe recursion with higher types and BCK-algebra},

  journal   = {Ann. Pure Appl. Logic},

  volume    = {104},

  number    = {1-3},

  pages     = {113--166},

  year      = {2000}

  }

@article{Terui04,

  author    = {Kazushige Terui},

  title     = {Light Affine Set Theory: {A} Naive Set Theory of Polynomial Time},

  journal   = {Studia Logica},

  volume    = {77},

  number    = {1},

  pages     = {9--40},

  year      = {2004}

  }

@article{Leivant94:found-delin-ptime,

  author    = {Daniel Leivant},

  title     = {A Foundational Delineation of Poly-time},

  journal   = {Inf. Comput.},

  volume    = {110},

  number    = {2},

  pages     = {391--420},

  year      = {1994}

  }

@book{Buss86book,

  title={Bounded arithmetic},

  author={Buss, Samuel R},

  volume={86},

  year={1986},

  publisher={Bibliopolis}

}

@inproceedings{Leivant94:intrinsic-theories,

  author    = {Daniel Leivant},

  title={Intrinsic Theories and Computational Complexity},

  booktitle     = {Logical and Computational Complexity. Selected Papers. Logic and Computational

               Complexity, International Workshop {LCC} '94, Indianapolis, Indiana,

               USA, 13-16 October 1994},

  series    = {Lecture Notes in Computer Science},

  volume    = {960},

  pages={177-194},

  publisher = {Springer},

  year      = {1995}

}

@article{Cantini02,

  author    = {Andrea Cantini},

  title     = {Polytime, combinatory logic and positive safe induction},

  journal   = {Arch. Math. Log.},

  volume    = {41},

  number    = {2},

  pages     = {169--189},

  year      = {2002}

  }

@inproceedings{Girard94:lll,

  author    = {Jean{-}Yves Girard},

  title     = {Light Linear Logic},

  booktitle = {Logical and Computational Complexity. Selected Papers. {LCC} '94.},

  pages     = {145--176},

  year      = {1994},

  crossref  = {DBLP:conf/lcc/1994},

  doi       = {10.1007/3-540-60178-3_83},

  timestamp = {Thu, 23 Jun 2011 19:50:18 +0200},

  bibsource = {dblp computer science bibliography, http://dblp.org}

 }

@article{LincolnMSS92,

  author    = {Patrick Lincoln and

               John C. Mitchell and

               Andre Scedrov and

               Natarajan Shankar},

  title     = {Decision Problems for Propositional Linear Logic},

  journal   = {Ann. Pure Appl. Logic},

  volume    = {56},

  number    = {1-3},

  pages     = {239--311},

  year      = {1992}

 }

@article{Murawski04,

  author    = {Andrzej S. Murawski and

               C.{-}H. Luke Ong},

  title     = {On an interpretation of safe recursion in light affine logic},

  journal   = {Theor. Comput. Sci.},

  volume    = {318},

  number    = {1-2},

  pages     = {197--223},

  year      = {2004}

}

@article{Avron88,

  author    = {Arnon Avron},

  title     = {The Semantics and Proof Theory of Linear Logic},

  journal   = {Theor. Comput. Sci.},

  volume    = {57},

  pages     = {161--184},

  year      = {1988}

}

@article{GirardSS92:bounded-ll,

  author    = {Jean{-}Yves Girard and

               Andre Scedrov and

               Philip J. Scott},

  title     = {Bounded Linear Logic: {A} Modular Approach to Polynomial-Time Computability},

  journal   = {Theor. Comput. Sci.},

  volume    = {97},

  number    = {1},

  pages     = {1--66},

  year      = {1992}

 }

@article{Lafont04,

  author    = {Yves Lafont},

  title     = {Soft linear logic and polynomial time},

  journal   = {Theor. Comput. Sci.},

  volume    = {318},

  number    = {1-2},

  pages     = {163--180},

  year      = {2004}

 }

@inproceedings{Lasson11,

  author    = {Marc Lasson},

  title     = {Controlling Program Extraction in Light Logics},

  booktitle = {Typed Lambda Calculi and Applications - 10th International Conference,

               {TLCA} 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings},

  pages     = {123--137},

  series    = {Lecture Notes in Computer Science},

  volume    = {6690},

  publisher = {Springer},

  year      = {2011}

 }

@book{Takeuti87,

  title={Proof Theory},

  author={Takeuti, G.},

  year={1987},

  publisher={North-Holland, Amsterdam},

  note={and ed.}

}

@article{Girard87,

  author    = {Jean{-}Yves Girard},

  title     = {Linear Logic},

  journal   = {Theor. Comput. Sci.},

  volume    = {50},

  pages     = {1--102},

  year      = {1987},

  url       = {http://dx.doi.org/10.1016/0304-3975(87)90045-4},

  doi       = {10.1016/0304-3975(87)90045-4},

  timestamp = {Wed, 07 Sep 2011 12:13:20 +0200},

  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tcs/Girard87},

  bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{Buss98:intro-proof-theory,

  title={An introduction to proof theory},

  author={Buss, Samuel R},

  journal={Handbook of proof theory},

  volume={137},

  pages={1--78},

  year={1998}

}

@incollection{Miller04,

	year = {2004},

	author = {Dale Miller},

	editor = {Thomas Ehrhard},

	pages = {316--119},

	booktitle = {Linear Logic in Computer Science},

	publisher = {Cambridge University Press},

	title = {Overview of Linear Logic Programming}

}

@article{Andreoli92,

	author    = {Jean{-}Marc Andreoli},

	title     = {Logic Programming with Focusing Proofs in Linear Logic},

	journal   = {J. Log. Comput.},

	volume    = {2},

	number    = {3},

	pages     = {297--347},

	year      = {1992},

	doi       = {10.1093/logcom/2.3.297},

	timestamp = {Wed, 29 Jun 2011 15:52:24 +0200},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{FriedmanM92,

	author    = {Harvey Friedman and

	Robert K. Meyer},

	title     = {Whither Relevant Arithmetic?},

	journal   = {J. Symb. Log.},

	volume    = {57},

	number    = {3},

	pages     = {824--831},

	year      = {1992},

	doi       = {10.2307/2275433},

	timestamp = {Tue, 05 Aug 2014 16:36:24 +0200},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@inproceedings{Marion01,

  author    = {Jean{-}Yves Marion},

  title     = {Actual Arithmetic and Feasibility},

  booktitle = {Proceedings of Computer Science Logic (CSL 2001)} ,

    pages     = {115--129},

   series    = {Lecture Notes in Computer Science},

  volume    = {2142},

  publisher = {Springer},

  year      = {2001}

  }

@book{Cook:2010:LFP:1734064,

	author = {Cook, Stephen and Nguyen, Phuong},

	title = {Logical Foundations of Proof Complexity},

	year = {2010},

	isbn = {052151729X, 9780521517294},

	edition = {1st},

	publisher = {Cambridge University Press},

	address = {New York, NY, USA},

} 

@article{Baillot15,

	author    = {Patrick Baillot},

	title     = {On the expressivity of elementary linear logic: Characterizing Ptime

	and an exponential time hierarchy},

	journal   = {Inf. Comput.},

	volume    = {241},

	pages     = {3--31},

	year      = {2015},

	url       = {http://dx.doi.org/10.1016/j.ic.2014.10.005},

	doi       = {10.1016/j.ic.2014.10.005},

	timestamp = {Sat, 25 Apr 2015 11:14:59 +0200},

	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/iandc/Baillot15},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@inproceedings{BaiDas16,

	author    = {Patrick Baillot and

	Anupam Das},

	title     = {Free-Cut Elimination in Linear Logic and an Application to a Feasible

	Arithmetic},

	booktitle = {25th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2016,

	August 29 - September 1, 2016, Marseille, France},

	pages     = {40:1--40:18},

	year      = {2016},

	crossref  = {DBLP:conf/csl/2016},

	url       = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.40},

	doi       = {10.4230/LIPIcs.CSL.2016.40},

	timestamp = {Tue, 30 Aug 2016 15:55:10 +0200},

	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/csl/BaillotD16},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@book{Krajicek:1996:BAP:225488,

	author = {Kraj\'{\i}\v{c}ek, Jan},

	title = {Bounded arithmetic, propositional logic, and complexity theory},

	year = {1995},

	isbn = {0-521-45205-8},

	publisher = {Cambridge University Press},

	address = {New York, NY, USA},

} 

@incollection{CloTak:1995:nc-ac,

	title={First order bounded arithmetic and small boolean circuit complexity classes},

	author={Clote, Peter and Takeuti, Gaisi},

	booktitle={Feasible Mathematics II},

	pages={154--218},

	year={1995},

	publisher={Springer}

}

@article{Strahm03,

  author    = {Thomas Strahm},

  title     = {Theories with self-application and computational complexity},

  journal   = {Inf. Comput.},

  volume    = {185},

  number    = {2},

  pages     = {263--297},

  year      = {2003},

  url       = {http://dx.doi.org/10.1016/S0890-5401(03)00086-5},

  doi       = {10.1016/S0890-5401(03)00086-5},

  timestamp = {Thu, 20 Nov 2003 12:03:25 +0100},

  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/iandc/Strahm03},

  bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{Zambella96,

	author    = {Domenico Zambella},

	title     = {Notes on Polynomially Bounded Arithmetic},

	journal   = {J. Symb. Log.},

	volume    = {61},

	number    = {3},

	pages     = {942--966},

	year      = {1996},

	url       = {http://dx.doi.org/10.2307/2275794},

	doi       = {10.2307/2275794},

	timestamp = {Tue, 05 Aug 2014 16:36:22 +0200},

	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jsyml/Zambella96},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{KahOit:13:ph-levels,

	author    = {Reinhard Kahle and

	Isabel Oitavem},

	title     = {Applicative theories for the polynomial hierarchy of time and its

	levels},

	journal   = {Ann. Pure Appl. Logic},

	volume    = {164},

	number    = {6},

	pages     = {663--675},

	year      = {2013},

	url       = {http://dx.doi.org/10.1016/j.apal.2012.05.006},

	doi       = {10.1016/j.apal.2012.05.006},

	timestamp = {Sat, 20 Apr 2013 19:07:47 +0200},

	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/apal/KahleO13},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{Buss:95:wfm-arith,

	title={The witness function method and provably recursive functions of Peano arithmetic},

	author={Buss, Samuel R},

	journal={Studies in Logic and the Foundations of Mathematics},

	volume={134},

	pages={29--68},

	year={1995},

	publisher={Elsevier}

}

	@article{troelstra1998realizability,

		title={Realizability},

		author={Troelstra, Anne Sjerp},

		journal={Handbook of Proof Theory},

		year={1998},

		publisher={North-Holland/Elsevier}

	}

	@article{avigad1998godel,

		title={G{\"o}del’s functional (“{D}ialectica”) interpretation},

		author={Avigad, Jeremy},

		journal={Handbook of Proof Theory},

		volume={137},

		year={1998}

	}

(perhaps compare with Cobham's using limited recursion)

\anupam{copied below from last year's paper}

We recall the Bellantoni-Cook  algebra BC of functions defined by \emph{safe} (or \emph{predicative}) recursion on notation \cite{BellantoniCook92}. These will be employed for proving both the completeness   (all polynomial time functions are provably convergent) and the soundness result (all provably total functions are polynomial time) of THEORY. We consider function symbols $f$ over the domain  $\Word$ with sorted arguments $(\vec u ; \vec x)$, where the inputs $\vec u$ are called \textit{normal} and $\vec x$ are called \textit{safe}. 

%Each symbol is given with an arity $m$ and a number $n\leq m$ of normal arguments, and will be denoted as $f(\vec{u};\vec{x})$ where $\vec{u}$ (resp. $\vec{x}$) are the normal (resp. safe) arguments.

%We say that an expression is well-sorted if the arities of function symbols in it is respected.

%\patrick{Note that below I used the terminology 'BC programs', to distinguish them from 'functions' in the extensional sense, which I find clearer. But if you prefer to keep 'BC functions' it is all right for me.}

\begin{definition}

	[BC programs]

	BC is the set of functions generated as follows:

	%	\paragraph{Initial functions}

	%	The initial functions are:

	\begin{enumerate}

		\item The constant functions $\epsilon^k$ which takes $k$ arguments and outputs $\epsilon \in \Word$.

		\item The projection functions $\pi^{m,n}_k ( x_1 , \dots , x_m ; x_{m+1} , \dots, x_{m+n} )  := x_k$ for $n,m \in \Word$ and $1 \leq k \leq m+n$.

		\item The successor functions $\succ_i ( ; x) := xi$ for $i = 0,1$.

		\item The predecessor function $\pred (; x) := \begin{cases}

		\epsilon &  \mbox{ if }  x = \epsilon \\

		x' &  \mbox{ if }  x = x'i

		\end{cases}$.

		\item The conditional function 

		\[

		%\begin{array}{rcl}

		%C (; \epsilon, y_\epsilon , y_0, y_1  ) & = & y_\epsilon \\

		%C(; x0 , y_\epsilon , y_0, y_1) & = & y_0 \\

		%C(; x1 , y_\epsilon , y_0, y_1) & = & y_1 

		%\end{array}

		C (; \epsilon, y_\epsilon , y_0, y_1  ) := y_\epsilon 

		\quad

		C(; x0 , y_\epsilon , y_0, y_1) := y_0 

		\quad

		C(; x1 , y_\epsilon , y_0, y_1) := y_1 

		\]

		%		$\cond (;x,y,z) := \begin{cases}

		%		y & \mbox{ if } x=x' 0 \\

		%		z & \text{otherwise}

		%		\end{cases}$.

	\end{enumerate}

	%	One considers the following closure schemes:

	\begin{enumerate}

		\setcounter{enumi}{5}

		\item Predicative recursion on notation (PRN). If $g, h_0, h_1 $ are in BC then so is $f$ defined by,

		\[

		\begin{array}{rcl}

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

		f (\succ_i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )

		\end{array}

		\]

		for $i = 0,1$,  so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).

		\item Safe composition. If $g, \vec h, \vec h'$ are in BC then so is $f$ defined by,

		\[

		f (\vec u ; \vec x) \quad := \quad g ( \vec h(\vec u ; ) ; \vec h' (\vec u ; \vec x) )

		\]

		so long as the expression is well-formed.

	\end{enumerate}

\end{definition}

%Note that the  programs of this class can be defined by equational specifications in a natural way, and in the following we will thus silently identify a BC program with the corresponding equational specification.

We will implicitly identify a BC function with the equational specification it induces.

The main property of BC programs is:

\begin{theorem}[\cite{BellantoniCook92}]

	The class of functions representable by BC programs is $\fptime$.

\end{theorem}	

Actually this property remains true if one replaces the PRN scheme by the following more general simultaneous PRN scheme \cite{BellantoniThesis}:

$(f^j)_{1\leq j\leq n}$ are defined by simultaneous PRN scheme  from $(g^j)_{1\leq j\leq n}$, $(h^j_0, h^j_1)_{1\leq j\leq n}$ if for $1\leq j\leq n$ we have:

\[

\begin{array}{rcl}

f^j(0, \vec v ; \vec x) & := & g^j(\vec v ; \vec x) \\

f^j(\succ_i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )

\end{array}

\]

for $i = 0,1$,  so long as the expressions are well-formed.

%\anupam{simultaneous recursion?}

%\anupam{also identity, hereditarily safe, expressions, etc.}

%\anupam{we implicitly associate a BC program with its equational specification} 

Consider a well-formed expression $t$ built from function symbols and variables. We say that a variable $y$ occurs \textit{hereditarily safe} in $t$ if, for every subexpression $f(\vec{r}; \vec{s})$ of $t$, the terms in $\vec{r}$ do not contain $y$.

For instance $y$ occurs hereditarily safe in $f(u;y,g(v;y))$, but not in $f(g(v;y);x)$.

\begin{proposition}

	[Properties of BC programs]

	\label{prop:bc-properties}

	We have the following properties:

	\begin{enumerate}

		\item The identity function is in BC.

		\item Let $t$ be a well-formed expression built from BC functions and variables, denote its free variables as $\{u_1,\dots, u_n,x_1,\dots, x_k\}$, and assume for each $1\leq i\leq k$, $x_i$ is hereditarily safe in $t$. Then the function $f(u_1,\dots, u_n; x_1,\dots, x_k):=t$ is in BC.

		\item If $f$ is a BC function, then the function $g(\vec{u},v;\vec{x})$ defined as $f(\vec{u};v,\vec{x})$

		is also a BC program.

	\end{enumerate}

	%\begin{proposition}

	%[Properties of BC programs]

	%\label{prop:bc-properties}

	%We have the following properties:

	%\begin{enumerate}

	%\item Hereditarily safe expressions over BC programs are BC definable.

	%\item Can pass safe input to normal input.

	%\end{enumerate}

\end{proposition}

\nb{TODO: extend with $\mu$s.}

\usepackage[dvipsnames]{xcolor}

PVBC+FCA+ safe induction characterises PHcd

\begin{definition}

[Axioms]

The \emph{functional comprehension} schema is the following:

\[

\exists f . \forall \vec u; \vec x . ( \exists y^\safe . A(\vec u ; \vec x , y) \ciff A(\vec u ; \vec x , f(\vec u ; \vec x) )

\]

(can parametrise by which $A$ permitted)

The \emph{recursion} schema is:

\[

\forall g , h_0 , h_1 . \exists f . \forall u , \vec u ; \vec x .

\left(

\begin{array}{rl}

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

\cand & f(\succ 0 u , \vec u ; \vec x) = h_0 (u , \vec u ; \vec x , f(u , \vec u ; \vec x)) \\

\cand & f(\succ 1 u , \vec u ; \vec x) = h_1 (u , \vec u ; \vec x , f(u , \vec u ; \vec x)) 

\end{array}

\right)

\]

(should be well typed. Cannot avoid due to sequentiality problem.)

\end{definition}

\anupam{Original PV has explicit recursion symbols. Also, Krajicek's PVi has explicit symbols for the characteristic functions of each $\Sigma^b_i$ predicate.}

\subsection{Soundness}

We show that provably total functions of $\pvbci i$ are in $\fphi i$.

The following is our main result:

\begin{theorem}

	If $\pvbci i \proves \forall \vec u^\normal , \vec x^\sigma . \exists \vec y^\sigma. A(\vec u , \vec x , \vec y)$, then there are $\mubci i $ programs $\vec f (\vec u ; \vec x)$ such that $\pvbci i \proves\forall \vec u^\normal , \vec x^\sigma . A(\vec u , \vec x , \vec f (\vec u ; \vec x) )  $.

\end{theorem}

\begin{definition}

	[Witness predicate]

	The \emph{witness predicate} is a $\mubci{}$ program $\wit{\vec a}{A}$, parametrised by variables $\vec a$ and a formula $A$ whose free variables are amongst $\vec a$, defined as follows.

	If $A$ is a $\Pi_{i}$ formula then:

	\[

	\begin{array}{rcl}

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

	\smallskip

	\wit{\vec u; \vec x}{s\neq t} (\vec u ; \vec x, w) & \dfn & \neg (;=(;s,t)) \\

	\smallskip

	\wit{\vec u ; \vec x}{A\cor B} (\vec u ; \vec x , w) & \dfn & \cor (; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\

	\smallskip

	\wit{\vec u ; \vec x}{A\cand B} (\vec u ; \vec x , w) & \dfn & \cand(; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\

	\smallskip

	\wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ;\vec x,  w) & \dfn & \begin{cases}

	1 & \exists x^\safe . \wit{\vec u; \vec x, x }{A(x)} (\vec u ;\vec x , x, w) = 1 \\

	0 & \text{otherwise} 

	\end{cases} \\

	\smallskip

	\wit{\vec u; \vec x}{\forall x^\safe . A(x)} (\vec u ;\vec x , w) & \dfn & 

	\begin{cases}

	0 & \exists x^\sigma. \wit{\vec u ; \vec x , x}{ A(x)} (\vec u; \vec x , x) = 0 \\

	1 & \text{otherwise}

	\end{cases}

	\end{array}

	\]

	We now define $\Wit{\vec a}{A}$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec a$.

	\[

	\begin{array}{rcl}

	\Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , w) & \dfn & \wit{\vec u ; \vec x}{A} (\vec u ; \vec x)  \text{ if $A$ is $\Pi_i$} \\

	\smallskip

	\Wit{\vec u ; \vec x}{A \cor B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B)  )  \\

	\smallskip

	\Wit{\vec u ; \vec x}{A \cand B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B)  )  \\

	\smallskip

	\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( \vec u ; \vec x , w , \vec w )

	\end{array}

	\]

\end{definition}

\nb{use (de)pairing to make sure only $i$ $\mu$s are used to express a $\Pi_i$ predicate.}

\begin{proposition}

	For $\Sigma_{i+1}$ formulae $A$, $\Wit{\vec u ; \vec x}{A}$ is a $\mubci{i} $ program.

\end{proposition}

\nb{In fact, need that $\wit{}{}$ is $\mubci{i}$ and $\Wit{}{}$ and the witness functions $\vec f$ are $\bc (\wit{}{})$}

Before proving the main theorem, we will need the following `witnessing lemma':

\begin{lemma}

	If $\pvbci{i+1} $ proves a $\Sigma^\safe_{i+1}$-sequent $\Gamma \seqar \Delta$ with free variables $\vec u^\normal , \vec x^\safe$ then there are $\mubci {i}$ functions $\vec f$ such that 

	\[

	\pvbci {i+1} \proves \Wit{\vec u , \vec x}{\bigwedge \Gamma} (\vec u ; \vec x , \vec w) \cimp \Wit{\vec u  , \vec x}{\bigvee \Delta } (\vec u ; \vec x, \vec f (\vec u ; \vec x , \vec w) )

	\]

	(we simply write $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w)$, instead of $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w) =1 $.

\end{lemma}

\begin{proof}

	By induction on the size of a $\pvbci{i+1} $ proof. 

	Interesting steps below:

	\begin{itemize}

		\item $\neg$-right. (Can assume only applies to atomic formulae, and so no effect.)

		\item $\exists$-right.

		\[

		\dfrac{\Gamma \seqar \Delta , A(t^\safe )}{ \Gamma \seqar \Delta, \exists x^\safe . A(x) }

		\]

		By the inductive hypothesis, have functions $\vec f(\vec u ; \vec x), \vec g (\vec u ; \vec x)$ such that,

		\[

		\pvbci{i+1} \proves 

		\Wit{\vec u ; \vec x}{\bigwedge \Gamma } (\vec u ; \vec x , \vec w)

		\cimp

		\left(

		\Wit{\vec u ; \vec x}{\bigvee \Delta} (\vec u ; \vec x , \vec f (\vec u ; \vec x , \vec w) )

		\cor

		\Wit{\vec u ; \vec x}{A(t)} (\vec u ; \vec x , \vec g (\vec u ; \vec x , \vec w))

		\right)

		\]

		(just use $t$ as one of the witness functions)

		\item $\forall$-right. (Must be a $\Pi_i$ formula, so forget witness and compute $\wit{}{}$)

		\item Contraction-right:

		\[

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

		\]

		By infuctive hypothesis have functions $\vec f, \vec g^1 , \vec g^2$ such that:

		\[

		todo

		\]

		(just use conditional with a call to $\Wit{}{}$)

		\item induction

		\[

		\dfrac{\{\Gamma , A(a) \seqar A(s_i a) , \Delta\}_{i=0,1} }{\Gamma, A(0) \seqar A(t) , \Delta}

		\]

	\end{itemize}

\end{proof}

\subsection{Completeness}

Here we show that every $\mubci{i}$ function is definable in $\pvbci {i+1}$.

\nb{WoP known as `minimization' principles in bounded arithmetic}

\begin{theorem}

	[Well ordering property]

	\[

	\pvbci{i+1} \proves \exists x^\safe . A(x) \cimp \exists  x^\safe . (A(x) \cand \forall y^\safe . (A(y) \cimp x \leq y ) )

	\]

\end{theorem}

\begin{proof}

	We work in $\pvbci{i+1}$ and show the contrapositive. 

	Suppose:

	\begin{equation}

	\label{eqn:no-least}

	\forall x^\safe. (A(x) \cimp \exists y^\safe . A(y) \cand y<x )

	\end{equation}

	We show that,

	\begin{equation}

	\label{eqn:ih-wop}

	\forall x. \forall y \leq a - x. (\cnot A(y) \cimp \cnot A(y + x))

	\end{equation}

	by polynomial induction on $x$.

	Let $B(x)$ be such that \eqref{eqn:ih-wop} is $\forall x . B(x)$.

	\nb{If $A \in \Sigma^\safe_i \cup \Pi^\safe_i$ then $B \in \Pi^\safe_{i+1}$.}

	When $x=0$, notice that \eqref{eqn:ih-wop} is just a generalised identity.

	Suppose that $B(x)$ and let us show that $B(2x)$.

	Let $y \leq a - 2x$ such that $\cnot A(y)$. 

	Then $y\leq a-x$ so by $B(x)$ we have that $\cnot A(y+x)$.

	We also have that $y+x \leq a-x$ so by $B(x)$ we have that $\cnot A(y+2x)$, as required.

	Now suppose that $B(x)$ and let us show that $B(2x+1)$.

	Let $y \leq a - 2x - 1$ such that $\cnot A(y)$.

	By similar reasoning to the $2x$ case, we have that $\cnot A(y + 2x )$.

\end{proof}

\subsection{What we want for WoP}

From bounded arithmetic:

$\Sigma_{i+1}$-LMIN $ \iff$ $\Sigma_{i+1}$-PIND $\implies$ $\Sigma_i$-IND $\iff$ $\Sigma_i$-MIN $ \iff$ $\Pi_{i+1}$-MIN.

\subsection{Completeness proof idea}

For each $\mubci i$ function $f(\vec u ; \vec x)$ we $\Sigma_i$-define a formula $A_f (\vec u ; \vec x  , y )$ in $\pvbci{i+1}$ such that:

\[

\proves A_f (\vec u ; \vec x , y)

\quad 

\iff

\quad

f(\vec u ; \vec x) = y

\]

and $A_f$ is provably total in $\pvbci{i+1}$.

For the $\mu$ case, say we have the function:

\[

\mu x^{+1} . f(\vec u ; \vec x , x) =_2 0

\]

Let $A_f (\vec u ; \vec x , y)$ be given by the inductive hypothesis.

We define $A(\vec u ; \vec x , z)$ as:

\[

\begin{array}{rl}

&\left(

z=0 \  \cand \ \forall x^\safe , y^\safe . (A_f (\vec u ; \vec x , x, y) \cimp y=_2 1)

\right) \\

\cor & \left(

\begin{array}{ll}

z\neq 0 

& \cand\   \forall y^\safe . (A_f (\vec u ; \vec x , z , y) \cimp y=_2 0 ) \\

& \cand\ \forall x^\safe < p(;z) . (\forall y^\safe . A_f (\vec u ; \vec x , x , y) \cimp y=_2 1) 

\end{array}

\right)

\end{array}

\]

Notice that $A$ is $\Pi_k$, since $A_f$ is $\Sigma_k$.

What about, say recursion on a formula? Need a form of `ranked comprehension'?

E.g., when $A$ is $\Sigma_k$ then we can introduce a rank $k$ symbol (a sort?) such that:

\[

\forall \vec u^\normal, \vec x^\safe . \exists ! y^\safe . A(\vec u ; \vec x , y)

\implies

\exists f^\safe_r . \forall \vec u^\normal,\vec x^\safe, y^\safe . (A(\vec u ; \vec x, y) \ciff f^\safe_r (\vec u ; \vec x) = y )

\]

Otherwise, can we use definability of computations? E.g., if:

\[

\begin{array}{rcl}

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

f(s_i u , \vec u ; \vec x) & \dfn & h_i (u , \vec u ; \vec x , f(u,\vec u ; \vec x))

\end{array}

\]

Suppose we have $A_g (\vec u ; \vec x,y)$ and $A_i (u , \vec u ; \vec x , y , z)$ defining $g$ and $h_i$ respectively.

We define $A_f (u ,\vec u ; \vec x , y)$ as:

\[

\exists z^\safe . \left(

\begin{array}{ll}

& Seq(z) \cand \exists y_0 . ( A_g (\vec u ; \vec x , y_0) \cand \beta_0 (z , y_0) ) \cand \beta_{|u|} ( z,y ) \\

\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta_k (z, y_i) \cand \beta_{k+1} (z, y_{k+1})  \cand A_i (u , \vec u ; \vec x , y_k , y_{k+1}) )

\end{array}

\right)

\]

(Can we really assume $z$ is safe here?)

POINT: for whatever formulation, we need to prove:

\[

\exists y^\safe . A_f (a , \vec u ; \vec x , y) 

\quad \seqar \quad

\exists y^\safe . A_f (s_i a, \vec u ; \vec x , y)

\]

SHOULD HAVE: $\beta (i;x)$ for $i$th element of sequence $x$. 

Therefore need 'sharply bounded' quantification for normal variables?

In fact, why not $\beta(;i,x) $? Should be fine. So only safe quantification is needed for PH, but lose level-by-level delineation.

GOALS:

\begin{enumerate}

	\item PVBC + FCA + $\safe$-IND characterises PH. (Recursion included in PVBC)

	\item Refinement of above with `ranks' to delineate levels (definitions of $\pvbci{i}$).

	\item Arithmetic including both safe and sharply bounded normal quantification. (for sequences)

	\item (if time) allow both bounded and safe quantifiers?

\end{enumerate}

FCA:

\[

\exists f^\safe . \forall \vec u ; \vec x .

\left(

\exists y^\safe . A(\vec u ; \vec x , y) \ciff A(\vec u ; \vec x , f^\safe(\vec u ; \vec x))

\right)

\]

(with typing information)

This could be enough with open induction if we introduce ranks later? Yup, seems like a good idea. Can then make into a real `open' theory.