View Related Documents

Abstract

This paper relates two distinct traditions: the one of complexity classes characterisations through light logics and models of nondeterminism. Light logics provide an implicit characterisation of P-Time algorithms through the Curry-Howard isomorphism: every derivation reduces to its normal form in polynomial time and every polynomial Turing machine can be simulated by a derivation. In this paper, we extend Intuitionistic Light Affine Logic, a logic with full weakening, with a simple rule for nondeterminism and get a completeness result for NP-Time algorithms which is, as far as we know, the first Curry-Howard characterisation of NP complexity. We conclude by a reformulation of the P ≠ NP conjecture.

Keywords  Light logics - implicit characterisations of complexity classes - NP complexity

Fulltext Preview

Image of the first page of the fulltext document