9
$\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$
  • 1
    $\begingroup$ Have you asked Harry? $\endgroup$ – Neel Krishnaswami Jun 3 '16 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$ – Noam Zeilberger Jun 3 '16 at 14:08
  • 1
    $\begingroup$ ...and actually, a modern textbook account would be great as well. $\endgroup$ – Noam Zeilberger Jun 3 '16 at 14:11
  • 1
    $\begingroup$ @NeelKrishnaswami Got a quick response! Alas, though, he does not have any more information about the source. $\endgroup$ – Noam Zeilberger Jun 3 '16 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$ – Noam Zeilberger Jun 7 '16 at 19:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.