The tiles a computation table is drawn with

The drawing behind DescriptiveComplexity.WideTiling's hardness, written as plain predicates before any formula: the tile system whose square is the computation table of a clocked wide machine – a column is a tape address, a row is a time step.

What a tile carries

A tile is a tagged triple of elements of the machine's instance (DescriptiveComplexity.TileTag):

• dig – not a tile at all, but a digit: the diagonal triples are the elements the grid's coordinates are subsets of, so the square is 2ⁿ × 2ⁿ with n the size of the machine's instance;
• sym a – a cell holding the symbol a, with no head;
• head a q τ – the head is here, in the state q, reading a and firing the transition τ;
• halt a q – the head is here, in the state q, and fires nothing;
• arrL a q / arrR a q – no head yet, and one is about to arrive from the left (right) in the state q.

The head component carries the transition, not merely the state, because the two local rules would otherwise each be free to choose their own: the vertical one fixes the symbol written, the horizontal one the direction taken, and a tile system whose two rules disagree describes no run at all.

Why an arrival is a tile of its own

A vertical rule sees one column, so it cannot know that the neighboring head is about to step into it; a horizontal rule sees one row, so it cannot know what the next row holds. The arrival tile is the handshake between them: the horizontal rule justifies it against the neighboring head, and the vertical rule turns it into the head of the next row. That is what keeps a row to exactly one head with rules that never see more than two cells.

The tags

inductive DescriptiveComplexity.TileTag : Type

The tags of the tiles a computation table is drawn with: the digits the grid's coordinates are made of, and the five kinds of cell.

• dig : TileTag

  A digit of a coordinate – not a tile.

• sym : TileTag

  A cell with no head, holding a symbol.

• head : TileTag

  The head, firing a transition.

• halt : TileTag

  The head, firing nothing.

• arrL : TileTag

  A head arriving from the left.

• arrR : TileTag

  A head arriving from the right.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqTileTag : DecidableEq TileTag

Equations

• DescriptiveComplexity.instDecidableEqTileTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.instFintypeTileTag : Fintype TileTag

Equations

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

instance DescriptiveComplexity.instNonemptyTileTag : Nonempty TileTag

The universe of the emitted instance

@[reducible, inline]

abbrev DescriptiveComplexity.TilePt (A : Type) : Type

A point of the emitted instance: a tag and three elements of the machine's.

Equations

• DescriptiveComplexity.TilePt A = (DescriptiveComplexity.TileTag × (Fin 3 → A))

def DescriptiveComplexity.tpSym {A : Type} (p : TilePt A) : A

The symbol a tile holds: its first coordinate.

Equations

• DescriptiveComplexity.tpSym p = p.2 0

def DescriptiveComplexity.tpState {A : Type} (p : TilePt A) : A

The state a head or an arrival carries: its second coordinate.

Equations

• DescriptiveComplexity.tpState p = p.2 1

def DescriptiveComplexity.tpTr {A : Type} (p : TilePt A) : A

The transition a head fires: its third coordinate.

Equations

• DescriptiveComplexity.tpTr p = p.2 2

def DescriptiveComplexity.TPDig {A : Type} (p : TilePt A) : Prop

Being a digit: the tag says so and the triple is diagonal, so the digits are one per element of the machine's instance.

Equations

• DescriptiveComplexity.TPDig p = (p.1 = DescriptiveComplexity.TileTag.dig ∧ p.2 0 = p.2 1 ∧ p.2 1 = p.2 2)

def DescriptiveComplexity.tpDig {A : Type} (x : A) : TilePt A

The digit of an element.

Equations

• DescriptiveComplexity.tpDig x = (DescriptiveComplexity.TileTag.dig, fun (x_1 : Fin 3) => x)

@[simp]

theorem DescriptiveComplexity.tpDig_isDig {A : Type} (x : A) : TPDig (tpDig x)

theorem DescriptiveComplexity.tpDig_injective {A : Type} : Function.Injective tpDig

def DescriptiveComplexity.TPTile {A : Type} [FirstOrder.Language.wide.Structure A] (p : TilePt A) : Prop

Being a tile: one of the five kinds of cell, and – at a head – a transition the machine may fire on the state and the symbol the tile carries. A digit is not a tile.

Equations

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

def DescriptiveComplexity.TPAcc {A : Type} [FirstOrder.Language.wide.Structure A] (p : TilePt A) : Prop

Being an accepting tile: the head is here, in an accepting state.

Equations

• DescriptiveComplexity.TPAcc p = ((p.1 = DescriptiveComplexity.TileTag.head ∨ p.1 = DescriptiveComplexity.TileTag.halt) ∧ DescriptiveComplexity.WMAcc (DescriptiveComplexity.tpState p))

def DescriptiveComplexity.TPNoHead {A : Type} (p : TilePt A) : Prop

A cell with no head: it holds a symbol, and it may be expecting one – the bottom row's description allows an arrival, since the machine's first step announces itself in a neighbor of the corner.

Equations

• DescriptiveComplexity.TPNoHead p = (p.1 = DescriptiveComplexity.TileTag.sym ∨ p.1 = DescriptiveComplexity.TileTag.arrL ∨ p.1 = DescriptiveComplexity.TileTag.arrR)

def DescriptiveComplexity.TPBase {A : Type} [FirstOrder.Language.wide.Structure A] (p : TilePt A) : Prop

A base tile: what a column the description says nothing about carries in the bottom row – a cell holding the blank.

Equations

• DescriptiveComplexity.TPBase p = (DescriptiveComplexity.TPNoHead p ∧ DescriptiveComplexity.WMBlank (DescriptiveComplexity.tpSym p))

def DescriptiveComplexity.TPStart {A : Type} [FirstOrder.Language.wide.Structure A] (p : TilePt A) : Prop

A start tile: what the corner carries – the head, in a start state, on the blank cell the machine begins on.

It is also where the machine's own well-formedness is folded in: a machine whose order is not linear, whose input is not functional or which has no single blank has no start tile at all, so its drawing has no tiling – which is what a no-instance must give. The order's linearity is folded in twice over, since the emitted order is linear only when the machine's is.

Equations

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

def DescriptiveComplexity.TPEdgeL {A : Type} (p : TilePt A) : Prop

A tile the leftmost column may carry: anything but a head arriving from the left, there being nothing to the left of that column to send one. This is the border condition that keeps a head from appearing out of nowhere at the edge of the square.

Equations

• DescriptiveComplexity.TPEdgeL p = (p.1 ≠ DescriptiveComplexity.TileTag.arrL)

def DescriptiveComplexity.TPEdgeR {A : Type} (p : TilePt A) : Prop

A tile the rightmost column may carry: anything but a head arriving from the right.

Equations

• DescriptiveComplexity.TPEdgeR p = (p.1 ≠ DescriptiveComplexity.TileTag.arrR)

def DescriptiveComplexity.TPFirst {A : Type} [FirstOrder.Language.wide.Structure A] (x p : TilePt A) : Prop

The bottom row's description: at the cell of an element carrying input, that input symbol, with no head.

Equations

• DescriptiveComplexity.TPFirst x p = ∃ (a : A), DescriptiveComplexity.TPDig x ∧ DescriptiveComplexity.TPNoHead p ∧ DescriptiveComplexity.WMInp (x.2 0) a ∧ DescriptiveComplexity.tpSym p = a

def DescriptiveComplexity.TPFirstR {A : Type} [FirstOrder.Language.wide.Structure A] (x p : TilePt A) : Prop

The bottom row's description at the ruler: the cell of an element holds that element's input symbol, and the blank where the element carries none. This is what a space-bounded wide machine's tape says, its cells being the initial segments of the whole instance rather than of a file, which is why the drawing carries the bottom row as a parameter.

Equations

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

The two compatibilities

def DescriptiveComplexity.TPVert {A : Type} [FirstOrder.Language.wide.Structure A] (p q : TilePt A) : Prop

What a cell becomes in the next row: the symbol is the written one under a head and unchanged elsewhere, and the head of the next row is exactly what this row's arrival announces. A halted head stays where it is, and a cell that neither holds nor expects a head simply copies itself.

Equations

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

def DescriptiveComplexity.TPHoriz {A : Type} [FirstOrder.Language.wide.Structure A] (p q : TilePt A) : Prop

What may stand immediately to the right of a cell: a head that moves right announces itself in the right neighbor's arrival and nowhere else, and a head that moves left in the left neighbor's – so an arrival is justified by a neighboring head, which is what keeps a row to one head.

Equations

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