Révision 209 CSL17/intro.tex
| intro.tex (revision 209) | ||
|---|---|---|
| 7 | 7 |
|
| 8 | 8 |
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.
|
| 9 | 9 |
But a more important (and somewhat orthogonal) distinction is whether the constraints on the logic or theory are |
| 10 |
\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representant of the first category is \textit{bounded arithmetic}, which has been investigated by Buss \cite{Buss86book}, as a first-order arithmetic with bounded quantifiers. Cobham's function algebra \cite{Cobham} for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or safe recursion \cite{BellantoniCook}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02}, \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, \cite{Leivant94:found-delin-ptime} and subsystems of linear logic \cite{Girard94:lll} \cite{Lafont04} .
|
|
| 10 |
\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representant of the first category is \textit{bounded arithmetic}, which has been investigated by Buss \cite{Buss86book}, as a first-order arithmetic with bounded quantifiers. Cobham's function algebra \cite{Cobham} for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or safe recursion \cite{BellantoniCook92}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02}, \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, \cite{Leivant94:found-delin-ptime} and subsystems of linear logic \cite{Girard94:lll} \cite{Lafont04} .
|
|
| 11 | 11 |
|
| 12 | 12 |
Bounded arithmetic is a deep and well-established theory, and one of its interests is its great versatility, as it has enabled to characterize a wide range of complexity classes, such as FP, the polynomial hierarchy FPH, PSPACE, NC \dots It is also tightly related to \textit{proof complexity}
|
| 13 | 13 |
\cite{Cook:2010:LFP:1734064}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}.
|
| 14 | 14 |
|
| 15 |
Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It has the interest of delineating some specific computing disciplines which correspond to classical complexity classes and can help shed some light for instance on the foundational nature of feasibility (see e.g. \cite{Leivant94:found-delin-ptime}). Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (\cite{Hofmann99SLR,Hofmann00}, \cite{Marion11} \dots). However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as NP or PH, in a purely logical way. Actually some characterizations of such classes do exist, but they either take the form of a function algebra or of a type system extended with a non-logical feature.
|
|
| 15 |
Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It has the interest of delineating some specific computing disciplines which correspond to classical complexity classes and can help shed some light for instance on the foundational nature of feasibility (see e.g. \cite{Leivant94:found-delin-ptime}). Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (\cite{Hofmann00,Hofmann03}, \cite{Marion11} \dots). However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as NP or PH, in a purely logical way. Actually some characterizations of such classes do exist, but they either take the form of a function algebra or of a type system extended with a non-logical feature.
|
|
| 16 | 16 |
|
| 17 | 17 |
In fact implicit complexity has obtained many of its techniques from a detailed study of the comprehension scheme, of the primitive recursion scheme and of the structural rules of proof systems (contraction rule). But it seems to us that first-order quantification has not yet been investigated as much as it deserves. We believe that this is one reason of the modest achievements of implicit complexity concerning non-deterministic classes. |
| 18 | 18 |
|
| 19 | 19 |
So in the present work we aim at exploring the power of first-order quantification in an implicit complexity arithmetic, and in particular we wish to characterize the polynomial hierarchy FPH and its levels. By implicit complexity arithmetic we mean that the quantifiers employed should not be bounded quantifiers. Our motivation is to bridge the fields of bounded arithmetic and implicit complexity, and to try pave the way for the design of systems bringing together simplicity (no explicit bounds) and versatility, in which one could transfer some of the main results of bounded arithmetic. |
| 20 | 20 |
|
| 21 |
Our methodology will be the following one: we will use the concept of \textit{ramification} coming from implicit complexity \cite{Leivant93,BellantoniCook92}, adapt it in the setting of first-order arithmetic, and then explore some properties relative to quantification. First recall that ramification, or safe recursion, is a discipline which aims at limiting the power of recursion by distinguishing two (or more) levels of integers: the \textit{safe} or level-0 integers, and the \textit{normal} or level-1 ones. In a nutshell, recursion, which is here recursion on notation (or binary words), is permitted on normal arguments, but recursive calls can only appear in safe positions. Basic operations, such as conditional, can be performed on safe arguments. Functions defined in this way correspond to polynomial time functions \cite{BellantoniCook92}.
|
|
| 21 |
Our methodology will be the following one: we will use the concept of \textit{ramification} coming from implicit complexity \cite{Leivant95,BellantoniCook92}, adapt it in the setting of first-order arithmetic, and then explore some properties relative to quantification. First recall that ramification, or safe recursion, is a discipline which aims at limiting the power of recursion by distinguishing two (or more) levels of integers: the \textit{safe} or level-0 integers, and the \textit{normal} or level-1 ones. In a nutshell, recursion, which is here recursion on notation (or binary words), is permitted on normal arguments, but recursive calls can only appear in safe positions. Basic operations, such as conditional, can be performed on safe arguments. Functions defined in this way correspond to polynomial time functions \cite{BellantoniCook92}.
|
|
| 22 | 22 |
|
| 23 | 23 |
This discipline can be transposed in first-order arithmetic by adding predicates for normal and safe integers and by limiting the induction scheme by allowing induction only on normal integers. The key step we make is to focus our attention on \textit{safe quantifiers} that is to say quantifiers on safe variables. These safe quantifiers will play a r\^ole analogous to bounded quantifiers in bounded arithmetic. In particular we will consider a hierarchy $\Sigma_i^{\safe}$ of formulas according to the number of alternances of safe quantifiers, and we will calibrate the use of induction by restricting the class to which the induction formula can belong. We will finally characterize in this way the levels of the polynomial hierarchy.
|
| 24 | 24 |
|
| ... | ... | |
| 27 | 27 |
A first axis of classification between the logics and arithmetics for complexity classes is the way by which they specify functions. The options at stake can be enumerated as follows: (i) \textit{formula specification}, as in first-order bounded arithmetic \cite{Buss86book}, (ii) \textit{equational specification}, as in Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories}, (iii) \textit{combinatory terms} as in applicative theories (e.g. \cite{Strahm03}) or $\lambda$-calculus terms. A second axis, as explained in the introduction, is whether the system is explicit or implicit.
|
| 28 | 28 |
|
| 29 | 29 |
Our approach in this paper is to use the formula-specification point of view, because it is convenient for the polynomial hierarchy. The arithmetic of \cite{KahOit:13:ph-levels} characterizes PH, but it fits in the explicit approach as it uses axioms defining bounded schemes.
|
| 30 |
Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes. Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories} allows to characterize FP, in the equational specification approach, and \cite{Cantini02} obtains an analogous result in the combinatory terms approach. The paper \cite{BelHof:02} also provides a characterization of FP, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. The difference with our setting is that equational specifications are used instead of formulas, unary integers instead of binary integers, and the class of functions characterized is that of elementary functions.
|
|
| 30 |
Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes. Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories} allows to characterize FP, in the equational specification approach, and \cite{Cantini02} obtains an analogous result in the combinatory terms approach. The paper \cite{BelHof:02} also provides a characterization of FP, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Our paper \cite{BaillotDas16} proves a similar result, but with a different method. Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. The difference with our setting is that equational specifications are used instead of formulas, unary integers instead of binary integers, and the class of functions characterized is that of elementary functions.
|
|
| 31 | 31 |
|
| 32 | 32 |
|
| 33 | 33 |
\textbf{Outline.} The rest of the paper will proceed as follows. We first give some background on function algebras for FP and FPH respectively. Then we describe an encoding of sequences which will be instrumental in the proof of our result. We present our arithmetical system in Sect. \ref{sect:arithmetic}, prove our soundness result, that is to say the provably total functions are in FPH, in Sect. \ref{sect:soundness}, and our completeness result, all FPH functions are provably total in the arithmetic, in Sect. \ref{sect:completeness}.
|
Formats disponibles : Unified diff