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.
- Harry Mairson. Linear lambda calculus and PTIME-completeness. JFP 14(6), 2004.
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.