Mairson showed that the problem of computing the $\beta$-normal form of a linear lambda term (or equivalently, computing its principal type) is complete for polynomial time.

In particular, he showed PTIME-hardness by reduction from the circuit value problem.

My question is about the restriction of the decision problem to linear lambda terms which are planar in the sense that they can be typed without using the exchange law (e.g., $B = \lambda x.\lambda y.\lambda z.x(yz)$ is planar, but $C = \lambda x.\lambda y.\lambda z.(xz)y$ is not). Is this an open problem? I would suspect that it has lower computational complexity, since Mairson's encoding of boolean circuits uses non-planarity in an essential way to distinguish "True" from "False".

I'm specifically interested in $\beta$-equality of planar lambda terms, but the problem is related to deciding equality of proofnets for non-commutative multiplicative linear logic, so I'd also be interested in any results in that direction.


1 Answer 1


If this proof sketch turns out to be correct, then β-equality of planar λ-terms is still P-complete. (Joint work by Anupam Das, Damiano Mazza, Noam Zeilberger and me; it's not yet peer-reviewed, and one of our previous proof attempts was flawed, so I don't want to say I'm 100% sure yet…)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.