Tiling a corridor is in PSPACE

The membership half: a corridor is a walk. Its states are the rows – one binary relation variable R x t, read as “the column x of this row carries the tile t” – its starting states are the rows the bottom-row description allows, its transitions are the vertical compatibility, and its accepting states are the rows carrying an accepting tile. That is exactly the shape of DescriptiveComplexity.SOTCSpec, so the specification is a transcription rather than a construction, and PSPACE is SO(TC).

Being a row – one tile per column, horizontally compatible, with the tiles the two edge columns allow – is asked of the starting state and of every state a transition enters, so every reachable state is a row.

The sentence shapes

The three sentences of the specification live over two different vocabularies (one copy of the block for the endpoints, two for the transition), so each shape is written once over an arbitrary vocabulary with its symbols as parameters, and read back by one realization lemma. Read over an exponential expansion the same specification asks about a corridor of exponential width, which is the EXPSPACE half.

Atoms and guards, over an arbitrary vocabulary

noncomputable def DescriptiveComplexity.atom₁ {L : FirstOrder.Language} {γ : Type} (r : L.Relations 1) (x : γ) : L.Formula γ

A unary relation, as a formula.

Equations

• DescriptiveComplexity.atom₁ r x = r.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.atom₂ {L : FirstOrder.Language} {γ : Type} (r : L.Relations 2) (x y : γ) : L.Formula γ

A binary relation, as a formula.

Equations

• DescriptiveComplexity.atom₂ r x y = r.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.atomEq {L : FirstOrder.Language} {γ : Type} (x y : γ) : L.Formula γ

Equality of two variables, as a formula.

Equations

• DescriptiveComplexity.atomEq x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.minPosF {L : FirstOrder.Language} {γ : Type} (posn : L.Relations 1) (le : L.Relations 2) (x : γ) : L.Formula γ

x is the least position.

Equations

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

noncomputable def DescriptiveComplexity.maxPosF {L : FirstOrder.Language} {γ : Type} (posn : L.Relations 1) (le : L.Relations 2) (x : γ) : L.Formula γ

x is the greatest position.

Equations

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

noncomputable def DescriptiveComplexity.succPosF {L : FirstOrder.Language} {γ : Type} (posn : L.Relations 1) (le : L.Relations 2) (x x' : γ) : L.Formula γ

x' is the position immediately above x.

Equations

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

theorem DescriptiveComplexity.realize_infS {L : FirstOrder.Language} {M : Type} [L.Structure M] (φ ψ : L.Sentence) : M ⊨ φ ⊓ ψ ↔ M ⊨ φ ∧ M ⊨ ψ

Splitting a conjunction of sentences, kept at the level of ⊨ so that the clause lemmas of this file still apply to the parts.

@[simp]

theorem DescriptiveComplexity.realize_atom₁ {L : FirstOrder.Language} {γ M : Type} [L.Structure M] {v : γ → M} (r : L.Relations 1) (x : γ) : (atom₁ r x).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x]

@[simp]

theorem DescriptiveComplexity.realize_atom₂ {L : FirstOrder.Language} {γ M : Type} [L.Structure M] {v : γ → M} (r : L.Relations 2) (x y : γ) : (atom₂ r x y).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x, v y]

@[simp]

theorem DescriptiveComplexity.realize_atomEq {L : FirstOrder.Language} {γ M : Type} [L.Structure M] {v : γ → M} (x y : γ) : (atomEq x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.realize_minPosF {L : FirstOrder.Language} {γ M : Type} [L.Structure M] {v : γ → M} (posn : L.Relations 1) (le : L.Relations 2) (x : γ) : (minPosF posn le x).Realize v ↔ MinPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) (v x)

@[simp]

theorem DescriptiveComplexity.realize_maxPosF {L : FirstOrder.Language} {γ M : Type} [L.Structure M] {v : γ → M} (posn : L.Relations 1) (le : L.Relations 2) (x : γ) : (maxPosF posn le x).Realize v ↔ MaxPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) (v x)

@[simp]

theorem DescriptiveComplexity.realize_succPosF {L : FirstOrder.Language} {γ M : Type} [L.Structure M] {v : γ → M} (posn : L.Relations 1) (le : L.Relations 2) (x x' : γ) : (succPosF posn le x x').Realize v ↔ SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) (v x) (v x')

What a row is, and what the walk asks of it

noncomputable def DescriptiveComplexity.rowTotalS {L : FirstOrder.Language} (posn tile : L.Relations 1) (row : L.Relations 2) : L.Sentence

Every column of this row carries a tile of the instance.

Equations

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

noncomputable def DescriptiveComplexity.rowFuncS {L : FirstOrder.Language} (row : L.Relations 2) : L.Sentence

And it carries only one.

Equations

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

noncomputable def DescriptiveComplexity.rowHorizS {L : FirstOrder.Language} (posn : L.Relations 1) (le horiz row : L.Relations 2) : L.Sentence

Neighboring columns of this row are compatible.

Equations

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

noncomputable def DescriptiveComplexity.rowEdgeLS {L : FirstOrder.Language} (posn ledge : L.Relations 1) (le row : L.Relations 2) : L.Sentence

Its leftmost column carries a tile allowed there.

Equations

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

noncomputable def DescriptiveComplexity.rowEdgeRS {L : FirstOrder.Language} (posn redge : L.Relations 1) (le row : L.Relations 2) : L.Sentence

And its rightmost column one allowed there.

Equations

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

noncomputable def DescriptiveComplexity.rowLegalS {L : FirstOrder.Language} (posn tile ledge redge : L.Relations 1) (le horiz row : L.Relations 2) : L.Sentence

Being a row: one tile per column, horizontally compatible, with the tiles the two edge columns allow.

Equations

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

noncomputable def DescriptiveComplexity.rowFirstS {L : FirstOrder.Language} (posn start base : L.Relations 1) (le first row : L.Relations 2) : L.Sentence

Being the bottom row: the corner carries a start tile and every other column one the description allows there.

Equations

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

noncomputable def DescriptiveComplexity.rowAccS {L : FirstOrder.Language} (posn acc : L.Relations 1) (row : L.Relations 2) : L.Sentence

Being an accepting row: some column of it carries an accepting tile.

Equations

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

noncomputable def DescriptiveComplexity.rowsVertS {L : FirstOrder.Language} (posn : L.Relations 1) (vert rowCur rowNext : L.Relations 2) : L.Sentence

One row above another: every column's two tiles are vertically compatible.

Equations

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

What each clause says

@[simp]

theorem DescriptiveComplexity.realize_rowTotalS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn tile : L.Relations 1) (row : L.Relations 2) : M ⊨ rowTotalS posn tile row ↔ ∀ (x : M), FirstOrder.Language.Structure.RelMap posn ![x] → ∃ (t : M), FirstOrder.Language.Structure.RelMap row ![x, t] ∧ FirstOrder.Language.Structure.RelMap tile ![t]

@[simp]

theorem DescriptiveComplexity.realize_rowFuncS {L : FirstOrder.Language} {M : Type} [L.Structure M] (row : L.Relations 2) : M ⊨ rowFuncS row ↔ ∀ (x t t' : M), FirstOrder.Language.Structure.RelMap row ![x, t] → FirstOrder.Language.Structure.RelMap row ![x, t'] → t = t'

@[simp]

theorem DescriptiveComplexity.realize_rowHorizS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn : L.Relations 1) (le horiz row : L.Relations 2) : M ⊨ rowHorizS posn le horiz row ↔ ∀ (x x' t t' : M), SuccPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) x x' → FirstOrder.Language.Structure.RelMap row ![x, t] → FirstOrder.Language.Structure.RelMap row ![x', t'] → FirstOrder.Language.Structure.RelMap horiz ![t, t']

@[simp]

theorem DescriptiveComplexity.realize_rowEdgeLS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn ledge : L.Relations 1) (le row : L.Relations 2) : M ⊨ rowEdgeLS posn ledge le row ↔ ∀ (x t : M), MinPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) x → FirstOrder.Language.Structure.RelMap row ![x, t] → FirstOrder.Language.Structure.RelMap ledge ![t]

@[simp]

theorem DescriptiveComplexity.realize_rowEdgeRS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn redge : L.Relations 1) (le row : L.Relations 2) : M ⊨ rowEdgeRS posn redge le row ↔ ∀ (x t : M), MaxPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) x → FirstOrder.Language.Structure.RelMap row ![x, t] → FirstOrder.Language.Structure.RelMap redge ![t]

@[simp]

theorem DescriptiveComplexity.realize_rowAccS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn acc : L.Relations 1) (row : L.Relations 2) : M ⊨ rowAccS posn acc row ↔ ∃ (x : M) (t : M), FirstOrder.Language.Structure.RelMap posn ![x] ∧ FirstOrder.Language.Structure.RelMap row ![x, t] ∧ FirstOrder.Language.Structure.RelMap acc ![t]

@[simp]

theorem DescriptiveComplexity.realize_rowsVertS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn : L.Relations 1) (vert rowCur rowNext : L.Relations 2) : M ⊨ rowsVertS posn vert rowCur rowNext ↔ ∀ (x t t' : M), FirstOrder.Language.Structure.RelMap posn ![x] → FirstOrder.Language.Structure.RelMap rowCur ![x, t] → FirstOrder.Language.Structure.RelMap rowNext ![x, t'] → FirstOrder.Language.Structure.RelMap vert ![t, t']

@[simp]

theorem DescriptiveComplexity.realize_rowFirstS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn start base : L.Relations 1) (le first row : L.Relations 2) : M ⊨ rowFirstS posn start base le first row ↔ ∀ (x t : M), FirstOrder.Language.Structure.RelMap posn ![x] → FirstOrder.Language.Structure.RelMap row ![x, t] → (MinPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) x → FirstOrder.Language.Structure.RelMap start ![t]) ∧ (¬MinPos (fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) (fun (a : M) => FirstOrder.Language.Structure.RelMap posn ![a]) x → FirstOrder.Language.Structure.RelMap first ![x, t] ∨ (∀ (u : M), ¬FirstOrder.Language.Structure.RelMap first ![x, u]) ∧ FirstOrder.Language.Structure.RelMap base ![t])

@[simp]

theorem DescriptiveComplexity.realize_rowLegalS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn tile ledge redge : L.Relations 1) (le horiz row : L.Relations 2) : M ⊨ rowLegalS posn tile ledge redge le horiz row ↔ M ⊨ rowTotalS posn tile row ∧ M ⊨ rowFuncS row ∧ M ⊨ rowHorizS posn le horiz row ∧ M ⊨ rowEdgeLS posn ledge le row ∧ M ⊨ rowEdgeRS posn redge le row

Well-formedness, as a sentence

noncomputable def DescriptiveComplexity.orderWfS {L : FirstOrder.Language} (posn : L.Relations 1) (le : L.Relations 2) : L.Sentence

The order is linear and there is a position: the promises the yes-instances fold in.

Equations

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

@[simp]

theorem DescriptiveComplexity.realize_orderWfS {L : FirstOrder.Language} {M : Type} [L.Structure M] (posn : L.Relations 1) (le : L.Relations 2) : M ⊨ orderWfS posn le ↔ (IsLinOrd fun (a b : M) => FirstOrder.Language.Structure.RelMap le ![a, b]) ∧ ∃ (p : M), FirstOrder.Language.Structure.RelMap posn ![p]

The specification

@[reducible]

def DescriptiveComplexity.corBlock : SOBlock

The block of the SO(TC) specification of the corridor: one binary relation variable, read as “the column x of this row carries the tile t”.

Marked @[reducible] so that the numerals of a tuple of its arity elaborate: without it w 1 at the type Fin (corBlock.arity i) → A has no OfNat instance.

Equations

• DescriptiveComplexity.corBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 2 }

def DescriptiveComplexity.corRowSym : corBlock.lang.Relations 2

The symbol of the row variable.

Equations

• DescriptiveComplexity.corRowSym = ⟨(), DescriptiveComplexity.corRowSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.corBase : FirstOrder.Language

The input vocabulary together with the order, over which the sentences of an SO(TC) specification live.

Equations

• DescriptiveComplexity.corBase = FirstOrder.Language.tiling.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.corLang₁ : FirstOrder.Language

The vocabulary of the endpoint sentences: one copy of the block.

Equations

• DescriptiveComplexity.corLang₁ = DescriptiveComplexity.corBase.sum DescriptiveComplexity.corBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.corLang₂ : FirstOrder.Language

The vocabulary of the transition sentence: two copies of the block.

Equations

• DescriptiveComplexity.corLang₂ = DescriptiveComplexity.corLang₁.sum DescriptiveComplexity.corBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.corIn₁ {n : ℕ} (r : FirstOrder.Language.tiling.Relations n) : corLang₁.Relations n

An input symbol, in the endpoint vocabulary.

Equations

• DescriptiveComplexity.corIn₁ r = Sum.inl (Sum.inl r)

@[reducible, inline]

abbrev DescriptiveComplexity.corIn₂ {n : ℕ} (r : FirstOrder.Language.tiling.Relations n) : corLang₂.Relations n

An input symbol, in the transition vocabulary.

Equations

• DescriptiveComplexity.corIn₂ r = Sum.inl (Sum.inl (Sum.inl r))

@[reducible, inline]

abbrev DescriptiveComplexity.corRow₁ : corLang₁.Relations 2

The row variable, in the endpoint vocabulary.

Equations

• DescriptiveComplexity.corRow₁ = Sum.inr DescriptiveComplexity.corRowSym

@[reducible, inline]

abbrev DescriptiveComplexity.corCur₂ : corLang₂.Relations 2

The row variable of the current state, in the transition vocabulary.

Equations

• DescriptiveComplexity.corCur₂ = Sum.inl (Sum.inr DescriptiveComplexity.corRowSym)

@[reducible, inline]

abbrev DescriptiveComplexity.corNext₂ : corLang₂.Relations 2

The row variable of the next state, in the transition vocabulary.

Equations

• DescriptiveComplexity.corNext₂ = Sum.inr DescriptiveComplexity.corRowSym

noncomputable def DescriptiveComplexity.corSpec : SOTCSpec FirstOrder.Language.tiling

The SO(TC) specification of the corridor. The states are the rows: a starting state is a row the bottom-row description allows, a transition is the vertical compatibility with a row entering it, and an accepting state is a row carrying an accepting tile. Being a row is asked of the source and of every state a transition enters, so every reachable state is one.

Equations

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

Reading the specification back

def DescriptiveComplexity.corRow {A : Type} (ρ : corBlock.Assignment A) : A → A → Prop

The row an assignment is.

Equations

• DescriptiveComplexity.corRow ρ x t = ρ () ![x, t]

def DescriptiveComplexity.RowLegal {A : Type} [FirstOrder.Language.tiling.Structure A] (R : A → A → Prop) : Prop

Being a row: one tile per column, horizontally compatible, with the tiles the two edge columns allow.

Equations

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

def DescriptiveComplexity.RowFirst {A : Type} [FirstOrder.Language.tiling.Structure A] (R : A → A → Prop) : Prop

Being the bottom row: the corner carries a start tile, every other column one the description allows there.

Equations

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

@[simp]

theorem DescriptiveComplexity.relMap_corIn₁ {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] {n : ℕ} (ρ : corBlock.Assignment A) (r : FirstOrder.Language.tiling.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (corIn₁ r) w ↔ FirstOrder.Language.Structure.RelMap r w

@[simp]

theorem DescriptiveComplexity.relMap_corRow₁ {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (ρ : corBlock.Assignment A) (w : Fin 2 → A) : FirstOrder.Language.Structure.RelMap corRow₁ w ↔ ρ () w

@[simp]

theorem DescriptiveComplexity.relMap_corIn₂ {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] {n : ℕ} (ρ σ : corBlock.Assignment A) (r : FirstOrder.Language.tiling.Relations n) (w : Fin n → A) : FirstOrder.Language.Structure.RelMap (corIn₂ r) w ↔ FirstOrder.Language.Structure.RelMap r w

@[simp]

theorem DescriptiveComplexity.relMap_corCur₂ {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (ρ σ : corBlock.Assignment A) (w : Fin 2 → A) : FirstOrder.Language.Structure.RelMap corCur₂ w ↔ ρ () w

@[simp]

theorem DescriptiveComplexity.relMap_corNext₂ {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (ρ σ : corBlock.Assignment A) (w : Fin 2 → A) : FirstOrder.Language.Structure.RelMap corNext₂ w ↔ σ () w

theorem DescriptiveComplexity.isSrc_iff {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (ρ : corBlock.Assignment A) : corSpec.IsSrc ρ ↔ (tileData A).WellFormed ∧ RowLegal (corRow ρ) ∧ RowFirst (corRow ρ)

What a starting state is: the instance is well-formed and the state is the bottom row.

theorem DescriptiveComplexity.step_iff {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (ρ σ : corBlock.Assignment A) : corSpec.Step ρ σ ↔ RowLegal (corRow σ) ∧ ∀ (x t t' : A), TLPosn x → corRow ρ x t → corRow σ x t' → TLVert t t'

What a transition is: the state entered is a row, and it stands above the state left.

theorem DescriptiveComplexity.isTgt_iff {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (ρ : corBlock.Assignment A) : corSpec.IsTgt ρ ↔ ∃ (x : A) (t : A), TLPosn x ∧ corRow ρ x t ∧ TLAcc t

What an accepting state is: a row with an accepting tile in it.

The walk is the corridor

def DescriptiveComplexity.corAsg {A : Type} (τ : ℕ → A → A) (k : ℕ) : corBlock.Assignment A

The assignment a row of a corridor is.

Equations

• DescriptiveComplexity.corAsg τ k x✝ w = (w 1 = τ k (w 0))

@[simp]

theorem DescriptiveComplexity.corRow_corAsg {A : Type} (τ : ℕ → A → A) (k : ℕ) (x t : A) : corRow (corAsg τ k) x t ↔ t = τ k x

theorem DescriptiveComplexity.accepts_of_corridor {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (hwf : (tileData A).WellFormed) (h : (tileData A).CorridorTileable) : corSpec.Accepts A

A corridor is a walk: its rows, read as assignments, start at a bottom row, step one above the other, and end at a row with an accepting tile.

noncomputable def DescriptiveComplexity.rowFun {A : Type} (R : A → A → Prop) : A → A

The tile a row puts in a column, read off the relation the walk carries.

Equations

• DescriptiveComplexity.rowFun R x = if h : ∃ (t : A), R x t then h.choose else x

theorem DescriptiveComplexity.rowFun_spec {A : Type} {R : A → A → Prop} {x : A} (h : ∃ (t : A), R x t) : R x (rowFun R x)

def DescriptiveComplexity.CorridorTo {A : Type} [FirstOrder.Language.tiling.Structure A] (n : ℕ) (τ : ℕ → A → A) (σ : corBlock.Assignment A) : Prop

The corridor a walk has built so far, with the row it has reached on top: the induction invariant of DescriptiveComplexity.corridor_of_accepts.

Equations

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

theorem DescriptiveComplexity.exists_corridorTo {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] {ρ σ : corBlock.Assignment A} (hsrc : corSpec.IsSrc ρ) (hreach : corSpec.Reach ρ σ) : ∃ (n : ℕ) (τ : ℕ → A → A), CorridorTo n τ σ

A row a walk reaches stands on a corridor: the rows it went through are its cells, and the row itself is its top.

theorem DescriptiveComplexity.corridor_of_accepts {A : Type} [FirstOrder.Language.tiling.Structure A] [LinearOrder A] (h : corSpec.Accepts A) : (tileData A).WellFormed ∧ (tileData A).CorridorTileable

A walk is a corridor: the rows it goes through tile one, up to the row where the accepting tile stands.

theorem DescriptiveComplexity.corridor_sotcDefinable : SOTCDefinable CORRIDOR

Tiling a corridor is SO(TC) definable: the walk on rows is the corridor.

theorem DescriptiveComplexity.corridor_mem_PSPACE : PSPACE.Mem CORRIDOR

Tiling a corridor is in PSPACE.