<p>If <a href="http://arxiv.org/abs/2404.05276" rel="nofollow noreferrer">this proof sketch</a> 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…)</p>

CC BY-SA 4.0
2024-04-09T08:07:53.753Z
2024-04-09T08:07:53.753Z
Lê Thành Dũng 'Tito' Nguyễn
<p>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.</p>

<ul>
<li>Harry Mairson. <a href="http://www.cs.brandeis.edu/~mairson/Papers/jfp02.pdf" rel="noreferrer">Linear lambda calculus and PTIME-completeness</a>. JFP 14(6), 2004.</li>
</ul>

<p>In particular, he showed PTIME-hardness by reduction from the <a href="https://en.wikipedia.org/wiki/Circuit_Value_Problem" rel="noreferrer">circuit value problem</a>.</p>

<p>My question is about the restriction of the decision problem to linear lambda terms which are <em>planar</em> 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".</p>

<p>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.</p>

<cc.complexity-theory><lambda-calculus><linear-logic>
deciding $\beta$-equality of planar lambda terms
Noam Zeilberger
# deciding $\beta$-equality of planar lambda terms

(Asked by: username_0 on 2017-06-28)

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](http://www.cs.brandeis.edu/~mairson/Papers/jfp02.pdf). JFP 14(6), 2004.

In particular, he showed PTIME-hardness by reduction from the [circuit value problem](https://en.wikipedia.org/wiki/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.

**Tags:** cc.complexity-theory, lambda-calculus, linear-logic

---

## 1 answers

### Answer by username_1 on 2024-04-09. Score: 2

If [this proof sketch](http://arxiv.org/abs/2404.05276) 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…)


---

