What a register file has to be

A wide machine cannot read the digits of the address it is on, so every program for one keeps a register file: one recognizable cell per element of the instance, holding one bit of a track. The walks, the tests and the mirror ask four things of that file and nothing else:

stand on the cell of u, write there, move to the cell of the next element, recognize the two ends.

This file says what a family of cells has to satisfy for those four to work, and the answer is short: it has to be strictly monotone, and no register may be the empty address.

The index is arbitrary. A space-bounded program's file has one register per element and that is what DescriptiveComplexity.RegFile names, but a program that has to lay its file out on a clock cannot afford that index – a rule sees the control and the cell under the head and nothing else, so the only addresses it can locate are a fixed number of tuple roll-overs from where it starts, and the elements are more. DescriptiveComplexity.IxFile is therefore the interface at an arbitrary ordered index, and DescriptiveComplexity.RegFile is its diagonal case (DescriptiveComplexity.RegFile.toIx), every elementwise statement below being the general one read there. Two linear orders are in play in the general form and only one at the diagonal: that of the addresses, over which the cells are compared, and that of the index, in which the registers are laid out.

• Monotonicity gives injectivity (DescriptiveComplexity.RegFile.injective) and the converse comparison (DescriptiveComplexity.RegFile.lt_iff), so the file is ordered exactly like the instance and a walk recovers the order and nothing else. It also gives the fact that turns a move between consecutive registers into a single scan: nothing is a register between two consecutive ones (DescriptiveComplexity.RegFile.gap), so the scan cannot overshoot or stop early.
• Nonemptiness of a cell (DescriptiveComplexity.RegFile.cell_nonempty) is what lets the head step below the first register, which is where a downward pass ends.

Two files satisfy this. The one a space-bounded program uses is the ladder the input channel marks – DescriptiveComplexity.wmSegFile, whose cell for x is the initial segment {y | y ≤ x} – and it is free, being in the instance before any transition is written. It is also, as DescriptiveComplexity.Problems.Wide.Marks explains, a geometric ruler lying in the top half of the tape, which a clocked program cannot afford to walk twice. A clocked program therefore builds its own file low on the tape and instantiates the same walks at it: that is what this interface is for, and why the walks above it name a DescriptiveComplexity.RegFile rather than DescriptiveComplexity.wmSeg.

An ordered index, its successors and its ranks

Everything a register walk asks of a file is about the order its cells are laid out in, and nothing about what indexes them. The index of the file a space-bounded program uses is the instance itself, which is why the elementwise names below read as “per element”; a program that has to lay its file out on a clock cannot afford that index, so the general form comes first and the elementwise one is its diagonal.

def DescriptiveComplexity.IxSucc {I : Type} (ile : I → I → Prop) (u u' : I) : Prop

The successor in an index's order: the least index strictly above one. The pointer of a register walk steps by this, in the control, while the head scans from one register to the next.

Equations

• DescriptiveComplexity.IxSucc ile u u' = (DescriptiveComplexity.WMLt ile u u' ∧ ∀ (v : I), DescriptiveComplexity.WMLt ile u v → ile u' v)

theorem DescriptiveComplexity.exists_ixSucc {I : Type} (ile : I → I → Prop) [Finite I] (h : IsLinOrd ile) {u : I} (hne : ∃ (v : I), WMLt ile u v) : ∃ (u' : I), IxSucc ile u u'

Every index but the greatest has a successor.

noncomputable def DescriptiveComplexity.ixRank {I : Type} (ile : I → I → Prop) (u : I) : ℕ

The rank of an index: the number of indices strictly below it, which is how many registers a walk has already crossed when its pointer reaches it. Every budget of a register walk is a difference of two of these, exactly as every budget of an address sweep is a difference of two DescriptiveComplexity.wideRanks.

Equations

• DescriptiveComplexity.ixRank ile u = DescriptiveComplexity.bitRank ile (fun (x : I) => True) u

theorem DescriptiveComplexity.ixRank_lt {I : Type} (ile : I → I → Prop) [Finite I] (h : IsLinOrd ile) {u u' : I} (hlt : WMLt ile u u') : ixRank ile u < ixRank ile u'

Rank increases strictly along the order.

theorem DescriptiveComplexity.ixRank_le_of_le {I : Type} (ile : I → I → Prop) [Finite I] (h : IsLinOrd ile) {u u' : I} (hle : ile u u') : ixRank ile u ≤ ixRank ile u'

Rank is monotone along the order.

theorem DescriptiveComplexity.ixRank_lt_card {I : Type} (ile : I → I → Prop) [Finite I] (u : I) : ixRank ile u < Nat.card I

The rank of an index is below the number of indices, so a walk of the file crosses fewer registers than there are of them.

theorem DescriptiveComplexity.ixRank_succ {I : Type} (ile : I → I → Prop) [Finite I] (h : IsLinOrd ile) {u u' : I} (hs : IxSucc ile u u') : ixRank ile u' = ixRank ile u + 1

Rank increases by exactly one along a successor, which is what makes a difference of ranks a count of registers.

The successor of an element

def DescriptiveComplexity.WMSucc (A : Type) [FirstOrder.Language.wide.Structure A] (u u' : A) : Prop

The successor of an element in the instance's order: the least element strictly above it, i.e., DescriptiveComplexity.IxSucc at the diagonal index.

Equations

• DescriptiveComplexity.WMSucc A u u' = DescriptiveComplexity.IxSucc DescriptiveComplexity.WMLe u u'

The rank of an element

noncomputable def DescriptiveComplexity.wmRank {A : Type} [FirstOrder.Language.wide.Structure A] (u : A) : ℕ

The rank of an element: the number of elements strictly below it.

Equations

• DescriptiveComplexity.wmRank u = DescriptiveComplexity.ixRank DescriptiveComplexity.WMLe u

@[simp]

theorem DescriptiveComplexity.wmRank_eq_ixRank {A : Type} [FirstOrder.Language.wide.Structure A] (u : A) : wmRank u = ixRank WMLe u

The rank of an element is the general rank at the diagonal index.

theorem DescriptiveComplexity.wmRank_lt {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {u u' : A} (hlt : WMLt WMLe u u') : wmRank u < wmRank u'

Rank increases strictly along the order.

theorem DescriptiveComplexity.wmRank_lt_card {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (u : A) : wmRank u < Nat.card A

The rank of an element is below the number of elements, so a walk of the file crosses fewer registers than there are elements.

The interface, at an arbitrary index

A file is a family of addresses indexed by something ordered, and the four things a walk asks of it are about that order alone. The index of the file a space-bounded program uses is the instance itself, which is why the interface below reads as “one cell per element”; a program that has to lay its file out on a clock cannot afford that index – it can only locate a fixed number of tuple roll-overs from where it starts, and the elements are more – so the interface is stated at an arbitrary ordered index and the elementwise one is its diagonal case.

Two linear orders are in play and they are not the same: the one of the addresses (DescriptiveComplexity.WMLe, over which the cells are compared) and the one of the index (which says in what order the registers are laid out). At the diagonal they coincide, which is why the elementwise statements below take one hypothesis where the general ones take two.

structure DescriptiveComplexity.IxFile (A : Type) [FirstOrder.Language.wide.Structure A] (I : Type) (ile : I → I → Prop) : Type

A register file over an index: one cell per index, ordered like the index, none of them the empty address.

Strict monotonicity is the whole of the interface. Everything a walk needs follows from it: the cells are distinct, they are comparable exactly as their indices are, and consecutive indices have no register between them, so one scan carries the head from each register to the next.

• cell : I → A → Prop

  The address of the register of an index.

• strictMono (u v : I) : WMLt ile u v → WMSetLt WMLe (self.cell u) (self.cell v)

  The registers are ordered like the indices that name them.

• cell_nonempty (u : I) : ∃ (x : A), self.cell u x

  No register is the empty address, so the head can always step below one.

theorem DescriptiveComplexity.IxFile.lt_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) (u v : I) (ha : IsLinOrd WMLe := by assumption) : WMSetLt WMLe (F.cell u) (F.cell v) ↔ WMLt ile u v

The registers are ordered exactly like the indices, so a program reading its file recovers that order and nothing else.

theorem DescriptiveComplexity.IxFile.injective {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) : Function.Injective F.cell

Distinct indices have distinct registers.

theorem DescriptiveComplexity.IxFile.gap {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {u u' : I} (hs : IxSucc ile u u') {r : A → Prop} (h1 : WMSetLt WMLe (F.cell u) r) (h2 : WMSetLt WMLe r (F.cell u')) (x : I) (ha : IsLinOrd WMLe := by assumption) : r ≠ F.cell x

Consecutive indices have consecutive registers: no address strictly between the register of an index and the register of its successor is a register.

theorem DescriptiveComplexity.IxFile.wmSetLt_empty_cell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (u : I) (ha : IsLinOrd WMLe := by assumption) : WMSetLt WMLe (fun (x : A) => False) (F.cell u)

The empty address is below every register, no register being empty.

theorem DescriptiveComplexity.IxFile.cell_le {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {u v : I} (hle : ile u v) (ha : IsLinOrd WMLe := by assumption) : WMSetLe WMLe (F.cell u) (F.cell v)

The registers are ordered like the indices non-strictly too.

theorem DescriptiveComplexity.IxFile.not_exists_cell_of_lt_bot {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {s : A → Prop} (hs : WMSetLt WMLe s (F.cell gbot)) (ha : IsLinOrd WMLe := by assumption) : ¬∃ (u : I), s = F.cell u

Nothing below the least register is a register, in existential form.

theorem DescriptiveComplexity.IxFile.le_cell_top_of_le {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {gtop gbot : I} (hbot : ∀ (y : I), ile gbot y) {s : A → Prop} (hs : WMSetLe WMLe s (F.cell gbot)) (ha : IsLinOrd WMLe := by assumption) : WMSetLe WMLe s (F.cell gtop)

Anything below the file is below its top register.

theorem DescriptiveComplexity.IxFile.le_cell_top {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {gtop gbot : I} (hbot : ∀ (y : I), ile gbot y) {s : A → Prop} (hs : WMSetLt WMLe s (F.cell gbot)) (ha : IsLinOrd WMLe := by assumption) : WMSetLe WMLe s (F.cell gtop)

theorem DescriptiveComplexity.IxFile.ne_cell_of_lt_cell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {r : A → Prop} (hlt : WMSetLt WMLe r (F.cell gbot)) (u : I) (ha : IsLinOrd WMLe := by assumption) : r ≠ F.cell u

Nothing strictly below the least register is a register.

theorem DescriptiveComplexity.IxFile.exists_not_cell {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) {u v : I} (hlt : WMLt ile u v) : ∃ (x : A), ¬F.cell u x

A register below another is not the whole tape.

The interface

structure DescriptiveComplexity.RegFile (A : Type) [FirstOrder.Language.wide.Structure A] : Type

A register file: one cell per element, ordered like the elements, none of them the empty address.

Strict monotonicity is the whole of the interface. Everything a walk needs follows from it: the cells are distinct, they are comparable exactly as their elements are, and consecutive elements have no register between them, so one scan carries the head from each register to the next.

• cell : A → A → Prop

  The address of the register of an element.

• strictMono (u v : A) : WMLt WMLe u v → WMSetLt WMLe (self.cell u) (self.cell v)

  The registers are ordered like the elements that name them.

• cell_nonempty (u : A) : ∃ (x : A), self.cell u x

  No register is the empty address, so the head can always step below one.

@[reducible]

def DescriptiveComplexity.RegFile.toIx {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) : IxFile A A WMLe

The elementwise file is the general one at its diagonal: index the instance, ordered by the instance's own order. Every statement below is its general form read there, the two linear orders having become one.

Equations

• F.toIx = { cell := F.cell, strictMono := ⋯, cell_nonempty := ⋯ }

@[simp]

theorem DescriptiveComplexity.RegFile.cell_toIx {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) : F.toIx.cell = F.cell

theorem DescriptiveComplexity.RegFile.lt_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) (u v : A) : WMSetLt WMLe (F.cell u) (F.cell v) ↔ WMLt WMLe u v

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

theorem DescriptiveComplexity.RegFile.injective {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) (h : IsLinOrd WMLe) : Function.Injective F.cell

Distinct elements have distinct registers. This is about the addresses; it says nothing about the symbols in them, which in a file marked by the input channel cannot all be distinct.

theorem DescriptiveComplexity.RegFile.gap {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {u u' : A} (hs : WMSucc A u u') {r : A → Prop} (h1 : WMSetLt WMLe (F.cell u) r) (h2 : WMSetLt WMLe r (F.cell u')) (x : A) : r ≠ F.cell x

Consecutive elements have consecutive registers: no address strictly between the register of an element and the register of its successor is a register. That is what makes a move between two registers one scan – the machine cannot overshoot, and nothing it passes can be mistaken for a register.

theorem DescriptiveComplexity.RegFile.wmSetLt_empty_cell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) (u : A) : WMSetLt WMLe (fun (x : A) => False) (F.cell u)

The empty address is below every register, no register being empty: the head starts below its file, wherever the file sits.

theorem DescriptiveComplexity.RegFile.cell_le {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {u v : A} (hle : WMLe u v) : WMSetLe WMLe (F.cell u) (F.cell v)

The registers are ordered like the elements non-strictly too: what a walk between two named registers is bounded by.

theorem DescriptiveComplexity.RegFile.not_exists_cell_of_lt_bot {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {gbot : A} (hbot : ∀ (y : A), WMLe gbot y) {s : A → Prop} (hs : WMSetLt WMLe s (F.cell gbot)) : ¬∃ (u : A), s = F.cell u

Nothing below the least register is a register, in existential form: the shape a walk's junk-address side condition takes.

theorem DescriptiveComplexity.RegFile.le_cell_top_of_le {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {gtop gbot : A} (hbot : ∀ (y : A), WMLe gbot y) {s : A → Prop} (hs : WMSetLe WMLe s (F.cell gbot)) : WMSetLe WMLe s (F.cell gtop)

Anything below the file is below its top register: what a walk up to the file needs of where it starts. At the input channel's ladder the top register is the whole tape and the bound is free; at a file a program builds it is not, and this is how a caller supplies it.

theorem DescriptiveComplexity.RegFile.le_cell_top {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {gtop gbot : A} (hbot : ∀ (y : A), WMLe gbot y) {s : A → Prop} (hs : WMSetLt WMLe s (F.cell gbot)) : WMSetLe WMLe s (F.cell gtop)

theorem DescriptiveComplexity.RegFile.ne_cell_of_lt_cell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {gbot : A} (hbot : ∀ (y : A), WMLe gbot y) {r : A → Prop} (hlt : WMSetLt WMLe r (F.cell gbot)) (u : A) : r ≠ F.cell u

Nothing strictly below the least register is a register, so a program working under its file can never mistake its own data for one.

theorem DescriptiveComplexity.RegFile.exists_not_cell {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) {u v : A} (hlt : WMLt WMLe u v) : ∃ (x : A), ¬F.cell u x

A register below another is not the whole tape, so the head standing on it can step up.

Where a file sits relative to the data

A walk asks nothing of where the file is, but a program does: it needs to know that what it writes in its working area cannot land on a register. For the file the input channel marks that is a fact about the layout – every marked cell holds the least element, and the addresses that do not are the working area – and a program that builds its own file has to arrange the same thing by choosing where to put it. Either way it is one condition, so it is asked for once.

structure DescriptiveComplexity.SitedFile (A : Type) [FirstOrder.Language.wide.Structure A] extends DescriptiveComplexity.RegFile A : Type

A register file, and the addresses a program works in: every working address lies strictly below every register, so the program's data and its registers cannot collide.

• cell : A → A → Prop
• strictMono (u v : A) : WMLt WMLe u v → WMSetLt WMLe (self.cell u) (self.cell v)
• cell_nonempty (u : A) : ∃ (x : A), self.cell u x
• Work : (A → Prop) → Prop

  The addresses the program computes with.

• work_lt_cell {r : A → Prop} : self.Work r → ∀ (u : A), WMSetLt WMLe r (self.cell u)

  They all lie below the file.

The file the input channel marks

The register file a space-bounded program gets for free: the cell of x is the initial segment x cuts, which is where the vocabulary's input channel writes. The facts of DescriptiveComplexity.Problems.Wide.Marks are exactly the two fields.

@[reducible]

def DescriptiveComplexity.wmSegFile {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : RegFile A

The register file of the input channel.

Reducible: a program written at an arbitrary file is read at this one by unification, and rw matches at instances transparency, so the projection (wmSegFile h).cell has to reduce to DescriptiveComplexity.wmSeg there.

Equations

• DescriptiveComplexity.wmSegFile h = { cell := DescriptiveComplexity.wmSeg, strictMono := ⋯, cell_nonempty := ⋯ }

@[simp]

theorem DescriptiveComplexity.cell_wmSegFile {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : (wmSegFile h).cell = wmSeg