Roaming: what a wide machine may do between its phases

DescriptiveComplexity.WideAcceptSpace and DescriptiveComplexity.DWideAcceptSpace put no bound on the length of a run: acceptance is Relation.ReflTransGen of the step relation, with no count anywhere. So their programs may roam – sweep up, sweep back down, and start again, as often as they like. DescriptiveComplexity.WideAccept counts its steps against the number of addresses, so its programs roam on a budget: as many phases as they like, provided the lengths add up to less than the number of addresses.

That is a different, and much larger, programming model than a single sweep, and this file is its interface. Every phase is stated twice – once with a budget (DescriptiveComplexity.TMData.ReachesIn, which composes by adding) and once without (Relation.ReflTransGen, its erasure) – so that the clocked and the space-bounded programs share their phases and differ only in whether the sum is taken:

• a phase sweeping up a stretch of addresses – DescriptiveComplexity.reachesIn_of_wideUp, erased as DescriptiveComplexity.reaches_of_wideUp;
• a phase sweeping back down one – DescriptiveComplexity.reachesIn_of_wideDown, erased as DescriptiveComplexity.reaches_of_wideDown;
• a phase running a whole subroutine per address – DescriptiveComplexity.reachesIn_of_wideRounds, erased as DescriptiveComplexity.reaches_of_wideRounds;
• a run that ends accepting – DescriptiveComplexity.accepts_of_wideRoam, erased as DescriptiveComplexity.acceptsSpace_of_wideRoam.

The third is the one an outer loop is written with, and the one whose two readings differ most: the budgeted form charges a round w steps and the whole phase the product of w with the number of addresses crossed, while the erased form charges nothing, which is what lets a space-bounded program iterate a fixed point through exponentially many stages.

On top of them sits the primitive a roaming program actually spends its time on – the scan, DescriptiveComplexity.reaches_scanRight and DescriptiveComplexity.reaches_scanLeft: hold the state, rewrite every symbol by itself, and walk until the cell where the scanning transition is no longer offered. A scan leaves the tape exactly as it found it, which is why its statement mentions one tape and not two, and it is how a program that cannot read the digits of its own address nevertheless finds its way back to a cell it has marked.

A program does not know which cell will stop its scan, only that one will, so the form it uses is DescriptiveComplexity.reaches_scanRight_least (and DescriptiveComplexity.reaches_scanLeft_greatest): the machine arrives at the first stopping cell and learns, on arrival, that nothing it passed was one. The extremum is taken there, once, so no phase of a program has to name the address a mark sits at.

The rank of an address

Every phase below is stated twice: once with a budget (DescriptiveComplexity.TMData.ReachesIn), which is what a clocked program needs, and once without (Relation.ReflTransGen), which is the erasure a space-bounded one uses. The budgets are all differences of ranks: the number of addresses strictly below a given one, which is exactly the number of steps a machine stepping once per increment spends reaching it from the empty address.

noncomputable def DescriptiveComplexity.wideRank {A : Type} [FirstOrder.Language.wide.Structure A] (s : A → Prop) : ℕ

The rank of an address: how many addresses lie strictly below it.

Equations

• DescriptiveComplexity.wideRank s = DescriptiveComplexity.bitRank (DescriptiveComplexity.wideData A).Le (DescriptiveComplexity.wideData A).Posn (Sum.inl s)

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

The empty address has rank zero: a program starts with nothing spent.

theorem DescriptiveComplexity.wideRank_incr {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {s t : A → Prop} (hi : WMIncr WMLe s t) : wideRank t = wideRank s + 1

Rank increases by one along an increment, which is what makes a difference of ranks a step count.

theorem DescriptiveComplexity.wideRank_mono {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {s t : A → Prop} (hle : WMSetLe WMLe s t) : wideRank s ≤ wideRank t

Rank is monotone along the address order: a budget stated at one address covers every address below it, which is how a phase whose stopping cell is unknown is charged against a known ceiling.

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

Rank is below the clock: the machine's step bound counts the addresses, so a program that sweeps the whole tape once is affordable and the arithmetic never leaves ℕ.

def DescriptiveComplexity.wideAddrEquiv {A : Type} [FirstOrder.Language.wide.Structure A] : { p : WPoint A // (wideData A).Posn p } ≃ (A → Prop)

The addresses are the subsets of the instance.

Equations

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

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

The clock of a wide machine is 2 ^ n. The whole arithmetic of the model: a reduction buys itself 2 ^ (|Tag| · nᵈ) steps by choosing the tags and the dimension of its interpretation, and nothing else it does changes the figure.

The size of a region

A clocked program keeps its data in the least significant blocks, so every address it visits is empty above a fixed set of positions. Such a region is much smaller than the tape, and the budget of every phase run inside it has to be charged against the region and not against the number of addresses – a bound by card_wideAddr is a bound by the clock itself, which proves nothing. The two lemmas here are what charges it: the addresses supported on a set of positions are that set's subsets, so an address supported there has rank below 2 ^ its size.

theorem DescriptiveComplexity.card_addr_supported {A : Type} [Finite A] (Q : A → Prop) : Nat.card { s : A → Prop // ∀ (x : A), s x → Q x } = 2 ^ Nat.card { x : A // Q x }

The addresses supported on a set of positions are its subsets.

theorem DescriptiveComplexity.wideRank_lt_two_pow_supported {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {Q s : A → Prop} (hclosed : ∀ (t : A → Prop), WMSetLe WMLe t s → ∀ (x : A), t x → Q x) : wideRank s < 2 ^ Nat.card { x : A // Q x }

An address of a region has rank below the region's size: if every address at or below s is empty off Q, then fewer than 2 ^ #Q addresses lie below s, since they are distinct subsets of Q and s is one more. This is the bound a clocked phase is charged against.

theorem DescriptiveComplexity.card_avoid_positions {T V : Type} [Finite T] [Finite V] (H : T → Prop) : Nat.card { p : T × V // ¬H p.1 } = Nat.card { τ : T // ¬H τ } * Nat.card V

The region's size, in the program's own numbers: the positions outside a set of blocks are one per surviving block and per tuple, so their number is k · m – which is the shape the clock compares against (DescriptiveComplexity.Draw.Data.nexTotal_lt_two_pow').

theorem DescriptiveComplexity.wideRank_lt_two_pow_avoids {T V : Type} [Finite T] [Finite V] [FirstOrder.Language.wide.Structure (T × V)] {LeT : T → T → Prop} {LeV : V → V → Prop} (hT : IsLinOrd LeT) (hV : IsLinOrd LeV) (hord : ∀ (x y : T × V), WMLe x y ↔ lexRel LeT LeV x y) {H : T → Prop} (hdown : ∀ (τ σ : T), LeT τ σ → H σ → H τ) {s : T × V → Prop} (hs : wmAvoids H s) : wideRank s < 2 ^ Nat.card { p : T × V // ¬H p.1 }

The size of the working region: at a universe drawn as blocks of tuples, an address whose blocks in a downward-closed set H are empty has rank below 2 ^ the number of positions outside H. That is the region a clocked program works in – DescriptiveComplexity.wmAvoids_of_wmSetLe is why it is an initial stretch – and this is what every phase run inside it is charged against.

def DescriptiveComplexity.wideLift {A : Type} (conf : (A → Prop) → Config (WPoint A)) : WPoint A → Config (WPoint A)

A family of configurations indexed by the addresses, read on the whole universe of the machine. Off the addresses the value is irrelevant – a phase never looks – so it repeats the one at the empty address.

Equations

• DescriptiveComplexity.wideLift conf (Sum.inl s) = conf s
• DescriptiveComplexity.wideLift conf (Sum.inr val) = conf fun (x : A) => False

@[simp]

theorem DescriptiveComplexity.wideLift_addr {A : Type} (conf : (A → Prop) → Config (WPoint A)) (s : A → Prop) : wideLift conf (Sum.inl s) = conf s

The two directions of a phase

theorem DescriptiveComplexity.reachesIn_of_wideUp {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : (A → Prop) → Config (WPoint A)} {s₀ s₁ : A → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (s t : A → Prop), WMIncr WMLe s t → WMSetLe WMLe s₀ s → WMSetLe WMLe t s₁ → (wideData A).Step (conf s) (conf t)) : (wideData A).ReachesIn (wideRank s₁ - wideRank s₀) (conf s₀) (conf s₁)

A phase sweeping up. Give the intended configuration at each address of a stretch and one step between each address of it and its increment; the machine then runs from the bottom of the stretch to the top.

This is DescriptiveComplexity.stepsIn_of_wideSweep with the count relaxed to a budget and the stretch bounded at both ends: a roaming program's phases stop where the next one begins, and the transitions carrying them need not exist beyond.

theorem DescriptiveComplexity.reaches_of_wideUp {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : (A → Prop) → Config (WPoint A)} {s₀ s₁ : A → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (s t : A → Prop), WMIncr WMLe s t → WMSetLe WMLe s₀ s → WMSetLe WMLe t s₁ → (wideData A).Step (conf s) (conf t)) : Relation.ReflTransGen (wideData A).Step (conf s₀) (conf s₁)

A phase sweeping up, the budget forgotten.

theorem DescriptiveComplexity.reachesIn_of_wideDown {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : (A → Prop) → Config (WPoint A)} {s₀ s₁ : A → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (s t : A → Prop), WMIncr WMLe s t → WMSetLe WMLe s₀ s → WMSetLe WMLe t s₁ → (wideData A).Step (conf t) (conf s)) : (wideData A).ReachesIn (wideRank s₁ - wideRank s₀) (conf s₁) (conf s₀)

A phase sweeping back down. The mirror of DescriptiveComplexity.reachesIn_of_wideUp: each address of the stretch carries a step from its increment, and the machine runs from the top of the stretch to the bottom, for the same price.

theorem DescriptiveComplexity.reaches_of_wideDown {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : (A → Prop) → Config (WPoint A)} {s₀ s₁ : A → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (s t : A → Prop), WMIncr WMLe s t → WMSetLe WMLe s₀ s → WMSetLe WMLe t s₁ → (wideData A).Step (conf t) (conf s)) : Relation.ReflTransGen (wideData A).Step (conf s₁) (conf s₀)

A phase sweeping back down, the budget forgotten.

A phase that does work at every address

DescriptiveComplexity.reaches_of_wideUp asks for one step per address, which is all a scan needs and all a machine on a clock can afford. A roaming program's outer loops are not like that: at each address it runs a whole subroutine – walk to the register file, increment the mirror, walk back – and only then moves on. So the round, not the step, is the unit.

theorem DescriptiveComplexity.reachesIn_of_wideRounds {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : (A → Prop) → Config (WPoint A)} {s₀ s₁ : A → Prop} {w : ℕ} (hround : ∀ (s t : A → Prop), WMIncr WMLe s t → WMSetLe WMLe s₀ s → WMSetLe WMLe t s₁ → (wideData A).ReachesIn w (conf s) (conf t)) (s : A → Prop) : WMSetLe WMLe s₀ s → WMSetLe WMLe s s₁ → (wideData A).ReachesIn ((wideRank s - wideRank s₀) * w) (conf s₀) (conf s)

A phase that runs a subroutine at every address. Give the intended configuration at each address of a stretch and, between each address and its increment, a run of at most w steps rather than a single step; the machine then gets from the bottom of the stretch to the top, and pays w for each address it crossed.

This is the shape of every outer loop of a wide program – seeking an address, sweeping a stage of a fixed-point iteration, comparing two tracks of the tape – and the product is what a clock reads: a program is affordable when the rounds it runs, times the width of one, stays below the number of addresses. A space-bounded program ignores the product (DescriptiveComplexity.reaches_of_wideRounds), which is what lets it iterate a fixed point.

theorem DescriptiveComplexity.reaches_of_wideRounds {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {conf : (A → Prop) → Config (WPoint A)} {s₀ s₁ : A → Prop} (hround : ∀ (s t : A → Prop), WMIncr WMLe s t → WMSetLe WMLe s₀ s → WMSetLe WMLe t s₁ → Relation.ReflTransGen (wideData A).Step (conf s) (conf t)) (s : A → Prop) : WMSetLe WMLe s₀ s → WMSetLe WMLe s s₁ → Relation.ReflTransGen (wideData A).Step (conf s₀) (conf s)

A phase that runs a subroutine at every address, the budget forgotten: each round is a run of any length whatever, which is what only a space-bounded program can afford.

theorem DescriptiveComplexity.holds_of_wideRounds {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {Q : (A → Prop) → Prop} {s₀ s₁ : A → Prop} (hbase : Q s₀) (hround : ∀ (s t : A → Prop), WMIncr WMLe s t → WMSetLe WMLe s₀ s → WMSetLe WMLe t s₁ → Q s → Q t) (s : A → Prop) : WMSetLe WMLe s₀ s → WMSetLe WMLe s s₁ → Q s

What a sweep leaves behind, address by address. The semantic twin of DescriptiveComplexity.reaches_of_wideRounds, at the same measure and the same stretch: a property of the addresses that holds at the bottom and is carried across each increment holds everywhere the sweep has been.

reaches_of_wideRounds says the machine gets to every address of the stretch; this says what is true when it does – the two are used together, the run theorem consuming the round's machine hypothesis and this one the round's tape hypothesis.

The accumulator of a sweep

A sweep that is asking a question of every address – do these two tracks agree everywhere? – carries one bit across exponentially many rounds, and since it sweeps upwards that bit is a function of the prefix: of the addresses strictly below the one it has reached. This is the address-scale twin of DescriptiveComplexity.accState, which does the same for a walk of the register file, and it is what the comparison sweep of a fixed-point program is written with.

noncomputable def DescriptiveComplexity.sweepState {A : Type} [FirstOrder.Language.wide.Structure A] (P : (A → Prop) → Prop) (qy qn : A) (w : A → Prop) : A

The state a sweep is in on arriving at an address: the first state exactly when the property holds at every address strictly below.

Equations

• DescriptiveComplexity.sweepState P qy qn w = if ∀ (r : A → Prop), DescriptiveComplexity.WMSetLt DescriptiveComplexity.WMLe r w → P r then qy else qn

noncomputable def DescriptiveComplexity.sweepStateAfter {A : Type} [FirstOrder.Language.wide.Structure A] (P : (A → Prop) → Prop) (qy qn : A) (w : A → Prop) : A

The state a sweep is in on leaving an address: the same with that address taken into account.

Equations

• DescriptiveComplexity.sweepStateAfter P qy qn w = if ∀ (r : A → Prop), DescriptiveComplexity.WMSetLe DescriptiveComplexity.WMLe r w → P r then qy else qn

theorem DescriptiveComplexity.sweepStateAfter_succ {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {P : (A → Prop) → Prop} {qy qn : A} (h : IsLinOrd WMLe) {w w' : A → Prop} (hi : WMIncr WMLe w w') : sweepStateAfter P qy qn w = sweepState P qy qn w'

Leaving one address is arriving at the next, which is what makes the two definitions one accumulator.

theorem DescriptiveComplexity.sweepState_bot {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {P : (A → Prop) → Prop} {qy qn : A} (h : IsLinOrd WMLe) : (sweepState P qy qn fun (x : A) => False) = qy

A sweep starts in the first state: nothing lies below the empty address.

theorem DescriptiveComplexity.sweepStateAfter_pos {A : Type} [FirstOrder.Language.wide.Structure A] {P : (A → Prop) → Prop} {qy qn : A} {w : A → Prop} (hall : ∀ (r : A → Prop), WMSetLe WMLe r w → P r) : sweepStateAfter P qy qn w = qy

A sweep that saw no failure ends in the first state.

theorem DescriptiveComplexity.sweepStateAfter_neg {A : Type} [FirstOrder.Language.wide.Structure A] {P : (A → Prop) → Prop} {qy qn : A} {w r : A → Prop} (hle : WMSetLe WMLe r w) (hP : ¬P r) : sweepStateAfter P qy qn w = qn

A sweep that saw a failure ends in the second state.

The scan

theorem DescriptiveComplexity.wmSetLt_of_wmIncr_le {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {r r' t : A → Prop} (hi : WMIncr WMLe r r') (hub : WMSetLe WMLe r' t) : WMSetLt WMLe r t

An address whose increment is at or below a bound is strictly below it: the side condition a rightward scan step needs.

theorem DescriptiveComplexity.wmSetLt_of_le_wmIncr {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {t r r' : A → Prop} (hlb : WMSetLe WMLe t r) (hi : WMIncr WMLe r r') : WMSetLt WMLe t r'

An address at or below one whose increment is taken is strictly below that increment: the side condition a leftward scan step needs.

theorem DescriptiveComplexity.reachesIn_scanRight {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {s t : A → Prop} (hle : WMSetLe WMLe s t) (hstep : ∀ (r : A → Prop), WMSetLe WMLe s r → WMSetLt WMLe r t → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : (wideData A).ReachesIn (wideRank t - wideRank s) { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

Scanning right. In a fixed state, at every cell from s up to but not including t, some transition of the instance rewrites the symbol by itself and moves right; the machine then walks from s to t, leaving state and tape as it found them.

This is how a program navigates: it cannot read the digits of the address it is on, so it writes a marker in the cell it means to come back to and scans until the scanning transition is withheld – at the marker, which is the only symbol the hypothesis is not asked about.

theorem DescriptiveComplexity.reaches_scanRight {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {s t : A → Prop} (hle : WMSetLe WMLe s t) (hstep : ∀ (r : A → Prop), WMSetLe WMLe s r → WMSetLt WMLe r t → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

Scanning right, the budget forgotten.

theorem DescriptiveComplexity.reachesIn_scanLeft {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {s t : A → Prop} (hle : WMSetLe WMLe t s) (hstep : ∀ (r : A → Prop), WMSetLt WMLe t r → WMSetLe WMLe r s → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ ¬WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : (wideData A).ReachesIn (wideRank s - wideRank t) { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

Scanning left, the same reading downwards: the transitions move left, and the machine walks from s down to t.

theorem DescriptiveComplexity.reaches_scanLeft {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {s t : A → Prop} (hle : WMSetLe WMLe t s) (hstep : ∀ (r : A → Prop), WMSetLt WMLe t r → WMSetLe WMLe r s → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ ¬WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

Scanning left, the budget forgotten.

Scanning to the first cell that stops the scan

The form a program uses in practice: it does not know which cell will stop its scan, only that some cell will, and it needs the arrival to come with the promise that nothing before it stopped.

theorem DescriptiveComplexity.reachesIn_scanRight_least {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t) (hstep : ∀ (r : A → Prop), WMSetLe WMLe s r → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe r t) → ¬Stop r → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t ∧ (∀ (r : A → Prop), WMSetLe WMLe s r → WMSetLt WMLe r t → ¬Stop r) ∧ (wideData A).ReachesIn (wideRank t - wideRank s) { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

A rightward scan arrives at the first cell that stops it. Given that some cell at or above s stops the scan, and that every cell at or above s which does not stop it offers the scanning transition, the machine reaches the least stopping cell – and learns, on arrival, that no cell it passed was one.

The caller never constructs that cell: this is where the extremum is taken, once, so a program's phases are stated about the marks they look for and not about the addresses those marks sit at. The budget is stated at the cell reached, and a caller that knows a ceiling for its marks charges the scan against that ceiling by DescriptiveComplexity.wideRank_mono and DescriptiveComplexity.TMData.ReachesIn.mono.

theorem DescriptiveComplexity.reaches_scanRight_least {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t) (hstep : ∀ (r : A → Prop), WMSetLe WMLe s r → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe r t) → ¬Stop r → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe s t ∧ (∀ (r : A → Prop), WMSetLe WMLe s r → WMSetLt WMLe r t → ¬Stop r) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

A rightward scan arrives at the first cell that stops it, the budget forgotten.

theorem DescriptiveComplexity.reachesIn_scanLeft_greatest {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s) (hstep : ∀ (r : A → Prop), WMSetLe WMLe r s → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t r) → ¬Stop r → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ ¬WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s ∧ (∀ (r : A → Prop), WMSetLt WMLe t r → WMSetLe WMLe r s → ¬Stop r) ∧ (wideData A).ReachesIn (wideRank s - wideRank t) { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

A leftward scan arrives at the first cell that stops it, the same reading downwards: the greatest stopping cell at or below s.

theorem DescriptiveComplexity.reaches_scanLeft_greatest {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q : A} {tp : WPoint A → WPoint A} {Stop : (A → Prop) → Prop} {s : A → Prop} (hex : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s) (hstep : ∀ (r : A → Prop), WMSetLe WMLe r s → (∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t r) → ¬Stop r → ∃ (τ : A) (a : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q ∧ WMWrite τ a ∧ ¬WMRight τ ∧ tp (Sum.inl r) = Sum.inr a) : ∃ (t : A → Prop), Stop t ∧ WMSetLe WMLe t s ∧ (∀ (r : A → Prop), WMSetLt WMLe t r → WMSetLe WMLe r s → ¬Stop r) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := tp } { state := Sum.inr q, head := Sum.inl t, tape := tp }

A leftward scan arrives at the first cell that stops it, the budget forgotten.

A run that accepts

theorem DescriptiveComplexity.acceptsSpace_of_wideRoam {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (hno : ∀ (x y : A), ¬WMInp x y) {q₀ b : A} (hq : WMStart q₀) (hb : WMBlank b) {c : Config (WPoint A)} (hreach : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := fun (x : WPoint A) => Sum.inr b } c) {qa : A} (hstate : c.state = Sum.inr qa) (hacc : WMAcc qa) : (wideData A).AcceptsSpace

A roaming program accepts. Start on the empty address in a start state with a blank tape – the initial configuration a reduction that leaves wmInp empty has (DescriptiveComplexity.isInit_wide) – reach any configuration by any chain of phases, and end in an accepting state.

There is no clock and no count: this is the whole of DescriptiveComplexity.WideAcceptSpace for a program, and the reason the space-bounded halves of the wide catalog are the ones a roaming program can reach.

theorem DescriptiveComplexity.accepts_of_wideRoam {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (hno : ∀ (x y : A), ¬WMInp x y) {q₀ b : A} (hq : WMStart q₀) (hb : WMBlank b) {n : ℕ} {c : Config (WPoint A)} (hreach : (wideData A).ReachesIn n { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := fun (x : WPoint A) => Sum.inr b } c) (hlt : n < Nat.card { p : WPoint A // (wideData A).Posn p }) {qa : A} (hstate : c.state = Sum.inr qa) (hacc : WMAcc qa) : (wideData A).Accepts

A clocked program accepts. The same run, with its budget kept and compared once with the clock: DescriptiveComplexity.WideAccept allows strictly fewer steps than there are addresses, so a program is affordable exactly when the sum of its phases stays below that.

The budget is the only difference between this and DescriptiveComplexity.acceptsSpace_of_wideRoam, and it is the whole difference between the two halves of the wide catalog: a program that iterates a fixed point has no bound to offer, and one that guesses a certificate and checks it in a fixed number of passes has.

theorem DescriptiveComplexity.accepts_of_wideRoam_lt_two_pow {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (hno : ∀ (x y : A), ¬WMInp x y) {q₀ b : A} (hq : WMStart q₀) (hb : WMBlank b) {n : ℕ} {c : Config (WPoint A)} (hreach : (wideData A).ReachesIn n { state := Sum.inr q₀, head := Sum.inl fun (x : A) => False, tape := fun (x : WPoint A) => Sum.inr b } c) (hlt : n < 2 ^ Nat.card A) {qa : A} (hstate : c.state = Sum.inr qa) (hacc : WMAcc qa) : (wideData A).Accepts

A clocked program accepts, with its budget compared against the count rather than against the number of positions: the same statement as DescriptiveComplexity.accepts_of_wideRoam in the form a program's arithmetic actually produces, since what a reduction controls is n – the size of the universe it draws – and not the subtype of positions.