The sequencer: heterogeneous stages in a row

The matrix of a step formula is evaluated atom by atom, and the gates block by block: a sequence of machineries of different shapes – a stage atom's random access here, a tag-branched element loop there – with a checkpoint between consecutive ones and an exit after the last. The chain combinator of DescriptiveComplexity.Problems.Wide.DrawChain fixes a single stage family; this file is its dependent sibling: n stages with their own phase and shape types (PA/SA-indexed families), n + 1 checkpoints, the k-th dispatching into stage k's entry and the last leaving.

The per-stage machineries and their separation are parameters, so the matrix instantiates this with the kind-dependent atom machineries and the gates with the per-block gate machinery, and neither needs a new checkpoint proof.

The shapes

inductive DescriptiveComplexity.Draw.SeqPh (n : ℕ) (PA : Fin n → Type) : Type

The phases of a sequence: n + 1 checkpoints and the stages'.

• chk {n : ℕ} {PA : Fin n → Type} : Fin (n + 1) → SeqPh n PA

  The checkpoint before stage k (at k = n: after the last).

• sub {n : ℕ} {PA : Fin n → Type} (a : Fin n) : PA a → SeqPh n PA

  A phase of stage a.

inductive DescriptiveComplexity.Draw.SeqSite (n : ℕ) (SA : Fin n → Type) : Type

The sites of a sequence.

• chk {n : ℕ} {SA : Fin n → Type} : Fin (n + 1) → SeqSite n SA

  A checkpoint site.

• sub {n : ℕ} {SA : Fin n → Type} (a : Fin n) : SA a → SeqSite n SA

  A site of stage a.

def DescriptiveComplexity.Draw.SeqSh (n : ℕ) {SA : Fin n → Type} (ShA : (a : Fin n) → SA a → Type) : SeqSite n SA → Type

The rule shape of each sequence site.

Equations

• DescriptiveComplexity.Draw.SeqSh n ShA (DescriptiveComplexity.Draw.SeqSite.chk a) = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.SeqSh n ShA (DescriptiveComplexity.Draw.SeqSite.sub a s) = ShA a s

def DescriptiveComplexity.Draw.seqOwn {n : ℕ} {PA SA : Fin n → Type} (ownA : (a : Fin n) → PA a → SA a) : SeqPh n PA → SeqSite n SA

The owner of each phase of a sequence, over the stages' owners.

Equations

• DescriptiveComplexity.Draw.seqOwn ownA (DescriptiveComplexity.Draw.SeqPh.chk k) = DescriptiveComplexity.Draw.SeqSite.chk k
• DescriptiveComplexity.Draw.seqOwn ownA (DescriptiveComplexity.Draw.SeqPh.sub a p) = DescriptiveComplexity.Draw.SeqSite.sub a (ownA a p)

def DescriptiveComplexity.Draw.seqRule {A Q W P : Type} {n : ℕ} {PA SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} (one : A) (wk rg : W) (emb : SeqPh n PA → P) (ruleA : (a : Fin n) → (s : SA a) → ShA a s → Rule A Q W P) (entry : (a : Fin n) → PA a) (enterSt : Fin n → (Q → A) → (W → A) → Q → A) (exitPh : P) (i : SeqSite n SA) : SeqSh n ShA i → Rule A Q W P

The rules of a sequence: per checkpoint the walk back and the dispatch – into the next stage's entry, or out after the last.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.seqRule one wk rg emb ruleA entry enterSt exitPh (DescriptiveComplexity.Draw.SeqSite.sub a s) ρ = ruleA a s ρ