$\newcommand\iddots{⋰}$In "A simple proof of a theorem of Statman" (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda calculus is not elementary recursive, i.e., cannot be done in time $O(2^{\iddots^{2^n}})$ for any finite tower of exponentials. It's a nice proof, that works by showing how to encode arbitrary formulas of what Mairson calls "higher-order type theory" as simply typed terms, such that a formula is valid iff the corresponding term evaluates to the Church boolean $true = \lambda x.\lambda y.x$. The phrase "higher-order type theory" sounds ambiguous to me, so for the purpose of this post I will just call these higher-order quantified boolean formulas (HOQBF) — please let me know if there is a more standard terminology.
HOQBF can be seen as a generalization of QBF, where quantifiers can range not just over the set of booleans $\mathbb{B} = \{ \mathbf{true}, \mathbf{false} \}$, but over sets of booleans $P(\mathbb{B})$, sets of sets of booleans $P(P(\mathbb{B}))$, and so on. In other words, the language of formulas is $$ F ::= \forall x^k.F \mid \exists x^k.F \mid F\wedge F \mid F \vee F \mid \neg F \mid x^k \in y^{k+1} $$ where the $k$ are natural numbers, and where variables $x^k$ are interpreted as ranging over $P^k(\mathbb{B})$. (Again, is there a standard name for such formulas?)
Mairson cites
- A. R. Meyer. The inherent computational complexity of theories of ordered sets. Proceedings of the International Congress of Mathematicians, 1974.
for the result that deciding formulas of HOQBF requires nonelementary time. I checked that paper, and unless I'm overlooking something it doesn't contain a direct proof of this result. I'm not 100% sure it contains a statement of it either...what looks most relevant is the theorem on page 4, which cites a list of results that various decision problems are nonelementary, including "7. The theory of pure finite types [M. Fischer and Meyer, FM75]". Naturally, the bibliography includes the line
[FM75] Fischer, M.J. and A.R. Meyer, (1975), in preparation.
and I can't find much evidence that such a paper ever surfaced.
I do believe the claim that deciding HOQBF requires nonelementary time, and moreover Mairson's paper also gives a separate encoding of Turing machines in simply typed lambda calculus, which computes the result of running the machine for any tower of exponential steps — so I suppose it might be possible to complete the circle and try to reduce the problem of deciding $\beta\eta$-equality of simply typed lambda terms back to HOQBF. Still, it would be nice to know if there is a classical reference for this result.
Question: Is there a reference for the result that deciding HOQBF requires nonelementary time? (Side question: Is there a standard name for HOQBF?)
Update (June 17): So I finally went ahead and looked at Statman's original paper, and it seems that Mairson got his citation from there! Statman begins by defining these formulas, which he calls "$\Omega$-sentences", then states the result that deciding whether they are true is non-elementary. This is listed as "Proposition 1 (Fischer and Meyer, Statman)", stated without proof, but with a citation to the Meyer survey paper (conference version) and the specific item "7" of the theorem I had in mind (which cites the [FM75] paper I have been unable to locate). Since Meyer is actually listed as the handling editor for Statman's paper, I'm beginning to suspect that there may not exist a more canonical reference for this...
