The tuple loop's run #
The run theorem of DescriptiveComplexity.Draw.tupleRule: per enumerated
tuple, a read trip at the source cell, the bit stored into the control, a
write trip at the destination cell reading it back, and the advance – so the
loop copies a bit per round, and the destination track evolves.
That evolution is what distinguishes this statement from the element loop's:
the background is a family over the enumeration, each round's write moving
the destination track from mD a to
DescriptiveComplexity.Draw.tuplePost – the update at the round's
destination cell with the round's source bit – and the next round's
background carrying exactly that. Everything else follows the established
shape: an abstract finite linear order for the enumeration, control families
fs0/fs1 around the store, and the loop closed by
DescriptiveComplexity.Draw.reflTransGen_of_ordLoop.
def
DescriptiveComplexity.Draw.tuplePost
{I ι : Type}
(mSrc : I → Prop)
(mD : ι → I → Prop)
(xS xD : ι → I)
(a : ι)
:
I → Prop
The destination track after a round's write: the round's source bit at its destination cell, everything else untouched.
Equations
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.tuple_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}
{I : Type}
{ile : I → I → Prop}
(RF : IxFile (Univ A R P K dd) I ile)
{wk rg : W}
{emb : ChainPh 3 TuplePS → P}
{tSrc tDst : W}
{MatchS MatchD : (Q → A) → (W → A) → Prop}
{bitFlag : (Q → A) → Prop}
{setBit : Bool → (Q → A) → (W → A) → Q → A}
{initLv advLv : (Q → A) → (W → A) → Q → A}
{IsMaxLv : (Q → A) → Prop}
{exitPh : P}
{rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R}
(hrules :
∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i),
PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv 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')
{ι : Type}
[LinearOrder ι]
[Finite ι]
{a₀ aT : ι}
(hbotI : ∀ (a : ι), a₀ ≤ a)
(htopI : ∀ (a : ι), a ≤ aT)
{restOf : ι → (Univ A R P K dd → Prop) → W → A}
{mSrc : I → Prop}
{mD : ι → I → Prop}
(hwkS : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r wk = bitVal PR.zero PR.one (r = v))
(hrg : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u))
(hsrc : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r tSrc = bitVal PR.zero PR.one (bitAtOf RF.cell mSrc r))
(hdst : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r tDst = bitVal PR.zero PR.one (bitAtOf RF.cell (mD a) r))
(hwkSrc : wk ≠ tSrc)
(hwkDst : wk ≠ tDst)
(hrgSrc : rg ≠ tSrc)
(hrgDst : rg ≠ tDst)
(xS xD : ι → I)
(fs0 fs1 : ι → Q → A)
(hnameS : ∀ (a : ι), MatchS (fs0 a) (PR.passTracksAt RF.cell tSrc (restOf a) mSrc (RF.cell (xS a))))
(huniqS :
∀ (a : ι) (r : Univ A R P K dd → Prop),
MatchS (fs0 a) (PR.passTracksAt RF.cell tSrc (restOf a) mSrc r) → r = RF.cell (xS a))
(hnameD : ∀ (a : ι), MatchD (fs1 a) (PR.passTracksAt RF.cell tDst (restOf a) (mD a) (RF.cell (xD a))))
(huniqD :
∀ (a : ι) (r : Univ A R P K dd → Prop),
MatchD (fs1 a) (PR.passTracksAt RF.cell tDst (restOf a) (mD a) r) → r = RF.cell (xD a))
(hstoreT : ∀ (a : ι), mSrc (xS a) → fs1 a = setBit true (fs0 a) (restOf a v))
(hstoreF : ∀ (a : ι), ¬mSrc (xS a) → fs1 a = setBit false (fs0 a) (restOf a v))
(hbitFlag : ∀ (a : ι), bitFlag (fs1 a) ↔ mSrc (xS a))
(hadv : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → advLv (fs1 a) (restOf a v) = fs0 a')
(hcov : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → ∀ (y : I), mD a' y ↔ tuplePost mSrc mD xS xD a y)
(hagree :
∀ (a a' : ι),
a < a' →
(∀ (b : ι), ¬(a < b ∧ b < a')) → ∀ (r : Univ A R P K dd → Prop) (s : W), s ≠ tDst → restOf a' r s = restOf a r s)
(hmaxT : IsMaxLv (fs1 aT))
(hmaxF : ∀ a < aT, ¬IsMaxLv (fs1 a))
{f₀ : Q → A}
(w : ℕ)
(hcost :
∀ (a : ι),
2 * (wideRank (RF.cell (xS a)) - wideRank v) + 2 ≤ w ∧ 2 * (wideRank (RF.cell (xD a)) - wideRank v) + 2 ≤ w)
(hinit : initLv f₀ (restOf a₀ v) = fs0 a₀)
:
(wideData (Univ A R P K dd)).ReachesIn ((2 * w + 8) * (Nat.card ι + 1) + 1)
{ state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, ⋯⟩)) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell tSrc (restOf a₀) mSrc) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh (fs1 aT)), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell tDst (restOf aT) (tuplePost mSrc mD xS xD aT)) (PR.syElt PR.blank) }
The tuple loop's run, on a clock: from the entry checkpoint at the marker to the exit phase one cell to its right, the destination track holding – round by round – the source track's bits at the enumerated cells, and the cost is one round's width once per element of the enumeration, plus the round that opens it and the step that leaves.
Dependency graph
theorem
DescriptiveComplexity.Draw.tuple_run
{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}
{ile : I → I → Prop}
(RF : IxFile (Univ A R P K dd) I ile)
{wk rg : W}
{emb : ChainPh 3 TuplePS → P}
{tSrc tDst : W}
{MatchS MatchD : (Q → A) → (W → A) → Prop}
{bitFlag : (Q → A) → Prop}
{setBit : Bool → (Q → A) → (W → A) → Q → A}
{initLv advLv : (Q → A) → (W → A) → Q → A}
{IsMaxLv : (Q → A) → Prop}
{exitPh : P}
{rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R}
(hrules :
∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i),
PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv 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')
{ι : Type}
[LinearOrder ι]
[Finite ι]
{a₀ aT : ι}
(hbotI : ∀ (a : ι), a₀ ≤ a)
(htopI : ∀ (a : ι), a ≤ aT)
{restOf : ι → (Univ A R P K dd → Prop) → W → A}
{mSrc : I → Prop}
{mD : ι → I → Prop}
(hwkS : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r wk = bitVal PR.zero PR.one (r = v))
(hrg : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u))
(hsrc : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r tSrc = bitVal PR.zero PR.one (bitAtOf RF.cell mSrc r))
(hdst : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r tDst = bitVal PR.zero PR.one (bitAtOf RF.cell (mD a) r))
(hwkSrc : wk ≠ tSrc)
(hwkDst : wk ≠ tDst)
(hrgSrc : rg ≠ tSrc)
(hrgDst : rg ≠ tDst)
(xS xD : ι → I)
(fs0 fs1 : ι → Q → A)
(hnameS : ∀ (a : ι), MatchS (fs0 a) (PR.passTracksAt RF.cell tSrc (restOf a) mSrc (RF.cell (xS a))))
(huniqS :
∀ (a : ι) (r : Univ A R P K dd → Prop),
MatchS (fs0 a) (PR.passTracksAt RF.cell tSrc (restOf a) mSrc r) → r = RF.cell (xS a))
(hnameD : ∀ (a : ι), MatchD (fs1 a) (PR.passTracksAt RF.cell tDst (restOf a) (mD a) (RF.cell (xD a))))
(huniqD :
∀ (a : ι) (r : Univ A R P K dd → Prop),
MatchD (fs1 a) (PR.passTracksAt RF.cell tDst (restOf a) (mD a) r) → r = RF.cell (xD a))
(hstoreT : ∀ (a : ι), mSrc (xS a) → fs1 a = setBit true (fs0 a) (restOf a v))
(hstoreF : ∀ (a : ι), ¬mSrc (xS a) → fs1 a = setBit false (fs0 a) (restOf a v))
(hbitFlag : ∀ (a : ι), bitFlag (fs1 a) ↔ mSrc (xS a))
(hadv : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → advLv (fs1 a) (restOf a v) = fs0 a')
(hcov : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → ∀ (y : I), mD a' y ↔ tuplePost mSrc mD xS xD a y)
(hagree :
∀ (a a' : ι),
a < a' →
(∀ (b : ι), ¬(a < b ∧ b < a')) → ∀ (r : Univ A R P K dd → Prop) (s : W), s ≠ tDst → restOf a' r s = restOf a r s)
(hmaxT : IsMaxLv (fs1 aT))
(hmaxF : ∀ a < aT, ¬IsMaxLv (fs1 a))
{f₀ : Q → A}
(hinit : initLv f₀ (restOf a₀ v) = fs0 a₀)
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, ⋯⟩)) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell tSrc (restOf a₀) mSrc) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh (fs1 aT)), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell tDst (restOf aT) (tuplePost mSrc mD xS xD aT)) (PR.syElt PR.blank) }
The tuple loop's run, the budget forgotten: what a space-bounded caller reads. The width of a trip is then the largest of the finitely many the loop takes.