The cells a wide machine can recognize

A wide machine cannot read the digits of the address it is on, so a program needs cells it can identify by their contents. The vocabulary gives it exactly n of them, for free, through the input channel:

wmInp x a puts the symbol a in the cell at the address {y | y ≤ x}, the initial segment cut by x, and every other cell starts blank.

So a reduction that writes a mark in every element's cell obtains n distinguished cells, spread through the tape in the instance's own order (DescriptiveComplexity.wmSetLt_wmSeg), findable by scanning (DescriptiveComplexity.Problems.Wide.Roam) and reusable as the machine's register file: one tape track over these n cells is one n-bit register, and an n-bit register is a mirror of an address – the thing the head cannot read off itself.

The marks cannot all be different, and need not be. A symbol is an element and there is one register per element, so distinct names would need as many symbols as elements, leaving none to be the blank – and the blank must differ from every mark, or a blank cell of the working area would stop a scan looking for a register. What a program actually needs is far less: the walks of DescriptiveComplexity.Problems.Wide.Walk carry their pointer in the control and only ever ask “is this cell a register?”, so one generic mark serves them all. Only the two ends of the file have to be recognized on sight – to begin a downward pass and to come back from one – and two distinguished symbols pay for that.

This file says what those cells are and where they sit:

fact	theorem
the marked cell of an element	DescriptiveComplexity.wmSeg
an address is a cell exactly when it is a segment	DescriptiveComplexity.wmDown_iff_eq_wmSeg
they are ordered like the elements	DescriptiveComplexity.wmSetLt_wmSeg_iff
nothing is marked between consecutive ones	DescriptiveComplexity.not_wmSeg_between
distinct elements mark distinct cells	DescriptiveComplexity.wmSeg_injective
the head does not start on one	DescriptiveComplexity.wmSetLt_empty_wmSeg
they all sit above the working area	DescriptiveComplexity.wmSetLt_wmSeg_of_not_bot
the working area is the interval below them	DescriptiveComplexity.wmIncr_wmWorkTop
a marked cell holds its symbol at time zero	DescriptiveComplexity.initTape_wmSeg
every other cell starts blank	DescriptiveComplexity.initTape_of_not_wmDown
the initial configuration, marks and all	DescriptiveComplexity.isInit_wide_marks

Nothing here is about a program: these are facts about the vocabulary, settled before any transition table is written.

The marked cell of an element

def DescriptiveComplexity.wmSeg {A : Type} [FirstOrder.Language.wide.Structure A] (x : A) : A → Prop

The cell an element marks: the initial segment it cuts, which is where the input channel writes its symbol.

Equations

• DescriptiveComplexity.wmSeg x y = DescriptiveComplexity.WMLe y x

theorem DescriptiveComplexity.wmDown_wmSeg {A : Type} [FirstOrder.Language.wide.Structure A] (x : A) : WMDown WMLe (wmSeg x) x

The cell of an element is the address the vocabulary calls its own.

theorem DescriptiveComplexity.wmDown_iff_eq_wmSeg {A : Type} [FirstOrder.Language.wide.Structure A] (s : A → Prop) (x : A) : WMDown WMLe s x ↔ s = wmSeg x

An address is the cell of an element exactly when it is its segment, so DescriptiveComplexity.WMDown never has to be unfolded again.

theorem DescriptiveComplexity.wmSeg_self {A : Type} [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) (x : A) : wmSeg x x

An element lies in its own cell, so no cell is the empty address.

Where the marked cells sit

theorem DescriptiveComplexity.wmSetLt_wmSeg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {x y : A} (hlt : WMLt WMLe x y) : WMSetLt WMLe (wmSeg x) (wmSeg y)

The marked cells are ordered like the elements that mark them. A scan rightwards therefore meets them in the instance's own order, which is what lets a program walk its register file with a pointer in its control.

theorem DescriptiveComplexity.wmSeg_injective {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : Function.Injective wmSeg

Distinct elements mark distinct cells. This is about the addresses: no two elements cut the same initial segment, so the register file really has one cell per element. It says nothing about the symbols in them, which cannot all be distinct (see the module docstring).

theorem DescriptiveComplexity.wmSetLt_wmSeg_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (x y : A) : WMSetLt WMLe (wmSeg x) (wmSeg y) ↔ WMLt WMLe x y

The marked cells are ordered exactly like the elements, so a program reading its register file recovers the order of the instance and nothing else. The direction that matters is the one this adds: a mark below another mark comes from an element below the other's.

theorem DescriptiveComplexity.not_wmSeg_between {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {u u' : A} (hsucc : ∀ (v : A), WMLt WMLe u v → WMLe u' v) {r : A → Prop} (h1 : WMSetLt WMLe (wmSeg u) r) (h2 : WMSetLt WMLe r (wmSeg u')) (x : A) : r ≠ wmSeg x

Consecutive elements mark consecutive cells: no cell strictly between the cell of an element and the cell of its successor is marked. That is what a program walking its register file needs – one scan carries it from each register to the next, and nothing it passes can be mistaken for a register.

theorem DescriptiveComplexity.wmSetLt_empty_wmSeg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (x : A) : WMSetLt WMLe (fun (x : A) => False) (wmSeg x)

The head does not start on a marked cell: it starts on the empty address, and every marked cell holds the element that marks it. So a program may write its own left-end marker where it stands without disturbing the register file.

The register file and the working area

The least element of the instance is the most significant digit of an address (DescriptiveComplexity.Problems.Wide.Increment), and every marked cell contains it. So the register file sits entirely in the upper half of the tape and the addresses that do not contain the least element – the working area, half the tape, exponentially many cells – lie below every register. A program's data therefore cannot collide with its registers: it reaches the file by scanning right and comes back by scanning left.

theorem DescriptiveComplexity.wmSeg_bot {A : Type} [FirstOrder.Language.wide.Structure A] {bot : A} (hbot : ∀ (v : A), WMLe bot v) (x : A) : wmSeg x bot

Every marked cell contains the least element.

theorem DescriptiveComplexity.wmSetLt_wmSeg_of_not_bot {A : Type} [FirstOrder.Language.wide.Structure A] {bot : A} (hbot : ∀ (v : A), WMLe bot v) {r : A → Prop} (hr : ¬r bot) (x : A) : WMSetLt WMLe r (wmSeg x)

The working area lies below the register file. An address missing the least element is below every marked cell, that element being the most significant digit – so the two never meet, whatever a program writes.

def DescriptiveComplexity.wmWorkTop {A : Type} (bot : A) : A → Prop

The last cell of the working area: the address holding every element but the least. A program's loops run over the interval from the empty address to this one, and DescriptiveComplexity.reaches_of_wideRounds is given those two endpoints.

Equations

• DescriptiveComplexity.wmWorkTop bot v = (v ≠ bot)

theorem DescriptiveComplexity.wmIncr_wmWorkTop {A : Type} [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) {bot : A} (hbot : ∀ (v : A), WMLe bot v) : WMIncr WMLe (wmWorkTop bot) (wmSeg bot)

The working area ends exactly where the register file begins: the top of the working area is the predecessor of the first register. So a machine that runs off the end of its data steps straight onto its registers, and nothing lies between.

The initial tape

theorem DescriptiveComplexity.initTape_wmSeg {A : Type} [FirstOrder.Language.wide.Structure A] {x a : A} (hinp : WMInp x a) : (wideData A).InitTape (Sum.inl (wmSeg x)) (Sum.inr a)

A marked cell starts holding its symbol. The input is functional in a well-formed instance, so this is the only symbol it can hold.

theorem DescriptiveComplexity.initTape_of_not_wmDown {A : Type} [FirstOrder.Language.wide.Structure A] {s : A → Prop} (hno : ∀ (x y : A), WMDown WMLe s x → ¬WMInp x y) (a : WPoint A) : (wideData A).InitTape (Sum.inl s) a ↔ (wideData A).Blank a

Every unmarked cell starts blank. Two ways for a cell to be unmarked: it is not the segment of any element, or the elements whose segment it is carry no input symbol.

theorem DescriptiveComplexity.initTape_of_marks {A : Type} [FirstOrder.Language.wide.Structure A] {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMInp x (sym x)) {tp : WPoint A → WPoint A} (hmark : ∀ (x : A), tp (Sum.inl (wmSeg x)) = Sum.inr (sym x)) (hrest : ∀ (p : WPoint A), (∀ (x : A), p ≠ Sum.inl (wmSeg x)) → tp p = Sum.inr b) (p : WPoint A) : (wideData A).InitTape p (tp p)

The initial tape of a program with a register file: the naming symbol of x in the cell of x, the blank in every other cell. A reduction gives the symbol as a function sym of the element and marks nothing else; the tape it gets is then a function, which is what a run has to be given.

theorem DescriptiveComplexity.isInit_wide_marks {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} (hb : WMBlank b) {sym : A → A} (hinp : ∀ (x : A), WMInp x (sym x)) {tp : WPoint A → WPoint A} (hmark : ∀ (x : A), tp (Sum.inl (wmSeg x)) = Sum.inr (sym x)) (hrest : ∀ (p : WPoint A), (∀ (x : A), p ≠ Sum.inl (wmSeg x)) → tp p = Sum.inr b) {q₀ : A} (hq : WMStart q₀) : (wideData A).IsInit { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := tp }

The initial configuration of a program with a register file: a start state, the head on the empty address – which is no element's cell – and the marked tape of DescriptiveComplexity.initTape_of_marks.