11
$\begingroup$

$\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...

$\endgroup$
9
  • 1
    $\begingroup$ Have you asked Harry? $\endgroup$ Jun 3, 2016 at 10:51
  • 1
    $\begingroup$ @Kaveh As I said, I believe the claim, but I'm interested in original references -- even a paper that just goes through the work of setting up the decision problem for HOQBF (and giving it a name!). $\endgroup$ Jun 3, 2016 at 14:08
  • 1
    $\begingroup$ ...and actually, a modern textbook account would be great as well. $\endgroup$ Jun 3, 2016 at 14:11
  • 1
    $\begingroup$ @NeelKrishnaswami Got a quick response! Alas, though, he does not have any more information about the source. $\endgroup$ Jun 3, 2016 at 19:08
  • 1
    $\begingroup$ HO seems to be related to what I'm asking about, but not quite the same thing. [HT06] is a result in descriptive complexity theory: they show that the class of languages which can be expressed by (i.e., represented as the collection of finite models of) formulas in higher-order logic is precisely the class ELEMENTARY. My question is about something different -- the complexity of the decision procedure for higher-order quantified boolean formulas -- although it's quite possibly related. $\endgroup$ Jun 7, 2016 at 19:12

1 Answer 1

3
$\begingroup$

One can be more precise than "non-elementary" and say that HOQBF is TOWER-complete — morally, TOWER is the complexity class just beyond elementary. This fact is explicitly stated and proved in the MFCS'22 paper Higher-Order Quantified Boolean Satisfiability by Chistikov, Haase, Hadizadeh & Mansutti.

In fact, while TOWER-completeness is a semi-recent notion, introduced by Schmitz less than a decade ago, older proofs of non-elementary lower bounds for various problems tend to be implicitly readable as actually proving TOWER-hardness. Chistikov et al. make some historical remarks that converge with yours (I've taken the liberty of expanding the numerical references e.g. [30] into more informative ones):

Statman […] shows that checking whether two λ-terms of the calculus reduce to the same normal form is non-elementary recursive (in fact, it shows that the problem is TOWER-complete).

[…]

According to [The typed λ-calculus is not elementary recursive, Statman 1979], TOWER-completeness of the satisfiability problem of Ω was announced by Meyer in [The inherent computational complexity of theories of ordered sets, Theorem 1(7)] as part of a forthcoming paper coauthored with Fischer. To the best of our knowledge, the latter paper was never published. To resolve this issue, in [A simple proof of a theorem of Statman] Mairson gives a revision of [Statman 1979] that provides a standalone proof of the TOWER-hardness of Ω and a simplification to the aforementioned Church encoding.

$\endgroup$
1
  • $\begingroup$ great to see that there is finally a good reference for this result, just under 50 years later! $\endgroup$ Nov 5, 2022 at 2:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.