The chain combinator: checkpoints around abstract stages

The outer program, the evaluation's spine and one variable's machinery all repeat one pattern: checkpoints – a phase whose stay rule walks left to the working-cell marker and whose dispatch rules fire there – between stages that are kit instances or further abstract blocks. The remaining machinery (the gates, the per-atom subroutines, the tuple and element loops) is more of the same, so this file is the pattern as a combinator, built once:

• DescriptiveComplexity.Draw.PreRule – a rule without its source phase, what a dispatch descriptor is;
• DescriptiveComplexity.Draw.ChainPh/ChainSite/ChainSh – n checkpoints (each carrying the three-rule gadget of DescriptiveComplexity.Draw.EvalChkRule) plus an abstract stage family;
• DescriptiveComplexity.Draw.chainRule – the rules, the dispatches given as descriptors per checkpoint (Fin n → Bool → PreRule): a descriptor's target may be any phase, so loops – a tuple loop's back edge – cost nothing;
• DescriptiveComplexity.Draw.chainSep/chainHosrc – separation and ownership, from two per-checkpoint hypotheses: every dispatch fires only at the marker, and the two dispatches of a checkpoint never fire together.

A machinery block is then a stage family (its kits, with their sep and exit_disjoint) plus a descriptor list, and nothing else.

Rules without their source phase

structure DescriptiveComplexity.Draw.PreRule (A Q W P : Type) : Type

A rule without its source phase: what a chain's dispatch descriptor is – the checkpoint it belongs to supplies the source.

• guard : (Q → A) → (W → A) → Prop

  When the rule applies.

• dstPh : P

  The phase the rule moves to.

• dstSt : (Q → A) → (W → A) → Q → A

  The pointer the rule leaves in the control.

• wr : (Q → A) → (W → A) → W → A

  The tracks the rule writes.

• moveRight : Prop

  Whether the rule moves the head right.

def DescriptiveComplexity.Draw.PreRule.toRule {A Q W P : Type} (r : PreRule A Q W P) (p : P) : Rule A Q W P

A descriptor, at a source phase.

Equations

• r.toRule p = { guard := r.guard, srcPh := p, dstPh := r.dstPh, dstSt := r.dstSt, wr := r.wr, moveRight := r.moveRight }

The chain's shapes

inductive DescriptiveComplexity.Draw.ChainPh (n : ℕ) (PS : Type) : Type

The phases of a chain: n checkpoints, and the stages'.

• chk {n : ℕ} {PS : Type} : Fin n → ChainPh n PS

  A checkpoint.

• sub {n : ℕ} {PS : Type} : PS → ChainPh n PS

  A stage phase.

instance DescriptiveComplexity.Draw.instFiniteChainPh {n : ℕ} {PS : Type} [Finite PS] : Finite (ChainPh n PS)

inductive DescriptiveComplexity.Draw.ChainSite (n : ℕ) (SS : Type) : Type

The sites of a chain.

• chk {n : ℕ} {SS : Type} : Fin n → ChainSite n SS

  A checkpoint site.

• sub {n : ℕ} {SS : Type} : SS → ChainSite n SS

  A stage site.

def DescriptiveComplexity.Draw.ChainSh (n : ℕ) (SS : Type) (ShS : SS → Type) : ChainSite n SS → Type

The rule shape of each chain site: checkpoints carry the three-rule gadget, stages their own shapes.

Equations

• DescriptiveComplexity.Draw.ChainSh n SS ShS (DescriptiveComplexity.Draw.ChainSite.chk a) = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.ChainSh n SS ShS (DescriptiveComplexity.Draw.ChainSite.sub s) = ShS s

The rules

def DescriptiveComplexity.Draw.chainRule {A Q W P PS SS : Type} {n : ℕ} {ShS : SS → Type} (one : A) (wk : W) (emb : ChainPh n PS → P) (ruleS : (s : SS) → ShS s → Rule A Q W P) (dsp : Fin n → Bool → PreRule A Q W P) (i : ChainSite n SS) : ChainSh n SS ShS i → Rule A Q W P

The rules of a chain: per checkpoint the walk back to the marker and its two dispatch descriptors; the stages' rules are the parameter.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.chainRule one wk emb ruleS dsp (DescriptiveComplexity.Draw.ChainSite.sub s) ρ = ruleS s ρ

theorem DescriptiveComplexity.Draw.chainRule_dstIn {A Q W P PS SS : Type} {n : ℕ} {ShS : SS → Type} {one : A} {wk : W} {emb : ChainPh n PS → P} {ruleS : (s : SS) → ShS s → Rule A Q W P} {dsp : Fin n → Bool → PreRule A Q W P} {S : P → Prop} (hemb : ∀ (p : ChainPh n PS), S (emb p)) (hdsp : ∀ (k : Fin n) (b : Bool), S (dsp k b).dstPh) (hS : ∀ (s : SS) (ρ : ShS s), S (ruleS s ρ).dstPh) (i : ChainSite n SS) (ρ : ChainSh n SS ShS i) : S (chainRule one wk emb ruleS dsp i ρ).dstPh

A property of a chain's phases and its dispatches' destinations holds of every phase it can move to: the checkpoints stay where they are, the dispatches go where their descriptors say, and the stages are the parameter. This is what a determinism-after-the-guess argument asks of a sequenced machinery (DescriptiveComplexity.Draw.Data.nexProg_uniqueFrom).

theorem DescriptiveComplexity.Draw.chainSep {A Q W P PS SS : Type} {n : ℕ} {ShS : SS → Type} {one : A} {wk : W} {emb : ChainPh n PS → P} {ruleS : (s : SS) → ShS s → Rule A Q W P} {dsp : Fin n → Bool → PreRule A Q W P} (hwk : ∀ (k : Fin n) (b : Bool) (f : Q → A) (g : W → A), (dsp k b).guard f g → g wk = one) (hAB : ∀ (k : Fin n) (f : Q → A) (g : W → A), ¬((dsp k false).guard f g ∧ (dsp k true).guard f g)) (hsepS : ∀ (s : SS) (ρ ρ' : ShS s) (f : Q → A) (g : W → A), (ruleS s ρ).guard f g → (ruleS s ρ').guard f g → (ruleS s ρ).srcPh = (ruleS s ρ').srcPh → ρ = ρ') (i : ChainSite n SS) (ρ ρ' : ChainSh n SS ShS i) (f : Q → A) (g : W → A) : (chainRule one wk emb ruleS dsp i ρ).guard f g → (chainRule one wk emb ruleS dsp i ρ').guard f g → (chainRule one wk emb ruleS dsp i ρ).srcPh = (chainRule one wk emb ruleS dsp i ρ').srcPh → ρ = ρ'

A chain separates in-shape: the stay's guard is disjoint from the dispatches' – they only fire at the marker – and the two dispatches of a checkpoint never fire together; the stages' separation is the parameter.

theorem DescriptiveComplexity.Draw.chainHosrc {A Q W P PS SS : Type} {n : ℕ} {ShS : SS → Type} {one : A} {wk : W} {emb : ChainPh n PS → P} {ruleS : (s : SS) → ShS s → Rule A Q W P} {dsp : Fin n → Bool → PreRule A Q W P} {S' : Type} (site : ChainSite n SS → S') (own : ChainPh n PS → S') (hownChk : ∀ (k : Fin n), own (ChainPh.chk k) = site (ChainSite.chk k)) (hosrcS : ∀ (s : SS) (ρ : ShS s), ∃ (p : ChainPh n PS), (ruleS s ρ).srcPh = emb p ∧ own p = site (ChainSite.sub s)) (i : ChainSite n SS) (ρ : ChainSh n SS ShS i) : ∃ (p : ChainPh n PS), (chainRule one wk emb ruleS dsp i ρ).srcPh = emb p ∧ own p = site i

Every chain rule fires from a phase its site owns; the stages' obligation is the parameter.