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

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