The tag-branched machinery's run #
The run theorem of DescriptiveComplexity.Draw.tagRule: the witness reads
store the argument points' tags one-hot into the control, the branch
checkpoint dispatches on the decoded tuple – its guard TagsAre holding at
exactly one tag tuple – and that tuple's element loop runs to the shared exit
phase by DescriptiveComplexity.Draw.elem_reachesIn.
The run comes with its cost (tag_reachesIn): the chain's reads at the
trip width the caller fixes, the branch's dispatch and walk back, and the
loop's own count. tag_run is it with the budget forgotten, at the width every
trip has anyway.
As in the element loop's run, the machinery is entered at its first phase
on the marker (the caller's dispatch steps right and
DescriptiveComplexity.Draw.tag_back walks back down), and it leaves through
the loop's exit dispatch one cell to the marker's right.
def
DescriptiveComplexity.Draw.tagPhaseAt
{P T : Type}
{m : ℕ}
{nrOf : T → ℕ}
(emb : TagPh m T nrOf → P)
(k : ℕ)
:
P
The phase before the k-th witness read – the branch checkpoint once
they are exhausted.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.tag_back
{A R P Q W K T : 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}
{m : ℕ}
{nrOf : T → ℕ}
{I : Type}
{ile : I → I → Prop}
(RF : IxFile (Univ A R P K dd) I ile)
{wk rg : W}
{emb : TagPh m T nrOf → P}
{rdTrackT : Fin m → W}
{MatchT : Fin m → (Q → A) → (W → A) → Prop}
{setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A}
{TagsAre : T → (Q → A) → Prop}
{rdTrackE : (τ : T) → Fin (nrOf τ) → W}
{MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop}
{setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A}
{initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A}
{IsMaxEl : T → (Q → A) → Prop}
{exitPh : P}
{rEmb : (i : TagSite m T nrOf) → TagSh m T nrOf i → R}
(hlin : IsLinOrd WMLe)
{v v' : Univ A R P K dd → Prop}
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P K dd → Prop) → W → A}
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
{t₀ : W}
{m₀ : I → Prop}
(hwkt₀ : wk ≠ t₀)
(hR : PR.table.Reads)
(hrules :
∀ (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i),
PR.rules (rEmb i ρ) = tagRule PR.one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl
exitPh i ρ)
{f : Q → A}
:
(wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt (tagFirstRd emb) f), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (tagFirstRd emb) f), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
The one leftward step a caller's rightward dispatch into the machinery owes: at its first phase, the walk back down to the marker.
Dependency graph
theorem
DescriptiveComplexity.Draw.tag_reachesIn
{A R P Q W K T : 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}
{m : ℕ}
{nrOf : T → ℕ}
{I : Type}
{ile : I → I → Prop}
(RF : IxFile (Univ A R P K dd) I ile)
{wk rg : W}
{emb : TagPh m T nrOf → P}
{rdTrackT : Fin m → W}
{MatchT : Fin m → (Q → A) → (W → A) → Prop}
{setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A}
{TagsAre : T → (Q → A) → Prop}
{rdTrackE : (τ : T) → Fin (nrOf τ) → W}
{MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop}
{setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A}
{initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A}
{IsMaxEl : T → (Q → A) → Prop}
{exitPh : P}
{rEmb : (i : TagSite m T nrOf) → TagSh m T nrOf i → R}
(hrules :
∀ (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i),
PR.rules (rEmb i ρ) = tagRule PR.one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl
exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{v v' : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P K dd → Prop) → W → A}
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
(hrg : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u))
{mT : Fin m → I → Prop}
(hmT :
∀ (i : Fin m) (r : Univ A R P K dd → Prop), rest r (rdTrackT i) = bitVal PR.zero PR.one (bitAtOf RF.cell (mT i) r))
(hnewkT : ∀ (i : Fin m), wk ≠ rdTrackT i)
(hnergT : ∀ (i : Fin m), rg ≠ rdTrackT i)
{t₀ : W}
{m₀ : I → Prop}
(hm₀ : ∀ (r : Univ A R P K dd → Prop), rest r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r))
(hwkt₀ : wk ≠ t₀)
(hrgt₀ : rg ≠ t₀)
(fsT : Fin (m + 1) → Q → A)
(xT : Fin m → I)
(hnameT : ∀ (i : Fin m), MatchT i (fsT i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) (RF.cell (xT i))))
(huniqT :
∀ (i : Fin m) (r : Univ A R P K dd → Prop),
MatchT i (fsT i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) r) → r = RF.cell (xT i))
(hfsTT : ∀ (i : Fin m), mT i (xT i) → fsT i.succ = setTagFlag i true (fsT i.castSucc) (rest v))
(hfsTF : ∀ (i : Fin m), ¬mT i (xT i) → fsT i.succ = setTagFlag i false (fsT i.castSucc) (rest v))
(c : ℕ)
(hcostT : ∀ (i : Fin m), 2 * (wideRank (RF.cell (xT i)) - wideRank v) + 2 ≤ c)
{τ : T}
(hτ : TagsAre τ (fsT (Fin.last m)))
{mE : Fin (nrOf τ) → I → Prop}
(hmE :
∀ (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop),
rest r (rdTrackE τ j) = bitVal PR.zero PR.one (bitAtOf RF.cell (mE j) r))
(hnewkE : ∀ (j : Fin (nrOf τ)), wk ≠ rdTrackE τ j)
(hnergE : ∀ (j : Fin (nrOf τ)), rg ≠ rdTrackE τ j)
{ι : Type}
[LinearOrder ι]
[Finite ι]
{a₀ aT : ι}
(hbotI : ∀ (a : ι), a₀ ≤ a)
(htopI : ∀ (a : ι), a ≤ aT)
(F : ι → Q → A)
(fsOf : ι → Fin (nrOf τ + 1) → Q → A)
(hlastF : ∀ (a : ι), fsOf a (Fin.last (nrOf τ)) = F a)
(xE : ι → Fin (nrOf τ) → I)
(hnameE :
∀ (a : ι) (j : Fin (nrOf τ)),
MatchE τ j (fsOf a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) (RF.cell (xE a j))))
(huniqE :
∀ (a : ι) (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop),
MatchE τ j (fsOf a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) r) → r = RF.cell (xE a j))
(hfsET : ∀ (a : ι) (j : Fin (nrOf τ)), mE j (xE a j) → fsOf a j.succ = setFlagE τ j true (fsOf a j.castSucc) (rest v))
(hfsEF : ∀ (a : ι) (j : Fin (nrOf τ)), ¬mE j (xE a j) → fsOf a j.succ = setFlagE τ j false (fsOf a j.castSucc) (rest v))
(hadv : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → advEl τ (F a) (rest v) = fsOf a' 0)
(hmaxT : IsMaxEl τ (F aT))
(hmaxF : ∀ a < aT, ¬IsMaxEl τ (F a))
(hinit : initEl τ (fsT (Fin.last m)) (rest v) = fsOf a₀ 0)
(hcostE : ∀ (a : ι) (j : Fin (nrOf τ)), 2 * (wideRank (RF.cell (xE a j)) - wideRank v) + 2 ≤ c)
:
(wideData (Univ A R P K dd)).ReachesIn ((c + 2) * m + 2 + ((2 + (c + 2) * nrOf τ) * (Nat.card ι + 1) + 1))
{ state := Sum.inr (PR.stElt (tagFirstRd emb) (fsT 0)), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh (exitSt τ (F aT) (rest v))), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
The tag-branched machinery's run, on a clock: from its first phase at the marker – the witness chain, the branch on the decoded tag tuple, and that tuple's element loop – to the exit phase one cell to the marker's right, at the chain's reads, the branch's two steps and the loop's own cost.
Dependency graph
theorem
DescriptiveComplexity.Draw.tag_run
{A R P Q W K T : 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}
{m : ℕ}
{nrOf : T → ℕ}
{I : Type}
{ile : I → I → Prop}
(RF : IxFile (Univ A R P K dd) I ile)
{wk rg : W}
{emb : TagPh m T nrOf → P}
{rdTrackT : Fin m → W}
{MatchT : Fin m → (Q → A) → (W → A) → Prop}
{setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A}
{TagsAre : T → (Q → A) → Prop}
{rdTrackE : (τ : T) → Fin (nrOf τ) → W}
{MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop}
{setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A}
{initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A}
{IsMaxEl : T → (Q → A) → Prop}
{exitPh : P}
{rEmb : (i : TagSite m T nrOf) → TagSh m T nrOf i → R}
(hrules :
∀ (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i),
PR.rules (rEmb i ρ) = tagRule PR.one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl
exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{v v' : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P K dd → Prop) → W → A}
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
(hrg : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u))
{mT : Fin m → I → Prop}
(hmT :
∀ (i : Fin m) (r : Univ A R P K dd → Prop), rest r (rdTrackT i) = bitVal PR.zero PR.one (bitAtOf RF.cell (mT i) r))
(hnewkT : ∀ (i : Fin m), wk ≠ rdTrackT i)
(hnergT : ∀ (i : Fin m), rg ≠ rdTrackT i)
{t₀ : W}
{m₀ : I → Prop}
(hm₀ : ∀ (r : Univ A R P K dd → Prop), rest r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r))
(hwkt₀ : wk ≠ t₀)
(hrgt₀ : rg ≠ t₀)
(fsT : Fin (m + 1) → Q → A)
(xT : Fin m → I)
(hnameT : ∀ (i : Fin m), MatchT i (fsT i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) (RF.cell (xT i))))
(huniqT :
∀ (i : Fin m) (r : Univ A R P K dd → Prop),
MatchT i (fsT i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) r) → r = RF.cell (xT i))
(hfsTT : ∀ (i : Fin m), mT i (xT i) → fsT i.succ = setTagFlag i true (fsT i.castSucc) (rest v))
(hfsTF : ∀ (i : Fin m), ¬mT i (xT i) → fsT i.succ = setTagFlag i false (fsT i.castSucc) (rest v))
{τ : T}
(hτ : TagsAre τ (fsT (Fin.last m)))
{mE : Fin (nrOf τ) → I → Prop}
(hmE :
∀ (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop),
rest r (rdTrackE τ j) = bitVal PR.zero PR.one (bitAtOf RF.cell (mE j) r))
(hnewkE : ∀ (j : Fin (nrOf τ)), wk ≠ rdTrackE τ j)
(hnergE : ∀ (j : Fin (nrOf τ)), rg ≠ rdTrackE τ j)
{ι : Type}
[LinearOrder ι]
[Finite ι]
{a₀ aT : ι}
(hbotI : ∀ (a : ι), a₀ ≤ a)
(htopI : ∀ (a : ι), a ≤ aT)
(F : ι → Q → A)
(fsOf : ι → Fin (nrOf τ + 1) → Q → A)
(hlastF : ∀ (a : ι), fsOf a (Fin.last (nrOf τ)) = F a)
(xE : ι → Fin (nrOf τ) → I)
(hnameE :
∀ (a : ι) (j : Fin (nrOf τ)),
MatchE τ j (fsOf a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) (RF.cell (xE a j))))
(huniqE :
∀ (a : ι) (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop),
MatchE τ j (fsOf a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) r) → r = RF.cell (xE a j))
(hfsET : ∀ (a : ι) (j : Fin (nrOf τ)), mE j (xE a j) → fsOf a j.succ = setFlagE τ j true (fsOf a j.castSucc) (rest v))
(hfsEF : ∀ (a : ι) (j : Fin (nrOf τ)), ¬mE j (xE a j) → fsOf a j.succ = setFlagE τ j false (fsOf a j.castSucc) (rest v))
(hadv : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → advEl τ (F a) (rest v) = fsOf a' 0)
(hmaxT : IsMaxEl τ (F aT))
(hmaxF : ∀ a < aT, ¬IsMaxEl τ (F a))
(hinit : initEl τ (fsT (Fin.last m)) (rest v) = fsOf a₀ 0)
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt (tagFirstRd emb) (fsT 0)), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh (exitSt τ (F aT) (rest v))), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }
The tag-branched machinery's run, the budget forgotten: what a space-bounded caller reads, at the width every trip has anyway.