The capture theorem for NL: FO(TC) is what a multi-head automaton recognizes

DescriptiveComplexity.HeadAutomaton compiles a machine into a DescriptiveComplexity.TCSpec, which is the easy half. This file is the other half: every FO(TC) definable problem is recognized by a two-way multi-head automaton, so that the two notions coincide and DescriptiveComplexity.NL is captured by the machine model as well as by the logic.

The machine

Given a specification with arity k, the machine has 2 * k + D + 1 heads:

• the first k hold the current tuple of the walk;
• the next k hold a candidate for the next tuple;
• the remaining D are the workspace of DescriptiveComplexity.HeadProgram.evalP, which evaluates the specification's formulas – D being the largest quantifier budget among them – plus one spare head so that the head type is never empty.

The mode of the walk is not on a head – it cannot be, a one-element universe having only one tuple – but in the control, which is what a finite control is for.

The loop

Written as a control graph over fragments (DescriptiveComplexity.HeadProgram.wireP), the machine is:

• pick a source mode: a chain of free choices (DescriptiveComplexity.HeadProgram.chooseP) walking the list of modes, so that any mode may be selected;
• try it: guess the current tuple (DescriptiveComplexity.HeadProgram.guessP, a head walked up the order by a nondeterministic number of steps) and evaluate the source formula; a failure leads nowhere;
• at a node: evaluate the target formula – if it holds, accept;
• otherwise pick a candidate mode, guess the candidate tuple, evaluate the transition formula, and, if it holds, commit: copy the candidate onto the current tuple and go back to evaluating the target formula.

Guessing is where the nondeterminism lives, and it is the only place: the evaluator itself is deterministic.

The proof

DescriptiveComplexity.HeadProgram.runs_wireP turns the machine's runs into a walk in the control graph, and the correctness is then an argument about that walk, in two directions:

• soundness – an invariant carried along the walk: at a node of the control graph, the tuple on the first k heads is a node of the specification reachable from a source. It is preserved by every arc, and at the accepting arc it says exactly that the specification accepts;
• completeness – by induction along DescriptiveComplexity.TCSpec.Reach: every step of the specification's walk is imitated by the loop above, unless the target formula holds on the way, in which case the machine has already accepted.

The result is DescriptiveComplexity.tcDefinable_iff_automaton, and with it DescriptiveComplexity.mem_NL_iff_automaton.

Free choices and guesses

def DescriptiveComplexity.HeadProgram.chooseP {L : FirstOrder.Language} {K : ℕ} : HeadProgram L K

A free choice: exit either way, moving no head. It is the only source of nondeterminism in the machines built here, together with DescriptiveComplexity.HeadProgram.guessP.

Equations

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

def DescriptiveComplexity.HeadProgram.guessStepP {L : FirstOrder.Language} {K : ℕ} (h : Fin K) : HeadProgram L K

One step of a guess: either walk head h to the next element, or stop.

Equations

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

@[simp]

theorem DescriptiveComplexity.HeadProgram.tr_chooseP {L : FirstOrder.Language} {K : ℕ} (s : chooseP.St) : chooseP.tr s = [{ guard := ⊤, moves := fun (x : Fin K) => HeadMove.stay, target := Sum.inr true }, { guard := ⊤, moves := fun (x : Fin K) => HeadMove.stay, target := Sum.inr false }]

@[simp]

theorem DescriptiveComplexity.HeadProgram.tr_guessStepP {L : FirstOrder.Language} {K : ℕ} (h : Fin K) (s : (guessStepP h).St) : (guessStepP h).tr s = [{ guard := ⊤, moves := setHead h (HeadMove.succ h), target := Sum.inr true }, { guard := ⊤, moves := fun (x : Fin K) => HeadMove.stay, target := Sum.inr false }]

theorem DescriptiveComplexity.HeadProgram.runs_chooseP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} : chooseP.Runs A m fun (x : Fin K → A) (x_1 : Bool) (y : Fin K → A) => HeadAgree m x y

theorem DescriptiveComplexity.HeadProgram.runs_guessStepP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (h : Fin K) (hh : ↑h < m) : (guessStepP h).Runs A m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => (b = true ∧ (x h < y h ∧ ∀ (e : A), ¬(x h < e ∧ e < y h)) ∧ ∀ (j : Fin K), ↑j < m → j ≠ h → y j = x j) ∨ b = false ∧ HeadAgree m x y

Guessing one head

inductive DescriptiveComplexity.HeadProgram.GuessNode : Type

The control nodes of a guess.

• reset : GuessNode

  Putting the head on the least element.

• loop : GuessNode

  Walking it up, for as long as the machine chooses to.

@[instance_reducible]

instance DescriptiveComplexity.HeadProgram.instDecidableEqGuessNode : DecidableEq GuessNode

Equations

• DescriptiveComplexity.HeadProgram.instDecidableEqGuessNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.HeadProgram.instFiniteGuessNode : Finite GuessNode

def DescriptiveComplexity.HeadProgram.guessWire : GuessNode → Bool → GuessNode ⊕ Bool

The wiring of a guess: walk up, or stop and answer true.

Equations

• DescriptiveComplexity.HeadProgram.guessWire DescriptiveComplexity.HeadProgram.GuessNode.reset x✝ = Sum.inl DescriptiveComplexity.HeadProgram.GuessNode.loop
• DescriptiveComplexity.HeadProgram.guessWire DescriptiveComplexity.HeadProgram.GuessNode.loop true = Sum.inl DescriptiveComplexity.HeadProgram.GuessNode.loop
• DescriptiveComplexity.HeadProgram.guessWire DescriptiveComplexity.HeadProgram.GuessNode.loop false = Sum.inr true

def DescriptiveComplexity.HeadProgram.guessFam {L : FirstOrder.Language} {K : ℕ} (h : Fin K) : GuessNode → HeadProgram L K

The fragments of a guess.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.guessFam h DescriptiveComplexity.HeadProgram.GuessNode.loop = DescriptiveComplexity.HeadProgram.guessStepP h

def DescriptiveComplexity.HeadProgram.guessP {L : FirstOrder.Language} {K : ℕ} (h : Fin K) : HeadProgram L K

Guessing a head: put head h on the least element and walk it up a nondeterministic number of steps, so that it may end anywhere.

Equations

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

def DescriptiveComplexity.HeadProgram.guessRel {K : ℕ} {A : Type} [LinearOrder A] (h : Fin K) (m : ℕ) : GuessNode → (Fin K → A) → Bool → (Fin K → A) → Prop

The relations the fragments of a guess run.

Equations

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

theorem DescriptiveComplexity.HeadProgram.runs_guessP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {m : ℕ} (h : Fin K) (hh : ↑h < m) : (guessP h).Runs A m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => b = true ∧ ∀ (j : Fin K), ↑j < m → j ≠ h → y j = x j

What a guess runs: head h may end anywhere, every other head staying where it was.

Guessing a block of heads

theorem DescriptiveComplexity.HeadProgram.runs_exitP_local {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (b : Bool) (m : ℕ) : (exitP b).Runs A m fun (x : Fin K → A) (b' : Bool) (y : Fin K → A) => b' = b ∧ HeadAgree m x y

theorem DescriptiveComplexity.HeadProgram.headLocal2_exitP {K : ℕ} {A : Type} (b : Bool) (m : ℕ) : HeadLocal2 m fun (x : Fin K → A) (b' : Bool) (y : Fin K → A) => b' = b ∧ HeadAgree m x y

def DescriptiveComplexity.HeadProgram.guessManyP {L : FirstOrder.Language} {K : ℕ} (hd : ℕ → Fin K) (lo : ℕ) : ℕ → HeadProgram L K

Guessing several heads: the heads hd lo, …, hd (lo + n - 1), in turn.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.guessManyP hd lo 0 = DescriptiveComplexity.HeadProgram.exitP true

theorem DescriptiveComplexity.HeadProgram.runs_guessManyP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (hd : ℕ → Fin K) (m : ℕ) (hhd : ∀ i < m, ↑(hd i) = i) (lo n : ℕ) : lo + n ≤ m → (guessManyP hd lo n).Runs A m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => b = true ∧ ∀ (j : Fin K), ↑j < m → ↑j < lo ∨ lo + n ≤ ↑j → y j = x j

What guessing a block runs: the heads of the block may end anywhere, and no other head moves.

The control graph of the machine

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

The control nodes of the machine simulating a specification: which mode the walk is in, and what it is doing. r is the number of modes, and the Fin (r + 1) indices walk the list of modes, one free choice at a time.

• pickSrc {M : Type} {r : ℕ} (i : Fin (r + 1)) : DrvNode M r

  Choosing which mode to start the walk in.

• trySrc {M : Type} {r : ℕ} (m : M) : DrvNode M r

  Guessing a starting tuple and testing the source formula.

• target {M : Type} {r : ℕ} (m : M) : DrvNode M r

  Testing the target formula at the current node.

• pickCand {M : Type} {r : ℕ} (m : M) (i : Fin (r + 1)) : DrvNode M r

  Choosing which mode to step into.

• tryCand {M : Type} {r : ℕ} (m m' : M) : DrvNode M r

  Guessing the next tuple and testing the transition formula.

• commit {M : Type} {r : ℕ} (m m' : M) : DrvNode M r

  Copying the guessed tuple onto the current one.

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

  Nothing more to do.

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

def DescriptiveComplexity.HeadProgram.drvWire {M : Type} {r : ℕ} (modeAt : Fin (r + 1) → Option M) (nextIx : Fin (r + 1) → Fin (r + 1)) (i₀ : Fin (r + 1)) : DrvNode M r → Bool → DrvNode M r ⊕ Bool

Where the machine goes when a fragment exits.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.pickSrc i) false = Sum.inl (DescriptiveComplexity.HeadProgram.DrvNode.pickSrc (nextIx i))
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.trySrc m) true = Sum.inl (DescriptiveComplexity.HeadProgram.DrvNode.target m)
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.trySrc m) false = Sum.inl DescriptiveComplexity.HeadProgram.DrvNode.dead
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.target m) true = Sum.inr true
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.target m) false = Sum.inl (DescriptiveComplexity.HeadProgram.DrvNode.pickCand m i₀)
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.tryCand m m') true = Sum.inl (DescriptiveComplexity.HeadProgram.DrvNode.commit m m')
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.tryCand m m') false = Sum.inl DescriptiveComplexity.HeadProgram.DrvNode.dead
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ (DescriptiveComplexity.HeadProgram.DrvNode.commit m m') x✝ = Sum.inl (DescriptiveComplexity.HeadProgram.DrvNode.target m')
• DescriptiveComplexity.HeadProgram.drvWire modeAt nextIx i₀ DescriptiveComplexity.HeadProgram.DrvNode.dead x✝ = Sum.inr false

The machine of a specification

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

The quantifier budget of a specification: the largest number of extra heads the evaluation of one of its formulas needs.

Equations

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

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

How many heads the machine of a specification has: two tuples, the evaluator's workspace, and a spare one so that there is always a head.

Equations

• DescriptiveComplexity.specHeads spec = 2 * spec.k + DescriptiveComplexity.specDepth spec + 1

theorem DescriptiveComplexity.two_k_lt_specHeads {L : FirstOrder.Language} (spec : TCSpec L) : 2 * spec.k < specHeads spec

noncomputable def DescriptiveComplexity.blk0 {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin spec.k) : Fin (specHeads spec)

The heads holding the current tuple.

Equations

• DescriptiveComplexity.blk0 spec i = ⟨↑i, ⋯⟩

noncomputable def DescriptiveComplexity.blk1 {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin spec.k) : Fin (specHeads spec)

The heads holding the candidate tuple.

Equations

• DescriptiveComplexity.blk1 spec i = ⟨spec.k + ↑i, ⋯⟩

noncomputable def DescriptiveComplexity.shd {L : FirstOrder.Language} (spec : TCSpec L) (i : ℕ) : Fin (specHeads spec)

The head at a given index, for the evaluator's workspace.

Equations

• DescriptiveComplexity.shd spec i = if h : i < DescriptiveComplexity.specHeads spec then ⟨i, h⟩ else ⟨0, ⋯⟩

theorem DescriptiveComplexity.shd_val {L : FirstOrder.Language} (spec : TCSpec L) {i : ℕ} (h : i < specHeads spec) : ↑(shd spec i) = i

@[simp]

theorem DescriptiveComplexity.blk0_val {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin spec.k) : ↑(blk0 spec i) = ↑i

@[simp]

theorem DescriptiveComplexity.blk1_val {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin spec.k) : ↑(blk1 spec i) = spec.k + ↑i

noncomputable def DescriptiveComplexity.curNode {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (m : spec.Mode) : spec.Node A

The node of the specification the machine is at: its mode, and the tuple on the first block of heads.

Equations

• DescriptiveComplexity.curNode spec x m = (m, fun (i : Fin spec.k) => x (DescriptiveComplexity.blk0 spec i))

noncomputable def DescriptiveComplexity.candNode {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (m : spec.Mode) : spec.Node A

The node the machine is considering stepping into: the tuple on the second block of heads.

Equations

• DescriptiveComplexity.candNode spec x m = (m, fun (i : Fin spec.k) => x (DescriptiveComplexity.blk1 spec i))

The fragments

theorem DescriptiveComplexity.qdepth_src_le {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram.qdepth (spec.src m) ≤ specDepth spec

theorem DescriptiveComplexity.qdepth_tgt_le {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram.qdepth (spec.tgt m) ≤ specDepth spec

theorem DescriptiveComplexity.qdepth_step_le {L : FirstOrder.Language} (spec : TCSpec L) (m m' : spec.Mode) : HeadProgram.qdepth (spec.step m m') ≤ specDepth spec

noncomputable def DescriptiveComplexity.hv0 {L : FirstOrder.Language} (spec : TCSpec L) : Fin spec.k ⊕ Fin 0 → Fin (specHeads spec)

The variables of a formula about the current tuple live in the first block of heads.

Equations

• DescriptiveComplexity.hv0 spec = Sum.elim (DescriptiveComplexity.blk0 spec) Fin.elim0

noncomputable def DescriptiveComplexity.hv01 {L : FirstOrder.Language} (spec : TCSpec L) : (Fin spec.k ⊕ Fin spec.k) ⊕ Fin 0 → Fin (specHeads spec)

The variables of a transition formula live in the two blocks of heads.

Equations

• DescriptiveComplexity.hv01 spec = Sum.elim (Sum.elim (DescriptiveComplexity.blk0 spec) (DescriptiveComplexity.blk1 spec)) Fin.elim0

theorem DescriptiveComplexity.hv0_low {L : FirstOrder.Language} (spec : TCSpec L) (v : Fin spec.k ⊕ Fin 0) : ↑(hv0 spec v) < 2 * spec.k

theorem DescriptiveComplexity.hv01_low {L : FirstOrder.Language} (spec : TCSpec L) (v : (Fin spec.k ⊕ Fin spec.k) ⊕ Fin 0) : ↑(hv01 spec v) < 2 * spec.k

noncomputable def DescriptiveComplexity.evalSrcP {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram L (specHeads spec)

The evaluator for a source formula.

Equations

• DescriptiveComplexity.evalSrcP spec m = DescriptiveComplexity.HeadProgram.evalP (DescriptiveComplexity.shd spec) (2 * spec.k) (DescriptiveComplexity.hv0 spec) (spec.src m)

noncomputable def DescriptiveComplexity.evalTgtP {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram L (specHeads spec)

The evaluator for a target formula.

Equations

• DescriptiveComplexity.evalTgtP spec m = DescriptiveComplexity.HeadProgram.evalP (DescriptiveComplexity.shd spec) (2 * spec.k) (DescriptiveComplexity.hv0 spec) (spec.tgt m)

noncomputable def DescriptiveComplexity.evalStepP {L : FirstOrder.Language} (spec : TCSpec L) (m m' : spec.Mode) : HeadProgram L (specHeads spec)

The evaluator for a transition formula.

Equations

• DescriptiveComplexity.evalStepP spec m m' = DescriptiveComplexity.HeadProgram.evalP (DescriptiveComplexity.shd spec) (2 * spec.k) (DescriptiveComplexity.hv01 spec) (spec.step m m')

noncomputable def DescriptiveComplexity.commitMoves {L : FirstOrder.Language} (spec : TCSpec L) : Fin (specHeads spec) → HeadMove (specHeads spec)

The moves that copy the candidate tuple onto the current one.

Equations

• DescriptiveComplexity.commitMoves spec j = if h : ↑j < spec.k then DescriptiveComplexity.HeadMove.copy (DescriptiveComplexity.blk1 spec ⟨↑j, h⟩) else DescriptiveComplexity.HeadMove.stay

theorem DescriptiveComplexity.hshd {L : FirstOrder.Language} (spec : TCSpec L) (i : ℕ) : i < specHeads spec → ↑(shd spec i) = i

theorem DescriptiveComplexity.decides_evalSrcP {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (m : spec.Mode) : (evalSrcP spec m).Decides A (2 * spec.k) fun (x : Fin (specHeads spec) → A) => spec.IsSrc (curNode spec x m)

theorem DescriptiveComplexity.decides_evalTgtP {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (m : spec.Mode) : (evalTgtP spec m).Decides A (2 * spec.k) fun (x : Fin (specHeads spec) → A) => spec.IsTgt (curNode spec x m)

theorem DescriptiveComplexity.decides_evalStepP {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (m m' : spec.Mode) : (evalStepP spec m m').Decides A (2 * spec.k) fun (x : Fin (specHeads spec) → A) => spec.Step (curNode spec x m) (candNode spec x m')

theorem DescriptiveComplexity.headLocal_isSrc {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m : spec.Mode) : HeadLocal (2 * spec.k) fun (x : Fin (specHeads spec) → A) => spec.IsSrc (curNode spec x m)

theorem DescriptiveComplexity.headLocal_isTgt {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m : spec.Mode) : HeadLocal (2 * spec.k) fun (x : Fin (specHeads spec) → A) => spec.IsTgt (curNode spec x m)

theorem DescriptiveComplexity.headLocal_step {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m m' : spec.Mode) : HeadLocal (2 * spec.k) fun (x : Fin (specHeads spec) → A) => spec.Step (curNode spec x m) (candNode spec x m')

The machine

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

The number of modes.

Equations

• DescriptiveComplexity.modeCard spec = Nat.card spec.Mode

noncomputable def DescriptiveComplexity.modeEquiv {L : FirstOrder.Language} (spec : TCSpec L) : spec.Mode ≃ Fin (modeCard spec)

An enumeration of the modes.

Equations

• DescriptiveComplexity.modeEquiv spec = Finite.equivFin spec.Mode

noncomputable def DescriptiveComplexity.modeAt {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin (modeCard spec + 1)) : Option spec.Mode

The mode at an index of the enumeration, if any.

Equations

• DescriptiveComplexity.modeAt spec i = if h : ↑i < DescriptiveComplexity.modeCard spec then some ((DescriptiveComplexity.modeEquiv spec).symm ⟨↑i, h⟩) else none

noncomputable def DescriptiveComplexity.nextIx {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin (modeCard spec + 1)) : Fin (modeCard spec + 1)

The next index of the enumeration; it stops at the last one.

Equations

• DescriptiveComplexity.nextIx spec i = if h : ↑i < DescriptiveComplexity.modeCard spec then ⟨↑i + 1, ⋯⟩ else i

noncomputable def DescriptiveComplexity.ix0 {L : FirstOrder.Language} (spec : TCSpec L) : Fin (modeCard spec + 1)

The index the enumeration starts at.

Equations

• DescriptiveComplexity.ix0 spec = ⟨0, ⋯⟩

noncomputable def DescriptiveComplexity.ixOf {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : Fin (modeCard spec + 1)

The index of a mode in the enumeration.

Equations

• DescriptiveComplexity.ixOf spec m = ⟨↑((DescriptiveComplexity.modeEquiv spec) m), ⋯⟩

theorem DescriptiveComplexity.modeAt_ixOf {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : modeAt spec (ixOf spec m) = some m

noncomputable def DescriptiveComplexity.drvFam {L : FirstOrder.Language} (spec : TCSpec L) : HeadProgram.DrvNode spec.Mode (modeCard spec) → HeadProgram L (specHeads spec)

The fragments of the machine.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.drvFam spec (DescriptiveComplexity.HeadProgram.DrvNode.pickSrc i) = DescriptiveComplexity.HeadProgram.chooseP
• DescriptiveComplexity.drvFam spec (DescriptiveComplexity.HeadProgram.DrvNode.target m) = DescriptiveComplexity.evalTgtP spec m
• DescriptiveComplexity.drvFam spec (DescriptiveComplexity.HeadProgram.DrvNode.pickCand m i) = DescriptiveComplexity.HeadProgram.chooseP
• DescriptiveComplexity.drvFam spec (DescriptiveComplexity.HeadProgram.DrvNode.commit m m') = DescriptiveComplexity.HeadProgram.moveP (DescriptiveComplexity.commitMoves spec)
• DescriptiveComplexity.drvFam spec DescriptiveComplexity.HeadProgram.DrvNode.dead = DescriptiveComplexity.HeadProgram.exitP false

noncomputable def DescriptiveComplexity.drvP {L : FirstOrder.Language} (spec : TCSpec L) : HeadProgram L (specHeads spec)

The machine of a specification: the loop described in the header, as a control graph over those fragments.

Equations

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

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

What the fragments of the machine run.

Equations

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

theorem DescriptiveComplexity.curNode_congr {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} {x y : Fin (specHeads spec) → A} (h : ∀ (j : Fin (specHeads spec)), ↑j < spec.k → y j = x j) (m : spec.Mode) : curNode spec y m = curNode spec x m

theorem DescriptiveComplexity.candNode_congr {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} {x y : Fin (specHeads spec) → A} (h : ∀ (j : Fin (specHeads spec)), spec.k ≤ ↑j → ↑j < 2 * spec.k → y j = x j) (m : spec.Mode) : candNode spec y m = candNode spec x m

theorem DescriptiveComplexity.hshd' {L : FirstOrder.Language} (spec : TCSpec L) (i : ℕ) : i < 2 * spec.k → ↑(shd spec i) = i

theorem DescriptiveComplexity.runs_drvFam {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (c : HeadProgram.DrvNode spec.Mode (modeCard spec)) : (drvFam spec c).Runs A (2 * spec.k) (drvRel spec c)

The fragments run what they are meant to.

theorem DescriptiveComplexity.headLocal2_drvRel {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (c : HeadProgram.DrvNode spec.Mode (modeCard spec)) : HeadLocal2 (2 * spec.k) (drvRel spec c)

The relations the fragments run see only the two tuples.

Soundness: what the machine knows

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

The invariant the machine carries: at a control node, the tuple on the first block of heads is a node of the specification reachable from a source – and, at commit, the candidate is a step away.

Equations

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

The wiring, arc by arc.

@[simp]

theorem DescriptiveComplexity.drvWire_pickSrc_true {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin (modeCard spec + 1)) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.pickSrc i) true = Sum.inl ((modeAt spec i).elim HeadProgram.DrvNode.dead HeadProgram.DrvNode.trySrc)

@[simp]

theorem DescriptiveComplexity.drvWire_pickSrc_false {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin (modeCard spec + 1)) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.pickSrc i) false = Sum.inl (HeadProgram.DrvNode.pickSrc (nextIx spec i))

@[simp]

theorem DescriptiveComplexity.drvWire_trySrc_true {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.trySrc m) true = Sum.inl (HeadProgram.DrvNode.target m)

@[simp]

theorem DescriptiveComplexity.drvWire_trySrc_false {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.trySrc m) false = Sum.inl HeadProgram.DrvNode.dead

@[simp]

theorem DescriptiveComplexity.drvWire_target_true {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.target m) true = Sum.inr true

@[simp]

theorem DescriptiveComplexity.drvWire_target_false {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.target m) false = Sum.inl (HeadProgram.DrvNode.pickCand m (ix0 spec))

@[simp]

theorem DescriptiveComplexity.drvWire_pickCand_true {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin (modeCard spec + 1)) (m : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.pickCand m i) true = Sum.inl ((modeAt spec i).elim HeadProgram.DrvNode.dead (HeadProgram.DrvNode.tryCand m))

@[simp]

theorem DescriptiveComplexity.drvWire_pickCand_false {L : FirstOrder.Language} (spec : TCSpec L) (i : Fin (modeCard spec + 1)) (m : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.pickCand m i) false = Sum.inl (HeadProgram.DrvNode.pickCand m (nextIx spec i))

@[simp]

theorem DescriptiveComplexity.drvWire_tryCand_true {L : FirstOrder.Language} (spec : TCSpec L) (m m' : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.tryCand m m') true = Sum.inl (HeadProgram.DrvNode.commit m m')

@[simp]

theorem DescriptiveComplexity.drvWire_tryCand_false {L : FirstOrder.Language} (spec : TCSpec L) (m m' : spec.Mode) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.tryCand m m') false = Sum.inl HeadProgram.DrvNode.dead

@[simp]

theorem DescriptiveComplexity.drvWire_commit {L : FirstOrder.Language} (spec : TCSpec L) (m m' : spec.Mode) (b : Bool) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) (HeadProgram.DrvNode.commit m m') b = Sum.inl (HeadProgram.DrvNode.target m')

@[simp]

theorem DescriptiveComplexity.drvWire_dead {L : FirstOrder.Language} (spec : TCSpec L) (b : Bool) : HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec) HeadProgram.DrvNode.dead b = Sum.inr false

theorem DescriptiveComplexity.drvInv_of_walk {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x₀ : Fin (specHeads spec) → A) {u : HeadProgram.DrvNode spec.Mode (modeCard spec) × (Fin (specHeads spec) → A)} (h : Relation.ReflTransGen (HeadProgram.wireStep (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec))) (HeadProgram.DrvNode.pickSrc (ix0 spec), x₀) u) : drvInv spec u

The invariant is carried along the machine's walk.

theorem DescriptiveComplexity.accepts_of_exit {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x₀ : Fin (specHeads spec) → A) {u : HeadProgram.DrvNode spec.Mode (modeCard spec) × (Fin (specHeads spec) → A)} {z : Fin (specHeads spec) → A} (hwalk : Relation.ReflTransGen (HeadProgram.wireStep (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec))) (HeadProgram.DrvNode.pickSrc (ix0 spec), x₀) u) (hexit : HeadProgram.wireExit (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec)) u true z) : spec.Accepts A

Soundness: if the machine accepts, the specification does.

Completeness: the machine imitates the walk

noncomputable def DescriptiveComplexity.putBlk0 {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (u : Fin spec.k → A) : Fin (specHeads spec) → A

Putting a tuple on the first block of heads.

Equations

• DescriptiveComplexity.putBlk0 spec x u j = if h : ↑j < spec.k then u ⟨↑j, h⟩ else x j

noncomputable def DescriptiveComplexity.putBlk1 {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (u : Fin spec.k → A) : Fin (specHeads spec) → A

Putting a tuple on the second block of heads.

Equations

• DescriptiveComplexity.putBlk1 spec x u j = if h : spec.k ≤ ↑j ∧ ↑j < 2 * spec.k then u ⟨↑j - spec.k, ⋯⟩ else x j

theorem DescriptiveComplexity.putBlk0_blk0 {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (u : Fin spec.k → A) (i : Fin spec.k) : putBlk0 spec x u (blk0 spec i) = u i

theorem DescriptiveComplexity.putBlk0_of_le {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (u : Fin spec.k → A) {j : Fin (specHeads spec)} (hj : spec.k ≤ ↑j) : putBlk0 spec x u j = x j

theorem DescriptiveComplexity.putBlk1_blk1 {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (u : Fin spec.k → A) (i : Fin spec.k) : putBlk1 spec x u (blk1 spec i) = u i

theorem DescriptiveComplexity.putBlk1_of_lt {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (x : Fin (specHeads spec) → A) (u : Fin spec.k → A) {j : Fin (specHeads spec)} (hj : ↑j < spec.k) : putBlk1 spec x u j = x j

theorem DescriptiveComplexity.walk_pickSrc {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x : Fin (specHeads spec) → A) (n : ℕ) (hn : n < modeCard spec + 1) : Relation.ReflTransGen (HeadProgram.wireStep (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec))) (HeadProgram.DrvNode.pickSrc (ix0 spec), x) (HeadProgram.DrvNode.pickSrc ⟨n, hn⟩, x)

The chain of free choices reaches every mode.

theorem DescriptiveComplexity.walk_pickCand {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x : Fin (specHeads spec) → A) (m : spec.Mode) (n : ℕ) (hn : n < modeCard spec + 1) : Relation.ReflTransGen (HeadProgram.wireStep (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec))) (HeadProgram.DrvNode.pickCand m (ix0 spec), x) (HeadProgram.DrvNode.pickCand m ⟨n, hn⟩, x)

The same chain, for the candidate mode.

theorem DescriptiveComplexity.walk_of_reach {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x₀ : Fin (specHeads spec) → A) {u₀ : spec.Node A} (hsrc : spec.IsSrc u₀) (w : spec.Node A) : spec.Reach u₀ w → (∃ (u : HeadProgram.DrvNode spec.Mode (modeCard spec) × (Fin (specHeads spec) → A)) (z : Fin (specHeads spec) → A), Relation.ReflTransGen (HeadProgram.wireStep (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec))) (HeadProgram.DrvNode.pickSrc (ix0 spec), x₀) u ∧ HeadProgram.wireExit (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec)) u true z) ∨ ∃ (x : Fin (specHeads spec) → A), curNode spec x w.1 = w ∧ Relation.ReflTransGen (HeadProgram.wireStep (drvRel spec) (HeadProgram.drvWire (modeAt spec) (nextIx spec) (ix0 spec))) (HeadProgram.DrvNode.pickSrc (ix0 spec), x₀) (HeadProgram.DrvNode.target w.1, x)

Completeness: the machine imitates the specification's walk, node by node, unless it has already accepted on the way.

The capture theorem

theorem DescriptiveComplexity.accepts_drvP {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ((drvP spec).compile false).Accepts A ↔ spec.Accepts A

The machine of a specification accepts exactly what the specification does.

The capture theorem

theorem DescriptiveComplexity.tcDefinable_iff_automaton {L : FirstOrder.Language} {P : DecisionProblem L} : TCDefinable P ↔ ∃ (k : ℕ) (M : HeadAutomaton L k), ∀ (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(TC): a problem is definable by a single transitive closure exactly when a two-way multi-head automaton recognizes it. One direction is DescriptiveComplexity.tcDefinable_of_automaton – a configuration is a node of a specification – and the other is the machine built here.

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

NL is the class of the two-way multi-head automata: membership in DescriptiveComplexity.NL is recognizability by such a machine.