On Light Logics, Uniform Encodings and
Ugo Dal Lago, Mura Anteo Zamboni, Patrick Baillot · 2006
Light Affine Logic is a variant of Linear Logic with a polynomial cut-elimination procedure. We study the extensional expressive power of Light Affine Logic with respect to a general notion of encoding of functions, in the setting of the Curry-Howard correspondence. We consider Light Affine Logic with both fixpoints of formulae and second-order quantifiers and analyze the properties of polytime soundness and polytime completeness for various fragments of this system. We show in particular that the implicative propositional fragment is not polytime complete, if we add some reasonable conditions on the encodings. Following previous work, we show that second order leads to polytime unsoundness. We then introduce simple constraints on second order quantification and fixpoints, proving the obtained fragments to be polytime sound and complete.