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.