The wide tiling: a square addressed by the subsets of its instance

The tile system of DescriptiveComplexity.TILING with one exponent added in the semantics of the problem, exactly as DescriptiveComplexity.WideAccept adds one to a machine:

the grid is indexed by the subsets of the instance, while the tiles – with their compatibilities, the bottom row and the accepting mark – stay an ordinary part of the instance.

So an instance of size n asks whether a 2ⁿ × 2ⁿ square can be tiled, which is the classical second complete problem of NEXPTIME beside a machine. Nothing is said about resources: the universe of the tiling is the universe of an exponential expansion of the instance (DescriptiveComplexity.Problems.Wide.TilingExp), so membership is the composition TILING ∘ expansion.

Where the order comes from

As for the wide machine, a decision problem may not read the ambient order of its instance, so the instance carries its own order wtLe and the order on addresses is the binary-number order it induces (DescriptiveComplexity.WMSetLe). Linearity is a promise, folded into the yes-instances through DescriptiveComplexity.TileData.WellFormed.

Where the bottom row goes

The bottom row is described at the initial-segment addresses: the address {y | y ≤ x} may carry the tiles wtFirst x names, and every other address may carry those wtFirst names of no element at all – the same device as the wide machine's input (wmInp), and for the same reason: a first-order condition on the element is what an expansion can carry, while a listing of 2ⁿ cells is not.

inductive FirstOrder.Language.wtileRel : ℕ → Type

Relation symbols of wide tile-system instances: the tiles of FirstOrder.Language.tiling with their compatibilities, and the positions and their order replaced by an order on the elements – the digits of an address.

• wle : wtileRel 2

  wtLe x y: the order on the elements, along which an address is read as a binary number.

• dig : wtileRel 1

  wtDig x: x is a digit – one of the elements the grid's coordinates are subsets of.

• tile : wtileRel 1

  wtTile t: t is a tile.

• tacc : wtileRel 1

  wtAcc t: t is an accepting tile.

• horiz : wtileRel 2

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

• vert : wtileRel 2

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

• first : wtileRel 2

  wtFirst x t: the bottom row's cell of x may carry t.

• base : wtileRel 1

  wtBase t: t is a base tile – what the bottom row carries where the description says nothing.

• tstart : wtileRel 1

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

• ledge : wtileRel 1

  wtEdgeL t: t may stand in the leftmost column.

• redge : wtileRel 1

  wtEdgeR t: t may stand in the rightmost column.

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

Equations

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

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqWtileRel {a✝ : ℕ} : DecidableEq (wtileRel a✝)

Equations

• FirstOrder.Language.instDecidableEqWtileRel = FirstOrder.Language.instDecidableEqWtileRel.decEq

def FirstOrder.Language.wtile : Language

The relational vocabulary of wide tile-system instances.

Equations

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

instance FirstOrder.Language.instIsRelationalWtile : Language.wtile.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.wtLe : Language.wtile.Relations 2

The order on the elements of the instance.

Equations

• FirstOrder.Language.wtLe = FirstOrder.Language.wtileRel.wle

@[reducible, inline]

abbrev FirstOrder.Language.wtDig : Language.wtile.Relations 1

The digit symbol.

Equations

• FirstOrder.Language.wtDig = FirstOrder.Language.wtileRel.dig

@[reducible, inline]

abbrev FirstOrder.Language.wtTile : Language.wtile.Relations 1

The tile symbol.

Equations

• FirstOrder.Language.wtTile = FirstOrder.Language.wtileRel.tile

@[reducible, inline]

abbrev FirstOrder.Language.wtAcc : Language.wtile.Relations 1

The accepting-tile symbol.

Equations

• FirstOrder.Language.wtAcc = FirstOrder.Language.wtileRel.tacc

@[reducible, inline]

abbrev FirstOrder.Language.wtHoriz : Language.wtile.Relations 2

The horizontal-compatibility symbol.

Equations

• FirstOrder.Language.wtHoriz = FirstOrder.Language.wtileRel.horiz

@[reducible, inline]

abbrev FirstOrder.Language.wtVert : Language.wtile.Relations 2

The vertical-compatibility symbol.

Equations

• FirstOrder.Language.wtVert = FirstOrder.Language.wtileRel.vert

@[reducible, inline]

abbrev FirstOrder.Language.wtFirst : Language.wtile.Relations 2

The bottom-row symbol.

Equations

• FirstOrder.Language.wtFirst = FirstOrder.Language.wtileRel.first

@[reducible, inline]

abbrev FirstOrder.Language.wtBase : Language.wtile.Relations 1

The base-tile symbol.

Equations

• FirstOrder.Language.wtBase = FirstOrder.Language.wtileRel.base

@[reducible, inline]

abbrev FirstOrder.Language.wtStart : Language.wtile.Relations 1

The start-tile symbol.

Equations

• FirstOrder.Language.wtStart = FirstOrder.Language.wtileRel.tstart

@[reducible, inline]

abbrev FirstOrder.Language.wtEdgeL : Language.wtile.Relations 1

The left-edge symbol.

Equations

• FirstOrder.Language.wtEdgeL = FirstOrder.Language.wtileRel.ledge

@[reducible, inline]

abbrev FirstOrder.Language.wtEdgeR : Language.wtile.Relations 1

The right-edge symbol.

Equations

• FirstOrder.Language.wtEdgeR = FirstOrder.Language.wtileRel.redge

The shorthands of the vocabulary

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

The order on the elements.

Equations

• DescriptiveComplexity.WTLe a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtLe ![a, b]

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

Being a digit: one of the elements the grid's coordinates are subsets of.

Equations

• DescriptiveComplexity.WTDig a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtDig ![a]

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

Being a tile.

Equations

• DescriptiveComplexity.WTTile a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtTile ![a]

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

Being an accepting tile.

Equations

• DescriptiveComplexity.WTAcc a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtAcc ![a]

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

Horizontal compatibility.

Equations

• DescriptiveComplexity.WTHoriz a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtHoriz ![a, b]

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

Vertical compatibility.

Equations

• DescriptiveComplexity.WTVert a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtVert ![a, b]

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

The bottom row, at the cell of an element.

Equations

• DescriptiveComplexity.WTFirst a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtFirst ![a, b]

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

Being a base tile.

Equations

• DescriptiveComplexity.WTBase a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtBase ![a]

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

Being a start tile.

Equations

• DescriptiveComplexity.WTStart a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtStart ![a]

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

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

Equations

• DescriptiveComplexity.WTEdgeL a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtEdgeL ![a]

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

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

Equations

• DescriptiveComplexity.WTEdgeR a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.wtEdgeR ![a]

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

An element the bottom row is described at: one whose cell carries a tile. These are the elements the file has cells for.

Equations

• DescriptiveComplexity.WTHasFirst a = ∃ (t : A), DescriptiveComplexity.WTFirst a t

The universe and the tile system

def DescriptiveComplexity.wtpPosn {A : Type} [FirstOrder.Language.wtile.Structure A] : WPoint A → Prop

Being a position: an address is one exactly when it holds digits alone, so the grid is indexed by the subsets of the marked part of the instance. That is what leaves the instance room for its tiles: a tile is an element like any other, and only the digits are coordinates.

Equations

• DescriptiveComplexity.wtpPosn (Sum.inl s) = ∀ (x : A), s x → DescriptiveComplexity.WTDig x
• DescriptiveComplexity.wtpPosn (Sum.inr val) = False

def DescriptiveComplexity.wtpLe {A : Type} [FirstOrder.Language.wtile.Structure A] : WPoint A → WPoint A → Prop

The order on the universe of the tiling: addresses first, in the binary-number order they inherit from the instance's own order, then the tiles in that same order.

Equations

• DescriptiveComplexity.wtpLe (Sum.inl s) (Sum.inl t) = DescriptiveComplexity.WMSetLe DescriptiveComplexity.WTLe s t
• DescriptiveComplexity.wtpLe (Sum.inl val) (Sum.inr val_1) = True
• DescriptiveComplexity.wtpLe (Sum.inr val) (Sum.inl val_1) = False
• DescriptiveComplexity.wtpLe (Sum.inr x_2) (Sum.inr y) = DescriptiveComplexity.WTLe x_2 y

def DescriptiveComplexity.wtpFirst {A : Type} [FirstOrder.Language.wtile.Structure A] : WPoint A → WPoint A → Prop

The bottom row: the cell of x – the segment x cuts among the elements the description names – may carry the tiles of x, and every other address a base tile. That is the same device as the register channel's input (DescriptiveComplexity.wpInpReg): a file of cells, not the ruler of all the segments, because a clocked machine's tape is described the same way and that is where this problem's hardness comes from.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.wtpFirst x✝¹ x✝ = False

def DescriptiveComplexity.wideTileData (A : Type) [FirstOrder.Language.wtile.Structure A] : TileData (WPoint A)

The wide tile system an instance describes: the tiles read off the instance, the positions being the addresses.

Equations

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

theorem DescriptiveComplexity.isLinOrd_wtpLe {A : Type} [FirstOrder.Language.wtile.Structure A] [Finite A] (h : IsLinOrd WTLe) : IsLinOrd wtpLe

The order of a wide tiling is linear as soon as the instance's is: the addresses are ordered as binary numbers, the tiles as in the instance, and the addresses come first.

theorem DescriptiveComplexity.wideTileData_wellFormed {A : Type} [FirstOrder.Language.wtile.Structure A] [Finite A] (h : IsLinOrd WTLe) : (wideTileData A).WellFormed

The promise of a wide tiling is a promise about its instance: the grid adds nothing to it, the empty address being a position whatever the instance says.

Isomorphism-invariance

def DescriptiveComplexity.wtPointEquiv {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) : WPoint A ≃ WPoint B

An isomorphism of instances is a bijection of the tilings' universes: an address goes to its image, a tile to its image.

Equations

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

theorem DescriptiveComplexity.wtLe_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a a' : A) : WTLe a a' ↔ WTLe (e a) (e a')

theorem DescriptiveComplexity.wtTile_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTTile a ↔ WTTile (e a)

theorem DescriptiveComplexity.wtAcc_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTAcc a ↔ WTAcc (e a)

theorem DescriptiveComplexity.wtHoriz_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a a' : A) : WTHoriz a a' ↔ WTHoriz (e a) (e a')

theorem DescriptiveComplexity.wtVert_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a a' : A) : WTVert a a' ↔ WTVert (e a) (e a')

theorem DescriptiveComplexity.wtFirst_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a a' : A) : WTFirst a a' ↔ WTFirst (e a) (e a')

theorem DescriptiveComplexity.wtBase_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTBase a ↔ WTBase (e a)

theorem DescriptiveComplexity.wtDig_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTDig a ↔ WTDig (e a)

theorem DescriptiveComplexity.wtStart_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTStart a ↔ WTStart (e a)

theorem DescriptiveComplexity.wtEdgeL_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTEdgeL a ↔ WTEdgeL (e a)

theorem DescriptiveComplexity.wtEdgeR_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTEdgeR a ↔ WTEdgeR (e a)

theorem DescriptiveComplexity.wtHasFirst_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (a : A) : WTHasFirst a ↔ WTHasFirst (e a)

The elements the bottom row is described at correspond.

theorem DescriptiveComplexity.wtFileSeg_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (s : A → Prop) (x : A) : WMFileSeg WTLe WTHasFirst s x ↔ WMFileSeg WTLe WTHasFirst (fun (y : B) => s (e.symm y)) (e x)

And so do the cells of the file.

theorem DescriptiveComplexity.wtPosn_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p : WPoint A) : (wideTileData A).Posn p ↔ (wideTileData B).Posn ((wtPointEquiv e) p)

The positions correspond: an address of digits is a position, a tile is not.

theorem DescriptiveComplexity.wtLe_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p q : WPoint A) : (wideTileData A).Le p q ↔ (wideTileData B).Le ((wtPointEquiv e) p) ((wtPointEquiv e) q)

The orders correspond: the binary-number order on addresses is the instance's order read through the isomorphism.

theorem DescriptiveComplexity.wtTile_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p : WPoint A) : (wideTileData A).Tile p ↔ (wideTileData B).Tile ((wtPointEquiv e) p)

The tiles correspond.

theorem DescriptiveComplexity.wtAcc_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p : WPoint A) : (wideTileData A).Acc p ↔ (wideTileData B).Acc ((wtPointEquiv e) p)

The accepting tiles correspond.

theorem DescriptiveComplexity.wtHoriz_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p q : WPoint A) : (wideTileData A).Horiz p q ↔ (wideTileData B).Horiz ((wtPointEquiv e) p) ((wtPointEquiv e) q)

Horizontal compatibility corresponds.

theorem DescriptiveComplexity.wtVert_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p q : WPoint A) : (wideTileData A).Vert p q ↔ (wideTileData B).Vert ((wtPointEquiv e) p) ((wtPointEquiv e) q)

Vertical compatibility corresponds.

theorem DescriptiveComplexity.wtFirst_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p q : WPoint A) : (wideTileData A).First p q ↔ (wideTileData B).First ((wtPointEquiv e) p) ((wtPointEquiv e) q)

The bottom row corresponds: the cell of an element goes to the cell of its image.

theorem DescriptiveComplexity.wtBase_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p : WPoint A) : (wideTileData A).Base p ↔ (wideTileData B).Base ((wtPointEquiv e) p)

The base tiles correspond.

theorem DescriptiveComplexity.wtStart_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p : WPoint A) : (wideTileData A).Start p ↔ (wideTileData B).Start ((wtPointEquiv e) p)

The start tiles correspond.

theorem DescriptiveComplexity.wtEdgeL_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p : WPoint A) : (wideTileData A).EdgeL p ↔ (wideTileData B).EdgeL ((wtPointEquiv e) p)

The left-edge tiles correspond.

theorem DescriptiveComplexity.wtEdgeR_point_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (p : WPoint A) : (wideTileData A).EdgeR p ↔ (wideTileData B).EdgeR ((wtPointEquiv e) p)

And so do the right-edge tiles.

The problem

theorem DescriptiveComplexity.wideTile_map {A B : Type} [FirstOrder.Language.wtile.Structure A] [FirstOrder.Language.wtile.Structure B] (e : FirstOrder.Language.wtile.Equiv A B) (h : (wideTileData A).WellFormed ∧ (wideTileData A).Tileable) : (wideTileData B).WellFormed ∧ (wideTileData B).Tileable

The two halves transport, in either direction: the wide tile system of the image is the source's read through the isomorphism.

def DescriptiveComplexity.WideTiling : DecisionProblem FirstOrder.Language.wtile

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

Equations

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