一句话：证明简单类型 λ-项的可转换性问题在 Blum-Ong 安全 λ-项片段上仍是 TOWER-完全。
本文研究两个简单类型 λ-项是否 β-可转换（等价于是否有相同范式）的判定问题。该问题已知是非初等的，精确复杂度为 TOWER-完全，但这一事实较少为人所知；本文也旨在普及该结果。作者的核心贡献是证明：当输入项属于 Blum 与 Ong 的安全 λ-演算——一个来自高阶递归方案研究的简单类型 λ-演算片段——时，β-可转换性仍保持 TOWER-完全。此前该安全片段问题的最好下界仅为 PSPACE-难。证明通过从 star-free 表达式等价问题进行归约，灵感来自作者与 Pradic 关于“typed λ-演算中的隐式自动机”的工作。结果同样适用于 βη-可转换性。
We consider the following decision problem: given two simply typed $\lambda$-terms, are they $\beta$-convertible? Equivalently, do they have the same normal form? It is famously non-elementary, but the precise complexity - namely TOWER-complete - is lesser known. One goal of this short paper is to popularize this fact. Our original contribution is to show that the problem stays TOWER-complete when the two input terms belong to Blum and Ong's safe $\lambda$-calculus, a fragment of the simply typed $\lambda$-calculus arising from the study of higher-order recursion schemes. Previously, the best known lower bound for this safe $\beta$-convertibility problem was PSPACE-hardness. Our proof proceeds by reduction from the star-free expression equivalence problem, taking inspiration from the author's work with Pradic on "implicit automata in typed $\lambda$-calculi". These results also hold for $\beta\eta$-convertibility.
@article{paperbot2728,
title = {Simply typed convertibility is TOWER-complete even for safe lambda-terms},
author = {Lê Thành Dũng Nguyên},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:21)2024}
}