On the complexity of normalization for the planar $\lambda$-calculus

Abstract

We sketch a tentative proof of P-completeness for the $\beta$-convertibility problem on untyped planar (a.k.a. ordered or non-commutative) $\lambda$-terms.

Abstract for the Trends in Linear Logic and Applications 2023 workshop, meant to be expanded into a proper paper in the future