Church => Scott = Ptime: an application of resource sensitive realizability

Aloïs Brunel
(ENS Lyon)
Kazushige Terui
(RIMS, Kyoto University)

We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.' We give a characterization of polynomial time functions, which is derived from (Leivant and Marion 93): a function is computable in polynomial time if and only if it can be represented by a term of type Church => Scott.

To prove soundness, we employ a resource sensitive realizability technique developed by Hofmann and Dal Lago.

In Patrick Baillot: Proceedings International Workshop on Developments in Implicit Computational complExity (DICE 2010), Paphos, Cyprus, 27-28th March 2010, Electronic Proceedings in Theoretical Computer Science 23, pp. 31–46.
Published: 5th May 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.23.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org