Reading one named register bit #
The leaves of the element loops read single bits of the machine's registers at
computed cells: a ρ-atom of an expansion sentence
is one bit of VAL or MIRROR at the cell whose name marks match a tuple held in
the control, a tag read is the same at a canonical cell. The trip is always
the same: turn off the working-cell marker, scan up to the first cell whose
tracks satisfy the name guard – unique by
DescriptiveComplexity.Draw.eq_of_slotMark_name-style facts – take one step
left reading the walked digit into the phase, and scan back down to the
marker.
DescriptiveComplexity.Draw.Prog.reaches_readBit_pos and _neg are the two
outcomes. The read changes nothing on the tape, so the two theorems mention
one tape; the caller cases on the bit.
theorem
DescriptiveComplexity.Draw.Prog.reachesIn_writeBit
{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}
(F : IxFile (Univ A R P K dd) I ile)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{t wk : W}
(hnewk : wk ≠ t)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{rest : (Univ A R P K dd → Prop) → W → A}
{m : I → Prop}
{v : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
{NameG : (W → A) → Prop}
{x₀ : I}
(hname : NameG (PR.passTracksAt F.cell t rest m (F.cell x₀)))
(huniq : ∀ (r : Univ A R P K dd → Prop), NameG (PR.passTracksAt F.cell t rest m r) → r = F.cell x₀)
{pStart pUp : P}
{fc : Q → A}
(hturn : ∀ (g : W → A), g wk = PR.one → PR.HasRight pStart fc g pUp fc g)
(hup : ∀ (g : W → A), ¬NameG g → PR.HasRight pUp fc g pUp fc g)
{b : Prop}
{pW : P}
(hwr :
PR.HasLeft pUp fc (PR.passTracksAt F.cell t rest m (F.cell x₀)) pW fc
(Function.update (PR.passTracksAt F.cell t rest m (F.cell x₀)) t (bitVal PR.zero PR.one b)))
(hbackW : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pW fc g pW fc g)
:
(wideData (Univ A R P K dd)).ReachesIn (2 * (wideRank (F.cell x₀) - wideRank v) + 2)
{ state := Sum.inr (PR.stElt pStart fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pW fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest fun (y : I) => y = x₀ ∧ b ∨ y ≠ x₀ ∧ m y) (PR.syElt PR.blank) }
Writing one named register bit: the same trip, with the walked track updated at the named cell on the way back down.
Dependency graph
theorem
DescriptiveComplexity.Draw.Prog.reaches_writeBit
{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}
(F : IxFile (Univ A R P K dd) I ile)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{t wk : W}
(hnewk : wk ≠ t)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{rest : (Univ A R P K dd → Prop) → W → A}
{m : I → Prop}
{v : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
{NameG : (W → A) → Prop}
{x₀ : I}
(hname : NameG (PR.passTracksAt F.cell t rest m (F.cell x₀)))
(huniq : ∀ (r : Univ A R P K dd → Prop), NameG (PR.passTracksAt F.cell t rest m r) → r = F.cell x₀)
{pStart pUp : P}
{fc : Q → A}
(hturn : ∀ (g : W → A), g wk = PR.one → PR.HasRight pStart fc g pUp fc g)
(hup : ∀ (g : W → A), ¬NameG g → PR.HasRight pUp fc g pUp fc g)
{b : Prop}
{pW : P}
(hwr :
PR.HasLeft pUp fc (PR.passTracksAt F.cell t rest m (F.cell x₀)) pW fc
(Function.update (PR.passTracksAt F.cell t rest m (F.cell x₀)) t (bitVal PR.zero PR.one b)))
(hbackW : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pW fc g pW fc g)
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt pStart fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pW fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest fun (y : I) => y = x₀ ∧ b ∨ y ≠ x₀ ∧ m y) (PR.syElt PR.blank) }
Writing one named register bit, the budget forgotten.
Dependency graph
theorem
DescriptiveComplexity.Draw.Prog.reachesIn_readBit_pos
{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}
(F : IxFile (Univ A R P K dd) I ile)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{t wk : W}
(hnewk : wk ≠ t)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{rest : (Univ A R P K dd → Prop) → W → A}
{m : I → Prop}
{v : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
{NameG : (W → A) → Prop}
{x₀ : I}
(hname : NameG (PR.passTracksAt F.cell t rest m (F.cell x₀)))
(huniq : ∀ (r : Univ A R P K dd → Prop), NameG (PR.passTracksAt F.cell t rest m r) → r = F.cell x₀)
{pStart pUp pRy : P}
{fc : Q → A}
(hturn : ∀ (g : W → A), g wk = PR.one → PR.HasRight pStart fc g pUp fc g)
(hup : ∀ (g : W → A), ¬NameG g → PR.HasRight pUp fc g pUp fc g)
(hrd1 : ∀ (g : W → A), NameG g → g t = PR.one → PR.HasLeft pUp fc g pRy fc g)
(hbackY : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pRy fc g pRy fc g)
(hm : m x₀)
:
(wideData (Univ A R P K dd)).ReachesIn (2 * (wideRank (F.cell x₀) - wideRank v) + 2)
{ state := Sum.inr (PR.stElt pStart fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pRy fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
Reading a set bit: the trip ends at the marker in the positive phase.
Dependency graph
theorem
DescriptiveComplexity.Draw.Prog.reaches_readBit_pos
{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}
(F : IxFile (Univ A R P K dd) I ile)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{t wk : W}
(hnewk : wk ≠ t)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{rest : (Univ A R P K dd → Prop) → W → A}
{m : I → Prop}
{v : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
{NameG : (W → A) → Prop}
{x₀ : I}
(hname : NameG (PR.passTracksAt F.cell t rest m (F.cell x₀)))
(huniq : ∀ (r : Univ A R P K dd → Prop), NameG (PR.passTracksAt F.cell t rest m r) → r = F.cell x₀)
{pStart pUp pRy : P}
{fc : Q → A}
(hturn : ∀ (g : W → A), g wk = PR.one → PR.HasRight pStart fc g pUp fc g)
(hup : ∀ (g : W → A), ¬NameG g → PR.HasRight pUp fc g pUp fc g)
(hrd1 : ∀ (g : W → A), NameG g → g t = PR.one → PR.HasLeft pUp fc g pRy fc g)
(hbackY : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pRy fc g pRy fc g)
(hm : m x₀)
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt pStart fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pRy fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
Reading a set bit: the trip ends at the marker in the positive phase.
Dependency graph
theorem
DescriptiveComplexity.Draw.Prog.reachesIn_readBit_neg
{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}
(F : IxFile (Univ A R P K dd) I ile)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{t wk : W}
(hnewk : wk ≠ t)
{gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{rest : (Univ A R P K dd → Prop) → W → A}
{m : I → Prop}
{v : Univ A R P K dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v))
{NameG : (W → A) → Prop}
{x₀ : I}
(hname : NameG (PR.passTracksAt F.cell t rest m (F.cell x₀)))
(huniq : ∀ (r : Univ A R P K dd → Prop), NameG (PR.passTracksAt F.cell t rest m r) → r = F.cell x₀)
{pStart pUp pRn : P}
{fc : Q → A}
(hturn : ∀ (g : W → A), g wk = PR.one → PR.HasRight pStart fc g pUp fc g)
(hup : ∀ (g : W → A), ¬NameG g → PR.HasRight pUp fc g pUp fc g)
(hrd0 : ∀ (g : W → A), NameG g → g t ≠ PR.one → PR.HasLeft pUp fc g pRn fc g)
(hbackN : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pRn fc g pRn fc g)
(hm : ¬m x₀)
:
(wideData (Univ A R P K dd)).ReachesIn (2 * (wideRank (F.cell x₀) - wideRank v) + 2)
{ state := Sum.inr (PR.stElt pStart fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pRn fc), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
Reading a clear bit: the trip ends at the marker in the negative phase.