Logic Colloquium 2008
Kazushige Terui Towards a logical foundation of computational complexity
Traditional theories of computational complexity are built on concrete machine models. As a result, the nature of explanation often tends to be procedural (eg. via transformation of machines). Aiming at a more algebraic account to complexity theoretic phenomena (eg. via logical isomorphisms), we propose a new foundation based on logic and functional computation (in the paradigm of Curry-Howard correspondence). The underlying framework is ludics of J.-Y. Girard, that is a pre-logical system upon which ordinary logics are to be built and analyzed. Due to its monistic nature, data and machines are both represented by abstract proofs, and the notion of acceptance is replaced by a fundamental notion of orthogonality. Space efficient composition of algorithms (which is usually explained by a peculiar construction of machines) is very naturally achieved by adopting a pointer-based normalization procedure (known as Krivine's abstract machine). After introducing the basic formalism, we shall illustrate how some basic complexity theoretic phenomena (eg. space compression) are explained by logical properties (eg. focalization) and logical isomorphisms.