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 #

source
theorem DescriptiveComplexity.TilingHard.wtHasFirst_tileStrR {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (hblank : ∃ (b : A), WMBlank b) (p : TilePt A) :
WTHasFirst p ↔ TPDig p

Every digit is described, as soon as the instance has a blank: an element with an input symbol has a tile holding it, and one without has the blank. That is what makes the drawing's file the machine's whole ruler.

Dependency graph
source
theorem DescriptiveComplexity.TilingHard.wmFileSeg_tpColR {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (hblank : ∃ (b : A), WMBlank b) (s : A → Prop) (x : A) :
WMFileSeg WTLe WTHasFirst (tpCol s) (tpDig x) ↔ WMDown WMLe s x

The cells of the drawing's file are the machine's own segments: a coordinate is the cell of the digit of x exactly when the address it is is the initial segment x cuts.

Dependency graph
source
theorem DescriptiveComplexity.TilingHard.wtpFirst_tpColR {A : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure A] (hblank : ∃ (b : A), WMBlank b) (s : A → Prop) (t : TilePt A) :
(wideTileData (TilePt A)).First (Sum.inl (tpCol s)) (Sum.inr t) ↔ ∃ (x : A), WMDown WMLe s x ∧ TPFirstR (tpDig x) t

The bottom row of the drawing is the machine's ruler: the cell of an element may carry a tile holding that element's input symbol, or the blank where it has none.

Dependency graph
source
theorem DescriptiveComplexity.TilingHard.wmDown_unique {A : Type} [FirstOrder.Language.wide.Structure A] (hlin : IsLinOrd WMLe) {s : A → Prop} {x x' : A} (h : WMDown WMLe s x) (h' : WMDown WMLe s x') :
x = x'

An address is the segment of at most one element: the two elements are each below the other.

Dependency graph

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
    source
    theorem DescriptiveComplexity.TilingHard.first_tableCorridor {A : Type} [Nonempty A] [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hwf : WideWF A) (hstep : ∀ i < n, StepWith (wideData A) (g i) (g (i + 1)) (tr i)) (hinit : (wideData A).IsInit (g 0)) {x : WPoint (TilePt A)} (hx : (wideTileData (TilePt A)).Posn x) :
    (MinPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn x → (wideTileData (TilePt A)).Start (tableCorridor g tr n 0 x)) ∧ (¬MinPos (wideTileData (TilePt A)).Le (wideTileData (TilePt A)).Posn x → (wideTileData (TilePt A)).FirstTile x (tableCorridor g tr n 0 x))

    The bottom row the table draws is the machine's initial tape, read at the ruler: the corner carries the machine's start, and every other column the input symbol of the element whose segment it is, or the blank.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.isCorridor_tableCorridor {A : Type} [Nonempty A] [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] {g : ℕ → Config (WPoint A)} {tr : ℕ → WPoint A} {n : ℕ} (hwf : WideWF A) (hinit : (wideData A).IsInit (g 0)) (hfreeze : ∀ (i : ℕ), n ≤ i → g i = g n) (hacc : (wideData A).Acc (g n).state) (hstep : ∀ i < n, StepWith (wideData A) (g i) (g (i + 1)) (tr i)) :
    (wideTileData (TilePt A)).IsCorridor n (tableCorridor g tr n)

    An accepting run in bounded space draws a corridor of the emitted square. Each of the conditions is the square's, with the clock taken out: the rows are the configurations, one per time step, and there is no bound on how many of them the run takes.

    Dependency graph
    source
    theorem DescriptiveComplexity.TilingHard.corridorTileable_of_acceptsSpace {A : Type} [Nonempty A] [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hwf : WideWF A) (h : (wideData A).AcceptsSpace) :
    (wideTileData (TilePt A)).WellFormed ∧ (wideTileData (TilePt A)).CorridorTileable

    The emitted corridor can be tiled when the machine accepts in bounded space.

    Dependency graph

    A corridor is an accepting run in bounded space #

    source
    theorem DescriptiveComplexity.TilingHard.wideAcceptSpace_of_corridorTileable {A : Type} [LinearOrder A] [Finite A] [FirstOrder.Language.wide.Structure A] (hwf0 : (wideTileData (TilePt A)).WellFormed) (h : (wideTileData (TilePt A)).CorridorTileable) :
    WideWF A ∧ (wideData A).AcceptsSpace

    A tiling of the emitted corridor is an accepting run of the machine. The columns are the machine's addresses and the rows its configurations, exactly as for the square; what the corridor drops is the clock.

    Dependency graph

    The reduction and the completeness #

    source
    theorem DescriptiveComplexity.wideCorridor_map_iff (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
    WideCorridor.Holds (TilingHard.tileInterpR.Map A) ↔ WideCorridor.Holds (TilePt A)

    The interpreted structure is a yes-instance exactly when the emitted one is.

    Dependency graph
    source
    noncomputable def DescriptiveComplexity.wideAcceptSpace_ordered_fo_reduction_wideCorridor :
    OrderedFOReduction WideAcceptSpace WideCorridor

    A wide machine bounded in space is drawn as a tiling of the emitted corridor. The drawing is the square's; what the corridor drops is the clock, which is the one thing a space-bounded machine does not have.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      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.

      Dependency graph