Tiling a square: the local problem behind the machines

The problem the exponential classes are usually read on (Fürer 1983; Börger, Grädel & Gurevich 1997 is the book-length account).

A tile system is a set of tiles with two compatibility relations – which tile may stand immediately to the right of which, and which immediately above which – a description of the bottom row, and a set of accepting tiles. The question is whether the square whose sides are the positions of the instance can be tiled: every cell carries a tile, neighbors are compatible, the bottom row and the two edge columns are as described, and some cell carries an accepting tile.

Nothing here is about resources. As with DescriptiveComplexity.NTMAccept, the grid is indexed by the elements the instance marks as positions, so an instance of size n asks about an n × n square and the problem sits in NP; read over an exponential expansion, the same definition asks about a 2ⁿ × 2ⁿ square and sits one exponential up (DescriptiveComplexity.Problems.Wide.Tiling).

Why the tiling and not the machine

A tile system has no head, no clock and no time: its conditions are local in two dimensions and quantify over neighbors alone. That is what makes it the cheap second complete problem of a class whose first one is a machine – the work is a drawing, not an evaluator.

The shape of the conditions

The two edge columns carry tiles marked ledge and redge, which is what the border colors of a classical tiling problem do: a condition on neighbors says nothing about the column at either end, where one neighbor is missing.

The bottom row is described by a relation first p t rather than listed, exactly as a machine's initial tape is described by inp p a: a first-order condition on the position, which is what an expansion can carry. The accepting condition is a mark on tiles, and it is what turns a tiling into a decision: without it every tile system with a compatible bottom row is a yes-instance.

inductive FirstOrder.Language.tilingRel : ℕ → Type

Relation symbols of tile-system instances.

• posn : tilingRel 1

  posn p: p is a position – a column, and equally a row.

• tile : tilingRel 1

  tile t: t is a tile.

• tacc : tilingRel 1

  tacc t: t is an accepting tile.

• tle : tilingRel 2

  tle p q: the linear order along which the grid is read.

• horiz : tilingRel 2

  horiz t t': t' may stand immediately to the right of t.

• vert : tilingRel 2

  vert t t': t' may stand immediately above t.

• first : tilingRel 2

  first p t: the cell of the bottom row in column p may carry t.

• base : tilingRel 1

  base t: t is a base tile – what the bottom row carries in a column the description says nothing about.

• tstart : tilingRel 1

  tstart t: t is a start tile – what the corner of the grid carries.

• ledge : tilingRel 1

  ledge t: t may stand in the leftmost column.

• redge : tilingRel 1

  redge t: t may stand in the rightmost column.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqTilingRel {a✝ : ℕ} : DecidableEq (tilingRel a✝)

Equations

• FirstOrder.Language.instDecidableEqTilingRel = FirstOrder.Language.instDecidableEqTilingRel.decEq

def FirstOrder.Language.instDecidableEqTilingRel.decEq {a✝ : ℕ} (x✝ x✝¹ : tilingRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

def FirstOrder.Language.tiling : Language

The relational vocabulary of tile-system instances: positions with their order, tiles with their two compatibility relations, the bottom row and the accepting tiles.

Equations

• FirstOrder.Language.tiling = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.tilingRel }

instance FirstOrder.Language.instIsRelationalTiling : Language.tiling.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.tlPosn : Language.tiling.Relations 1

The position symbol.

Equations

• FirstOrder.Language.tlPosn = FirstOrder.Language.tilingRel.posn

@[reducible, inline]

abbrev FirstOrder.Language.tlTile : Language.tiling.Relations 1

The tile symbol.

Equations

• FirstOrder.Language.tlTile = FirstOrder.Language.tilingRel.tile

@[reducible, inline]

abbrev FirstOrder.Language.tlAcc : Language.tiling.Relations 1

The accepting-tile symbol.

Equations

• FirstOrder.Language.tlAcc = FirstOrder.Language.tilingRel.tacc

@[reducible, inline]

abbrev FirstOrder.Language.tlLe : Language.tiling.Relations 2

The order symbol.

Equations

• FirstOrder.Language.tlLe = FirstOrder.Language.tilingRel.tle

@[reducible, inline]

abbrev FirstOrder.Language.tlHoriz : Language.tiling.Relations 2

The horizontal-compatibility symbol.

Equations

• FirstOrder.Language.tlHoriz = FirstOrder.Language.tilingRel.horiz

@[reducible, inline]

abbrev FirstOrder.Language.tlVert : Language.tiling.Relations 2

The vertical-compatibility symbol.

Equations

• FirstOrder.Language.tlVert = FirstOrder.Language.tilingRel.vert

@[reducible, inline]

abbrev FirstOrder.Language.tlFirst : Language.tiling.Relations 2

The bottom-row symbol.

Equations

• FirstOrder.Language.tlFirst = FirstOrder.Language.tilingRel.first

@[reducible, inline]

abbrev FirstOrder.Language.tlBase : Language.tiling.Relations 1

The base-tile symbol.

Equations

• FirstOrder.Language.tlBase = FirstOrder.Language.tilingRel.base

@[reducible, inline]

abbrev FirstOrder.Language.tlStart : Language.tiling.Relations 1

The start-tile symbol.

Equations

• FirstOrder.Language.tlStart = FirstOrder.Language.tilingRel.tstart

@[reducible, inline]

abbrev FirstOrder.Language.tlEdgeL : Language.tiling.Relations 1

The left-edge symbol.

Equations

• FirstOrder.Language.tlEdgeL = FirstOrder.Language.tilingRel.ledge

@[reducible, inline]

abbrev FirstOrder.Language.tlEdgeR : Language.tiling.Relations 1

The right-edge symbol.

Equations

• FirstOrder.Language.tlEdgeR = FirstOrder.Language.tilingRel.redge

The tile system an instance describes

structure DescriptiveComplexity.TileData (A : Type) : Type

A tile system, read off an instance: the positions with their order, the tiles with their compatibilities, the bottom row and the accepting tiles. As with DescriptiveComplexity.TMData, the record is a plain bundle of predicates, so everything about tilings is stated once and read at whatever structure supplies them.

• Posn : A → Prop

  Being a position – a column, and equally a row.

• Le : A → A → Prop

  The order on positions.

• Tile : A → Prop

  Being a tile.

• Acc : A → Prop

  Being an accepting tile.

• Horiz : A → A → Prop

  The right neighbor may carry this tile.

• Vert : A → A → Prop

  The upper neighbor may carry this tile.

• First : A → A → Prop

  The bottom row's cell in this column may carry this tile.

• Base : A → Prop

  Being a base tile: what a column the description says nothing about carries in the bottom row.

• Start : A → Prop

  Being a start tile: what the corner of the grid carries.

• EdgeL : A → Prop

  Being a left-edge tile: what the leftmost column may carry.

• EdgeR : A → Prop

  Being a right-edge tile: what the rightmost column may carry.

def DescriptiveComplexity.TileData.FirstTile {A : Type} (T : TileData A) (x t : A) : Prop

The tiles the bottom row may carry in a column: the ones the description names there, and the base tiles in a column it names none. This is DescriptiveComplexity.TMData.InitTape's device – a description of the row rather than a listing – and it is what lets an expansion carry it.

Equations

• T.FirstTile x t = (T.First x t ∨ (∀ (u : A), ¬T.First x u) ∧ T.Base t)

def DescriptiveComplexity.TileData.IsTiling {A : Type} (T : TileData A) (τ : A → A → A) : Prop

A tiling of the square: every cell carries a tile, the bottom row is one the description allows, the two edge columns carry tiles allowed there, horizontal and vertical neighbors are compatible, and some cell carries an accepting tile.

The two edge conditions are what the classical border colors of a tiling problem do. A condition on neighbors says nothing about a column with no neighbor on one side, so without them a tile whose meaning is “something is arriving from the left” could stand in the leftmost column, justified by nothing; a machine drawn as a tiling would then grow a head out of nowhere.

Equations

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

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

The square is tileable: some assignment of tiles to cells is a tiling. The assignment is a function on the whole universe – what it does off the grid is not read, so nothing is lost by not restricting it.

Equations

• T.Tileable = ∃ (τ : A → A → A), T.IsTiling τ

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

Well-formedness, folded into the yes-instances exactly as DescriptiveComplexity.TMData.WellFormed is: the order is linear, and there is a position to index the grid by.

Equations

• T.WellFormed = (DescriptiveComplexity.IsLinOrd T.Le ∧ ∃ (p : A), T.Posn p)

Transport along a bijection

theorem DescriptiveComplexity.TileData.minPos_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')) (a : A) : MinPos T.Le T.Posn a ↔ MinPos S.Le S.Posn (u a)

The least position of the image is the image of the least position.

theorem DescriptiveComplexity.TileData.maxPos_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')) (a : A) : MaxPos T.Le T.Posn a ↔ MaxPos S.Le S.Posn (u a)

The greatest position of the image is the image of the greatest one.

theorem DescriptiveComplexity.TileData.succPos_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')) (a a' : A) : SuccPos T.Le T.Posn a a' ↔ SuccPos S.Le S.Posn (u a) (u a')

And the successor of the image is the image of the successor.

theorem DescriptiveComplexity.TileData.isTiling_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)) {τ : A → A → A} (h : T.IsTiling τ) : S.IsTiling fun (x y : B) => u (τ (u.symm x) (u.symm y))

A bijection matching the two systems carries a tiling across.

theorem DescriptiveComplexity.TileData.tileable_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.Tileable) : S.Tileable

And with it, tileability.

theorem DescriptiveComplexity.TileData.wellFormed_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')) (h : T.WellFormed) : S.WellFormed

And well-formedness: the order is linear and there is a position.

The shorthands of the vocabulary

def DescriptiveComplexity.TLPosn {A : Type} [FirstOrder.Language.tiling.Structure A] (a : A) : Prop

Being a position.

Equations

• DescriptiveComplexity.TLPosn a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlPosn ![a]

def DescriptiveComplexity.TLTile {A : Type} [FirstOrder.Language.tiling.Structure A] (a : A) : Prop

Being a tile.

Equations

• DescriptiveComplexity.TLTile a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlTile ![a]

def DescriptiveComplexity.TLAcc {A : Type} [FirstOrder.Language.tiling.Structure A] (a : A) : Prop

Being an accepting tile.

Equations

• DescriptiveComplexity.TLAcc a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlAcc ![a]

def DescriptiveComplexity.TLLe {A : Type} [FirstOrder.Language.tiling.Structure A] (a b : A) : Prop

The order on positions.

Equations

• DescriptiveComplexity.TLLe a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlLe ![a, b]

def DescriptiveComplexity.TLHoriz {A : Type} [FirstOrder.Language.tiling.Structure A] (a b : A) : Prop

Horizontal compatibility.

Equations

• DescriptiveComplexity.TLHoriz a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlHoriz ![a, b]

def DescriptiveComplexity.TLVert {A : Type} [FirstOrder.Language.tiling.Structure A] (a b : A) : Prop

Vertical compatibility.

Equations

• DescriptiveComplexity.TLVert a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlVert ![a, b]

def DescriptiveComplexity.TLFirst {A : Type} [FirstOrder.Language.tiling.Structure A] (a b : A) : Prop

The bottom row.

Equations

• DescriptiveComplexity.TLFirst a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlFirst ![a, b]

def DescriptiveComplexity.TLBase {A : Type} [FirstOrder.Language.tiling.Structure A] (a : A) : Prop

Being a base tile.

Equations

• DescriptiveComplexity.TLBase a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlBase ![a]

def DescriptiveComplexity.TLStart {A : Type} [FirstOrder.Language.tiling.Structure A] (a : A) : Prop

Being a start tile.

Equations

• DescriptiveComplexity.TLStart a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlStart ![a]

def DescriptiveComplexity.TLEdgeL {A : Type} [FirstOrder.Language.tiling.Structure A] (a : A) : Prop

Being a left-edge tile.

Equations

• DescriptiveComplexity.TLEdgeL a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlEdgeL ![a]

def DescriptiveComplexity.TLEdgeR {A : Type} [FirstOrder.Language.tiling.Structure A] (a : A) : Prop

Being a right-edge tile.

Equations

• DescriptiveComplexity.TLEdgeR a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tlEdgeR ![a]

def DescriptiveComplexity.tileData (A : Type) [FirstOrder.Language.tiling.Structure A] : TileData A

The tile system an instance describes.

Equations

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

The problem

theorem DescriptiveComplexity.tlPosn_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a : A) : TLPosn a ↔ TLPosn (e a)

theorem DescriptiveComplexity.tlTile_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a : A) : TLTile a ↔ TLTile (e a)

theorem DescriptiveComplexity.tlAcc_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a : A) : TLAcc a ↔ TLAcc (e a)

theorem DescriptiveComplexity.tlLe_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a a' : A) : TLLe a a' ↔ TLLe (e a) (e a')

theorem DescriptiveComplexity.tlHoriz_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a a' : A) : TLHoriz a a' ↔ TLHoriz (e a) (e a')

theorem DescriptiveComplexity.tlVert_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a a' : A) : TLVert a a' ↔ TLVert (e a) (e a')

theorem DescriptiveComplexity.tlFirst_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a a' : A) : TLFirst a a' ↔ TLFirst (e a) (e a')

theorem DescriptiveComplexity.tlBase_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a : A) : TLBase a ↔ TLBase (e a)

theorem DescriptiveComplexity.tlStart_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a : A) : TLStart a ↔ TLStart (e a)

theorem DescriptiveComplexity.tlEdgeL_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a : A) : TLEdgeL a ↔ TLEdgeL (e a)

theorem DescriptiveComplexity.tlEdgeR_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (a : A) : TLEdgeR a ↔ TLEdgeR (e a)

theorem DescriptiveComplexity.isTiling_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) {τ : A → A → A} (h : (tileData A).IsTiling τ) : (tileData B).IsTiling fun (u v : B) => e (τ (e.symm u) (e.symm v))

An isomorphism carries a tiling across: the tiling of the image is the tiling of the source read through the isomorphism, and every condition is a condition on relations the isomorphism preserves.

theorem DescriptiveComplexity.wellFormed_map {A B : Type} [FirstOrder.Language.tiling.Structure A] [FirstOrder.Language.tiling.Structure B] (e : FirstOrder.Language.tiling.Equiv A B) (h : (tileData A).WellFormed) : (tileData B).WellFormed

And it carries well-formedness across: the order and the positions are relations of the vocabulary.

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

Tileability is an isomorphism invariant.

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

And so is well-formedness.

def DescriptiveComplexity.TILING : DecisionProblem FirstOrder.Language.tiling

Tiling a square. Can the square whose sides are the positions of the instance be tiled, with the bottom row the description allows and an accepting tile somewhere? The well-formedness promises of DescriptiveComplexity.TileData.WellFormed are folded into the yes-instances, exactly as for DescriptiveComplexity.NTMAccept.

Equations

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