Révision 204

CSL17/intro.tex (revision 204)
14 14
15 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.
16 16
17 
  In fact implicit complexity has taken many of its techniques from a detailed study of the comprehension scheme, of recursion and of the structural rules of proof systems (contraction rule). But it seems to us that first-order quantification has not 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.
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 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 
  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.
19 20 
  \patrick{
20 21 
  \begin{itemize}
21 22 
  \item our goal: design an unbounded arithmetic for FPH.

Formats disponibles : Unified diff