Random access: seeking the working cell to a target address #
The R-atoms of the EXPSPACE program read the tape at a computed address: the machine builds the address in its TARGET register, resets the working-cell marker to the empty address, and advances it – mirror in tow – until a file test says MIRROR = TARGET. This file is that loop.
DescriptiveComplexity.Draw.Prog.reaches_fileSeekTo is one theorem: from the
checkpoint at the empty address, the machine reaches the verdict configuration
on the target's cell.
The loop is stated at an arbitrary file
(DescriptiveComplexity.Draw.Prog.reachesIn_ixSeekTo), because a clocked program
has no register per element: the walked track's mark is then the address's bits
at the registers (DescriptiveComplexity.ixMark) rather than the address
itself, and what makes it the same proof is that the correspondence carries the
order (DescriptiveComplexity.Problems.Wide.IxAddr) – so the file test's
verdict, the two marks agreeing at every register, is again the equality of the
two addresses, as long as both are addresses the file can hold. The elementwise
statement is that one at the diagonal. Each round is a turnaround step off the marker, a
DescriptiveComplexity.Draw.Prog.reaches_fileRoundTrip around the file test
(DescriptiveComplexity.Draw.Prog.reaches_fileTestG at the walked mirror digit
agrees with the target digit), and – the test having failed below the
target – an DescriptiveComplexity.Draw.Prog.reaches_fileAdvance; the loop is
DescriptiveComplexity.reaches_of_wideRounds, and the mirror invariant –
the mirror track is the marker's address – holds by construction, the two
being the same predicate.
The nine phases and their rule families are exactly the call sites of the
loop; their disjointness at the program level is by the guards (wk set vs
clear, rl set vs clear, register vs working area), as everywhere in the
layer.
The seek at an arbitrary file #
theorem
DescriptiveComplexity.Draw.Prog.reachesIn_ixSeekTo
{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}
[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)
{elt : I → Univ A R P K dd}
{Use : I → Prop}
(hinj : Function.Injective elt)
(hmono : ∀ (u u' : I), WMLt ile u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup : ∀ (u : I) (x : Univ A R P K dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
{t rg rl wk tg : W}
(hnerg : t ≠ rg)
(hnerl : rl ≠ t)
(hnewk : wk ≠ t)
(hnetg : tg ≠ t)
{gtop gbot : I}
(htop : ∀ (y : I), ile y gtop)
(hbot : ∀ (y : I), ile gbot y)
{T : Univ A R P K dd → Prop}
(hTh : IxHolds elt Use T)
(hT : WMSetLt WMLe T (F.cell gbot))
{bg : (Univ A R P K dd → Prop) → (Univ A R P K dd → Prop) → W → A}
{bgN : (Univ A R P K dd → Prop) → W → A}
(hbgwk : ∀ (v r : Univ A R P K dd → Prop), bg v r wk = bitVal PR.zero PR.one (r = v))
(hbgNwk : ∀ (r : Univ A R P K dd → Prop), bgN r wk = PR.zero)
(hbgNoth : ∀ (v r : Univ A R P K dd → Prop) (s : W), s ≠ wk → bgN r s = bg v r s)
(hbgrg : ∀ (v r : Univ A R P K dd → Prop), bg v r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u))
(hbgrl : ∀ (v r : Univ A R P K dd → Prop), bg v r rl = bitVal PR.zero PR.one (r = F.cell gtop))
(hbgtg : ∀ (v : Univ A R P K dd → Prop) (u : I), bg v (F.cell u) tg = bitVal PR.zero PR.one (ixMark elt T u))
{pChk pScan pT2b pTy pTn pA1 pA2 pA2b pA3 : P}
{fc : Q → A}
(hturn : ∀ (g : W → A), g wk = PR.one → g rg ≠ PR.one → PR.HasRight pChk fc g pScan fc g)
(hscanT : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight pScan fc g pScan fc g)
(hbT₁ : ∀ (g : W → A), g rl = PR.one → PR.HasLeft pScan fc g pT2b fc g)
(hbT₂ : ∀ (g : W → A), PR.HasRight pT2b fc g pTy fc g)
(hpass : ∀ (g : W → A), (g t = PR.one ↔ g tg = PR.one) → g rg = PR.one → PR.HasLeft pTy fc g pTy fc g)
(hfail : ∀ (g : W → A), ¬(g t = PR.one ↔ g tg = PR.one) → g rg = PR.one → PR.HasLeft pTy fc g pTn fc g)
(hheldN : ∀ (g : W → A), g rg = PR.one → PR.HasLeft pTn fc g pTn fc g)
(hstayY : ∀ (g : W → A), g rg ≠ PR.one → g wk ≠ PR.one → PR.HasLeft pTy fc g pTy fc g)
(hbackN : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pTn fc g pTn fc g)
(hA₀ :
∀ (v v' : Univ A R P K dd → Prop),
WMIncr WMLe v v' →
WMSetLe WMLe v' T →
PR.HasRight pTn fc (PR.passTracksAt F.cell t (bg v) (ixMark elt v) v) pA1 fc
(PR.passTracksAt F.cell t bgN (ixMark elt v) v))
(hA₁ :
∀ (v v' : Univ A R P K dd → Prop),
WMIncr WMLe v v' →
WMSetLe WMLe v' T →
PR.HasRight pA1 fc (PR.passTracksAt F.cell t bgN (ixMark elt v) v') pA2 fc
(PR.passTracksAt F.cell t (bg v') (ixMark elt v) v'))
(hscanA : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight pA2 fc g pA2 fc g)
(hbA₁ : ∀ (g : W → A), g rl = PR.one → PR.HasLeft pA2 fc g pA2b fc g)
(hbA₂ : ∀ (g : W → A), PR.HasRight pA2b fc g pA3 fc g)
(hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft pA3 fc g pA3 fc (Function.update g t PR.zero))
(hset : ∀ (g : W → A), g t = PR.zero → g rg = PR.one → PR.HasLeft pA3 fc g pChk fc (Function.update g t PR.one))
(hholdC : ∀ (g : W → A), g rg = PR.one → PR.HasLeft pChk fc g pChk fc g)
(hstayA : ∀ (g : W → A), g rg ≠ PR.one → g wk ≠ PR.one → PR.HasLeft pA3 fc g pA3 fc g)
(hbackC : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pChk fc g pChk fc g)
{w : ℕ}
(hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w)
:
(wideData (Univ A R P K dd)).ReachesIn
(wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank ile gtop - ixRank ile gbot) * w + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank ile gtop - ixRank ile gbot) * w + wideRank (F.cell gbot)))
{ state := Sum.inr (PR.stElt pChk fc), head := Sum.inl fun (x : Univ A R P K dd) => False,
tape :=
wideTape (PR.trackTapeAt F.cell t (bg fun (x : Univ A R P K dd) => False) fun (x : I) => False)
(PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pTy fc), head := Sum.inl T,
tape := wideTape (PR.trackTapeAt F.cell t (bg T) (ixMark elt T)) (PR.syElt PR.blank) }
Dependency graph
theorem
DescriptiveComplexity.Draw.Prog.reaches_fileSeekTo
{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}
(F : RegFile (Univ A R P K dd))
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{t rg rl wk tg : W}
(hnerg : t ≠ rg)
(hnerl : rl ≠ t)
(hnewk : wk ≠ t)
(hnetg : tg ≠ t)
{gtop gbot : Univ A R P K dd}
(htop : ∀ (y : Univ A R P K dd), WMLe y gtop)
(hbot : ∀ (y : Univ A R P K dd), WMLe gbot y)
{T : Univ A R P K dd → Prop}
(hT : WMSetLt WMLe T (F.cell gbot))
{bg : (Univ A R P K dd → Prop) → (Univ A R P K dd → Prop) → W → A}
{bgN : (Univ A R P K dd → Prop) → W → A}
(hbgwk : ∀ (v r : Univ A R P K dd → Prop), bg v r wk = bitVal PR.zero PR.one (r = v))
(hbgNwk : ∀ (r : Univ A R P K dd → Prop), bgN r wk = PR.zero)
(hbgNoth : ∀ (v r : Univ A R P K dd → Prop) (s : W), s ≠ wk → bgN r s = bg v r s)
(hbgrg : ∀ (v r : Univ A R P K dd → Prop), bg v r rg = bitVal PR.zero PR.one (∃ (u : Univ A R P K dd), r = F.cell u))
(hbgrl : ∀ (v r : Univ A R P K dd → Prop), bg v r rl = bitVal PR.zero PR.one (r = F.cell gtop))
(hbgtg : ∀ (v : Univ A R P K dd → Prop) (u : Univ A R P K dd), bg v (F.cell u) tg = bitVal PR.zero PR.one (T u))
{pChk pScan pT2b pTy pTn pA1 pA2 pA2b pA3 : P}
{fc : Q → A}
(hturn : ∀ (g : W → A), g wk = PR.one → g rg ≠ PR.one → PR.HasRight pChk fc g pScan fc g)
(hscanT : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight pScan fc g pScan fc g)
(hbT₁ : ∀ (g : W → A), g rl = PR.one → PR.HasLeft pScan fc g pT2b fc g)
(hbT₂ : ∀ (g : W → A), PR.HasRight pT2b fc g pTy fc g)
(hpass : ∀ (g : W → A), (g t = PR.one ↔ g tg = PR.one) → g rg = PR.one → PR.HasLeft pTy fc g pTy fc g)
(hfail : ∀ (g : W → A), ¬(g t = PR.one ↔ g tg = PR.one) → g rg = PR.one → PR.HasLeft pTy fc g pTn fc g)
(hheldN : ∀ (g : W → A), g rg = PR.one → PR.HasLeft pTn fc g pTn fc g)
(hstayY : ∀ (g : W → A), g rg ≠ PR.one → g wk ≠ PR.one → PR.HasLeft pTy fc g pTy fc g)
(hbackN : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pTn fc g pTn fc g)
(hA₀ :
∀ (v v' : Univ A R P K dd → Prop),
WMIncr WMLe v v' →
WMSetLe WMLe v' T →
PR.HasRight pTn fc (PR.passTracksAt F.cell t (bg v) v v) pA1 fc (PR.passTracksAt F.cell t bgN v v))
(hA₁ :
∀ (v v' : Univ A R P K dd → Prop),
WMIncr WMLe v v' →
WMSetLe WMLe v' T →
PR.HasRight pA1 fc (PR.passTracksAt F.cell t bgN v v') pA2 fc (PR.passTracksAt F.cell t (bg v') v v'))
(hscanA : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight pA2 fc g pA2 fc g)
(hbA₁ : ∀ (g : W → A), g rl = PR.one → PR.HasLeft pA2 fc g pA2b fc g)
(hbA₂ : ∀ (g : W → A), PR.HasRight pA2b fc g pA3 fc g)
(hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft pA3 fc g pA3 fc (Function.update g t PR.zero))
(hset : ∀ (g : W → A), g t = PR.zero → g rg = PR.one → PR.HasLeft pA3 fc g pChk fc (Function.update g t PR.one))
(hholdC : ∀ (g : W → A), g rg = PR.one → PR.HasLeft pChk fc g pChk fc g)
(hstayA : ∀ (g : W → A), g rg ≠ PR.one → g wk ≠ PR.one → PR.HasLeft pA3 fc g pA3 fc g)
(hbackC : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pChk fc g pChk fc g)
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt pChk fc), head := Sum.inl fun (x : Univ A R P K dd) => False,
tape :=
wideTape (PR.trackTapeAt F.cell t (bg fun (x : Univ A R P K dd) => False) fun (x : Univ A R P K dd) => False)
(PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pTy fc), head := Sum.inl T,
tape := wideTape (PR.trackTapeAt F.cell t (bg T) T) (PR.syElt PR.blank) }
The seek loop, the budget forgotten.