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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.