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.

theorem DescriptiveComplexity.Draw.blkNext_snd_of_ne_tupTop {A K : Type} [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] {dd : ℕ} [Nonempty A] {u : Wide.BlkIx K A dd} (hu : u.2 ≠ tupTop A dd) : (blkNext A K dd u).2 = tupNext u.2

Within a block the advance is the tuple's own successor: the layout order is block-major and the tuples are ordered lexicographically, so below the last tuple the next register is the same block at the next tuple.

noncomputable def DescriptiveComplexity.Draw.blkTopB (K : Type) [LinearOrder K] [Finite K] [Nonempty K] : Option K

The greatest block: the last of the layout's blocks, which is a fact about the block order alone and not about the instance.

Equations

• DescriptiveComplexity.Draw.blkTopB K = ⋯.choose

theorem DescriptiveComplexity.Draw.fst_blkTop {A K : Type} [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] {dd : ℕ} [Nonempty A] [Nonempty K] : (blkTop A K dd).1 = blkTopB K

The last register's block is that greatest block: the layout order is block-major, so the greatest index sits in the greatest block whatever the instance. This is what makes the sweep's stop test a question the formula can be built from – it compares the phase's block with a constant.

theorem DescriptiveComplexity.Draw.snd_blkBot_apply {A K : Type} [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] {dd : ℕ} [Nonempty A] [Nonempty K] {zero : A} (hbot : ∀ (a : A), zero ≤ a) (j : Fin dd) : (blkBot A K dd).2 j = zero

The first register's tuple is the least element everywhere: the layout order is block-major and lexicographic within a block, so the least index of a block carries the least tuple. This is what the sweep's exit writes into the pointer when it resets to the file's first register.

theorem DescriptiveComplexity.Draw.tupLeLex_const_bot {A : Type} [LinearOrder A] {dd : ℕ} [Nonempty A] {zero : A} (hbot : ∀ (a : A), zero ≤ a) (t : Fin dd → A) : tupLeLex (fun (x : Fin dd) => zero) t

The least tuple is below every tuple: at the first differing coordinate the least element is smaller, which is what the lexicographic order asks.

theorem DescriptiveComplexity.Draw.blkTag_lt_of_gt_tupTop {A K : Type} [LinearOrder A] [Finite A] [LinearOrder K] {dd : ℕ} [Nonempty A] {b : Option K} {v : Wide.BlkIx K A dd} (h : WMLt (Wide.blkLe K A dd) (b, tupTop A dd) v) : Wide.blkTagLe K b v.1 ∧ b ≠ v.1

Above the last tuple of a block lies another block: nothing in the block is above its last tuple, so a strictly greater index has a strictly greater block.

noncomputable def DescriptiveComplexity.Draw.blkNextTag (K : Type) [LinearOrder K] [Finite K] [Nonempty K] (b : Option K) : Option K

The next block, as a fact about the block order: the least block above this one, or this one if there is none.

Equations

• DescriptiveComplexity.Draw.blkNextTag K b = if h : ∃ (c : Option K), DescriptiveComplexity.WMLt (DescriptiveComplexity.Wide.blkTagLe K) b c then ⋯.choose else b

theorem DescriptiveComplexity.Draw.blkNextB_eq {A K : Type} [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] {dd : ℕ} [Nonempty A] [Nonempty K] (b : Option K) : blkNextB A K dd b = blkNextTag K b

The sweep's next block is that one, so it is chosen when the formula is built and not at the instance – which is what a destination phase being a constant asks for.

theorem DescriptiveComplexity.Draw.blkNext_snd_of_tupTop {A K : Type} [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] {dd : ℕ} [Nonempty A] [Nonempty K] {b : Option K} (hne : (b, tupTop A dd) ≠ blkTop A K dd) {zero : A} (hbot : ∀ (a : A), zero ≤ a) (j : Fin dd) : (blkNext A K dd (b, tupTop A dd)).2 j = zero

A roll-over resets the tuple: at the last tuple of a block that is not the last, the next register is the first of the next block, so the pointer's coordinates all become the least element.

theorem DescriptiveComplexity.Draw.fst_blkBot {A K : Type} [LinearOrder A] [Finite A] [LinearOrder K] [Finite K] {dd : ℕ} [Nonempty A] [Nonempty K] : (blkBot A K dd).1 = none

The first register's block is the blockless one: the layout puts the registers that stand for no block first, so the least index's block is none.

theorem DescriptiveComplexity.Draw.tupTop_apply {A : Type} [LinearOrder A] [Finite A] {dd : ℕ} [Nonempty A] {one : A} (htop : ∀ (a : A), a ≤ one) (j : Fin dd) : tupTop A dd j = one

The greatest tuple is the greatest element everywhere: what the sweep's roll-over test asks about the pointer, coordinate by coordinate.

theorem DescriptiveComplexity.Draw.eq_tupTop_iff {A : Type} [LinearOrder A] [Finite A] {dd : ℕ} [Nonempty A] {one : A} (htop : ∀ (a : A), a ≤ one) (t : Fin dd → A) : t = tupTop A dd ↔ ∀ (j : Fin dd), t j = one

A tuple is the greatest exactly when every coordinate is, which is the form the roll-over test takes as a formula.

The clocked spine

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_nexEvalRule {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {PM SM B : Type} {nv : ℕ} {ShM : SM → Type} {ruleM : (e : Env L) → (s : SM) → ShM s → Rule e.α Q dt.SlotIx (NexPh B (EvalPh nv PM))} {subEntry : Fin nv → PM} {exitPh : NexPh B (EvalPh nv PM)} (hM : URulesDefinable ruleM) : URulesDefinable fun (e : Env L) => dt.nexEvalRule e.one (ruleM e) subEntry exitPh

The clocked evaluation's spine is definable: one checkpoint per spine position, with two rules each – the walk back to the marker, and the dispatch, which goes into the position's machinery below the last checkpoint and out of the evaluation at it. There is no third rule, the clocked evaluation running once and leaving into whatever phase its caller names.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_nexSmRule {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {B : Type} {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.nexSmRule e.zero e.one (args e)

The clocked evaluation's machineries are definable: the same tower the space-bounded program runs, one copy per spine position and the output's, at the clocked program's own phases.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_nexEvalRuleF {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {B : Type} {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.nexEvalRuleF e.zero e.one (args e)

The clocked evaluation is definable: its spine over those machineries.

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.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_ptrTup_eq_tupTop {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (coord : Fin dt.dd → dt.CtlIx) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.ptrTup coord f = tupTop e.α dt.dd

The roll-over test is definable: the pointer holds the last tuple exactly when every coordinate slot holds the greatest element.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_done {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [Nonempty dt.KIx] (coord : Fin dt.dd → dt.CtlIx) (b : Option dt.KIx) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => (b, dt.ptrTup coord f) = blkTop e.α dt.KIx dt.dd

The stop test is definable: the pointer is at the last register exactly when its block is the last one – a comparison the formula is built with – and every coordinate slot holds the greatest element.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_st0 {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [Nonempty dt.KIx] (coord : Fin dt.dd → dt.CtlIx) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.ctlOf coord f (blkBot e.α dt.KIx dt.dd).2

The reset to the file's first register is definable: the coordinate slots take the least element and every other slot keeps what it held. Which slots are coordinates is decided when the formula is built.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_atBot {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [Nonempty dt.KIx] (coord : Fin dt.dd → dt.CtlIx) (b : Option dt.KIx) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => (b, dt.ptrTup coord f) = blkBot e.α dt.KIx dt.dd

The first-register test is definable: the pointer is at the file's first register exactly when its block is the blockless one – decided when the formula is built – and every coordinate slot holds the least element.

theorem DescriptiveComplexity.Draw.Data.uTrDefinable_buildWr {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [Nonempty dt.KIx] (coord : Fin dt.dd → dt.CtlIx) (b : Option dt.KIx) : UTrDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.buildWr e.zero e.one coord b f

What the file-laying sweep writes is definable: the register mark and its two ends, the block one-hot, the name slots the pointer holds, the padding test, and the blank in every track the file does not carry. Every one of them is a slot of the control or a designated element, which is what makes the sweep a definable write.

theorem DescriptiveComplexity.Draw.Data.uSlotDefinable_tupNext_coord {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (coord : Fin dt.dd → dt.CtlIx) (j : Fin dt.dd) : USlotDefinable fun (x : Env L) (f : dt.CtlIx → x.α) (x_1 : dt.SlotIx → x.α) => tupNext (dt.ptrTup coord f) j

The pointer's next tuple is definable, coordinate by coordinate: which coordinate rolls over is a question about which coordinates are maximal, and the value at it is the order's own successor. This is DescriptiveComplexity.Draw.Data.uSlotDefinable_tupNext_lvC at the sweep's own coordinates.

theorem DescriptiveComplexity.Draw.Data.uStDefinable_ptrNext {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [Nonempty dt.KIx] {coord : Fin dt.dd → dt.CtlIx} (hcoord : Function.Injective coord) (b : Option dt.KIx) : UStDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.ptrNext coord b f

The sweep's advance is definable: at a coordinate slot the pointer takes the next register's own tuple – the lexicographic successor within a block, the least element at a roll-over – and every other slot keeps what it held. This is the one write of the whole program that is not a copy.

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.uSweepSpecDef_buildSpec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [Nonempty dt.KIx] {coord : Fin dt.dd → dt.CtlIx} (hcoord : Function.Injective coord) : USweepSpecDef fun (e : Env L) => dt.buildSpec e.zero e.one coord

The file-laying sweep is definable, field by field: what it writes is the file's background at the register the pointer names, where it leaves the pointer is the next register's tuple, its exit resets to the file's first register, and its two tests ask whether the pointer is at the last tuple and at the last register. The next block is a function of the phase, so it is chosen when the formula is built.

theorem DescriptiveComplexity.Draw.Data.uSweepSpecDef_nullSpec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {B : Type} : USweepSpecDef fun (e : Env L) => dt.nullSpec B

The sweep that does nothing is definable: every field is the identity or a constant, and its two tests are True – which is what makes the phase a single step. This is the specification a program that is handed its file puts where a file-laying one puts uSweepSpecDef_buildSpec.

theorem DescriptiveComplexity.Draw.Data.uTrDefinable_guessWr {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (x : dt.d.B.ι → Bool) : UTrDefinable fun (e : Env L) (x_1 : dt.CtlIx → e.α) (g : dt.SlotIx → e.α) => dt.guessWr e.zero e.one x g

What the guessing sweep writes is definable: the stage tracks take the guessed bit – a designated element, chosen when the formula is built, since the value guessed is the rule's own shape – and every other slot keeps what it held.

theorem DescriptiveComplexity.Draw.Data.uGuessSpecDef_regionSpec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : UGuessSpecDef fun (e : Env L) => dt.regionSpec e.zero e.one

The guessing sweep is definable: it writes the guessed bit and moves no pointer, so every field but the write is the identity or a constant. Its stop is not a test at all – the sweep stops nondeterministically, which is why Roll is always true and Done never.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_nexRule {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {PE SE B G : Type} {ShE : SE → Type} {β : (e : Env L) → SweepSpec e.α Q dt.SlotIx B} {γ : (e : Env L) → GuessSpec e.α Q dt.SlotIx B G} {ruleE : (e : Env L) → (s : SE) → ShE s → Rule e.α Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} (hβ : USweepSpecDef β) (hγ : UGuessSpecDef γ) (hE : URulesDefinable ruleE) : URulesDefinable fun (e : Env L) => dt.nexRule e.one (β e) (γ e) (ruleE e) evalEntry bot

The clocked program's outer layer is definable: the opening step that plants the two marks, the approach walk and its stop, the file-laying sweep at its specification, the walk home and its turn, the guessing sweep at its own specification and its stop, the second walk home, and the evaluation's rules as the parameter.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_nexProgRule {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {B G : Type} {β : (e : Env L) → SweepSpec e.α Q dt.SlotIx B} {γ : (e : Env L) → GuessSpec e.α Q dt.SlotIx B G} {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} {bot : B} (hβ : USweepSpecDef β) (hγ : UGuessSpecDef γ) (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.nexRule e.one (β e) (γ e) (dt.nexEvalRuleF e.zero e.one (args e)) (EvalPh.chk 0) bot

The clocked program's whole rule set is definable: the outer layer around the evaluation, at any two sweep specifications that are themselves definable.

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.