Tiling a corridor: the same tiles, one dimension unbounded

The corridor is DescriptiveComplexity.TILING with the square replaced by a strip (Fürer 1983 for the two complexities the pair carries): the columns are still the positions of the instance, but the rows are numbers, and the question is whether the description can be continued upward until an accepting tile appears.

Nothing about tiles changes – the vocabulary, the two compatibilities, the bottom row, the edge marks and the accepting mark are DescriptiveComplexity.TileData as before – so a tile system is read off an instance exactly once and asked two different questions. What changes is the resource: a square of the instance's own side is a polynomial object and the tiling of it sits in NP, while a corridor is a walk whose states are the rows, so it sits in PSPACE and, read over an exponential expansion, in EXPSPACE.

Why the height is a number and the width is not

A row is an assignment of tiles to positions – an object of the same size as the instance – and the corridor asks for a sequence of them, one above the other. A walk of that shape is exactly what DescriptiveComplexity.SOTCSpec describes, which is why the height is a plain ℕ here and not a coordinate of the instance: nothing in the problem bounds it.

def DescriptiveComplexity.TileData.IsCorridor {A : Type} (T : TileData A) (h : ℕ) (τ : ℕ → A → A) : Prop

A tiling of the corridor up to a given height: every cell of the strip carries a tile, the bottom row is one the description allows, the two edge columns carry tiles allowed there, neighbors in a row and rows one above the other are compatible, and the top row carries an accepting tile.

The height is where a corridor differs from DescriptiveComplexity.TileData.IsTiling: nothing in the instance bounds it, and the tiles above the accepting row are not asked about at all.

Equations

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

def DescriptiveComplexity.TileData.CorridorTileable {A : Type} (T : TileData A) : Prop

The corridor can be tiled: some assignment of tiles to its cells is a tiling of it, of some height.

Equations

• T.CorridorTileable = ∃ (h : ℕ) (τ : ℕ → A → A), T.IsCorridor h τ

Transport along a bijection

theorem DescriptiveComplexity.TileData.isCorridor_map {A : Type} (T : TileData A) {B : Type} (u : A ≃ B) (S : TileData B) (hposn : ∀ (a : A), T.Posn a ↔ S.Posn (u a)) (hle : ∀ (a a' : A), T.Le a a' ↔ S.Le (u a) (u a')) (htile : ∀ (a : A), T.Tile a ↔ S.Tile (u a)) (hacc : ∀ (a : A), T.Acc a ↔ S.Acc (u a)) (hhoriz : ∀ (a a' : A), T.Horiz a a' ↔ S.Horiz (u a) (u a')) (hvert : ∀ (a a' : A), T.Vert a a' ↔ S.Vert (u a) (u a')) (hfirst : ∀ (a a' : A), T.First a a' ↔ S.First (u a) (u a')) (hbase : ∀ (a : A), T.Base a ↔ S.Base (u a)) (hstart : ∀ (a : A), T.Start a ↔ S.Start (u a)) (hedgeL : ∀ (a : A), T.EdgeL a ↔ S.EdgeL (u a)) (hedgeR : ∀ (a : A), T.EdgeR a ↔ S.EdgeR (u a)) {h : ℕ} {τ : ℕ → A → A} (hcor : T.IsCorridor h τ) : S.IsCorridor h fun (k : ℕ) (x : B) => u (τ k (u.symm x))

A bijection matching the two systems carries a corridor across.

theorem DescriptiveComplexity.TileData.corridorTileable_map {A : Type} (T : TileData A) {B : Type} (u : A ≃ B) (S : TileData B) (hposn : ∀ (a : A), T.Posn a ↔ S.Posn (u a)) (hle : ∀ (a a' : A), T.Le a a' ↔ S.Le (u a) (u a')) (htile : ∀ (a : A), T.Tile a ↔ S.Tile (u a)) (hacc : ∀ (a : A), T.Acc a ↔ S.Acc (u a)) (hhoriz : ∀ (a a' : A), T.Horiz a a' ↔ S.Horiz (u a) (u a')) (hvert : ∀ (a a' : A), T.Vert a a' ↔ S.Vert (u a) (u a')) (hfirst : ∀ (a a' : A), T.First a a' ↔ S.First (u a) (u a')) (hbase : ∀ (a : A), T.Base a ↔ S.Base (u a)) (hstart : ∀ (a : A), T.Start a ↔ S.Start (u a)) (hedgeL : ∀ (a : A), T.EdgeL a ↔ S.EdgeL (u a)) (hedgeR : ∀ (a : A), T.EdgeR a ↔ S.EdgeR (u a)) (h : T.CorridorTileable) : S.CorridorTileable

And with it, the corridor's tileability.

The problem

theorem DescriptiveComplexity.isCorridor_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) {h : ℕ} {τ : ℕ → A → A} (hcor : (tileData A).IsCorridor h τ) : (tileData B).IsCorridor h fun (k : ℕ) (u : B) => e (τ k (e.symm u))

An isomorphism carries a corridor across.

theorem DescriptiveComplexity.corridorTileable_congr {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) : (tileData A).CorridorTileable ↔ (tileData B).CorridorTileable

Tileability of the corridor is an isomorphism invariant.

def DescriptiveComplexity.CORRIDOR : DecisionProblem FirstOrder.Language.tiling

Tiling a corridor. Can the strip whose width is the positions of the instance be tiled upward, from the bottom row the description allows until an accepting tile appears? The well-formedness promises are folded into the yes-instances, exactly as for DescriptiveComplexity.TILING.

Equations

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