Journal of Functional Programming



Functional pearls

FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness


HARRY G. MAIRSON a1
a1 Computer Science Department, Volen Center for Complex Numbers, Brandeis University, Waltham, MA 02254, UA (email: mairson@cs.brandeis.edu)

Article author query
mairson hg   [Google Scholar] 
 

Abstract

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.