Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-11-25T05:40:26.188Z Has data issue: false hasContentIssue false

On light logics, uniform encodings and polynomial time

Published online by Cambridge University Press:  07 July 2006

UGO DAL LAGO
Affiliation:
Dipartimento di Scienze dell'Informazione, Università di Bologna, Mura Anteo Zamboni 7, 40127 Bologna, Italy. Email: [email protected]
PATRICK BAILLOT
Affiliation:
Laboratoire d'Informatique de Paris-Nord (UMR 7030 CNRS), Université Paris 13, Intsitut Galilée, 99 avenue Jean-Baptiste Clément, 93430 Villetaneuse, France. Email: [email protected]

Abstract

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 analyse the properties of polytime soundness and polytime completeness for various fragments of this system. In particular, we show that the implicative propositional fragment is not polytime complete if we place 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, and prove that the fragments obtained are polytime sound and complete.

Type
Paper
Copyright
2006 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)