Documentation

DescriptiveComplexity.Problems.Wide.DrawSweep

Plain sweeps: one step per address, a flag or a write #

COMPARE and COPY are plain sweeps: one step per address of a stretch, no register visits, no rounds. This file is their two shapes.

Both take their rules cell-coupled and bounded to the stretch, for the reason DrawAdv taught: a sweep whose stepping rules covered every cell could never stop. How a program's actual rules respect the bound is its own business – the intended device is a permanent end marker planted at the top of the logical interval once, at startup, since a cell of the working area is not otherwise recognizable (its tracks are stage bits like any other).

theorem DescriptiveComplexity.Draw.Prog.reachesIn_flagSweep {A R P Q W K : Type} {dd : } [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : IUniv A R P K ddProp} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {rest : (Univ A R P K ddProp)WA} {m : IProp} {Test : (Univ A R P K ddProp)Prop} {py pn : P} {f : QA} {s₀ s₁ : Univ A R P K ddProp} (hle : WMSetLe WMLe s₀ s₁) (hstepY : ∀ (r r' : Univ A R P K ddProp), WMIncr WMLe r r'WMSetLe WMLe s₀ rWMSetLe WMLe r' s₁Test rPR.HasRight py f (PR.passTracksAt cell t rest m r) py f (PR.passTracksAt cell t rest m r)) (hstepN : ∀ (r r' : Univ A R P K ddProp), WMIncr WMLe r r'WMSetLe WMLe s₀ rWMSetLe WMLe r' s₁¬Test rPR.HasRight py f (PR.passTracksAt cell t rest m r) pn f (PR.passTracksAt cell t rest m r)) (hstepP : ∀ (r r' : Univ A R P K ddProp), WMIncr WMLe r r'WMSetLe WMLe s₀ rWMSetLe WMLe r' s₁PR.HasRight pn f (PR.passTracksAt cell t rest m r) pn f (PR.passTracksAt cell t rest m r)) :
(wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (sweepState Test (PR.stElt py f) (PR.stElt pn f) s₀), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (sweepState Test (PR.stElt py f) (PR.stElt pn f) s₁), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

A sweep asking one question per cell, the verdict in the phase: from the bottom of the stretch in the passing phase, the machine arrives at the top in the phase DescriptiveComplexity.sweepState names – passing exactly when every cell strictly below passed. The three rule families are the two branches of the passing phase and the cruise of the failing one, each at the cells of the stretch only.

Dependency graph
theorem DescriptiveComplexity.Draw.Prog.reaches_flagSweep {A R P Q W K : Type} {dd : } [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : IUniv A R P K ddProp} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {rest : (Univ A R P K ddProp)WA} {m : IProp} {Test : (Univ A R P K ddProp)Prop} {py pn : P} {f : QA} {s₀ s₁ : Univ A R P K ddProp} (hle : WMSetLe WMLe s₀ s₁) (hstepY : ∀ (r r' : Univ A R P K ddProp), WMIncr WMLe r r'WMSetLe WMLe s₀ rWMSetLe WMLe r' s₁Test rPR.HasRight py f (PR.passTracksAt cell t rest m r) py f (PR.passTracksAt cell t rest m r)) (hstepN : ∀ (r r' : Univ A R P K ddProp), WMIncr WMLe r r'WMSetLe WMLe s₀ rWMSetLe WMLe r' s₁¬Test rPR.HasRight py f (PR.passTracksAt cell t rest m r) pn f (PR.passTracksAt cell t rest m r)) (hstepP : ∀ (r r' : Univ A R P K ddProp), WMIncr WMLe r r'WMSetLe WMLe s₀ rWMSetLe WMLe r' s₁PR.HasRight pn f (PR.passTracksAt cell t rest m r) pn f (PR.passTracksAt cell t rest m r)) :
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (sweepState Test (PR.stElt py f) (PR.stElt pn f) s₀), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (sweepState Test (PR.stElt py f) (PR.stElt pn f) s₁), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

A flag sweep, the budget forgotten.

Dependency graph
theorem DescriptiveComplexity.Draw.Prog.reachesIn_writeSweepSt {A R P Q W K : Type} {dd : } [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : IUniv A R P K ddProp} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : IProp} {restAt : (Univ A R P K ddProp)(Univ A R P K ddProp)WA} {ph : (Univ A R P K ddProp)P} {fc : (Univ A R P K ddProp)QA} {s₀ s₁ : Univ A R P K ddProp} (hle : WMSetLe WMLe s₀ s₁) (hframe : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁∀ (r : Univ A R P K ddProp), r srestAt u r = restAt s r) (hstep : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁PR.HasRight (ph s) (fc s) (PR.passTracksAt cell t (restAt s) m s) (ph u) (fc u) (PR.passTracksAt cell t (restAt u) m s)) :
(wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt (ph s₀) (fc s₀)), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t (restAt s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (ph s₁) (fc s₁)), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t (restAt s₁) m) (PR.syElt PR.blank) }

A writing sweep carrying a pointer. The same sweep with the state's pointer advancing with the head: at the cell s the program stands in the phase p at the pointer fc s, and the rule that rewrites s leaves it at fc u. The phase does not move, so this is still one rule family.

A pointer that varies is what lets a sweep write something different in every cell. The tape a phase like this starts from is blank, so the rule has nothing to read that distinguishes one cell from the next; what distinguishes them is the pointer, whose slots hold elements of the instance. That is how a program lays down a pattern indexed by the elements – its own register file, for instance.

Dependency graph
theorem DescriptiveComplexity.Draw.Prog.reachesIn_writeSweep {A R P Q W K : Type} {dd : } [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : IUniv A R P K ddProp} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : IProp} {restAt : (Univ A R P K ddProp)(Univ A R P K ddProp)WA} {p : P} {f : QA} {s₀ s₁ : Univ A R P K ddProp} (hle : WMSetLe WMLe s₀ s₁) (hframe : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁∀ (r : Univ A R P K ddProp), r srestAt u r = restAt s r) (hstep : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁PR.HasRight p f (PR.passTracksAt cell t (restAt s) m s) p f (PR.passTracksAt cell t (restAt u) m s)) :
(wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt p f), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t (restAt s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t (restAt s₁) m) (PR.syElt PR.blank) }

A sweep rewriting each cell once: the background is a function of the frontier – everything strictly below has its new value, everything at or above its old one – and one rule per cell writes the change as the head leaves. COPY is this sweep.

Dependency graph
theorem DescriptiveComplexity.Draw.Prog.reaches_writeSweep {A R P Q W K : Type} {dd : } [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : IUniv A R P K ddProp} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : IProp} {restAt : (Univ A R P K ddProp)(Univ A R P K ddProp)WA} {p : P} {f : QA} {s₀ s₁ : Univ A R P K ddProp} (hle : WMSetLe WMLe s₀ s₁) (hframe : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁∀ (r : Univ A R P K ddProp), r srestAt u r = restAt s r) (hstep : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁PR.HasRight p f (PR.passTracksAt cell t (restAt s) m s) p f (PR.passTracksAt cell t (restAt u) m s)) :
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t (restAt s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t (restAt s₁) m) (PR.syElt PR.blank) }

A writing sweep, the budget forgotten.

Dependency graph

Installing a background #

The two phases a clocked program opens with – laying its own register file out and guessing the certificate onto its working region – are one shape: sweep a stretch replacing the background wholesale, one cell per step. The frontier form DescriptiveComplexity.midTape is what makes them a sweep rather than an induction, and the new background is a parameter, so the guessing reading is the same statement at an arbitrary choice.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_installSweep {A R P Q W K : Type} {dd : } [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : IUniv A R P K ddProp} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : IProp} {bg₀ bg₁ : (Univ A R P K ddProp)WA} {ph : (Univ A R P K ddProp)P} {fc : (Univ A R P K ddProp)QA} {s₀ s₁ : Univ A R P K ddProp} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁PR.HasRight (ph s) (fc s) (PR.passTracksAt cell t bg₀ m s) (ph u) (fc u) (PR.passTracksAt cell t bg₁ m s)) :
(wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt (ph s₀) (fc s₀)), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t (midTape bg₀ bg₁ s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (ph s₁) (fc s₁)), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t (midTape bg₀ bg₁ s₁) m) (PR.syElt PR.blank) }

A phase installing a new background over a stretch. From the bottom of the stretch with the old background everywhere, one rule per cell rewrites that cell and moves right; the run ends at the top of the stretch with the new background below it and the old one above. The pointer walks along, so the rule at a cell may write something that depends on where the head is.

Dependency graph
theorem DescriptiveComplexity.Draw.Prog.reachesIn_installOut {A R P Q W K : Type} {dd : } [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {cell : IUniv A R P K ddProp} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : IProp} {bg₀ bg₁ : (Univ A R P K ddProp)WA} {ph : (Univ A R P K ddProp)P} {fc : (Univ A R P K ddProp)QA} {s₀ s₁ : Univ A R P K ddProp} (hle : WMSetLe WMLe s₀ s₁) (hbelow : ∀ (r : Univ A R P K ddProp), WMSetLt WMLe r s₀bg₁ r = bg₀ r) (habove : ∀ (r : Univ A R P K ddProp), ¬WMSetLt WMLe r s₁bg₁ r = bg₀ r) (hstep : ∀ (s u : Univ A R P K ddProp), WMIncr WMLe s uWMSetLe WMLe s₀ sWMSetLe WMLe u s₁PR.HasRight (ph s) (fc s) (PR.passTracksAt cell t bg₀ m s) (ph u) (fc u) (PR.passTracksAt cell t bg₁ m s)) :
(wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt (ph s₀) (fc s₀)), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t bg₀ m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (ph s₁) (fc s₁)), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t bg₁ m) (PR.syElt PR.blank) }

A phase installing a background that already agrees outside the stretch. The sweep only ever writes inside the stretch, so if the background it is installing is the one already there below the start and at or above the end, the run begins and ends at that background whole rather than at a frontier form. That is the shape every opening phase of a program takes: what it changes lies in a stretch, and what lies outside it was right to begin with.

Dependency graph