The capture theorem for L: the deterministic machine of a specification

DescriptiveComplexity.HeadCapture builds a machine for an FO(TC) definition by guessing. A deterministic machine may not guess, and this file builds the one that does not: it searches where the other one guesses, and it counts so that a search leading nowhere is abandoned. With it, FO(DTC) definability is recognizability by a deterministic two-way multi-head automaton (DescriptiveComplexity.dtcDefinable_iff_automaton, DescriptiveComplexity.mem_LOGSPACE_iff_automaton), the deterministic counterpart of DescriptiveComplexity.tcDefinable_iff_automaton.

Where the deterministic machine differs

Both machines simulate the walk of a specification, holding the current tuple on one block of heads and a candidate on another, with the mode in the control. Three things change.

• The candidate is scanned, not guessed. The walk being deterministic (DescriptiveComplexity.TCSpec.det_functional), a node has at most one successor, so the machine may look for it: DescriptiveComplexity.HeadProgram.lexNextP walks the candidate block through every tuple in turn, and the transition formula is evaluated at each. The tuple that passes is the successor.
• The source is scanned too, on a third block, and the machine keeps it there: when a walk leads nowhere it comes back and takes the next source.
• The walk is given a budget. A deterministic walk that does not reach an accepting node cycles, and a machine following it would never come back. So the machine counts its steps on a fourth block – with a mode in the control, giving exactly as many counter values as the specification has nodes – and abandons the source when the counter overflows. That this is enough is DescriptiveComplexity.exists_iterate_lt_card: a node reachable along a functional relation is reachable in fewer steps than the type has elements.

Every block needs to know when a head is at the greatest element, which is not a quantifier-free fact of one head; so one further head is parked there once and for all (DescriptiveComplexity.HeadProgram.dmk), shared by the three odometers as their marker.

The machine, and the half that says it never lies

DescriptiveComplexity.HeadProgram.DetNode (the control graph), DescriptiveComplexity.HeadProgram.dFam and DescriptiveComplexity.HeadProgram.dWire (its fragments and its arcs), DescriptiveComplexity.HeadProgram.dP (the machine), the layout of the heads with the fact that the protected heads are exactly the four blocks and the marker (DescriptiveComplexity.HeadProgram.dHeadAgree_iff), the relations its fragments run (DescriptiveComplexity.HeadProgram.dRel) with all of them proved (DescriptiveComplexity.HeadProgram.runs_dFam) and local (DescriptiveComplexity.HeadProgram.headLocal2_dRel), and soundness: DescriptiveComplexity.HeadProgram.dInv – at any node of the walk phase the tuple on the first block is a node of the specification reachable from a source, and at commit the candidate is one deterministic step away – is carried along every arc (DescriptiveComplexity.HeadProgram.dInv_of_walk), and at the accepting arc it says that the specification accepts (DescriptiveComplexity.HeadProgram.accepts_of_dExit).

The search for the successor

It is proved in full, and both ways. Over the tuples of one mode – DescriptiveComplexity.HeadProgram.scanFound (if the current node's successor, unique by DescriptiveComplexity.TCSpec.det_step_iff, is in the mode being tried with a tuple at or above the block's, the scan walks the block up to it and reaches commit holding it) and DescriptiveComplexity.HeadProgram.scanNone (if there is no successor in that mode, the scan runs the block to its greatest tuple and moves on) – both inductions downwards along the lexicographic order, in the style of DescriptiveComplexity.HeadProgram.decides_scanP. And over the chain of modes – DescriptiveComplexity.HeadProgram.modeFound and DescriptiveComplexity.HeadProgram.modeNone, inductions on the number of mode indices left. So from candMode the machine provably reaches commit holding the successor when there is one, and srcNext when there is none, in both cases leaving the current tuple, the source and the counter as they were.

One step of the simulated walk follows (DescriptiveComplexity.HeadProgram.walkStep) – at a node that is not accepting but has a successor, with a counter block that can still be stepped, the machine tests the target formula, searches out the successor, commits it onto the current block and ticks, arriving at tgtTest one node along with the counter's tuple advanced by one in the lexicographic order.

The counter, and the two ways a walk ends

The counter is read as a value of one finite linear order (DescriptiveComplexity.HeadProgram.dcount): the index of its mode, lexicographically above the tuple on its block. This is the whole of the budget argument, because a tick is a cover in that order – dcount_covBy_tup where the tuple can be stepped, dcount_covBy_mode where it cannot and the machine resets it and moves to the next counter mode – and because the order has exactly as many elements as the specification has nodes (DescriptiveComplexity.HeadProgram.card_dcount), which is the number DescriptiveComplexity.exists_iterate_lt_card bounds a walk by. DescriptiveComplexity.HeadProgram.dTick packages one tick: at a node that is neither accepting nor stuck, with a cover above the counter, the machine moves to the successor and its counter to that cover.

A walk then ends in one of two ways, and both are proved:

• DescriptiveComplexity.HeadProgram.walkAcc – if the walk reaches an accepting node within the budget, the machine accepts: an induction on the number of steps left, Ticks supplying the cover dTick needs at each of them;
• DescriptiveComplexity.HeadProgram.walkOut – whatever the specification does, the machine comes back: it accepts, or it reaches srcNext with its source block untouched. This is an induction downwards along the counter's order (DescriptiveComplexity.order_induction_down), the measure being the counter itself; at the top of the order the tuple is greatest and the mode last, so the tick fails and tickReset falls through to the next source (DescriptiveComplexity.HeadProgram.dcount_of_isTop), and where the walk is stuck DescriptiveComplexity.HeadProgram.walkStuck reaches srcNext through the exhausted chain of candidate modes.

The source enumeration, and the theorem

DescriptiveComplexity.HeadProgram.srcEnum walks the sources in the same order – mode index above source tuple – downwards from any position at or below the source the specification accepts from: at each position the machine either accepts (walkAcc, when the position is that source) or comes back to srcNext (DescriptiveComplexity.HeadProgram.srcTried, which is walkOut with the start arc in front of it), and the odometer of DescriptiveComplexity.HeadLex then advances the position by exactly one cover – stepping the tuple, or resetting it and taking the next source mode.

DescriptiveComplexity.HeadProgram.accepts_dP conjoins the two halves: the machine accepts exactly what the determinized specification does. Its fragments are evaluators, odometers and moves, all deterministic, so the program is (DescriptiveComplexity.HeadProgram.deterministic_dP) and DescriptiveComplexity.HeadProgram.compile true – at most one enabled transition per reading whatever the guards, and agreeing with the program where they are exclusive – gives a machine that DescriptiveComplexity.HeadAutomaton.IsDeterministic holds of on the nose. DescriptiveComplexity.dtcDefinable_of_automaton closes the loop.

The control graph

inductive DescriptiveComplexity.HeadProgram.DetNode (M : Type) (r : ℕ) : Type

The control nodes of the deterministic machine. Besides what it is doing, a node carries the source mode ms it is walking from, the current mode m, and the mode component cm of the step counter.

• init {M : Type} {r : ℕ} : DetNode M r

  Park the marker at the greatest element and start the source scan.

• srcMode {M : Type} {r : ℕ} (i : Fin (r + 1)) : DetNode M r

  Dispatch on the source mode of index i.

• srcTest {M : Type} {r : ℕ} (ms : M) : DetNode M r

  Test the source formula of ms on the source block.

• srcNext {M : Type} {r : ℕ} (ms : M) : DetNode M r

  Step the source block to the next tuple.

• srcReset {M : Type} {r : ℕ} (ms : M) : DetNode M r

  Reset the source block and move on to the next source mode.

• start {M : Type} {r : ℕ} (ms : M) : DetNode M r

  Copy the source onto the current block and reset the counter.

• tgtTest {M : Type} {r : ℕ} (ms m cm : M) : DetNode M r

  Test the target formula of m on the current block.

• candMode {M : Type} {r : ℕ} (ms m cm : M) (i : Fin (r + 1)) : DetNode M r

  Reset the candidate block and dispatch on the candidate mode of index i.

• candTest {M : Type} {r : ℕ} (ms m cm m' : M) : DetNode M r

  Test the transition formula from m to m'.

• candNext {M : Type} {r : ℕ} (ms m cm m' : M) : DetNode M r

  Step the candidate block to the next tuple.

• commit {M : Type} {r : ℕ} (ms m cm m' : M) : DetNode M r

  Copy the candidate onto the current block.

• tick {M : Type} {r : ℕ} (ms m cm : M) : DetNode M r

  Step the counter.

• tickReset {M : Type} {r : ℕ} (ms m cm : M) : DetNode M r

  Reset the counter block and step its mode component.

• dead {M : Type} {r : ℕ} : DetNode M r

  Nothing more to do.

instance DescriptiveComplexity.HeadProgram.instFiniteDetNode {M : Type} [Finite M] {r : ℕ} : Finite (DetNode M r)

Evaluating a formula on any block

theorem DescriptiveComplexity.HeadProgram.decides_evalFormula {L : FirstOrder.Language} {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] [Finite A] (sh : ℕ → Fin K) (hsh : ∀ i < K, ↑(sh i) = i) (prot : ℕ) (φ : (L.sum FirstOrder.Language.order).Formula α) (hv : α → Fin K) (hlow : ∀ (a : α), ↑(hv a) < prot) (hK : prot + qdepth φ ≤ K) : (evalP sh prot (Sum.elim hv Fin.elim0) φ).Decides A prot fun (x : Fin K → A) => φ.Realize fun (a : α) => x (hv a)

The evaluator, with the formula's variables read off any heads below the protected level.

The layout of the heads

noncomputable def DescriptiveComplexity.HeadProgram.dHeads {L : FirstOrder.Language} (spec : TCSpec L) : ℕ

How many heads the deterministic machine has: four blocks – current tuple, candidate, source, counter – a marker parked at the greatest element, the evaluator's workspace, and a spare.

Equations

• DescriptiveComplexity.HeadProgram.dHeads spec = 4 * spec.k + DescriptiveComplexity.specDepth spec.det + 2

noncomputable def DescriptiveComplexity.HeadProgram.dprot {L : FirstOrder.Language} (spec : TCSpec L) : ℕ

The heads the machine's fragments must give back untouched.

Equations

• DescriptiveComplexity.HeadProgram.dprot spec = 4 * spec.k + 1

theorem DescriptiveComplexity.HeadProgram.dprot_lt_dHeads {L : FirstOrder.Language} (spec : TCSpec L) : dprot spec < dHeads spec

noncomputable def DescriptiveComplexity.HeadProgram.dblk {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) (i : Fin spec.k) : Fin (dHeads spec)

Block t of the machine's heads: 0 the current tuple, 1 the candidate, 2 the source, 3 the counter.

Equations

• DescriptiveComplexity.HeadProgram.dblk spec t i = ⟨↑t * spec.k + ↑i, ⋯⟩

noncomputable def DescriptiveComplexity.HeadProgram.dmk {L : FirstOrder.Language} (spec : TCSpec L) : Fin (dHeads spec)

The marker head, parked at the greatest element.

Equations

• DescriptiveComplexity.HeadProgram.dmk spec = ⟨4 * spec.k, ⋯⟩

noncomputable def DescriptiveComplexity.HeadProgram.dshd {L : FirstOrder.Language} (spec : TCSpec L) (i : ℕ) : Fin (dHeads spec)

The head at a given index.

Equations

• DescriptiveComplexity.HeadProgram.dshd spec i = if h : i < DescriptiveComplexity.HeadProgram.dHeads spec then ⟨i, h⟩ else ⟨0, ⋯⟩

@[simp]

theorem DescriptiveComplexity.HeadProgram.dblk_val {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) (i : Fin spec.k) : ↑(dblk spec t i) = ↑t * spec.k + ↑i

@[simp]

theorem DescriptiveComplexity.HeadProgram.dmk_val {L : FirstOrder.Language} (spec : TCSpec L) : ↑(dmk spec) = 4 * spec.k

theorem DescriptiveComplexity.HeadProgram.dshd_val {L : FirstOrder.Language} (spec : TCSpec L) {i : ℕ} (h : i < dHeads spec) : ↑(dshd spec i) = i

theorem DescriptiveComplexity.HeadProgram.dshd_val' {L : FirstOrder.Language} (spec : TCSpec L) (i : ℕ) : i < dHeads spec → ↑(dshd spec i) = i

theorem DescriptiveComplexity.HeadProgram.dblk_lt {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) (i : Fin spec.k) : ↑(dblk spec t i) < 4 * spec.k

theorem DescriptiveComplexity.HeadProgram.dblk_lt_prot {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) (i : Fin spec.k) : ↑(dblk spec t i) < dprot spec

theorem DescriptiveComplexity.HeadProgram.dmk_lt_prot {L : FirstOrder.Language} (spec : TCSpec L) : ↑(dmk spec) < dprot spec

theorem DescriptiveComplexity.HeadProgram.dblk_inj {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) : Function.Injective (dblk spec t)

theorem DescriptiveComplexity.HeadProgram.dblk_ne_dmk {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) (i : Fin spec.k) : dblk spec t i ≠ dmk spec

noncomputable def DescriptiveComplexity.HeadProgram.dTup {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (t : Fin 4) (x : Fin (dHeads spec) → A) : Fin spec.k → A

The tuple block t holds.

Equations

• DescriptiveComplexity.HeadProgram.dTup spec t x i = x (DescriptiveComplexity.HeadProgram.dblk spec t i)

theorem DescriptiveComplexity.HeadProgram.dHeadAgree_iff {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} {x y : Fin (dHeads spec) → A} : HeadAgree (dprot spec) x y ↔ (∀ (t : Fin 4) (i : Fin spec.k), x (dblk spec t i) = y (dblk spec t i)) ∧ x (dmk spec) = y (dmk spec)

The protected heads are exactly the four blocks and the marker: there is nothing else below the protected level.

def DescriptiveComplexity.HeadProgram.dKeepBut {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (t : Fin 4) (x y : Fin (dHeads spec) → A) : Prop

Everything but block t is where it was.

Equations

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

The moves

theorem DescriptiveComplexity.HeadProgram.dblk_range {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) (i : Fin spec.k) : ↑t * spec.k ≤ ↑(dblk spec t i) ∧ ↑(dblk spec t i) < ↑t * spec.k + spec.k

theorem DescriptiveComplexity.HeadProgram.dblk_notMem_range {L : FirstOrder.Language} (spec : TCSpec L) {t t' : Fin 4} (i : Fin spec.k) (h : t' ≠ t) : ¬(↑t * spec.k ≤ ↑(dblk spec t' i) ∧ ↑(dblk spec t' i) < ↑t * spec.k + spec.k)

theorem DescriptiveComplexity.HeadProgram.dmk_notMem_range {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) : ¬(↑t * spec.k ≤ ↑(dmk spec) ∧ ↑(dmk spec) < ↑t * spec.k + spec.k)

theorem DescriptiveComplexity.HeadProgram.high_notMem_range {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) {h : Fin (dHeads spec)} (hh : dprot spec ≤ ↑h) : ¬(↑t * spec.k ≤ ↑h ∧ ↑h < ↑t * spec.k + spec.k)

noncomputable def DescriptiveComplexity.HeadProgram.dParkMoves {L : FirstOrder.Language} (spec : TCSpec L) : Fin (dHeads spec) → HeadMove (dHeads spec)

The moves that park the marker at the greatest element.

Equations

• DescriptiveComplexity.HeadProgram.dParkMoves spec h = if ↑h = 4 * spec.k then DescriptiveComplexity.HeadMove.toMax else DescriptiveComplexity.HeadMove.stay

noncomputable def DescriptiveComplexity.HeadProgram.dResetMoves {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) : Fin (dHeads spec) → HeadMove (dHeads spec)

The moves that send block t to the least element.

Equations

• DescriptiveComplexity.HeadProgram.dResetMoves spec t h = if ↑t * spec.k ≤ ↑h ∧ ↑h < ↑t * spec.k + spec.k then DescriptiveComplexity.HeadMove.toMin else DescriptiveComplexity.HeadMove.stay

noncomputable def DescriptiveComplexity.HeadProgram.dCopyMoves {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) : Fin (dHeads spec) → HeadMove (dHeads spec)

The moves that copy block t onto block 0.

Equations

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

noncomputable def DescriptiveComplexity.HeadProgram.dStartMoves {L : FirstOrder.Language} (spec : TCSpec L) : Fin (dHeads spec) → HeadMove (dHeads spec)

The moves that start a walk: the source onto the current block, and the counter back to the least tuple.

Equations

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

theorem DescriptiveComplexity.HeadProgram.dshd_dblk {L : FirstOrder.Language} (spec : TCSpec L) (t : Fin 4) (i : Fin spec.k) : dshd spec (↑t * spec.k + ↑i) = dblk spec t i

The machine

noncomputable def DescriptiveComplexity.HeadProgram.dFam {L : FirstOrder.Language} (spec : TCSpec L) : DetNode spec.Mode (modeCard spec) → HeadProgram L (dHeads spec)

The fragments of the deterministic machine.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.dFam spec DescriptiveComplexity.HeadProgram.DetNode.init = DescriptiveComplexity.HeadProgram.moveP (DescriptiveComplexity.HeadProgram.dParkMoves spec)
• DescriptiveComplexity.HeadProgram.dFam spec (DescriptiveComplexity.HeadProgram.DetNode.srcMode i) = DescriptiveComplexity.HeadProgram.exitP true
• DescriptiveComplexity.HeadProgram.dFam spec (DescriptiveComplexity.HeadProgram.DetNode.srcReset ms) = DescriptiveComplexity.HeadProgram.moveP (DescriptiveComplexity.HeadProgram.dResetMoves spec 2)
• DescriptiveComplexity.HeadProgram.dFam spec (DescriptiveComplexity.HeadProgram.DetNode.start ms) = DescriptiveComplexity.HeadProgram.moveP (DescriptiveComplexity.HeadProgram.dStartMoves spec)
• DescriptiveComplexity.HeadProgram.dFam spec DescriptiveComplexity.HeadProgram.DetNode.dead = DescriptiveComplexity.HeadProgram.exitP false

noncomputable def DescriptiveComplexity.HeadProgram.dWire {L : FirstOrder.Language} (spec : TCSpec L) : DetNode spec.Mode (modeCard spec) → Bool → DetNode spec.Mode (modeCard spec) ⊕ Bool

Where the deterministic machine goes when a fragment exits.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.dWire spec DescriptiveComplexity.HeadProgram.DetNode.init x✝ = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.srcMode (DescriptiveComplexity.ix0 spec))
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.srcTest ms) true = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.start ms)
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.srcTest ms) false = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.srcNext ms)
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.srcNext ms) true = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.srcTest ms)
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.srcNext ms) false = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.srcReset ms)
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.tgtTest ms m cm) true = Sum.inr true
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.candTest ms m cm m') true = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.commit ms m cm m')
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.candTest ms m cm m') false = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.candNext ms m cm m')
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.candNext ms m cm m') true = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.candTest ms m cm m')
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.commit ms m cm m') x✝ = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.tick ms m' cm)
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.tick ms m cm) true = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.tgtTest ms m cm)
• DescriptiveComplexity.HeadProgram.dWire spec (DescriptiveComplexity.HeadProgram.DetNode.tick ms m cm) false = Sum.inl (DescriptiveComplexity.HeadProgram.DetNode.tickReset ms m cm)
• DescriptiveComplexity.HeadProgram.dWire spec DescriptiveComplexity.HeadProgram.DetNode.dead x✝ = Sum.inr false

noncomputable def DescriptiveComplexity.HeadProgram.dP {L : FirstOrder.Language} (spec : TCSpec L) : HeadProgram L (dHeads spec)

The deterministic machine of a specification.

Equations

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

noncomputable def DescriptiveComplexity.HeadProgram.dRel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : DetNode spec.Mode (modeCard spec) → (Fin (dHeads spec) → A) → Bool → (Fin (dHeads spec) → A) → Prop

What the fragments of the deterministic machine run.

Equations

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

What the fragments run

theorem DescriptiveComplexity.HeadProgram.runs_resetP {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (t : Fin 4) : (moveP (dResetMoves spec t)).Runs A (dprot spec) fun (x : Fin (dHeads spec) → A) (b : Bool) (y : Fin (dHeads spec) → A) => b = true ∧ (∀ (i : Fin spec.k) (a : A), y (dblk spec t i) ≤ a) ∧ dKeepBut spec t x y

theorem DescriptiveComplexity.HeadProgram.runs_copyP {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : (moveP (dCopyMoves spec 1)).Runs A (dprot spec) fun (x : Fin (dHeads spec) → A) (b : Bool) (y : Fin (dHeads spec) → A) => b = true ∧ (∀ (i : Fin spec.k), y (dblk spec 0 i) = x (dblk spec 1 i)) ∧ dKeepBut spec 0 x y

theorem DescriptiveComplexity.HeadProgram.dblk_of_range {L : FirstOrder.Language} (spec : TCSpec L) {t : Fin 4} {j : Fin (dHeads spec)} (h1 : ↑t * spec.k ≤ ↑j) (h2 : ↑j < ↑t * spec.k + spec.k) : ∃ (i : Fin spec.k), j = dblk spec t i

theorem DescriptiveComplexity.HeadProgram.runs_parkP {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : (moveP (dParkMoves spec)).Runs A (dprot spec) (dRel spec DetNode.init)

theorem DescriptiveComplexity.HeadProgram.runs_startP {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (ms : spec.Mode) : (moveP (dStartMoves spec)).Runs A (dprot spec) (dRel spec (DetNode.start ms))

theorem DescriptiveComplexity.HeadProgram.runs_dFam {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (c : DetNode spec.Mode (modeCard spec)) : (dFam spec c).Runs A (dprot spec) (dRel spec c)

The fragments of the deterministic machine run what they are meant to.

theorem DescriptiveComplexity.HeadProgram.headLocal2_dRel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (c : DetNode spec.Mode (modeCard spec)) : HeadLocal2 (dprot spec) (dRel spec c)

The relations the fragments run see only the four blocks and the marker.

Soundness

theorem DescriptiveComplexity.HeadProgram.dblk_ne_dblk {L : FirstOrder.Language} (spec : TCSpec L) {t t' : Fin 4} (ht : t ≠ t') (i i' : Fin spec.k) : dblk spec t i ≠ dblk spec t' i'

theorem DescriptiveComplexity.HeadProgram.dTup_of_keepBut {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} {t t' : Fin 4} (ht : t' ≠ t) {x y : Fin (dHeads spec) → A} (h : dKeepBut spec t x y) : dTup spec t' y = dTup spec t' x

theorem DescriptiveComplexity.HeadProgram.dTup_of_agree {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} {t : Fin 4} {x y : Fin (dHeads spec) → A} (h : HeadAgree (dprot spec) x y) : dTup spec t y = dTup spec t x

theorem DescriptiveComplexity.HeadProgram.dTup_of_lexRel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [LinearOrder A] {t t' : Fin 4} (ht : t' ≠ t) {x y : Fin (dHeads spec) → A} {b : Bool} (h : lexRel (dblk spec t) (dmk spec) (dprot spec) x b y) : dTup spec t' y = dTup spec t' x

def DescriptiveComplexity.HeadProgram.dInv {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (u : DetNode spec.Mode (modeCard spec) × (Fin (dHeads spec) → A)) : Prop

The invariant the deterministic machine carries: the tuple on the first block is a node reachable from a source, and at commit the candidate is one deterministic step away.

Equations

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

theorem DescriptiveComplexity.HeadProgram.dInv_of_walk {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x₀ : Fin (dHeads spec) → A) {u : DetNode spec.Mode (modeCard spec) × (Fin (dHeads spec) → A)} (h : Relation.ReflTransGen (wireStep (dRel spec) (dWire spec)) (DetNode.init, x₀) u) : dInv spec u

The invariant is carried along the machine's walk.

theorem DescriptiveComplexity.HeadProgram.accepts_of_dExit {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x₀ : Fin (dHeads spec) → A) {u : DetNode spec.Mode (modeCard spec) × (Fin (dHeads spec) → A)} {z : Fin (dHeads spec) → A} (hwalk : Relation.ReflTransGen (wireStep (dRel spec) (dWire spec)) (DetNode.init, x₀) u) (hexit : wireExit (dRel spec) (dWire spec) u true z) : spec.det.Accepts A

Soundness: if the deterministic machine accepts, the specification does.

Completeness: the candidate scan

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.DReach {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] : DetNode spec.Mode (modeCard spec) × (Fin (dHeads spec) → A) → DetNode spec.Mode (modeCard spec) × (Fin (dHeads spec) → A) → Prop

Reachability in the machine's control graph.

Equations

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

theorem DescriptiveComplexity.HeadProgram.dstep_candTest_true {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm m' : spec.Mode} {x : Fin (dHeads spec) → A} (h : spec.det.Step (m, dTup spec 0 x) (m', dTup spec 1 x)) : wireStep (dRel spec) (dWire spec) (DetNode.candTest ms m cm m', x) (DetNode.commit ms m cm m', x)

theorem DescriptiveComplexity.HeadProgram.dstep_candTest_false {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm m' : spec.Mode} {x : Fin (dHeads spec) → A} (h : ¬spec.det.Step (m, dTup spec 0 x) (m', dTup spec 1 x)) : wireStep (dRel spec) (dWire spec) (DetNode.candTest ms m cm m', x) (DetNode.candNext ms m cm m', x)

theorem DescriptiveComplexity.HeadProgram.dstep_candNext_true {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm m' : spec.Mode} {x y : Fin (dHeads spec) → A} (h : lexRel (dblk spec 1) (dmk spec) (dprot spec) x true y) : wireStep (dRel spec) (dWire spec) (DetNode.candNext ms m cm m', x) (DetNode.candTest ms m cm m', y)

theorem DescriptiveComplexity.HeadProgram.dstep_candNext_false {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm m' : spec.Mode} {x y : Fin (dHeads spec) → A} (h : lexRel (dblk spec 1) (dmk spec) (dprot spec) x false y) : wireStep (dRel spec) (dWire spec) (DetNode.candNext ms m cm m', x) (DetNode.candMode ms m cm (nextIx spec (ixOf spec m')), y)

theorem DescriptiveComplexity.HeadProgram.dmk_ne_blk1 {L : FirstOrder.Language} {spec : TCSpec L} (i : Fin spec.k) : dmk spec ≠ dblk spec 1 i

theorem DescriptiveComplexity.HeadProgram.covBy_unique {C : Type} [LinearOrder C] {a b b' : C} (h : a ⋖ b) (h' : a ⋖ b') : b = b'

Covers are unique in a linear order.

theorem DescriptiveComplexity.HeadProgram.scanFound {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm m' : spec.Mode) (w' : spec.Node A) (hw1 : w'.1 = m') (c : Lex (Fin spec.k → A)) (x : Fin (dHeads spec) → A) : (∀ (a : A), a ≤ x (dmk spec)) → dTup spec 1 x = ofLex c → spec.det.Step (m, dTup spec 0 x) w' → c ≤ toLex w'.2 → ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.candTest ms m cm m', x) (DetNode.commit ms m cm m', x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 0 x' = dTup spec 0 x ∧ dTup spec 1 x' = w'.2 ∧ dTup spec 2 x' = dTup spec 2 x ∧ dTup spec 3 x' = dTup spec 3 x

The tuple scan finds the successor: from the candidate block at c, if the (unique) successor of the current node is in mode m' with a tuple at or above c, the scan reaches commit holding it.

theorem DescriptiveComplexity.HeadProgram.scanNone {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm m' : spec.Mode) (c : Lex (Fin spec.k → A)) (x : Fin (dHeads spec) → A) : (∀ (a : A), a ≤ x (dmk spec)) → dTup spec 1 x = ofLex c → (∀ (t : Fin spec.k → A), ¬spec.det.Step (m, dTup spec 0 x) (m', t)) → ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.candTest ms m cm m', x) (DetNode.candMode ms m cm (nextIx spec (ixOf spec m')), x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 0 x' = dTup spec 0 x ∧ dTup spec 2 x' = dTup spec 2 x ∧ dTup spec 3 x' = dTup spec 3 x

The tuple scan exhausts: if the current node has no successor in mode m', the scan walks the candidate block to its greatest tuple and moves on to the next candidate mode.

Completeness: the chain of candidate modes

theorem DescriptiveComplexity.HeadProgram.exists_dReset {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] [Finite A] (t : Fin 4) (x : Fin (dHeads spec) → A) : ∃ (y : Fin (dHeads spec) → A), (∀ (i : Fin spec.k) (a : A), y (dblk spec t i) ≤ a) ∧ dKeepBut spec t x y

theorem DescriptiveComplexity.HeadProgram.dstep_candMode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm : spec.Mode} {i : Fin (modeCard spec + 1)} {x y : Fin (dHeads spec) → A} (h1 : ∀ (i' : Fin spec.k) (a : A), y (dblk spec 1 i') ≤ a) (h2 : dKeepBut spec 1 x y) : wireStep (dRel spec) (dWire spec) (DetNode.candMode ms m cm i, x) ((modeAt spec i).elim (DetNode.srcNext ms) fun (m' : spec.Mode) => DetNode.candTest ms m cm m', y)

theorem DescriptiveComplexity.HeadProgram.ixOf_of_modeAt {L : FirstOrder.Language} {spec : TCSpec L} {i : Fin (modeCard spec + 1)} {m : spec.Mode} (h : modeAt spec i = some m) : ixOf spec m = i

theorem DescriptiveComplexity.HeadProgram.nextIx_val {L : FirstOrder.Language} {spec : TCSpec L} {i : Fin (modeCard spec + 1)} (hi : ↑i < modeCard spec) : ↑(nextIx spec i) = ↑i + 1

theorem DescriptiveComplexity.HeadProgram.modeFound {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm : spec.Mode) (w' : spec.Node A) (d : ℕ) (i : Fin (modeCard spec + 1)) (x : Fin (dHeads spec) → A) : ↑i + d = ↑(ixOf spec w'.1) → (∀ (a : A), a ≤ x (dmk spec)) → spec.det.Step (m, dTup spec 0 x) w' → ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.candMode ms m cm i, x) (DetNode.commit ms m cm w'.1, x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 0 x' = dTup spec 0 x ∧ dTup spec 1 x' = w'.2 ∧ dTup spec 2 x' = dTup spec 2 x ∧ dTup spec 3 x' = dTup spec 3 x

The chain of candidate modes finds the successor.

theorem DescriptiveComplexity.HeadProgram.modeNone {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm : spec.Mode) (d : ℕ) (i : Fin (modeCard spec + 1)) (x : Fin (dHeads spec) → A) : modeCard spec ≤ ↑i + d → (∀ (a : A), a ≤ x (dmk spec)) → (∀ (w : spec.Node A), ¬spec.det.Step (m, dTup spec 0 x) w) → ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.candMode ms m cm i, x) (DetNode.srcNext ms, x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 0 x' = dTup spec 0 x ∧ dTup spec 2 x' = dTup spec 2 x ∧ dTup spec 3 x' = dTup spec 3 x

The chain of candidate modes exhausts: with no successor to find, the machine tries every mode and moves on to the next source.

Completeness: one step of the simulated walk

theorem DescriptiveComplexity.HeadProgram.exists_dCopy {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (t : Fin 4) (x : Fin (dHeads spec) → A) : ∃ (y : Fin (dHeads spec) → A), (∀ (i : Fin spec.k), y (dblk spec 0 i) = x (dblk spec t i)) ∧ dKeepBut spec 0 x y

theorem DescriptiveComplexity.HeadProgram.dstep_tgtTest_false {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm : spec.Mode} {x : Fin (dHeads spec) → A} (h : ¬spec.IsTgt (m, dTup spec 0 x)) : wireStep (dRel spec) (dWire spec) (DetNode.tgtTest ms m cm, x) (DetNode.candMode ms m cm (ix0 spec), x)

theorem DescriptiveComplexity.HeadProgram.dstep_commit {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm m' : spec.Mode} {x y : Fin (dHeads spec) → A} (h1 : ∀ (i : Fin spec.k), y (dblk spec 0 i) = x (dblk spec 1 i)) (h2 : dKeepBut spec 0 x y) : wireStep (dRel spec) (dWire spec) (DetNode.commit ms m cm m', x) (DetNode.tick ms m' cm, y)

theorem DescriptiveComplexity.HeadProgram.dstep_tick_true {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm : spec.Mode} {x y : Fin (dHeads spec) → A} (h : lexRel (dblk spec 3) (dmk spec) (dprot spec) x true y) : wireStep (dRel spec) (dWire spec) (DetNode.tick ms m cm, x) (DetNode.tgtTest ms m cm, y)

theorem DescriptiveComplexity.HeadProgram.dmk_ne_blk3 {L : FirstOrder.Language} {spec : TCSpec L} (i : Fin spec.k) : dmk spec ≠ dblk spec 3 i

theorem DescriptiveComplexity.HeadProgram.walkStep {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm : spec.Mode) (x : Fin (dHeads spec) → A) (hmk : ∀ (a : A), a ≤ x (dmk spec)) (hntgt : ¬spec.IsTgt (m, dTup spec 0 x)) {w' : spec.Node A} (hstep : spec.det.Step (m, dTup spec 0 x) w') (hnotTop : ¬∀ (i : Fin spec.k) (a : A), a ≤ x (dblk spec 3 i)) : ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.tgtTest ms m cm, x) (DetNode.tgtTest ms w'.1 cm, x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 0 x' = w'.2 ∧ dTup spec 2 x' = dTup spec 2 x ∧ TupSucc (dTup spec 3 x) (dTup spec 3 x')

One step of the simulated walk: at a node that is not accepting but has a successor, with a counter that can still be stepped, the machine moves to the successor and ticks.

Completeness: the counter as a linear order

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.DCount {L : FirstOrder.Language} (spec : TCSpec L) (B : Type) [LinearOrder B] : Type

The value of the counter: the mode it carries in the control together with the tuple on its block, ordered lexicographically with the mode most significant. A tick of the machine is a cover in this order (DescriptiveComplexity.HeadProgram.dcount_covBy_tup within a mode, DescriptiveComplexity.HeadProgram.dcount_covBy_mode across one), and the order has exactly as many elements as the specification has nodes (DescriptiveComplexity.HeadProgram.card_dcount) – which is what makes the budget long enough.

Equations

• DescriptiveComplexity.HeadProgram.DCount spec B = Lex (Fin (DescriptiveComplexity.modeCard spec) × Lex (Fin spec.k → B))

noncomputable def DescriptiveComplexity.HeadProgram.dcount {L : FirstOrder.Language} (spec : TCSpec L) {B : Type} [LinearOrder B] (cm : spec.Mode) (t : Fin spec.k → B) : DCount spec B

The counter's value, read off the mode in the control and the tuple on the block.

Equations

• DescriptiveComplexity.HeadProgram.dcount spec cm t = toLex ((DescriptiveComplexity.modeEquiv spec) cm, toLex t)

theorem DescriptiveComplexity.HeadProgram.dcount_inj {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] {cm cm' : spec.Mode} {t t' : Fin spec.k → A} (h : dcount spec cm t = dcount spec cm' t') : cm = cm' ∧ t = t'

The counter's value determines the mode and the tuple.

theorem DescriptiveComplexity.HeadProgram.dcount_covBy_tup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] [Nonempty A] (cm : spec.Mode) {t t' : Fin spec.k → A} (h : TupSucc t t') : dcount spec cm t ⋖ dcount spec cm t'

Stepping the tuple is a cover of the counter.

theorem DescriptiveComplexity.HeadProgram.modeEquiv_of_modeAt {L : FirstOrder.Language} {spec : TCSpec L} {i : Fin (modeCard spec + 1)} {m : spec.Mode} (h : modeAt spec i = some m) : ↑((modeEquiv spec) m) = ↑i

The index of a mode the enumeration produces.

theorem DescriptiveComplexity.HeadProgram.dcount_covBy_mode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] [Nonempty A] {cm cm' : spec.Mode} {t t' : Fin spec.k → A} (hnext : modeAt spec (nextIx spec (ixOf spec cm)) = some cm') (htop : ∀ (i : Fin spec.k) (a : A), a ≤ t i) (hbot : ∀ (i : Fin spec.k) (a : A), t' i ≤ a) : dcount spec cm t ⋖ dcount spec cm' t'

Running the tuple out and moving to the next mode is a cover of the counter.

theorem DescriptiveComplexity.HeadProgram.dcount_isBot {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] {cm : spec.Mode} {t : Fin spec.k → A} (h0 : modeAt spec (ix0 spec) = some cm) (hbot : ∀ (i : Fin spec.k) (a : A), t i ≤ a) (u : DCount spec A) : dcount spec cm t ≤ u

The counter starts at the bottom of its order.

theorem DescriptiveComplexity.HeadProgram.dcount_isTop {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] {cm : spec.Mode} {t : Fin spec.k → A} (htop : ∀ (i : Fin spec.k) (a : A), a ≤ t i) (hnone : modeAt spec (nextIx spec (ixOf spec cm)) = none) (u : DCount spec A) : u ≤ dcount spec cm t

The counter is exhausted when its tuple is the greatest one and its mode is the last of the enumeration.

theorem DescriptiveComplexity.HeadProgram.dcount_of_isTop {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] {cm : spec.Mode} {t : Fin spec.k → A} (h : ∀ (u : DCount spec A), u ≤ dcount spec cm t) : (∀ (i : Fin spec.k) (a : A), a ≤ t i) ∧ modeAt spec (nextIx spec (ixOf spec cm)) = none

At the top of the counter there is nothing left: the tuple is the greatest one and the mode is the last of the enumeration.

theorem DescriptiveComplexity.HeadProgram.card_dcount {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] : Nat.card (DCount spec A) = Nat.card (spec.det.Node A)

The counter has exactly as many values as the specification has nodes.

Completeness: the remaining arcs

theorem DescriptiveComplexity.HeadProgram.exists_dPark {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] [Finite A] (x : Fin (dHeads spec) → A) : ∃ (y : Fin (dHeads spec) → A), (∀ (a : A), a ≤ y (dmk spec)) ∧ ∀ (t : Fin 4) (i : Fin spec.k), y (dblk spec t i) = x (dblk spec t i)

The marker can be parked at the greatest element.

theorem DescriptiveComplexity.HeadProgram.exists_dStart {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [LinearOrder A] [Finite A] (x : Fin (dHeads spec) → A) : ∃ (y : Fin (dHeads spec) → A), (∀ (i : Fin spec.k), y (dblk spec 0 i) = x (dblk spec 2 i)) ∧ (∀ (i : Fin spec.k) (a : A), y (dblk spec 3 i) ≤ a) ∧ (∀ (t : Fin 4) (i : Fin spec.k), t ≠ 0 → t ≠ 3 → y (dblk spec t i) = x (dblk spec t i)) ∧ y (dmk spec) = x (dmk spec)

A walk can be started: the source is copied onto the current block and the counter is set to its least tuple.

theorem DescriptiveComplexity.HeadProgram.dstep_init {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {x y : Fin (dHeads spec) → A} (hmk : ∀ (a : A), a ≤ y (dmk spec)) (hkeep : ∀ (t : Fin 4) (i : Fin spec.k), y (dblk spec t i) = x (dblk spec t i)) : wireStep (dRel spec) (dWire spec) (DetNode.init, x) (DetNode.srcMode (ix0 spec), y)

theorem DescriptiveComplexity.HeadProgram.dstep_srcMode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {i : Fin (modeCard spec + 1)} {ms : spec.Mode} (h : modeAt spec i = some ms) (x : Fin (dHeads spec) → A) : wireStep (dRel spec) (dWire spec) (DetNode.srcMode i, x) (DetNode.srcTest ms, x)

theorem DescriptiveComplexity.HeadProgram.dstep_srcTest_true {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms : spec.Mode} {x : Fin (dHeads spec) → A} (h : spec.IsSrc (ms, dTup spec 2 x)) : wireStep (dRel spec) (dWire spec) (DetNode.srcTest ms, x) (DetNode.start ms, x)

theorem DescriptiveComplexity.HeadProgram.dstep_srcTest_false {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms : spec.Mode} {x : Fin (dHeads spec) → A} (h : ¬spec.IsSrc (ms, dTup spec 2 x)) : wireStep (dRel spec) (dWire spec) (DetNode.srcTest ms, x) (DetNode.srcNext ms, x)

theorem DescriptiveComplexity.HeadProgram.dstep_start {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms : spec.Mode} {x y : Fin (dHeads spec) → A} (hcopy : ∀ (i : Fin spec.k), y (dblk spec 0 i) = x (dblk spec 2 i)) (hreset : ∀ (i : Fin spec.k) (a : A), y (dblk spec 3 i) ≤ a) (hkeep : ∀ (t : Fin 4) (i : Fin spec.k), t ≠ 0 → t ≠ 3 → y (dblk spec t i) = x (dblk spec t i)) (hmk : y (dmk spec) = x (dmk spec)) : wireStep (dRel spec) (dWire spec) (DetNode.start ms, x) ((modeAt spec (ix0 spec)).elim DetNode.dead fun (cm : spec.Mode) => DetNode.tgtTest ms ms cm, y)

theorem DescriptiveComplexity.HeadProgram.dstep_srcNext_true {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms : spec.Mode} {x y : Fin (dHeads spec) → A} (h : lexRel (dblk spec 2) (dmk spec) (dprot spec) x true y) : wireStep (dRel spec) (dWire spec) (DetNode.srcNext ms, x) (DetNode.srcTest ms, y)

theorem DescriptiveComplexity.HeadProgram.dstep_srcNext_false {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms : spec.Mode} {x y : Fin (dHeads spec) → A} (h : lexRel (dblk spec 2) (dmk spec) (dprot spec) x false y) : wireStep (dRel spec) (dWire spec) (DetNode.srcNext ms, x) (DetNode.srcReset ms, y)

theorem DescriptiveComplexity.HeadProgram.dstep_srcReset {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms : spec.Mode} {x y : Fin (dHeads spec) → A} (h1 : ∀ (i : Fin spec.k) (a : A), y (dblk spec 2 i) ≤ a) (h2 : dKeepBut spec 2 x y) : wireStep (dRel spec) (dWire spec) (DetNode.srcReset ms, x) (DetNode.srcMode (nextIx spec (ixOf spec ms)), y)

theorem DescriptiveComplexity.HeadProgram.dstep_tick_false {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm : spec.Mode} {x y : Fin (dHeads spec) → A} (h : lexRel (dblk spec 3) (dmk spec) (dprot spec) x false y) : wireStep (dRel spec) (dWire spec) (DetNode.tick ms m cm, x) (DetNode.tickReset ms m cm, y)

theorem DescriptiveComplexity.HeadProgram.dstep_tickReset {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm : spec.Mode} {x y : Fin (dHeads spec) → A} (h1 : ∀ (i : Fin spec.k) (a : A), y (dblk spec 3 i) ≤ a) (h2 : dKeepBut spec 3 x y) : wireStep (dRel spec) (dWire spec) (DetNode.tickReset ms m cm, x) ((modeAt spec (nextIx spec (ixOf spec cm))).elim (DetNode.srcNext ms) fun (cm' : spec.Mode) => DetNode.tgtTest ms m cm', y)

theorem DescriptiveComplexity.HeadProgram.dexit_tgtTest {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ms m cm : spec.Mode} {x : Fin (dHeads spec) → A} (h : spec.IsTgt (m, dTup spec 0 x)) : wireExit (dRel spec) (dWire spec) (DetNode.tgtTest ms m cm, x) true x

def DescriptiveComplexity.HeadProgram.DAccepts {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (u : DetNode spec.Mode (modeCard spec) × (Fin (dHeads spec) → A)) : Prop

The machine accepts from here: its control walk reaches the true exit.

Equations

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

theorem DescriptiveComplexity.HeadProgram.DAccepts.mono {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {u v : DetNode spec.Mode (modeCard spec) × (Fin (dHeads spec) → A)} (h : DReach spec u v) (ha : DAccepts spec v) : DAccepts spec u

Completeness: one tick of the counter

theorem DescriptiveComplexity.HeadProgram.dmk_ne_blk2 {L : FirstOrder.Language} {spec : TCSpec L} (i : Fin spec.k) : dmk spec ≠ dblk spec 2 i

theorem DescriptiveComplexity.HeadProgram.walkToTickReset {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm : spec.Mode) (x : Fin (dHeads spec) → A) (hmk : ∀ (a : A), a ≤ x (dmk spec)) (hntgt : ¬spec.IsTgt (m, dTup spec 0 x)) {w' : spec.Node A} (hstep : spec.det.Step (m, dTup spec 0 x) w') (htop : ∀ (i : Fin spec.k) (a : A), a ≤ x (dblk spec 3 i)) : ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.tgtTest ms m cm, x) (DetNode.tickReset ms w'.1 cm, x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 0 x' = w'.2 ∧ dTup spec 2 x' = dTup spec 2 x ∧ dTup spec 3 x' = dTup spec 3 x

A step of the walk taken with the counter at its greatest tuple: the machine moves to the successor, fails to tick, and lands at tickReset.

theorem DescriptiveComplexity.HeadProgram.dTick {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm : spec.Mode) (x : Fin (dHeads spec) → A) (hmk : ∀ (a : A), a ≤ x (dmk spec)) (hntgt : ¬spec.IsTgt (m, dTup spec 0 x)) {w' : spec.Node A} (hstep : spec.det.Step (m, dTup spec 0 x) w') {z : DCount spec A} (hcov : dcount spec cm (dTup spec 3 x) ⋖ z) : ∃ (cm' : spec.Mode) (x' : Fin (dHeads spec) → A), DReach spec (DetNode.tgtTest ms m cm, x) (DetNode.tgtTest ms w'.1 cm', x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 0 x' = w'.2 ∧ dTup spec 2 x' = dTup spec 2 x ∧ dcount spec cm' (dTup spec 3 x') = z

One tick: at a node that is not accepting but has a successor, with a counter that still has a cover above it, the machine moves to the successor and sets its counter to that cover – stepping the tuple where it can, and crossing over to the next counter mode where it cannot.

Completeness: the walk, and its two outcomes

theorem DescriptiveComplexity.HeadProgram.walkStuck {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms m cm : spec.Mode) (x : Fin (dHeads spec) → A) (hmk : ∀ (a : A), a ≤ x (dmk spec)) (hntgt : ¬spec.IsTgt (m, dTup spec 0 x)) (hns : ∀ (w : spec.Node A), ¬spec.det.Step (m, dTup spec 0 x) w) : ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.tgtTest ms m cm, x) (DetNode.srcNext ms, x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 2 x' = dTup spec 2 x

A walk that leads nowhere is abandoned: with no successor to go to, the machine tries every candidate mode and comes back for the next source.

theorem DescriptiveComplexity.HeadProgram.walkAcc {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms : spec.Mode) (n : ℕ) (m cm : spec.Mode) (x : Fin (dHeads spec) → A) : (∀ (a : A), a ≤ x (dmk spec)) → Ticks n (dcount spec cm (dTup spec 3 x)) → spec.det.IsTgt ((stepNext spec.det.Step)^[n] (m, dTup spec 0 x)) → DAccepts spec (DetNode.tgtTest ms m cm, x)

The machine follows the walk while its counter lasts: if the walk reaches an accepting node within the budget, the machine accepts.

theorem DescriptiveComplexity.HeadProgram.walkOut {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms : spec.Mode) (z : DCount spec A) (m cm : spec.Mode) (x : Fin (dHeads spec) → A) : (∀ (a : A), a ≤ x (dmk spec)) → dcount spec cm (dTup spec 3 x) = z → DAccepts spec (DetNode.tgtTest ms m cm, x) ∨ ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.tgtTest ms m cm, x) (DetNode.srcNext ms, x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 2 x' = dTup spec 2 x

A walk always comes to an end: whatever the specification does, the machine either accepts or comes back for the next source, its source block untouched. The measure is the counter, which the machine steps once per node visited.

Completeness: the source enumeration

theorem DescriptiveComplexity.HeadProgram.exists_modeAt_ix0 {L : FirstOrder.Language} {spec : TCSpec L} (m : spec.Mode) : ∃ (cm₀ : spec.Mode), modeAt spec (ix0 spec) = some cm₀

The counter mode the machine starts a walk with.

theorem DescriptiveComplexity.HeadProgram.srcTried {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (ms : spec.Mode) (x : Fin (dHeads spec) → A) (hmk : ∀ (a : A), a ≤ x (dmk spec)) : DAccepts spec (DetNode.srcTest ms, x) ∨ ∃ (x' : Fin (dHeads spec) → A), DReach spec (DetNode.srcTest ms, x) (DetNode.srcNext ms, x') ∧ (∀ (a : A), a ≤ x' (dmk spec)) ∧ dTup spec 2 x' = dTup spec 2 x

A source is tried: from the test of a source, the machine either accepts or comes back for the next tuple of the enumeration, its source block where it was.

theorem DescriptiveComplexity.HeadProgram.srcEnum {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {u₀ : spec.det.Node A} (hsrc : spec.IsSrc u₀) {n : ℕ} (hn : n < Nat.card (spec.det.Node A)) (htgt : spec.det.IsTgt ((stepNext spec.det.Step)^[n] u₀)) (z : DCount spec A) (ms : spec.Mode) (x : Fin (dHeads spec) → A) : (∀ (a : A), a ≤ x (dmk spec)) → dcount spec ms (dTup spec 2 x) = z → z ≤ dcount spec u₀.1 u₀.2 → DAccepts spec (DetNode.srcTest ms, x)

The source enumeration reaches the source that works: from any position of the enumeration at or below a source from which the walk accepts within the budget, the machine accepts.

The machine of a specification

theorem DescriptiveComplexity.HeadProgram.deterministic_dP {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] : (dP spec).Deterministic A

theorem DescriptiveComplexity.HeadProgram.accepts_dP {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ((dP spec).compile true).Accepts A ↔ spec.det.Accepts A

The deterministic machine of a specification accepts exactly what the determinized specification does. Soundness is the invariant of DescriptiveComplexity.HeadProgram.dInv; completeness is the source enumeration, each source walked out to its end – or to the budget, which DescriptiveComplexity.exists_iterate_lt_card says is long enough.

The capture theorem

theorem DescriptiveComplexity.dtcDefinable_iff_automaton {L : FirstOrder.Language} {P : DecisionProblem L} : DTCDefinable P ↔ ∃ (k : ℕ) (M : HeadAutomaton L k) (_ : M.IsDeterministic), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ M.Accepts A

The capture theorem for FO(DTC): a problem is definable by a single deterministic transitive closure exactly when a deterministic two-way multi-head automaton recognizes it. One direction is DescriptiveComplexity.dtcDefinable_of_automaton – a configuration is a node of a specification, and determinism of the control is functionality of the walk – and the other is the machine built here: it scans where the machine of DescriptiveComplexity.HeadCapture guesses, and counts so that a walk leading nowhere is abandoned.

theorem DescriptiveComplexity.mem_LOGSPACE_iff_automaton {L : FirstOrder.Language} {P : DecisionProblem L} : LOGSPACE.Mem P ↔ ∃ (k : ℕ) (M : HeadAutomaton L k) (_ : M.IsDeterministic), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ M.Accepts A

LOGSPACE is the class of the deterministic two-way multi-head automata: membership in DescriptiveComplexity.LOGSPACE is recognizability by such a machine, the deterministic counterpart of DescriptiveComplexity.mem_NL_iff_automaton.