The evaluation's spine: the per-variable loop

The per-address evaluation the outer program abstracts (DescriptiveComplexity.Problems.Wide.DrawOuter) factors once more, the same way: a spine – one checkpoint per variable position, dispatching into that variable's machinery and, after the last, back into the outer loop – around per-variable sub-machineries (the gates, the VAL loop, the atom subroutines, the stage write) that stay abstract here.

A checkpoint phase chk k owns two things: the walk back to the marker (entering rules step right off it, as everywhere in the assembly) and the dispatch at the marker. For k < nv the dispatch enters variable k's machinery; at k = nv it is the pair of outer boundary rules the outer file promised – erase the marker and step right, into the sweep's advance below the ltp cell, into the post-sweep reset at it. A sub-machinery's final exit targets the next checkpoint, which is how the spine needs to know nothing about its internals.

The spine's shapes

inductive DescriptiveComplexity.Draw.EvalPh (nv : ℕ) (PM : Type) : Type

The phases of the evaluation: one checkpoint per variable position (the last is the return to the outer loop), and the sub-machineries'.

• chk {nv : ℕ} {PM : Type} : Fin (nv + 1) → EvalPh nv PM

  The checkpoint before variable k (at k = nv: after the last).

• sub {nv : ℕ} {PM : Type} : PM → EvalPh nv PM

  A phase of a sub-machinery.

instance DescriptiveComplexity.Draw.instFiniteEvalPh {nv : ℕ} {PM : Type} [Finite PM] : Finite (EvalPh nv PM)

inductive DescriptiveComplexity.Draw.EvalSite (nv : ℕ) (SM : Type) : Type

The sites of the evaluation: one per checkpoint, and the sub-machineries'.

• chk {nv : ℕ} {SM : Type} : Fin (nv + 1) → EvalSite nv SM

  A checkpoint site.

• sub {nv : ℕ} {SM : Type} : SM → EvalSite nv SM

  A sub-machinery site.

inductive DescriptiveComplexity.Draw.EvalChkRule : Type

The rules of a checkpoint: the walk back to the marker, and the two dispatches (the second is only live at the last checkpoint).

• stay : EvalChkRule

  Walk left back to the marker.

• dspA : EvalChkRule

  Dispatch: into the variable's machinery, or – at the last checkpoint, below the ltp cell – into the sweep's advance.

• dspB : EvalChkRule

  Dispatch at the last checkpoint, at the ltp cell: into the post-sweep reset. Dead below the last checkpoint.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqEvalChkRule : DecidableEq EvalChkRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqEvalChkRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteEvalChkRule : Finite EvalChkRule

def DescriptiveComplexity.Draw.EvalSh (nv : ℕ) (SM : Type) (ShM : SM → Type) : EvalSite nv SM → Type

The rule shape of each evaluation site.

Equations

• DescriptiveComplexity.Draw.EvalSh nv SM ShM (DescriptiveComplexity.Draw.EvalSite.chk a) = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.EvalSh nv SM ShM (DescriptiveComplexity.Draw.EvalSite.sub s) = ShM s

noncomputable def DescriptiveComplexity.Draw.Data.evalRule {L : FirstOrder.Language} (dt : Data L) {A Q PM SM : Type} {nv : ℕ} (zero one : A) {ShM : SM → Type} (ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (OuterPh (EvalPh nv PM))) (subEntry : Fin nv → PM) (i : EvalSite nv SM) : EvalSh nv SM ShM i → Rule A Q dt.SlotIx (OuterPh (EvalPh nv PM))

The rules of the evaluation's spine: per checkpoint the walk back and the dispatches; the sub-machineries' rules are the parameter.

Equations

• One or more equations did not get rendered due to their size.
• dt.evalRule zero one ruleM subEntry (DescriptiveComplexity.Draw.EvalSite.sub s) ρ = ruleM s ρ

def DescriptiveComplexity.Draw.Data.evalOwn {PM SM : Type} {nv : ℕ} (ownM : PM → SM) : EvalPh nv PM → EvalSite nv SM

The ownership of the evaluation's phases.

Equations

• DescriptiveComplexity.Draw.Data.evalOwn ownM (DescriptiveComplexity.Draw.EvalPh.chk k) = DescriptiveComplexity.Draw.EvalSite.chk k
• DescriptiveComplexity.Draw.Data.evalOwn ownM (DescriptiveComplexity.Draw.EvalPh.sub p) = DescriptiveComplexity.Draw.EvalSite.sub (ownM p)

theorem DescriptiveComplexity.Draw.Data.evalHosrc {L : FirstOrder.Language} (dt : Data L) {A Q PM SM : Type} {nv : ℕ} (zero one : A) {ShM : SM → Type} {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (OuterPh (EvalPh nv PM))} {subEntry : Fin nv → PM} {ownM : PM → SM} (hosrcM : ∀ (s : SM) (ρ : ShM s), ∃ (p : PM), (ruleM s ρ).srcPh = OuterPh.evalP (EvalPh.sub p) ∧ ownM p = s) (e : EvalSite nv SM) (ρ : EvalSh nv SM ShM e) : ∃ (p : EvalPh nv PM), (dt.evalRule zero one ruleM subEntry e ρ).srcPh = OuterPh.evalP p ∧ evalOwn ownM p = e

Every spine rule fires from a phase its site owns; the sub-machineries' obligation is the parameter.

theorem DescriptiveComplexity.Draw.Data.evalSep {L : FirstOrder.Language} (dt : Data L) {A Q PM SM : Type} {nv : ℕ} (zero one : A) {ShM : SM → Type} {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (OuterPh (EvalPh nv PM))} {subEntry : Fin nv → PM} (hsepM : ∀ (s : SM) (ρ ρ' : ShM s) (f : Q → A) (g : dt.SlotIx → A), (ruleM s ρ).guard f g → (ruleM s ρ').guard f g → (ruleM s ρ).srcPh = (ruleM s ρ').srcPh → ρ = ρ') (e : EvalSite nv SM) (ρ ρ' : EvalSh nv SM ShM e) (f : Q → A) (g : dt.SlotIx → A) : (dt.evalRule zero one ruleM subEntry e ρ).guard f g → (dt.evalRule zero one ruleM subEntry e ρ').guard f g → (dt.evalRule zero one ruleM subEntry e ρ).srcPh = (dt.evalRule zero one ruleM subEntry e ρ').srcPh → ρ = ρ'

The spine separates in-shape: per checkpoint, the walk's guard is disjoint from the dispatches' and the two dispatches split on the ltp mark; the sub-machineries' separation is the parameter.