The exponential classes: EXPTIME, NEXPTIME, EXPSPACE #
The three classes, and the bridge theorems that let everything else about them be inherited rather than reproved.
| definition | equal, by theorem | |
|---|---|---|
DescriptiveComplexity.EXPTIME | SO(≤, LFP) | PTIME.exp |
DescriptiveComplexity.NEXPTIME | NP.exp – ∃SO over the expanded universe | – |
DescriptiveComplexity.EXPSPACE | SO(≤, PFP) | PSPACE.exp |
The library elsewhere splits definition from theorem the other way round –
PTIME is defined by SO-Horn and equals FO(LFP) by theorem, PSPACE is
defined by SO(TC) and equals FO(PFP) by theorem. At the exponential level the
fixpoint logic takes the definition slot, because there is no comparably
canonical restricted syntax to define these classes by, and because naming a
class after its fixpoint is what makes its statements readable: EXPTIME ⊆ EXPSPACE is SO(LFP) ⊆ SO(PFP).
Why NEXPTIME is presented differently #
Its literature spelling is existential third-order logic (Leivant
1989; Hella–Turull-Torres
2006), and this development deliberately builds no
third-order syntax layer: the two fixpoint logics need none, since an expansion
has already lowered the type of the objects a second-order fixpoint ranges
over. A “Σ¹₁ over the expansion” definition would be no more informative than
NP.exp, since that is what NP.exp unfolds to. So NEXPTIME is defined as
the succinct-instance form of NP, and this is an honest and narrow gap: the
library does not prove NEXPTIME = Σ²₁, because it does not have the syntax to
state it. NEXPTIME still gets its logical reading – guess a relation over the
expanded universe, check a first-order condition there – its machine problem
and its complete problems, exactly like the other two.
What is not claimed #
SO(LFP) = EXPTIME and SO(PFP) = EXPSPACE are definitions here, so nothing is asserted and no capture theorem is being claimed. Abiteboul–Vardi–Vianu 1997 is the reason these are the right logics to name the classes after, cited as motivation and not as a theorem proved here; it is stated in the relational (order-free, generic) setting, which is a second reason not to cite it flatly.
The three classes #
The class EXPTIME, defined as SO(≤, LFP) – equivalently, and with no
order in the statement at all, as SO(LFP)
(DescriptiveComplexity.mem_EXPTIME_iff_solfpDefinableFree): a least fixed point over a
second-order universe. Equivalently, and by theorem, polynomial time read over
an exponential expansion (DescriptiveComplexity.EXPTIME_eq_PTIME_exp).
The three membership closure obligations are borrowed through the bridge
theorem: DescriptiveComplexity.Exponential.Class proved them once, for
ExpDefinable C at an arbitrary class C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The class EXPSPACE, defined as SO(≤, PFP) – equivalently, and with no
order in the statement at all, as SO(PFP)
(DescriptiveComplexity.mem_EXPSPACE_iff_sopfpDefinableFree): a partial fixed point over a
second-order universe. Equivalently, and by theorem, polynomial space read over
an exponential expansion (DescriptiveComplexity.EXPSPACE_eq_PSPACE_exp).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The class NEXPTIME: NP read over an exponential expansion – guess a
relation over the expanded universe, check a first-order condition there. See
the module docstring for why this one is presented as NP.exp rather than as a
fixpoint logic.
Instances For
Dependency graph
coEXPTIME, the complement class of EXPTIME. That it coincides with
EXPTIME is DescriptiveComplexity.EXPTIME_eq_coEXPTIME.
Instances For
Dependency graph
coEXPSPACE, the complement class of EXPSPACE; it coincides with EXPSPACE
(DescriptiveComplexity.EXPSPACE_eq_coEXPSPACE).
Instances For
Dependency graph
coNEXPTIME, the complement class of NEXPTIME. No coincidence is claimed here: NEXPTIME is not expected to be closed under complement.
Instances For
Dependency graph
Membership, unfolded #
Dependency graph
Dependency graph
Dependency graph
The bridge theorems #
Every later result about the exponential classes is stated about
EXPTIME/EXPSPACE/NEXPTIME and proved by rewriting along these, so that
the work happens once, at DescriptiveComplexity.ComplexityClass.exp and an
arbitrary class.
EXPTIME is polynomial time on succinct instances.
Dependency graph
EXPSPACE is polynomial space on succinct instances.
Dependency graph
NEXPTIME is NP on succinct instances, by definition.
Dependency graph
Hardness over relational vocabularies #
The shape every hardness proof of the exponential catalog discharges, one per
class; each is DescriptiveComplexity.cofinalHard_iff read through the bridge
theorem.
Dependency graph
Dependency graph
Dependency graph
A problem is EXPTIME-hard as soon as every SO(≤, LFP) definable problem reduces to it.
Dependency graph
A problem is EXPSPACE-hard as soon as every SO(≤, PFP) definable problem reduces to it.
Dependency graph
A problem is NEXPTIME-hard as soon as every problem NP-definable over an expanded universe reduces to it.