Révision 138 CharacterizingPH/draft.tex
| draft.tex (revision 138) | ||
|---|---|---|
| 72 | 72 |
\section{Introduction and motivation}
|
| 73 | 73 |
Today, there are countless approaches towards characterising complexity classes via logic. |
| 74 | 74 |
Foremost amongst these lies the proof-theoretic approach, characterising classes as the `representable' functions of some logic or theory. |
| 75 |
Examples include bounded arithmetic \cite{Buss86book}, (Krajicek, Cook etc.), applicative theories (Feferman, Kahle, Oitavaem,) \cite{Cantini02} , intrinsic and ramified theories , \cite{Leivant94:intrinsic-theories} (Bellantoni, Hofmann etc.) \cite{BelHof:02}, fragments of linear logic \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.
|
|
| 75 |
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{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.
|
|
| 76 | 76 |
|
| 77 | 77 |
To some extent there is a distinction between various notions of `representability', namely between logics that type terms computing functions of a given complexity class, and theories that prove the totality of functions in a given complexity class. |
| 78 | 78 |
Perhaps a more important (and somewhat orthogonal) distinction for the \textsc{Dice-Fopara} community is whether the constraints on the logic or theory are \emph{implicit} or \emph{explicit}. The former includes constraints such as ramification, type level and substructural considerations, while the latter includes bounded quantification, bounded modalities (e.g. in bounded linear logic) etc. This distinction is also naturally exhibited in associated function algebras, e.g. Cobham vs. Bellantoni-Cook \cite{Cobham,BellantoniCook92}.
|
Formats disponibles : Unified diff