Light Linear Logic

We are seeking a ``logic of polytime'', not yet one more axiomatization, but an intrinsically polytime system. Our methodological bias will be to consider that the expressive power of a system is the complexity of its cut-elimination procedure, and we therefore seek a system with a polytime complexity for cut-elimination (to be precise: besides the size of the proof, there will be an auxiliary parameter, the depth, controlling the degree of the polynomial). This cannot be achieved within classical or intuitionistic logics because of structural rules, especially contraction: this is why the complexity of cut-elimination in all extant logical systems (including the standard version of linear logic which controls structural rules without forbidding them) is catastrophic, elementary (towers of exponentials) or worse. Light Linear Logic (LLL) is a purely logical system with a more careful handling of structural rules: this system is strong enough to represent all polytime functions, but cut-elimination is (locally) polytime. With LLL, our control over the complexity of cut-elimination improves greatly. But this is not the only potentiality of LLL: why not transform it into a system of mathematics and try to formalize ``polytime mathematics'' in the same way as Heyting arithmetic formalizes constructive mathematics? The possibility is clearly open, since LLL admits extensions into a naive set-theory, with full comprehension, still with polytime cut-elimination. This system admits full induction on data types, which shows that, within LLL, induction is compatible with low complexity.

Authors

• Jean-Yves Girard

Keywords

No keywords are indexed for this paper.