Documentation

DescriptiveComplexity.Problems.Wide.CorridorHard

Tiling a wide corridor is EXPSPACE-complete #

The corridor is the square's reduction with the clock taken out: the columns are still the machine's addresses, the rows are still its configurations, but there is no bound on how many of them there are – which is exactly a machine bounded in space and not in time.

Everything the drawing consists of is the square's (DescriptiveComplexity.Problems.Wide.TilingHard): the tiles, the transition a head carries, the arrival that hands it on, the border marks. Only the bottom row differs, because the two machines describe their tapes differently – the clocked one by a register file, the space-bounded one by the ruler of all the segments – which is why the drawing carries that row as a parameter (DescriptiveComplexity.TilingHard.tileStrOf).

The bottom row at the ruler #

An accepting run draws a corridor #

source
noncomputable def DescriptiveComplexity.TilingHard.tableCorridor {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] (g : ℕ → Config (WPoint A)) (tr : ℕ → WPoint A) (n : ℕ) :
ℕ → WPoint (TilePt A) → WPoint (TilePt A)

The corridor a run draws: the row of index k is the configuration at time k, and its cell at a column is the tile that configuration puts there.

Equations
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.tableCorridor_tpCol {A : Type} [Nonempty A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (k : ℕ) (s : A → Prop) :
    tableCorridor g tr n k (Sum.inl (tpCol s)) = Sum.inr (tileAt g tr n k (Sum.inl s))
    Dependency graph

    A corridor is an accepting run in bounded space #

    The reduction and the completeness #

    source
    theorem DescriptiveComplexity.wideCorridor_EXPSPACE_hard :
    EXPSPACE.Hard WideCorridor

    Tiling a wide corridor is EXPSPACE-hard: the space-bounded wide machine is, and it is drawn as one.

    Dependency graph
    source
    theorem DescriptiveComplexity.wideCorridor_EXPSPACE_complete :
    EXPSPACE.Complete WideCorridor

    Tiling a wide corridor is EXPSPACE-complete. The membership half is DescriptiveComplexity.wideCorridor_mem_EXPSPACE: a wide corridor is an ordinary corridor of an exponential expansion, and that problem is a walk on rows, hence in PSPACE. Registered in the Lax archive as Lax822549.TilingsComplete.wideCorridor_EXPSPACE_complete.

    Dependency graph