The wide machine: a machine addressed by the subsets of its instance #

The machine model of the exponential classes. A DescriptiveComplexity.TMData read over the instance itself is a machine with polynomially many cells, and the library's bounds are unary by construction, so DescriptiveComplexity.NTMAccept lands in NP and DescriptiveComplexity.NTMAcceptSpace in PSPACE. The wide machine is the same model with one exponent added in the semantics of the problem, and nowhere else:

its tape is addressed by the subsets of the instance, while its control – the transitions, the states, the symbols – stays an ordinary part of the instance.

So an instance of size n describes a machine with 2^n cells and 2^n time steps, and the two resource variants land one exponential up: DescriptiveComplexity.WideAccept in NEXPTIME and DescriptiveComplexity.WideAcceptSpace in EXPSPACE (DescriptiveComplexity.Problems.Wide.Membership). A reduction of dimension d buys itself 2^(nᵈ) cells exactly as a reduction into DescriptiveComplexity.NTMAccept buys itself nᵈ.

The universe of the machine #

The machine runs over DescriptiveComplexity.WPoint, the disjoint union of

the addresses A → Prop – the subsets of the instance, which are the tape cells and equally the time steps; and
the control elements, the elements of the instance themselves, which are its states, its symbols and its transitions.

That is exactly the universe an exponential expansion of the instance has, with one tag for each summand (DescriptiveComplexity.Problems.Wide.Expansion), and it is why the membership proofs are the composition NTMAccept ∘ expansion rather than an argument about resources.

Where the order comes from #

DescriptiveComplexity.TMData needs a linear order on its universe, and a decision problem may not read the ambient order of its instance. So the instance carries its own order wmLe, and the order on addresses is the binary-number order it induces: one subset is below another when, at the wmLe-least element where they differ, the second contains it and the first does not (DescriptiveComplexity.WMSetLe). Addresses come below control elements, so the least position is the empty address. That the resulting relation is linear is a promise, folded into the yes-instances through DescriptiveComplexity.TMData.WellFormed exactly as for DescriptiveComplexity.NTMAccept.

Where the input goes #

The initial tape is described by the binary symbol wmInp of the instance, read at the initial-segment addresses: the address {y | y ≤ x} holds the input symbol of x, and every other address – including the empty one, where the head starts – holds the blank. Initial segments are ordered like the elements they come from, so the input appears along the tape in the instance's own order, and the whole of it is first-order describable over the instance, which is what the expansion needs.

The wide machine: a machine addressed by the subsets of its instance #

The universe of the machine #

Where the order comes from #

Where the input goes #

The shorthands of the vocabulary #

The universe and the machine #

Isomorphism-invariance #

The problems #