Locally definable acceptance types for polynomial time machines

Abstract

We introduce m-valued locally definable acceptance types, a new model generalizing the idea of alternating machines and their acceptance behaviour. Roughly, a locally definable acceptance type consists of a set F of functions from {0,…, m−1}r into {0,…, m−1}, which can appear as labels in a computation tree of a nondeterministic polynomial time machine. The computation tree then uses these functions to evaluate a tree value, and accepts or rejects depending on that value. The case m = 2 was (in some different context) investigated by Goldschlager and Parberry [GP86]. In [He91b] a complete classification of the classes (F)P is given, when F consists of only one binary 3-valued function. In the current paper we justify the restriction to the case of one binary function by proving a normal form theorem stating that for every finite acceptance type there exists a finite acceptance type that characterizes the same class, but consists only of one binary function. Further we use the normal form theorem to show that the system of characterizable classes is closed under operators like ∃, ∀, ⊕, and others. In a similar fashion we show that all levels of boolean hierarchies over characterizable classes are characterizable. As corollaries from these results we obtain characterizations of all levels of the polynomial time hierarchy and the boolean hierarchy over NP, or more generally Σpk.