Documentation

DescriptiveComplexity.Problems.Wide.DrawIncrKit

The increment kit: a round trip around the block-indexed mirror increment #

The kit wrapping DescriptiveComplexity.Draw.Prog.reaches_fileIncrBlk in its round trip: scan up to the file top, bounce, run the binary increment down the file – clearing set digits until the first clear one, setting it – and return to the marker in the phase of the block that carried. The inner VAL loop of the EXPSPACE program folds its accumulators against exactly that block, which is why the landing phase is indexed.

The carry block is read off the mark of the register cell that carried: the kit takes one slot per block (bs), set exactly at the registers of that block, and its set rule comes in one copy per block. The one-hot clause in that rule's guard is what makes two copies separable – at an arbitrary symbol two block slots could both be set, and the third hardening of the layer (DescriptiveComplexity.Draw.Prog.reaches_fileIncrBlk's one-hot hypothesis) made the demand and the guard match.

Rules are owned by their source phase: entry (at the scan phase) and exit (at the marker, in a landing phase, guarded wk = one ∧ rg ≠ one) belong to the caller.

The increment trip's shapes #

source
inductive DescriptiveComplexity.Draw.IncrPh (B : Type) :
Type

The phases of an increment trip: the up-scan, the bounce, the carry phase, and one landing phase per block.

  • up {B : Type} : IncrPh B

    Scanning up to the file top.

  • b2 {B : Type} : IncrPh B

    Bounced off the top, about to re-enter rightwards.

  • pc {B : Type} : IncrPh B

    Clearing set digits, looking for the first clear one.

  • pd {B : Type} : B → IncrPh B

    The digit of this block was set: walking home.

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.Draw.instDecidableEqIncrPh {B : Type} [DecidableEq B] :
    DecidableEq (IncrPh B)
    Equations
    Dependency graph
    source
    instance DescriptiveComplexity.Draw.instFiniteIncrPh {B : Type} [Finite B] :
    Finite (IncrPh B)
    Dependency graph
    source
    inductive DescriptiveComplexity.Draw.IncrRule (B : Type) :
    Type

    The rule families of an increment trip, the acting ones per block.

    • up {B : Type} : IncrRule B

      Scan right while the file-top mark is clear.

    • b1 {B : Type} : IncrRule B

      At the file top: step left into the bounce phase.

    • b2go {B : Type} : IncrRule B

      Bounce: step back right into the carry phase.

    • clear {B : Type} : IncrRule B

      At a register with a set digit: clear it, carry on.

    • set {B : Type} : B → IncrRule B

      At a register of this block with a clear digit: set it, land.

    • walk {B : Type} : IncrRule B

      Walk left over unmarked cells in the carry phase.

    • stay {B : Type} : B → IncrRule B

      Hold at registers, walk and return, in this block's landing phase.

    Instances For
      Dependency graph
      source
      instance DescriptiveComplexity.Draw.instFiniteIncrRule {B : Type} [Finite B] :
      Finite (IncrRule B)
      Dependency graph
      source
      structure DescriptiveComplexity.Draw.IncrKit (A Q W P B : Type) :
      Type

      An increment kit: the walked track, the service slots, the per-block mark slots, and the phases.

      • t : W

        The walked track being incremented.

      • rg : W

        The register mark.

      • rl : W

        The file-top mark.

      • wk : W

        The working-cell marker slot.

      • bs : B → W

        The block mark: set exactly at the registers of that block.

      • emb : IncrPh B → P

        The kit's phases in the program.

      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.Draw.IncrKit.rule {A Q W P B : Type} [DecidableEq W] (κ : IncrKit A Q W P B) (zero one : A) :
        IncrRule B → Rule A Q W P

        The kit's rules.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.Draw.IncrKit.dstPh_emb {A Q W P B : Type} [DecidableEq W] (κ : IncrKit A Q W P B) (zero one : A) (ρ : IncrRule B) :
          ∃ (p : IncrPh B), (κ.rule zero one ρ).dstPh = κ.emb p

          The trip stays inside its own phases: every rule lands in one the kit was given.

          Dependency graph
          source
          theorem DescriptiveComplexity.Draw.IncrKit.sep {A Q W P B : Type} [DecidableEq W] (κ : IncrKit A Q W P B) (zero one : A) (hzo : zero ≠ one) (hemb : Function.Injective κ.emb) (ρ ρ' : IncrRule B) (f : Q → A) (g : W → A) :
          (κ.rule zero one ρ).guard f g → (κ.rule zero one ρ').guard f g → (κ.rule zero one ρ).srcPh = (κ.rule zero one ρ').srcPh → ρ = ρ'

          In-shape separation. The two indexed families separate through their index: the set rules by the one-hot clause of their guards, the stay rules by their source phases.

          Dependency graph
          source
          theorem DescriptiveComplexity.Draw.IncrKit.exit_disjoint {A Q W P B : Type} [DecidableEq W] (κ : IncrKit A Q W P B) (zero one : A) (hemb : Function.Injective κ.emb) (ρ : IncrRule B) (f : Q → A) (g : W → A) (b : B) :
          (κ.rule zero one ρ).guard f g → g κ.wk = one → g κ.rg ≠ one → (κ.rule zero one ρ).srcPh = κ.emb (IncrPh.pd b) → False

          Exit disjointness at the kit's landing phases.

          Dependency graph

          The discharge #

          source
          theorem DescriptiveComplexity.Draw.IncrKit.reachesIn {A R P Q W K B : 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} {κ : IncrKit A Q W P B} {rEmb : IncrRule B → R} (hrules : ∀ (ρ : IncrRule B), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) (hbs : ∀ (b : B), κ.bs b ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m m' : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {blkOf : I → B} (hblk : ∀ (u : I) (b : B), rest (F.cell u) (κ.bs b) = bitVal PR.zero PR.one (blkOf u = b)) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) (hi : WMIncr ile m m') :
          ∃ (u₀ : I), (¬m u₀ ∧ ∀ (v : I), WMLt ile u₀ v → m v) ∧ (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + 2 + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot)) { state := Sum.inr (PR.stElt (κ.emb IncrPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb (IncrPh.pd (blkOf u₀))) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m') (PR.syElt PR.blank) }

          The kit increments its track, and lands at the marker in the phase of the block that carried: from the scan phase anywhere, up to the file top, the binary increment down the file, and back.

          Dependency graph
          source
          theorem DescriptiveComplexity.Draw.IncrKit.reaches {A R P Q W K B : 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} {κ : IncrKit A Q W P B} {rEmb : IncrRule B → R} (hrules : ∀ (ρ : IncrRule B), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) (hbs : ∀ (b : B), κ.bs b ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m m' : I → Prop} {wkAddr : Univ A R P K dd → Prop} (hwkLt : WMSetLt WMLe wkAddr (F.cell gbot)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrl : ∀ (r : Univ A R P K dd → Prop), rest r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r κ.wk = bitVal PR.zero PR.one (r = wkAddr)) {blkOf : I → B} (hblk : ∀ (u : I) (b : B), rest (F.cell u) (κ.bs b) = bitVal PR.zero PR.one (blkOf u = b)) {fc : Q → A} {s : Univ A R P K dd → Prop} (hsle : WMSetLe WMLe s (F.cell gtop)) (hi : WMIncr ile m m') :
          ∃ (u₀ : I), (¬m u₀ ∧ ∀ (v : I), WMLt ile u₀ v → m v) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb IncrPh.up) fc), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb (IncrPh.pd (blkOf u₀))) fc), head := Sum.inl wkAddr, tape := wideTape (PR.trackTapeAt F.cell κ.t rest m') (PR.syElt PR.blank) }

          The kit increments its track, the budget forgotten.

          Dependency graph