The clocked machine, written down

DescriptiveComplexity.Draw.Data.reads_progFrom says of a program that the interpreted structure reads its table, and it says it of DescriptiveComplexity.Draw.Data.progFrom – the program assembled from a definable rule set, a start phase, an accepting predicate and an initial mark. The clocked program is written by hand (DescriptiveComplexity.Draw.Data.nexProg), so what is needed here is that the two are the same program: they differ in one field only, the initial pointer, and there the file's first register carries the least tuple, which is clear at every coordinate.

With that, the clocked machine is written down exactly as the space-bounded one is: nexInterp is the interpretation and reads_nexProg the fact a reduction hands the run layer. What is left to a reduction emitting it is its own DescriptiveComplexity.Draw.Data.VarArgs, the obligation the space-bounded reduction already meets.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexRTag {L : FirstOrder.Language} (dt : Data L) (G : Type) : Type

The clocked program's rule names, as the interpretation names them: a site of the outer layer or of the evaluation, and one of that site's rules.

Equations

• dt.NexRTag G = DescriptiveComplexity.Draw.Data.RTagOf (DescriptiveComplexity.Draw.NexSite dt.SEF) (DescriptiveComplexity.Draw.NexSh dt.SEF (Option dt.KIx) G dt.NexSESh)

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexPF {L : FirstOrder.Language} (dt : Data L) : Type

The clocked program's phases.

Equations

• dt.NexPF = DescriptiveComplexity.Draw.NexPh (Option dt.KIx) (DescriptiveComplexity.Draw.EvalPh dt.nv dt.PMF)

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexITag {L : FirstOrder.Language} (dt : Data L) (G : Type) : Type

The tags of the clocked machine's universe.

Equations

• dt.NexITag G = dt.ITagOf (DescriptiveComplexity.Draw.NexSite dt.SEF) (DescriptiveComplexity.Draw.NexSh dt.SEF (Option dt.KIx) G dt.NexSESh) dt.NexPF

theorem DescriptiveComplexity.Draw.Data.nexProg_eq_progFrom {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite dt.KIx] [Nonempty dt.KIx] {G : Type} (e : Env L) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (coord : Fin dt.dd → dt.CtlIx) (β : SweepSpec e.α dt.CtlIx dt.SlotIx (Option dt.KIx)) (γ : GuessSpec e.α dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) : dt.nexProg e.zero e.one ⋯ hpl coord β γ args bot = progFrom hpl e (fun (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) G dt.NexSESh i) => dt.nexRule e.one β γ (dt.nexEvalRuleF e.zero e.one args) (EvalPh.chk 0) bot i ρ) NexPh.start (fun (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → e.α) => p = NexPh.acceptP ∧ (args none).accBit f) blankMark

The clocked program is the program the interpretation writes down: the rules are the same function of the rule name, the start phase, the accepting predicate and the blank tape are the same, and the initial pointer – the file's first register – is clear at every coordinate, because the least index of the layout carries the least tuple.

The interpretation, and what it reads

The clocked program's guess writes one bit per fixed-point variable of the source, so the guessed data of its outer layer is dt.d.B.ι → Bool; that is the rule names' second component, and the reduction supplies the two orders on the names and the phases (any linear order will do – they are finite types).

noncomputable def DescriptiveComplexity.Draw.Data.nexInterp {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty dt.KIx] [LinearOrder (dt.NexRTag (dt.d.B.ι → Bool))] [LinearOrder dt.NexPF] {coord : Fin dt.dd → dt.CtlIx} {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hcoord : Function.Injective coord) (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) (bot : Option dt.KIx) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.wide (dt.NexITag (dt.d.B.ι → Bool)) dt.dd

The clocked machine, written down: the interpretation of the wide-machine vocabulary whose universe is tagged by the clocked program's own rule names and phases.

Equations

• DescriptiveComplexity.Draw.Data.nexInterp hpl hcoord h bot = DescriptiveComplexity.Draw.Data.drawInterp hpl ⋯ ⋯ DescriptiveComplexity.Draw.NexPh.start DescriptiveComplexity.Draw.Data.blankMark

theorem DescriptiveComplexity.Draw.Data.reads_nexProg {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite dt.KIx] [Nonempty dt.KIx] [LinearOrder (dt.NexRTag (dt.d.B.ι → Bool))] [LinearOrder dt.NexPF] {coord : Fin dt.dd → dt.CtlIx} {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hcoord : Function.Injective coord) (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) (bot : Option dt.KIx) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (dt.NexRTag (dt.d.B.ι → Bool)) dt.NexPF dt.KIx dt.dd)] (hws : ws = (nexInterp hpl hcoord h bot).mapStructure e.α) : (dt.nexProg e.zero e.one ⋯ hpl coord (dt.buildSpec e.zero e.one coord) (dt.regionSpec e.zero e.one) (args e) bot).table.Reads

The interpreted structure reads the clocked program's table: the whole point of the definability layer, at the program the reduction emits. This is what the run layer's lemmas are stated under.