Hostname: page-component-7c8c6479df-r7xzm Total loading time: 0 Render date: 2024-03-17T20:23:55.613Z Has data issue: false hasContentIssue false

FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness

Published online by Cambridge University Press:  27 October 2004

HARRY G. MAIRSON
Affiliation:
Computer Science Department, Volen Center for Complex Numbers, Brandeis University, Waltham, MA 02254, UA (email: mairson@cs.brandeis.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We give transparent proofs of the PTIME-completeness of two decision problems for terms in the λ-calculus. The first is a reproof of the theorem that type inference for the simply-typed λ-calculus is PTIME-complete. Our proof is interesting because it uses no more than the standard combinators Church knew of some 70 years ago, in which the terms are linear affine – each bound variable occurs at most once. We then derive a modification of Church's coding of Booleans that is linear, where each bound variable occurs exactly once. A consequence of this construction is that any interpreter for linear λ-calculus requires polynomial time. The logical interpretation of this consequence is that the problem of normalizing proofnets for multiplicative linear logic (MLL) is also PTIME-complete.

Type
Functional pearls
Copyright
© 2004 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.