
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.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, BC1-199, Computer Science - Programming Languages, Logic, computer science - programming languages, QA75.5-76.95, [INFO] Computer Science [cs], non-elementary complexity, Logic in Computer Science (cs.LO), computer science - logic in computer science, safe λ-calculus, Electronic computers. Computer science, Programming Languages (cs.PL)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, BC1-199, Computer Science - Programming Languages, Logic, computer science - programming languages, QA75.5-76.95, [INFO] Computer Science [cs], non-elementary complexity, Logic in Computer Science (cs.LO), computer science - logic in computer science, safe λ-calculus, Electronic computers. Computer science, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
