The wide corridor: a strip as wide as the addresses

DescriptiveComplexity.CORRIDOR with one exponent added in the semantics of the problem, exactly as DescriptiveComplexity.WideTiling adds one to DescriptiveComplexity.TILING: the columns are the subsets of the instance, while the tiles stay an ordinary part of it, and the rows are numbers.

So an instance of size n asks whether a corridor of width 2ⁿ can be tiled upward until an accepting tile appears – the classical second complete problem of EXPSPACE beside a machine. The tile system it reads off an instance is the same DescriptiveComplexity.wideTileData as the square's, so the two problems differ only in the question asked, and the membership is again a composition: the corridor of the exponential expansion, CORRIDOR being in PSPACE.

The problem

theorem DescriptiveComplexity.wideCorridor_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (h : (wideTileData A).WellFormed ∧ (wideTileData A).CorridorTileable) : (wideTileData B).WellFormed ∧ (wideTileData B).CorridorTileable

The two halves transport, in either direction.

def DescriptiveComplexity.WideCorridor : DecisionProblem FirstOrder.Language.wtile

Tiling a wide corridor. Can the strip whose width is the subsets of the instance be tiled upward, from the bottom row the description allows until an accepting tile appears?

Equations

• One or more equations did not get rendered due to their size.

The membership

theorem DescriptiveComplexity.wideCorridor_iff_expansion (A : Type) [FirstOrder.Language.wtile.Structure A] [LinearOrder A] : WideCorridor.Holds A ↔ CORRIDOR.Holds (WideTile.wtileExp.Map A)

A wide corridor is an ordinary corridor of the expansion. The tile system is the one DescriptiveComplexity.WideTile.wtileAgree matches field by field; only the question differs.

theorem DescriptiveComplexity.wideCorridor_mem_EXPSPACE : EXPSPACE.Mem WideCorridor

The wide corridor is in EXPSPACE, which is PSPACE.exp: the expansion turns it into DescriptiveComplexity.CORRIDOR, and that problem is in PSPACE. This is the second natural member the class has, beside the wide machine.