A register file on a stretch of consecutive addresses

The register file the input channel marks (DescriptiveComplexity.wmSegFile) is free, but it is a geometric ruler: the cell of the j-th element sits at address 2 ^ m − 2 ^ (m − j − 1), so the file lies entirely in the top half of the tape and reaching its upper registers costs almost the whole tape. A machine with no clock does not care. A machine whose clock counts the addresses can walk that file once and never again.

This file builds the other one:

the registers are n consecutive addresses, the register of the j-th element being the address of rank base + j.

Everything a walk asks for follows at once, since DescriptiveComplexity.RegFile asks only for strict monotonicity: ranks are monotone, so the cells are (DescriptiveComplexity.segFile). What indexes the registers plays no part in that, so the construction is made at an arbitrary ordered index (DescriptiveComplexity.ixSegFile) and the elementwise file is its diagonal – which is what a program too tightly clocked to afford one register per element will build its own file with. What the geometry buys is the cost: consecutive registers are consecutive addresses (DescriptiveComplexity.segFile_gap), so a move of the walk is one step and a pass over the whole file costs n, against the whole tape for the ruler.

Where the stretch sits is the caller's choice, and it is not a free one. The subroutines written for the input channel's file assume it lies above the addresses the program computes with, since that is where the ruler is (DescriptiveComplexity.Problems.Wide.Marks): a scan looking for a register scans upwards, and the bound it is given is a register. A program that builds its own file and wants those subroutines unchanged puts it above its data as well; one that wants it out of the way takes base = 1, DescriptiveComplexity.lowFile, whose registers are the first n nonempty addresses and which therefore lies below everything (DescriptiveComplexity.wideRank_lowCell_le).

There is nothing to arrange for the addresses to exist: the cell of an element uses no marked symbol, so a program with this file writes its own names into those cells – one per cell, as it walks the bottom of the tape in its first n steps – and the two ends are recognized like any other register. The one fact that has to be proved is that there is room, and there is, with room to spare: there are 2 ^ n addresses for n elements (DescriptiveComplexity.card_wideAddr, the clock of the model read as a count).

Comparing addresses by rank

theorem DescriptiveComplexity.wideRank_lt_iff {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (s t : A → Prop) : wideRank s < wideRank t ↔ WMSetLt WMLe s t

An address is below another exactly when its rank is smaller. The rank determines the address, so a family of addresses is strictly monotone as soon as its ranks are.

There is room at the bottom

theorem DescriptiveComplexity.card_lt_card_wideAddr {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] : Nat.card A < Nat.card { p : WPoint A // (wideData A).Posn p }

There are strictly more addresses than elements, which is the room the construction below needs: one address per element, and one more for the empty address it starts above.

The addresses from the bottom, one by one

noncomputable def DescriptiveComplexity.addrSeq {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : ℕ → A → Prop

The j-th address from the bottom: the empty address, then increments. Beyond the last address the sequence stands still, which never happens below the number of addresses.

Equations

• DescriptiveComplexity.addrSeq h 0 = fun (x : A) => False
• DescriptiveComplexity.addrSeq h j.succ = if hex : ∃ (x : A), ¬DescriptiveComplexity.addrSeq h j x then Classical.choose ⋯ else DescriptiveComplexity.addrSeq h j

The file, and where it sits

Which stretch of the tape the registers occupy is the caller's choice, and it is not a free one. The file the input channel marks lies above every address a program computes with (DescriptiveComplexity.Problems.Wide.Marks), and the subroutines written for it are stated that way – a scan looking for a register scans upwards, and the bound it is given is a register. A program that builds its own file and wants those subroutines unchanged must therefore put it above its data as well, which here means high in its working region; one that wants the file out of the way puts it at the bottom. Both are the same construction at a different base.

The file, at an arbitrary index

noncomputable def DescriptiveComplexity.ixSegCell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} (ile : I → I → Prop) (h : IsLinOrd WMLe) (base : ℕ) (u : I) : A → Prop

The register of an index in the file based at base: the address whose rank is base above the index's, so the file is the stretch of consecutive addresses whose ranks start at base.

Equations

• DescriptiveComplexity.ixSegCell ile h base u = DescriptiveComplexity.addrSeq h (base + DescriptiveComplexity.ixRank ile u)

theorem DescriptiveComplexity.wideRank_ixSegCell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} [Finite I] (ile : I → I → Prop) (h : IsLinOrd WMLe) {base : ℕ} (hbase : base + Nat.card I ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) (u : I) : wideRank (ixSegCell ile h base u) = base + ixRank ile u

The rank of a register is its index's, shifted by the base.

noncomputable def DescriptiveComplexity.ixSegFile {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} [Finite I] (ile : I → I → Prop) (h : IsLinOrd WMLe) (hi : IsLinOrd ile) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card I ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) : IxFile A I ile

A register file on a stretch of consecutive addresses, one register per index. The base says where the stretch starts; it must be positive, so that no register is the empty address the head starts on, and the stretch must fit below the top of the tape.

Equations

• DescriptiveComplexity.ixSegFile ile h hi hpos hbase = { cell := DescriptiveComplexity.ixSegCell ile h base, strictMono := ⋯, cell_nonempty := ⋯ }

@[simp]

theorem DescriptiveComplexity.cell_ixSegFile {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} [Finite I] (ile : I → I → Prop) (h : IsLinOrd WMLe) (hi : IsLinOrd ile) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card I ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) : (ixSegFile ile h hi hpos hbase).cell = ixSegCell ile h base

theorem DescriptiveComplexity.wmIncr_ixSegCell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} [Finite I] (ile : I → I → Prop) (h : IsLinOrd WMLe) (hi : IsLinOrd ile) {base : ℕ} (hbase : base + Nat.card I ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) {u u' : I} (hs : IxSucc ile u u') : WMIncr WMLe (ixSegCell ile h base u) (ixSegCell ile h base u')

The successor of a register's address is the next register's, so a sweep of the file's stretch and a walk of the file step together: the address the sweep moves to is the cell of the index the pointer moves to. This is what lets the file-laying phase name every cell it writes.

noncomputable def DescriptiveComplexity.segCell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (base : ℕ) (u : A) : A → Prop

The register of an element in the file based at base: the address whose rank is base above the element's, so the file is the stretch of n consecutive addresses whose ranks start at base.

Equations

• DescriptiveComplexity.segCell h base u = DescriptiveComplexity.ixSegCell DescriptiveComplexity.WMLe h base u

noncomputable def DescriptiveComplexity.segFile {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card A ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) : RegFile A

A register file on a stretch of consecutive addresses. The base says where the stretch starts; it must be positive, so that no register is the empty address the head starts on, and the stretch must fit below the top of the tape.

Equations

• DescriptiveComplexity.segFile h hpos hbase = { cell := DescriptiveComplexity.segCell h base, strictMono := ⋯, cell_nonempty := ⋯ }

@[simp]

theorem DescriptiveComplexity.cell_segFile {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card A ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) : (segFile h hpos hbase).cell = segCell h base

theorem DescriptiveComplexity.segFile_gap {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card A ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) {u u' : A} (hs : WMSucc A u u') : wideRank ((segFile h hpos hbase).cell u') - wideRank ((segFile h hpos hbase).cell u) ≤ 1

Consecutive registers are consecutive addresses, wherever the file sits, so a move of a walk over it is a single step and a pass over the whole file costs one step per element. This is the hypothesis the budgeted walks ask for, with w = 1.

The file at the bottom

The base-1 case: the registers are the first n nonempty addresses, so the machine builds the file in its first n steps and everything above it is free.

noncomputable def DescriptiveComplexity.lowCell {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (u : A) : A → Prop

The register of an element in the file at the bottom of the tape.

Equations

• DescriptiveComplexity.lowCell h u = DescriptiveComplexity.segCell h 1 u

theorem DescriptiveComplexity.one_add_card_le {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] : 1 + Nat.card A ≤ Nat.card { p : WPoint A // (wideData A).Posn p }

There is room for the file at the bottom: there are strictly more addresses than elements.

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

The register file at the bottom of the tape.

Equations

• DescriptiveComplexity.lowFile h = DescriptiveComplexity.segFile h Nat.one_pos ⋯

@[simp]

theorem DescriptiveComplexity.cell_lowFile {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) : (lowFile h).cell = lowCell h

Which addresses the registers are

A program does not merely need its file to exist: the phase that builds it walks the bottom of the tape writing one name per cell, so it needs to know that the cells it passes are exactly the registers, and which element each belongs to. Both are read off the ranks.

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

An address is determined by its rank, ranks being a strictly monotone map of a linear order.

noncomputable def DescriptiveComplexity.ixSegTop {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (I : Type) [Finite I] (h : IsLinOrd WMLe) (base : ℕ) : A → Prop

The address just above a file's stretch: where a sweep of the file stops, one past its last register.

Equations

• DescriptiveComplexity.ixSegTop I h base = DescriptiveComplexity.addrSeq h (base + Nat.card I)

What a file's stretch costs

A sweep of the stretch costs the difference of the two ranks, and these are what that difference is: the stretch is exactly as long as the file has registers, and the last register sits one short of its end. Every budget of the opening phases is one of these two numbers.

theorem DescriptiveComplexity.exists_ixSegCell_eq {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} [Finite I] (ile : I → I → Prop) (h : IsLinOrd WMLe) (hi : IsLinOrd ile) {base : ℕ} (hbase : base + Nat.card I ≤ Nat.card { p : WPoint A // (wideData A).Posn p }) {s : A → Prop} (h1 : base ≤ wideRank s) (h2 : wideRank s < base + Nat.card I) : ∃ (u : I), ixSegCell ile h base u = s

The registers of a file on a stretch are exactly the addresses of that stretch. So a sweep of the stretch is a walk of the file: every cell it stops at is some register's, which is what lets the sweep's pointer name the cell it is writing.

theorem DescriptiveComplexity.exists_lowCell_eq {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {s : A → Prop} (h1 : 1 ≤ wideRank s) (h2 : wideRank s ≤ Nat.card A) : ∃ (u : A), lowCell h u = s

The registers of the bottom file are exactly the addresses of rank between 1 and n. So the phase that builds the file walks the first n cells above the empty address, writing at each the name of the element whose rank is one below the cell's.

theorem DescriptiveComplexity.wideRank_lowCell_le {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (u : A) : wideRank ((lowFile h).cell u) ≤ Nat.card A

The file at the bottom lies in the initial stretch of n + 1 addresses: everything the machine keeps above that stretch is out of its way.