Révision 253 CSL17/tech-report/intro.tex

intro.tex (revision 253)
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 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 quantifiers 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 there are various systems of \textit{implicit computational complexity}, for instance function algebras based on \emph{ramification} or \emph{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 \emph{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 representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantifiers 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 there are various systems of \textit{implicit computational complexity}, for instance function algebras based on \emph{ramification} or \emph{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 \emph{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}. 


  		












Formats disponibles :
  Unified diff