Révision 226 CSL17/intro.tex

intro.tex (revision 226)
6 6 
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}.
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
  
  
    
A perhaps more important 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 representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantiiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. 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} .


  		





  
  9
  
    
But a perhaps more important 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 representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantiiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. 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,Leivant95}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02},  \cite{Leivant94:intrinsic-theories} \cite{BelHof:02},  \cite{Marion01}, \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 field, and one of its advantages is its great versatility, allowing a characterization of a wide range of complexity classes, such as $\ptime$, the polynomial hierarchy $\ph$, $\pspace$, $\mathbf{NC}^i$ etc. 


  		





  13
  13
  
    
 %It is also closely related to \textit{proof complexity}, 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 aims to relate certain computing disciplines which with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}). 


  		





  16
  
  
    
  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} etc.).  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 $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{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 aims to relate certain computing disciplines with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}). 


  		





  
  16
  
    
  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 (e.g. \cite{Hofmann00,Hofmann03}, \cite{Marion11}).  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 $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{Actually some characterizations of such classes do exist, but they either take the form of a function algebra \cite{bellantoni1995fph} or of a type system extended with a non-logical feature \cite{GaboardiMarionRonchi12}.} 


  		





  17
  17
  
    
  


  		





  18
  18
  
    
 Systems in implicit complexity typically imposes constraints on the comprehension scheme, the primitive recursion scheme or the structural rules of proof systems (namely \emph{contraction}). 


  		





  19
  19
  
    
% 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.


  		












Formats disponibles :
  Unified diff