Révision 252

CSL17/intro.tex (revision 252)
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}. 


  		












  

    
      CSL17/preliminaries.tex	(revision 252)
    
  






  142
  142
  
    

  		





  143
  143
  
    
%\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }


  		





  144
  144
  
    

  		





  
  145
  
    
We denote $|x|=\ulcorner \log(x+1) \urcorner.$


  		





  145
  146
  
    
\begin{example}


  		





  146
  147
  
    
	[Some simple functions]


  		





  147
  148
  
    
	\label{ex:simple-bc-fns}


  		





  ......




  153
  154
  
    
	%\item $\bit(l;x)$ returns the $\mode l$th bit of $x$.


  		





  154
  155
  
    
	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1101)=0$.


  		





  155
  156
  
    
	


  		





  156
  
  
    
	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|+1$ prefix of $x$, as follows:


  		





  
  157
  
    
	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:


  		





  157
  158
  
    
	\begin{eqnarray*}


  		





  158
  159
  
    
	\shorten(0;x) &=&x\\


  		





  159
  
  
    
	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x))


  		





  
  160
  
    
	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x)) \mbox{ if $l\neq 0$.}


  		





  160
  161
  
    
	\end{eqnarray*}


  		





  161
  162
  
    
	Then we define $\bit(l;x)$  as follows:


  		





  162
  163
  
    
	$$\bit(l;x)=C(;\shorten(l;x),0,1).$$ 


  		












Formats disponibles :
  Unified diff