Documentation

DescriptiveComplexity.Problems.Wide.DrawRunEval

The evaluation spine's run #

The run theorem of DescriptiveComplexity.Draw.Data.evalRule: from the checkpoint before the first variable to the checkpoint after the last, one abstract sub-machinery run per position – the spine contributes only its dispatches and walk-backs, so it needs to know nothing about a machinery's internals beyond its entry phase, its control transform and its tape transform.

The run comes with its cost (eval_reachesIn): one machinery's width plus its dispatch and its walk back, once per variable. eval_run is it with the budget forgotten.

The two boundary steps at the last checkpoint – erase the marker rightwards into the sweep's advance, or into the post-sweep reset at the ltp cell – are separate single-step lemmas, consumed by the outer composition.

source
theorem DescriptiveComplexity.Draw.Data.eval_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R Q PM SM : Type} {nv : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh nv PM))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh nv PM))] {ShM : SM → Type} {PR : Prog A R (OuterPh (EvalPh nv PM)) Q dt.SlotIx dt.KIx dt.dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd) I ile) {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (OuterPh (EvalPh nv PM))} {subEntry : Fin nv → PM} {rEmb : (i : EvalSite nv SM) → EvalSh nv SM ShM i → R} (hrules : ∀ (i : EvalSite nv SM) (ρ : EvalSh nv SM ShM i), PR.rules (rEmb i ρ) = dt.evalRule PR.zero PR.one ruleM subEntry i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {restOf : Fin (nv + 1) → (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {mvOf : Fin (nv + 1) → I → Prop} (hwkOf : ∀ (k : Fin (nv + 1)) (r : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop), restOf k r Slot.wk = bitVal PR.zero PR.one (r = v)) (hrgOf : ∀ (k : Fin (nv + 1)) (r : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop), restOf k r Slot.reg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (fs : Fin (nv + 1) → Q → A) (w : ℕ) (hVar : ∀ (k : Fin nv), (wideData (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)).ReachesIn w { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (subEntry k))) (fs k.castSucc)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf k.castSucc) (mvOf k.castSucc)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk k.succ)) (fs k.succ)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf k.succ) (mvOf k.succ)) (PR.syElt PR.blank) }) :
(wideData (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)).ReachesIn ((w + 2) * nv) { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk 0)) (fs 0)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf 0) (mvOf 0)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk (Fin.last nv))) (fs (Fin.last nv))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf (Fin.last nv)) (mvOf (Fin.last nv))) (PR.syElt PR.blank) }

The spine's run, on a clock: from the checkpoint before the first variable at the marker to the checkpoint after the last, one machinery run per position, each with its dispatch and its walk back.

Dependency graph
source
theorem DescriptiveComplexity.Draw.Data.eval_run {L : FirstOrder.Language} (dt : Data L) {A R Q PM SM : Type} {nv : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh nv PM))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh nv PM))] {ShM : SM → Type} {PR : Prog A R (OuterPh (EvalPh nv PM)) Q dt.SlotIx dt.KIx dt.dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd) I ile) {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (OuterPh (EvalPh nv PM))} {subEntry : Fin nv → PM} {rEmb : (i : EvalSite nv SM) → EvalSh nv SM ShM i → R} (hrules : ∀ (i : EvalSite nv SM) (ρ : EvalSh nv SM ShM i), PR.rules (rEmb i ρ) = dt.evalRule PR.zero PR.one ruleM subEntry i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {restOf : Fin (nv + 1) → (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {mvOf : Fin (nv + 1) → I → Prop} (hwkOf : ∀ (k : Fin (nv + 1)) (r : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop), restOf k r Slot.wk = bitVal PR.zero PR.one (r = v)) (hrgOf : ∀ (k : Fin (nv + 1)) (r : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop), restOf k r Slot.reg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (fs : Fin (nv + 1) → Q → A) (hVarR : ∀ (k : Fin nv), Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (subEntry k))) (fs k.castSucc)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf k.castSucc) (mvOf k.castSucc)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk k.succ)) (fs k.succ)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf k.succ) (mvOf k.succ)) (PR.syElt PR.blank) }) :
Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk 0)) (fs 0)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf 0) (mvOf 0)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk (Fin.last nv))) (fs (Fin.last nv))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf (Fin.last nv)) (mvOf (Fin.last nv))) (PR.syElt PR.blank) }

The spine's run, the budget forgotten: what a space-bounded caller reads, its machineries' runs carrying no count.

Dependency graph