The clocked program's rules are definable

A reduction has to write its machine down: the emitted table must be read off the interpreted structure, which is what DescriptiveComplexity.Draw.Data.reads_progFrom asks, and what it asks of the rules is that each of them be first-order definable in the sense of DescriptiveComplexity.Draw.URulesDefinable.

The clocked program shares its whole tower with the space-bounded one, so the tower's definability (DescriptiveComplexity.Draw.Data.uRulesDefinable_varRuleF) serves unchanged; what is new is the spine, whose checkpoints have two rules instead of three, and the outer layer, whose sweeps are specifications rather than kits. Both are here, and so are the program's own two specifications: uRulesDefinable_nexProg is the whole clocked rule set, and what a reduction still owes is its own VarArgs, the same obligation the space-bounded one already meets.

What the file's advance computes

The one thing a clocked program writes that is not a copy of a slot is its sweep's pointer, and what it holds after a step is the next register's own tuple. Below the last tuple of a block that is the tuple's lexicographic successor, which is what the definability of the advance is read off.

The clocked spine

The file-laying sweep's own definability

What USweepSpecDef asks of DescriptiveComplexity.Draw.Data.buildSpec, one field at a time. The two tests are questions about the pointer's coordinates – each is the greatest element, or the pointer is at the last register – and the st0 reset writes the least element into them.

The outer layer

A clocked program's two sweeps are specifications rather than kits: what they write at a cell, where they leave the pointer, and when they are over are the caller's, so their definability is the caller's too. These are the two bundles, and everything else in the outer layer – the opening step, the approach, the two walks home and their exits, the guess's stop – is a constant rule with a guard the toolkit already has.

structure DescriptiveComplexity.Draw.Data.USweepSpecDef {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {B : Type} (β : (e : Env L) → SweepSpec e.α Q dt.SlotIx B) : Prop

What makes a file-laying sweep definable: its write, its three pointers and its two tests. The next block is a function of the phase alone, so nothing is asked of it.

• wr (b : B) : UTrDefinable fun (e : Env L) => (β e).wr b

  The tracks it leaves at the cell.

• st (b : B) : UStDefinable fun (e : Env L) => (β e).st b

  The pointer it leaves within a block.

• st0 : UStDefinable fun (e : Env L) => (β e).st0

  The pointer the exit resets to the file's first register.

• stRoll (b : B) : UStDefinable fun (e : Env L) => (β e).stRoll b

  The pointer it leaves at a roll-over.

• nx (b : B) : ∃ (b' : B), ∀ (e : Env L), (β e).nx b = b'

  The next block is chosen when the formula is built, not at the instance.

• roll (b : B) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => (β e).Roll b f

  The roll-over test.

• done (b : B) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => (β e).Done b f

  The stop test.

structure DescriptiveComplexity.Draw.Data.UGuessSpecDef {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {B G : Type} (γ : (e : Env L) → GuessSpec e.α Q dt.SlotIx B G) : Prop

And what makes a guessing sweep definable: the same, at each value it may guess.

• wr (b : B) (x : G) : UTrDefinable fun (e : Env L) => (γ e).wr b x

  The tracks it leaves at the cell, at this value.

• st (b : B) (x : G) : UStDefinable fun (e : Env L) => (γ e).st b x

  The pointer it leaves, at this value.

• stRoll (b : B) (x : G) : UStDefinable fun (e : Env L) => (γ e).stRoll b x

  The pointer it leaves at a roll-over.

• nx (b : B) : ∃ (b' : B), ∀ (e : Env L), (γ e).nx b = b'

  The next block is chosen when the formula is built.

• roll (b : B) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => (γ e).Roll b f

  The roll-over test.

• done (b : B) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => (γ e).Done b f

  The stop test.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_nexProg {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty dt.KIx] {coord : Fin dt.dd → dt.CtlIx} (hcoord : Function.Injective coord) {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.nexRule e.one (dt.buildSpec e.zero e.one coord) (dt.regionSpec e.zero e.one) (dt.nexEvalRuleF e.zero e.one (args e)) (EvalPh.chk 0) bot

The clocked program's own rule set is definable: the two sweeps it actually runs, the tower it shares with the space-bounded program, and the outer layer around them. This is what a reduction emitting the clocked machine has to hand DescriptiveComplexity.Draw.Data.reads_progFrom; what is left to it is its own VarArgs, which is the same obligation the space-bounded reduction already meets.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_nexProgHanded {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.nexRule e.one (dt.nullSpec (Option dt.KIx)) (dt.regionSpec e.zero e.one) (dt.nexEvalRuleF e.zero e.one (args e)) (EvalPh.chk 0) bot

The rule set of a clocked program that is handed its file is definable, and needs no coordinate map: the sweep that would have laid the file is nullSpec, whose definability is free, so nothing in the program asks for an injective Fin dd → CtlIx – which is the map no wide machine's control can hold (DescriptiveComplexity.Draw.card_ctl_lt_card_univ). This is the rule set a reduction into DescriptiveComplexity.WideRegAccept emits.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_nexAccept {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {B PE : Type} {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (h : UVarArgsDef none fun (e : Env L) => args e none) (p : NexPh B PE) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => p = NexPh.acceptP ∧ (args e none).accBit f

The clocked program's accepting predicate is definable: the phase is decided when the formula is built, and the bit it conjoins is the outermost variable's verdict – the same field the space-bounded program accepts on.