Incrementing the mirror

The first real subroutine of a wide machine, and the one every address computation goes through. A program keeps a mirror of the address it is working on – one bit per element, in a track over its register file (DescriptiveComplexity.IxFile) – because the head cannot read the digits of its own address. Moving the working cell one to the right means adding one to the mirror, and adding one is:

walk the register file downwards, clearing the digits that are set; at the first digit that is clear, set it and stop clearing.

That is the binary increment of DescriptiveComplexity.Problems.Wide.Increment, whose least significant digit is the WMLe-greatest element – which is why the walk runs downwards – and DescriptiveComplexity.IxFile.reachesIn_mirrorIncr says the program computes it: from the last register in the carrying state with the mirror at s, the machine arrives below the first register in the stopped state with the mirror at t, for the unique t with WMIncr WMLe s t. It costs one move per register plus the step off the file, so a caller that is counting bounds the moves and gets the product.

What a caller supplies

The tape is given as a function of the mirror, tapeOf m, with one coherence condition: changing the mirror at one element changes the tape at that element's cell and nowhere else. Everything else a program keeps on its tape is therefore carried along untouched, and no track discipline has to be fixed here. Three transition families do the work – clear a set digit and keep carrying, set a clear digit and stop, rewrite anything once stopped – plus the scanning transitions that carry the head between consecutive registers.

The states are the caller's: qc for carrying, and a family qd for stopped. The family is the point – the machine ends in qd u₀ where u₀ is the carry position, the digit the increment set, and the conclusion says so along with its characterization. A state may hold an element, so reporting the carry costs nothing in the control, and it is what the fold of DescriptiveComplexity.Problems.Wide.Fold needs: which block rolled over decides which accumulators reset. So the caller reads both “the increment is finished” and “here is where it carried” off the state, and neither off the tape.

The other writing pass

DescriptiveComplexity.IxFile.reachesIn_fileWrite is the same walk with nothing accumulated: one state throughout, and every register simply given its new digit. Copying the mirror into a spare register, clearing a track and loading a computed value are all that pass. Together with the read-only pass of DescriptiveComplexity.Problems.Wide.Test these are the three shapes a program's register work comes in – write with an accumulator, write without one, read with one – and nothing below them is ever a case split again.

The mirror during the walk

What the increment does to a digit

Processing one register

The whole case analysis of the subroutine happens here, once: what the machine does at the register of w depends only on whether every digit above w is set and on whether the digit at w is. Everything after this is bookkeeping, and none of it is a case split.

The subroutine

theorem DescriptiveComplexity.IxFile.reachesIn_mirrorIncr {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} {s t : I → Prop} {qc : A} {qd : I → A} [Finite A] [Finite I] (F : IxFile A I ile) (h : IsLinOrd ile) (ha : IsLinOrd WMLe) (hi : WMIncr ile s t) {b : A} {w : ℕ} {tapeOf : (I → Prop) → (A → Prop) → A} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) (hcoh : ∀ (m m' : I → Prop) (u : I), (∀ (v : I), v ≠ u → (m v ↔ m' v)) → ∀ (r : A → Prop), r ≠ F.cell u → tapeOf m r = tapeOf m' r) (hone : ∀ (m : I → Prop) (u : I), m u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qc ∧ WMRead τ (tapeOf m (F.cell u)) ∧ WMDst τ qc ∧ WMWrite τ (tapeOf (fun (v : I) => m v ∧ v ≠ u) (F.cell u)) ∧ ¬WMRight τ) (hzero : ∀ (m : I → Prop) (u : I), ¬m u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qc ∧ WMRead τ (tapeOf m (F.cell u)) ∧ WMDst τ (qd u) ∧ WMWrite τ (tapeOf (fun (v : I) => m v ∨ v = u) (F.cell u)) ∧ ¬WMRight τ) (hkeep : ∀ (u : I) (m : I → Prop) (v : I), ∃ (τ : A), WMTr τ ∧ WMSrc τ (qd u) ∧ WMRead τ (tapeOf m (F.cell v)) ∧ WMDst τ (qd u) ∧ WMWrite τ (tapeOf m (F.cell v)) ∧ ¬WMRight τ) (hskip : ∀ (q : A), (q = qc ∨ ∃ (u : I), q = qd u) → ∀ (m : I → Prop) (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m r) ∧ WMDst τ q ∧ WMWrite τ (tapeOf m r) ∧ ¬WMRight τ) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (u₀ : I) (p : A → Prop), (¬s u₀ ∧ ∀ (v : I), WMLt ile u₀ v → s v) ∧ WMIncr WMLe p (F.cell bot) ∧ (wideData A).ReachesIn ((ixRank ile top - ixRank ile bot) * w + 1) { state := Sum.inr qc, head := Sum.inl (F.cell top), tape := wideTape (tapeOf s) b } { state := Sum.inr (qd u₀), head := Sum.inl p, tape := wideTape (tapeOf t) b }

The mirror increment. From the last register of the file, carrying, with the mirror at s, the machine walks down the file and arrives just below the first register, stopped, with the mirror at the increment of s.

The three transition families do the arithmetic and the scanning ones carry the head between consecutive registers; the coherence condition hcoh is what says the rest of the tape – whatever else the program keeps there – comes through untouched. The cost is one move per register, each bounded by w, plus the step off the file.

theorem DescriptiveComplexity.IxFile.reaches_mirrorIncr {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} {s t : I → Prop} {qc : A} {qd : I → A} [Finite A] [Finite I] (F : IxFile A I ile) (h : IsLinOrd ile) (ha : IsLinOrd WMLe) (hi : WMIncr ile s t) {b : A} {tapeOf : (I → Prop) → (A → Prop) → A} (hcoh : ∀ (m m' : I → Prop) (u : I), (∀ (v : I), v ≠ u → (m v ↔ m' v)) → ∀ (r : A → Prop), r ≠ F.cell u → tapeOf m r = tapeOf m' r) (hone : ∀ (m : I → Prop) (u : I), m u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qc ∧ WMRead τ (tapeOf m (F.cell u)) ∧ WMDst τ qc ∧ WMWrite τ (tapeOf (fun (v : I) => m v ∧ v ≠ u) (F.cell u)) ∧ ¬WMRight τ) (hzero : ∀ (m : I → Prop) (u : I), ¬m u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qc ∧ WMRead τ (tapeOf m (F.cell u)) ∧ WMDst τ (qd u) ∧ WMWrite τ (tapeOf (fun (v : I) => m v ∨ v = u) (F.cell u)) ∧ ¬WMRight τ) (hkeep : ∀ (u : I) (m : I → Prop) (v : I), ∃ (τ : A), WMTr τ ∧ WMSrc τ (qd u) ∧ WMRead τ (tapeOf m (F.cell v)) ∧ WMDst τ (qd u) ∧ WMWrite τ (tapeOf m (F.cell v)) ∧ ¬WMRight τ) (hskip : ∀ (q : A), (q = qc ∨ ∃ (u : I), q = qd u) → ∀ (m : I → Prop) (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m r) ∧ WMDst τ q ∧ WMWrite τ (tapeOf m r) ∧ ¬WMRight τ) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (u₀ : I) (p : A → Prop), (¬s u₀ ∧ ∀ (v : I), WMLt ile u₀ v → s v) ∧ WMIncr WMLe p (F.cell bot) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr qc, head := Sum.inl (F.cell top), tape := wideTape (tapeOf s) b } { state := Sum.inr (qd u₀), head := Sum.inl p, tape := wideTape (tapeOf t) b }

The mirror increment, the budget forgotten.

Overwriting a track

The same walk with nothing accumulated: the state never changes, and every register is simply given its new digit. Copying the mirror into a spare register, clearing a track and loading a computed value are all this pass.

theorem DescriptiveComplexity.IxFile.reachesIn_fileWrite {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} {s t : I → Prop} [Finite A] [Finite I] (F : IxFile A I ile) (h : IsLinOrd ile) (ha : IsLinOrd WMLe) {b q : A} {w : ℕ} {tapeOf : (I → Prop) → (A → Prop) → A} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) (hcoh : ∀ (m m' : I → Prop) (u : I), (∀ (v : I), v ≠ u → (m v ↔ m' v)) → ∀ (r : A → Prop), r ≠ F.cell u → tapeOf m r = tapeOf m' r) (hstep : ∀ (m : I → Prop) (u : I), ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m (F.cell u)) ∧ WMDst τ q ∧ WMWrite τ (tapeOf (fun (v : I) => v = u ∧ t v ∨ v ≠ u ∧ m v) (F.cell u)) ∧ ¬WMRight τ) (hskip : ∀ (m : I → Prop) (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m r) ∧ WMDst τ q ∧ WMWrite τ (tapeOf m r) ∧ ¬WMRight τ) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (p : A → Prop), WMIncr WMLe p (F.cell bot) ∧ (wideData A).ReachesIn ((ixRank ile top - ixRank ile bot) * w + 1) { state := Sum.inr q, head := Sum.inl (F.cell top), tape := wideTape (tapeOf s) b } { state := Sum.inr q, head := Sum.inl p, tape := wideTape (tapeOf t) b }

Overwriting a track. A pass down the file in a single state, replacing the track's digit at every register: the machine starts at the last register with the track at s and arrives just below the first register with it at t.

Since nothing is accumulated, t is arbitrary – the caller's transitions say what to write at each register, and may read the old digit to decide.

theorem DescriptiveComplexity.IxFile.reaches_fileWrite {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} {s t : I → Prop} [Finite A] [Finite I] (F : IxFile A I ile) (h : IsLinOrd ile) (ha : IsLinOrd WMLe) {b q : A} {tapeOf : (I → Prop) → (A → Prop) → A} (hcoh : ∀ (m m' : I → Prop) (u : I), (∀ (v : I), v ≠ u → (m v ↔ m' v)) → ∀ (r : A → Prop), r ≠ F.cell u → tapeOf m r = tapeOf m' r) (hstep : ∀ (m : I → Prop) (u : I), ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m (F.cell u)) ∧ WMDst τ q ∧ WMWrite τ (tapeOf (fun (v : I) => v = u ∧ t v ∨ v ≠ u ∧ m v) (F.cell u)) ∧ ¬WMRight τ) (hskip : ∀ (m : I → Prop) (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m r) ∧ WMDst τ q ∧ WMWrite τ (tapeOf m r) ∧ ¬WMRight τ) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (p : A → Prop), WMIncr WMLe p (F.cell bot) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (F.cell top), tape := wideTape (tapeOf s) b } { state := Sum.inr q, head := Sum.inl p, tape := wideTape (tapeOf t) b }

Overwriting a track, the budget forgotten.

The same, at the file the input channel marks

theorem DescriptiveComplexity.reaches_mirrorIncr {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {s t : A → Prop} {qc : A} {qd : A → A} (h : IsLinOrd WMLe) (hi : WMIncr WMLe s t) {b : A} {tapeOf : (A → Prop) → (A → Prop) → A} (hcoh : ∀ (m m' : A → Prop) (u : A), (∀ (v : A), v ≠ u → (m v ↔ m' v)) → ∀ (r : A → Prop), r ≠ wmSeg u → tapeOf m r = tapeOf m' r) (hone : ∀ (m : A → Prop) (u : A), m u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qc ∧ WMRead τ (tapeOf m (wmSeg u)) ∧ WMDst τ qc ∧ WMWrite τ (tapeOf (fun (v : A) => m v ∧ v ≠ u) (wmSeg u)) ∧ ¬WMRight τ) (hzero : ∀ (m : A → Prop) (u : A), ¬m u → ∃ (τ : A), WMTr τ ∧ WMSrc τ qc ∧ WMRead τ (tapeOf m (wmSeg u)) ∧ WMDst τ (qd u) ∧ WMWrite τ (tapeOf (fun (v : A) => m v ∨ v = u) (wmSeg u)) ∧ ¬WMRight τ) (hkeep : ∀ (u : A) (m : A → Prop) (w : A), ∃ (τ : A), WMTr τ ∧ WMSrc τ (qd u) ∧ WMRead τ (tapeOf m (wmSeg w)) ∧ WMDst τ (qd u) ∧ WMWrite τ (tapeOf m (wmSeg w)) ∧ ¬WMRight τ) (hskip : ∀ (q : A), (q = qc ∨ ∃ (u : A), q = qd u) → ∀ (m r : A → Prop), (∃ (x : A), WMSetLe WMLe (wmSeg x) r) → (∀ (x : A), r ≠ wmSeg x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m r) ∧ WMDst τ q ∧ WMWrite τ (tapeOf m r) ∧ ¬WMRight τ) {top bot : A} (htop : ∀ (v : A), WMLe v top) (hbot : ∀ (v : A), WMLe bot v) : ∃ (u₀ : A) (p : A → Prop), (¬s u₀ ∧ ∀ (v : A), WMLt WMLe u₀ v → s v) ∧ WMIncr WMLe p (wmSeg bot) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr qc, head := Sum.inl (wmSeg top), tape := wideTape (tapeOf s) b } { state := Sum.inr (qd u₀), head := Sum.inl p, tape := wideTape (tapeOf t) b }

The mirror increment over the file the input channel marks.

theorem DescriptiveComplexity.reaches_fileWrite {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {s t : A → Prop} (h : IsLinOrd WMLe) {b q : A} {tapeOf : (A → Prop) → (A → Prop) → A} (hcoh : ∀ (m m' : A → Prop) (u : A), (∀ (v : A), v ≠ u → (m v ↔ m' v)) → ∀ (r : A → Prop), r ≠ wmSeg u → tapeOf m r = tapeOf m' r) (hstep : ∀ (m : A → Prop) (u : A), ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m (wmSeg u)) ∧ WMDst τ q ∧ WMWrite τ (tapeOf (fun (v : A) => v = u ∧ t v ∨ v ≠ u ∧ m v) (wmSeg u)) ∧ ¬WMRight τ) (hskip : ∀ (m r : A → Prop), (∃ (x : A), WMSetLe WMLe (wmSeg x) r) → (∀ (x : A), r ≠ wmSeg x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (tapeOf m r) ∧ WMDst τ q ∧ WMWrite τ (tapeOf m r) ∧ ¬WMRight τ) {top bot : A} (htop : ∀ (v : A), WMLe v top) (hbot : ∀ (v : A), WMLe bot v) : ∃ (p : A → Prop), WMIncr WMLe p (wmSeg bot) ∧ Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (wmSeg top), tape := wideTape (tapeOf s) b } { state := Sum.inr q, head := Sum.inl p, tape := wideTape (tapeOf t) b }

Overwriting a track of the file the input channel marks.