Non-uniform polytime computation in the infinitary affine lambda-calculus

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We give an implicit, functional characterization of the class of non-uniform polynomial time languages, based on an infinitary affine lambda-calculus and on previously defined bounded-complexity subsystems of linear (or affine) logic. The fact that the characterization is implicit means that the complexity is guaranteed by structural properties of programs rather than explicit resource bounds. As a corollary, we obtain a proof of the (already known) P-completeness of the normalization problem for the affine lambda-calculus which mimics in an interesting way Ladner's P-completeness proof of CIRCUIT VALUE (essentially, the argument giving the Cook-Levin theorem). This suggests that the relationship between affine and usual lambda-calculus is deeply similar to that between Boolean circuits and Turing machines.

Original languageEnglish
Title of host publicationAutomata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Proceedings
PublisherSpringer Verlag
Pages305-317
Number of pages13
EditionPART 2
ISBN (Print)9783662439500
DOIs
Publication statusPublished - 1 Jan 2014
Externally publishedYes
Event41st International Colloquium on Automata, Languages, and Programming, ICALP 2014 - Copenhagen, Denmark
Duration: 8 Jul 201411 Jul 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
NumberPART 2
Volume8573 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference41st International Colloquium on Automata, Languages, and Programming, ICALP 2014
Country/TerritoryDenmark
CityCopenhagen
Period8/07/1411/07/14

Fingerprint

Dive into the research topics of 'Non-uniform polytime computation in the infinitary affine lambda-calculus'. Together they form a unique fingerprint.

Cite this