NP ⊆ AP

An alternating machine without universal states is a nondeterministic machine (Turing.MultiTapeATM.accepts_iff_toNTM_accepts). Guessing a certificate and verifying it is done by a finite fair-coin machine whose nondeterministic machine decides a problem in NP within polynomial time (Cslib.Complexity.IsVerifier.exists_decidesInTime); labelling all its states existential decides the problem as an alternating machine, so NP ⊆ AP (Cslib.Complexity.NP_subset_AP) Chandra, Kozen and Stockmeyer.

Main results

• Cslib.Complexity.NP_subset_AP, Cslib.Complexity.P_subset_AP.

References

• A. K. Chandra, D. C. Kozen, L. J. Stockmeyer, Alternation
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Cslib.Complexity.NP_subset_AP {α : Type} {enc : α ↪ List Bool} : NP enc ⊆ AP enc

NP ⊆ AP: the machine guessing and verifying a certificate, with every state labelled existential, decides the problem within the same polynomial time bound.

theorem Cslib.Complexity.P_subset_AP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ AP enc

P ⊆ AP, through NP.