Kits for the plain sweeps

The kits wrapping the two plain-sweep composites of DescriptiveComplexity.Problems.Wide.DrawSweep – one step per address of a stretch, no register visits. DescriptiveComplexity.Draw.FlagSweepKit asks one question per cell with the verdict in the phase (COMPARE); DescriptiveComplexity.Draw.WriteSweepKit rewrites each cell once (COPY).

Both composites take their rules bounded to the stretch, and the kits realize the bound the way the program does: a permanent end marker ltp planted at the top of the stretch once, at startup. Every stepping rule is guarded ltp ≠ one, so the sweep has no rule at the marked cell and stops there; the caller's exit rule at ltp = one is disjoint from every rule here.

The flag sweep's shapes

inductive DescriptiveComplexity.Draw.SweepPh : Type

The phases of a flag sweep: still passing, or failed.

• py : SweepPh

  Every cell so far passed.

• pn : SweepPh

  Some cell failed.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqSweepPh : DecidableEq SweepPh

Equations

• DescriptiveComplexity.Draw.instDecidableEqSweepPh x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteSweepPh : Finite SweepPh

inductive DescriptiveComplexity.Draw.SweepRule : Type

The rule families of a flag sweep.

• yGo : SweepRule

  The cell passes: step on in the passing phase.

• yFail : SweepRule

  The cell fails: step on in the failing phase.

• nGo : SweepRule

  Cruise in the failing phase.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqSweepRule : DecidableEq SweepRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqSweepRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteSweepRule : Finite SweepRule

structure DescriptiveComplexity.Draw.FlagSweepKit (A Q W P : Type) : Type

A flag-sweep kit: the walked track, the end-marker slot, the per-cell question, and the phases.

• t : W

  The walked track.

• ltp : W

  The end-marker slot: set exactly at the top of the stretch.

• TestG : (W → A) → Prop

  The per-cell question, decided by the tracks.

• emb : SweepPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.FlagSweepKit.rule {A Q W P : Type} (κ : FlagSweepKit A Q W P) (one : A) : SweepRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.FlagSweepKit.sep {A Q W P : Type} (κ : FlagSweepKit A Q W P) (one : A) (hemb : Function.Injective κ.emb) (ρ ρ' : SweepRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → (κ.rule one ρ').guard f g → (κ.rule one ρ).srcPh = (κ.rule one ρ').srcPh → ρ = ρ'

In-shape separation.

theorem DescriptiveComplexity.Draw.FlagSweepKit.exit_disjoint {A Q W P : Type} (κ : FlagSweepKit A Q W P) (one : A) (ρ : SweepRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → g κ.ltp = one → False

Exit disjointness: no kit rule fires at the end-marked cell, in any phase – the caller's exit rules there, guarded ltp = one, are disjoint from the whole kit.

The discharge

theorem DescriptiveComplexity.Draw.FlagSweepKit.reachesIn {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} {κ : FlagSweepKit A Q W P} {rEmb : SweepRule → R} (hrules : ∀ (ρ : SweepRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {cell : Univ A R P K dd → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hneltp : κ.ltp ≠ κ.t) {rest : (Univ A R P K dd → Prop) → W → A} {m ltpAddr : Univ A R P K dd → Prop} (hltp : ∀ (r : Univ A R P K dd → Prop), rest r κ.ltp = bitVal PR.zero PR.one (r = ltpAddr)) {Test : (Univ A R P K dd → Prop) → Prop} (hcompat : ∀ (r : Univ A R P K dd → Prop), κ.TestG (PR.passTracksAt cell κ.t rest m r) ↔ Test r) {fc : Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (htp : WMSetLe WMLe s₁ ltpAddr) : (wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (sweepState Test (PR.stElt (κ.emb SweepPh.py) fc) (PR.stElt (κ.emb SweepPh.pn) fc) s₀), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (sweepState Test (PR.stElt (κ.emb SweepPh.py) fc) (PR.stElt (κ.emb SweepPh.pn) fc) s₁), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell κ.t rest m) (PR.syElt PR.blank) }

The kit runs its sweep: one step per address of the stretch, the verdict in the phase via DescriptiveComplexity.sweepState. The stretch's top must sit at or below the end marker's address.

theorem DescriptiveComplexity.Draw.FlagSweepKit.reaches {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} {κ : FlagSweepKit A Q W P} {rEmb : SweepRule → R} (hrules : ∀ (ρ : SweepRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {cell : Univ A R P K dd → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hneltp : κ.ltp ≠ κ.t) {rest : (Univ A R P K dd → Prop) → W → A} {m ltpAddr : Univ A R P K dd → Prop} (hltp : ∀ (r : Univ A R P K dd → Prop), rest r κ.ltp = bitVal PR.zero PR.one (r = ltpAddr)) {Test : (Univ A R P K dd → Prop) → Prop} (hcompat : ∀ (r : Univ A R P K dd → Prop), κ.TestG (PR.passTracksAt cell κ.t rest m r) ↔ Test r) {fc : Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (htp : WMSetLe WMLe s₁ ltpAddr) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (sweepState Test (PR.stElt (κ.emb SweepPh.py) fc) (PR.stElt (κ.emb SweepPh.pn) fc) s₀), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (sweepState Test (PR.stElt (κ.emb SweepPh.py) fc) (PR.stElt (κ.emb SweepPh.pn) fc) s₁), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell κ.t rest m) (PR.syElt PR.blank) }

The kit runs its sweep, the budget forgotten.

The write sweep's shape

inductive DescriptiveComplexity.Draw.WSweepRule : Type

The rule of a write sweep: one family, rewriting each cell as the head leaves it.

• put : WSweepRule

  Rewrite the cell and step on.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqWSweepRule : DecidableEq WSweepRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqWSweepRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteWSweepRule : Finite WSweepRule

structure DescriptiveComplexity.Draw.WriteSweepKit (A Q W P : Type) : Type

A write-sweep kit: the walked track, the end-marker slot, the per-cell rewrite as a function of the tracks, and the one phase.

• t : W

  The walked track.

• ltp : W

  The end-marker slot: set exactly at the top of the stretch.

• wrG : (W → A) → W → A

  The per-cell rewrite, computed from the tracks.

• ph : P

  The kit's phase in the program.

def DescriptiveComplexity.Draw.WriteSweepKit.rule {A Q W P : Type} (κ : WriteSweepKit A Q W P) (one : A) : WSweepRule → Rule A Q W P

The kit's rule.

Equations

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

theorem DescriptiveComplexity.Draw.WriteSweepKit.sep {A Q W P : Type} (κ : WriteSweepKit A Q W P) (one : A) (ρ ρ' : WSweepRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → (κ.rule one ρ').guard f g → (κ.rule one ρ).srcPh = (κ.rule one ρ').srcPh → ρ = ρ'

In-shape separation: one rule, nothing to separate.

theorem DescriptiveComplexity.Draw.WriteSweepKit.exit_disjoint {A Q W P : Type} (κ : WriteSweepKit A Q W P) (one : A) (ρ : WSweepRule) (f : Q → A) (g : W → A) : (κ.rule one ρ).guard f g → g κ.ltp = one → False

Exit disjointness: the single rule never fires at the end-marked cell.

The discharge

theorem DescriptiveComplexity.Draw.WriteSweepKit.reachesIn {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} {κ : WriteSweepKit A Q W P} {rEmb : WSweepRule → R} (hrules : ∀ (ρ : WSweepRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {cell : Univ A R P K dd → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hneltp : κ.ltp ≠ κ.t) {m : Univ A R P K dd → Prop} {restAt : (Univ A R P K dd → Prop) → (Univ A R P K dd → Prop) → W → A} {ltpAddr : Univ A R P K dd → Prop} (hltp : ∀ (k r : Univ A R P K dd → Prop), restAt k r κ.ltp = bitVal PR.zero PR.one (r = ltpAddr)) {fc : Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (htp : WMSetLe WMLe s₁ ltpAddr) (hframe : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → ∀ (r : Univ A R P K dd → Prop), r ≠ s → restAt u r = restAt s r) (hwr : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → κ.wrG (PR.passTracksAt cell κ.t (restAt s) m s) = 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 fc), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell κ.t (restAt s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt κ.ph fc), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell κ.t (restAt s₁) m) (PR.syElt PR.blank) }

The kit runs its sweep: one rewrite per address, the background a function of the frontier. The rewrite the kit's rule computes must match the background's change at each cell, which is the one semantic hypothesis.

theorem DescriptiveComplexity.Draw.WriteSweepKit.reaches {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} {κ : WriteSweepKit A Q W P} {rEmb : WSweepRule → R} (hrules : ∀ (ρ : WSweepRule), PR.rules (rEmb ρ) = κ.rule PR.one ρ) {cell : Univ A R P K dd → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hneltp : κ.ltp ≠ κ.t) {m : Univ A R P K dd → Prop} {restAt : (Univ A R P K dd → Prop) → (Univ A R P K dd → Prop) → W → A} {ltpAddr : Univ A R P K dd → Prop} (hltp : ∀ (k r : Univ A R P K dd → Prop), restAt k r κ.ltp = bitVal PR.zero PR.one (r = ltpAddr)) {fc : Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (htp : WMSetLe WMLe s₁ ltpAddr) (hframe : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → ∀ (r : Univ A R P K dd → Prop), r ≠ s → restAt u r = restAt s r) (hwr : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → κ.wrG (PR.passTracksAt cell κ.t (restAt s) m s) = PR.passTracksAt cell κ.t (restAt u) m s) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt κ.ph fc), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell κ.t (restAt s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt κ.ph fc), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell κ.t (restAt s₁) m) (PR.syElt PR.blank) }

The kit runs its sweep, the budget forgotten.