Assembling a program from call sites

The EXPSPACE program is large, but its rule set is a sum over call sites of small, separately checkable contributions – kit instantiations plus their exit rules. This file is the assembly: a DescriptiveComplexity.Draw.Assembly packages a family of per-site rule shapes, an ownership map from phases to sites, and the two coherence facts (every rule fires from a phase its site owns; each site separates in-shape); DescriptiveComplexity.Draw.Assembly.prog is the program whose rule names are the sigma, and DescriptiveComplexity.Draw.Assembly.sep its separation – via DescriptiveComplexity.Draw.sep_sigma, so DescriptiveComplexity.Draw.Table.deterministic applies with no global case bash.

The point of the shape: the concrete program need never be stated as one monolithic rule inductive. Each call site is built and checked in its own file – its Sh i a kit rule type (or a sum of one with its exit rules), its hsep i the kit's sep plus its exit_disjoint – and the assembly is the only place they meet.

structure DescriptiveComplexity.Draw.Assembly (A Q W P S : Type) [Fintype Q] [Fintype W] : Type 1

A program assembled from call sites: a family of rule shapes, one per site, an ownership map from phases to sites, and the two coherence facts that make the whole separate. The remaining fields of DescriptiveComplexity.Draw.Prog – the designated elements and the machine's constants – are carried alongside, untouched by the assembly.

• Sh : S → Type

  The rule shape of each site.

• rule (i : S) : self.Sh i → Rule A Q W P

  The rules each site contributes.

• owner : P → S

  Which site owns each phase.

• howner (i : S) (ρ : self.Sh i) : self.owner (self.rule i ρ).srcPh = i

  Every rule fires from a phase its site owns.

• hsep (i : S) (ρ ρ' : self.Sh i) (f : Q → A) (g : W → A) : (self.rule i ρ).guard f g → (self.rule i ρ').guard f g → (self.rule i ρ).srcPh = (self.rule i ρ').srcPh → ρ = ρ'

  Each site separates in-shape.

def DescriptiveComplexity.Draw.Assembly.prog {A Q W P S K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (asm : Assembly A Q W P S) (zero one : A) (hzo : zero ≠ one) (hpl : Fintype.card (Q ⊕ W) ≤ dd) (startPh : P) (startSt : Q → A) (accept : P → (Q → A) → Prop) (blank : W → A) (mark : Univ A ((i : S) × asm.Sh i) P K dd → W → A) : Prog A ((i : S) × asm.Sh i) P Q W K dd

The assembled program: rule names are the sigma of the sites' shapes; everything else is the supplied constants.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Assembly.sep {A Q W P S K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (asm : Assembly A Q W P S) {zero one : A} {hzo : zero ≠ one} {hpl : Fintype.card (Q ⊕ W) ≤ dd} {startPh : P} {startSt : Q → A} {accept : P → (Q → A) → Prop} {blank : W → A} {mark : Univ A ((i : S) × asm.Sh i) P K dd → W → A} : (asm.prog zero one hzo hpl startPh startSt accept blank mark).table.Sep

The assembled program separates: cross-site by ownership, in-site by the sites' own separation – DescriptiveComplexity.Draw.Prog.sep_of then yields DescriptiveComplexity.Draw.Table.Sep, and with DescriptiveComplexity.Draw.Table.deterministic the emitted instance is deterministic.