Evaluating a first-order formula with heads

The half of the capture theorem that has content: a two-way multi-head automaton can decide any fixed first-order formula of its head positions, spending two extra heads per quantifier.

The guards of a DescriptiveComplexity.HeadProgram are quantifier-free by fiat – a control that could read a quantified fact would be first-order logic in disguise. This file removes the apparent limitation: quantifiers are not read, they are walked. To decide ∀ x, φ(x) the program parks a head at the greatest element, sweeps another head from the least element upwards, and evaluates φ at each stop; it answers false at the first stop where φ fails, and true when the sweep reaches the parked head. Existential quantification is ∀ with → ⊥ around it, which the imp case already handles, so a single sweep serves both.

The two combinators

• DescriptiveComplexity.HeadProgram.iteP – run a fragment, then one of two others depending on its answer. This is branching, sequencing and negation at once.
• DescriptiveComplexity.HeadProgram.scanP – the sweep just described, on a pair of heads: h walks, hm marks the greatest element. Why two heads and not one: the sweep must know when to stop, and "this head is at the greatest element" is not a quantifier-free fact of one head – while "these two heads are equal" is, being an atom. A single parked head buys the test. The step off the end is not needed as a guard: DescriptiveComplexity.HeadMove.succ is simply disabled there.

Both are DescriptiveComplexity.HeadProgram.wireP over a four- or three-node control graph, and both are proved by DescriptiveComplexity.HeadProgram.runs_wireP: the sweep's proof is an induction downwards along the order (DescriptiveComplexity.order_induction_down), which is the direction that knows about the elements a walker has not yet reached.

The evaluator

DescriptiveComplexity.HeadProgram.evalP is defined by structural recursion on a BoundedFormula, with a fixed layout of the heads:

• the free variables live wherever the caller says, through a map hv into heads below the protection level d;
• the i-th bound variable lives at head d + 2 * i-ish – precisely, entering a quantifier at level d claims heads d and d + 1 and recurses at level d + 2, so DescriptiveComplexity.HeadProgram.qdepth counts two heads per nested quantifier;
• everything from the current level up is scratch.

The recursion never inspects a state: each case is a combinator, and its correctness is the corresponding combinator lemma applied to the inductive hypothesis. The result, DescriptiveComplexity.HeadProgram.decides_evalP, is a DescriptiveComplexity.HeadProgram.Decides, and DescriptiveComplexity.HeadProgram.deterministic_evalP records that the evaluator is deterministic – a sweep is not a guess – which is what lets the same evaluator serve the deterministic capture.

Moving a single head

def DescriptiveComplexity.HeadProgram.setHead {K : ℕ} (h : Fin K) (mv : HeadMove K) : Fin K → HeadMove K

The moves that send head h along mv and leave every other head where it is.

Equations

• DescriptiveComplexity.HeadProgram.setHead h mv j = if j = h then mv else DescriptiveComplexity.HeadMove.stay

@[simp]

theorem DescriptiveComplexity.HeadProgram.setHead_self {K : ℕ} (h : Fin K) (mv : HeadMove K) : setHead h mv h = mv

@[simp]

theorem DescriptiveComplexity.HeadProgram.setHead_of_ne {K : ℕ} {h j : Fin K} (mv : HeadMove K) (hj : j ≠ h) : setHead h mv j = HeadMove.stay

theorem DescriptiveComplexity.HeadProgram.runs_moveP_local {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (mvs : Fin K → HeadMove K) (m : ℕ) (hstay : ∀ (j : Fin K), m ≤ ↑j → mvs j = HeadMove.stay) : (moveP mvs).Runs A m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => b = true ∧ ∀ (j : Fin K), ↑j < m → (mvs j).Holds x j (y j)

Moving, seen from the interface: a fragment that only moves heads below m runs a relation about those heads alone.

Branching

inductive DescriptiveComplexity.HeadProgram.IteNode : Type

The control nodes of a branch: the test, and its two continuations.

• test : IteNode

  Running the test.

• thenB : IteNode

  Running the continuation taken when the test says true.

• elseB : IteNode

  Running the continuation taken when the test says false.

@[instance_reducible]

instance DescriptiveComplexity.HeadProgram.instDecidableEqIteNode : DecidableEq IteNode

Equations

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

instance DescriptiveComplexity.HeadProgram.instFiniteIteNode : Finite IteNode

def DescriptiveComplexity.HeadProgram.iteWire : IteNode → Bool → IteNode ⊕ Bool

The wiring of a branch: the test hands over to one of the continuations, which then answer for the whole.

Equations

• DescriptiveComplexity.HeadProgram.iteWire DescriptiveComplexity.HeadProgram.IteNode.test true = Sum.inl DescriptiveComplexity.HeadProgram.IteNode.thenB
• DescriptiveComplexity.HeadProgram.iteWire DescriptiveComplexity.HeadProgram.IteNode.test false = Sum.inl DescriptiveComplexity.HeadProgram.IteNode.elseB
• DescriptiveComplexity.HeadProgram.iteWire x✝¹ x✝ = Sum.inr x✝

def DescriptiveComplexity.HeadProgram.iteFam {L : FirstOrder.Language} {K : ℕ} (F G H : HeadProgram L K) : IteNode → HeadProgram L K

The fragments of a branch.

Equations

• F.iteFam G H DescriptiveComplexity.HeadProgram.IteNode.test = F
• F.iteFam G H DescriptiveComplexity.HeadProgram.IteNode.thenB = G
• F.iteFam G H DescriptiveComplexity.HeadProgram.IteNode.elseB = H

def DescriptiveComplexity.HeadProgram.iteP {L : FirstOrder.Language} {K : ℕ} (F G H : HeadProgram L K) : HeadProgram L K

Branching: run F; continue with G if it says true and with H if it says false, and answer what the continuation answers.

Equations

• F.iteP G H = DescriptiveComplexity.HeadProgram.wireP (F.iteFam G H) DescriptiveComplexity.HeadProgram.iteWire DescriptiveComplexity.HeadProgram.IteNode.test

theorem DescriptiveComplexity.HeadProgram.iteWalk {K : ℕ} {A : Type} {R : IteNode → (Fin K → A) → Bool → (Fin K → A) → Prop} {x : Fin K → A} {u : IteNode × (Fin K → A)} (h : Relation.ReflTransGen (wireStep R iteWire) (IteNode.test, x) u) : u = (IteNode.test, x) ∨ (∃ (y : Fin K → A), u = (IteNode.thenB, y) ∧ R IteNode.test x true y) ∨ ∃ (y : Fin K → A), u = (IteNode.elseB, y) ∧ R IteNode.test x false y

The walk of a branch: from the test, one either has not moved, or has handed over to one of the two continuations.

def DescriptiveComplexity.HeadProgram.iteRel {K : ℕ} {A : Type} (R S T : (Fin K → A) → Bool → (Fin K → A) → Prop) : IteNode → (Fin K → A) → Bool → (Fin K → A) → Prop

The relations the fragments of a branch run.

Equations

• DescriptiveComplexity.HeadProgram.iteRel R S T DescriptiveComplexity.HeadProgram.IteNode.test = R
• DescriptiveComplexity.HeadProgram.iteRel R S T DescriptiveComplexity.HeadProgram.IteNode.thenB = S
• DescriptiveComplexity.HeadProgram.iteRel R S T DescriptiveComplexity.HeadProgram.IteNode.elseB = T

theorem DescriptiveComplexity.HeadProgram.runs_iteP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} {F G H : HeadProgram L K} {R S T : (Fin K → A) → Bool → (Fin K → A) → Prop} (hF : F.Runs A m R) (hG : G.Runs A m S) (hH : H.Runs A m T) (hRl : HeadLocal2 m R) (hSl : HeadLocal2 m S) (hTl : HeadLocal2 m T) : (F.iteP G H).Runs A m fun (x : Fin K → A) (b : Bool) (z : Fin K → A) => ∃ (y : Fin K → A), R x true y ∧ S y b z ∨ R x false y ∧ T y b z

What a branch runs: the test, followed by whichever continuation its answer selects.

theorem DescriptiveComplexity.HeadProgram.decides_iteP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} {F G H : HeadProgram L K} {P Q₁ Q₂ : (Fin K → A) → Prop} (hF : F.Decides A m P) (hG : G.Decides A m Q₁) (hH : H.Decides A m Q₂) (hP : HeadLocal m P) (hQ₁ : HeadLocal m Q₁) (hQ₂ : HeadLocal m Q₂) : (F.iteP G H).Decides A m fun (x : Fin K → A) => P x ∧ Q₁ x ∨ ¬P x ∧ Q₂ x

What a branch decides: the test's property, with the continuations' properties under it.

theorem DescriptiveComplexity.HeadProgram.deterministic_iteP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F G H : HeadProgram L K} (hF : F.Deterministic A) (hG : G.Deterministic A) (hH : H.Deterministic A) : (F.iteP G H).Deterministic A

A branch is deterministic as soon as its three fragments are.

Sweeping a head along the order

def DescriptiveComplexity.HeadProgram.MoveLocal {K : ℕ} (m : ℕ) : HeadMove K → Prop

Which heads a move looks at: the ones a fragment protecting m heads may mention.

Equations

• DescriptiveComplexity.HeadProgram.MoveLocal m DescriptiveComplexity.HeadMove.stay = True
• DescriptiveComplexity.HeadProgram.MoveLocal m DescriptiveComplexity.HeadMove.toMin = True
• DescriptiveComplexity.HeadProgram.MoveLocal m DescriptiveComplexity.HeadMove.toMax = True
• DescriptiveComplexity.HeadProgram.MoveLocal m (DescriptiveComplexity.HeadMove.copy i) = (↑i < m)
• DescriptiveComplexity.HeadProgram.MoveLocal m (DescriptiveComplexity.HeadMove.succ i) = (↑i < m)
• DescriptiveComplexity.HeadProgram.MoveLocal m (DescriptiveComplexity.HeadMove.pred i) = (↑i < m)

theorem DescriptiveComplexity.HeadProgram.holds_congr {K : ℕ} {A : Type} [LinearOrder A] {mv : HeadMove K} {m : ℕ} (hmv : MoveLocal m mv) {x x' : Fin K → A} (hx : HeadAgree m x x') {j : Fin K} (hj : ↑j < m) (v : A) : mv.Holds x j v ↔ mv.Holds x' j v

A move that looks only at the first m heads cannot tell two assignments agreeing there apart.

theorem DescriptiveComplexity.HeadProgram.headLocal2_moveP {K : ℕ} {A : Type} [LinearOrder A] {mvs : Fin K → HeadMove K} {m : ℕ} (hloc : ∀ (j : Fin K), ↑j < m → MoveLocal m (mvs j)) : HeadLocal2 m fun (x : Fin K → A) (b : Bool) (y : Fin K → A) => b = true ∧ ∀ (j : Fin K), ↑j < m → (mvs j).Holds x j (y j)

The relation a move fragment runs is local when its moves are.

inductive DescriptiveComplexity.HeadProgram.ScanNode : Type

The control nodes of a sweep.

• reset : ScanNode

  Putting the walking head at the least element and the marker at the greatest.

• body : ScanNode

  Evaluating the body at the current value of the walking head.

• atMax : ScanNode

  Asking whether the walking head has reached the marker.

• bump : ScanNode

  Stepping the walking head to the next element.

@[instance_reducible]

instance DescriptiveComplexity.HeadProgram.instDecidableEqScanNode : DecidableEq ScanNode

Equations

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

instance DescriptiveComplexity.HeadProgram.instFiniteScanNode : Finite ScanNode

def DescriptiveComplexity.HeadProgram.scanWire : ScanNode → Bool → ScanNode ⊕ Bool

The wiring of a sweep: a body that fails ends it, a body that succeeds asks whether the sweep is over, and if it is not the walking head steps on.

Equations

• DescriptiveComplexity.HeadProgram.scanWire DescriptiveComplexity.HeadProgram.ScanNode.reset x✝ = Sum.inl DescriptiveComplexity.HeadProgram.ScanNode.body
• DescriptiveComplexity.HeadProgram.scanWire DescriptiveComplexity.HeadProgram.ScanNode.body true = Sum.inl DescriptiveComplexity.HeadProgram.ScanNode.atMax
• DescriptiveComplexity.HeadProgram.scanWire DescriptiveComplexity.HeadProgram.ScanNode.body false = Sum.inr false
• DescriptiveComplexity.HeadProgram.scanWire DescriptiveComplexity.HeadProgram.ScanNode.atMax true = Sum.inr true
• DescriptiveComplexity.HeadProgram.scanWire DescriptiveComplexity.HeadProgram.ScanNode.atMax false = Sum.inl DescriptiveComplexity.HeadProgram.ScanNode.bump
• DescriptiveComplexity.HeadProgram.scanWire DescriptiveComplexity.HeadProgram.ScanNode.bump x✝ = Sum.inl DescriptiveComplexity.HeadProgram.ScanNode.body

def DescriptiveComplexity.HeadProgram.resetMoves {K : ℕ} (h hm : Fin K) : Fin K → HeadMove K

The moves that start a sweep: the walking head to the least element, the marker to the greatest.

Equations

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

def DescriptiveComplexity.HeadProgram.scanFam {L : FirstOrder.Language} {K : ℕ} (h hm : Fin K) (F : HeadProgram L K) : ScanNode → HeadProgram L K

The fragments of a sweep.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.scanFam h hm F DescriptiveComplexity.HeadProgram.ScanNode.reset = DescriptiveComplexity.HeadProgram.moveP (DescriptiveComplexity.HeadProgram.resetMoves h hm)
• DescriptiveComplexity.HeadProgram.scanFam h hm F DescriptiveComplexity.HeadProgram.ScanNode.body = F
• DescriptiveComplexity.HeadProgram.scanFam h hm F DescriptiveComplexity.HeadProgram.ScanNode.atMax = DescriptiveComplexity.HeadProgram.leafP (DescriptiveComplexity.HeadMove.eqVarF L h hm) ⋯

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

The sweep: run F at every value of head h in turn, from the least element up to the marker head hm; answer false at the first value where F does, and true if it never does.

Equations

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

def DescriptiveComplexity.HeadProgram.scanRel {K : ℕ} {A : Type} [LinearOrder A] (d : ℕ) (h hm : Fin K) (P : (Fin K → A) → Prop) : ScanNode → (Fin K → A) → Bool → (Fin K → A) → Prop

The relations the fragments of a sweep run.

Equations

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

theorem DescriptiveComplexity.HeadProgram.Decides.congr {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F : HeadProgram L K} {m : ℕ} {P P' : (Fin K → A) → Prop} (h : F.Decides A m P) (hPP : ∀ (x : Fin K → A), P x ↔ P' x) : F.Decides A m P'

Restating what a fragment decides.

theorem DescriptiveComplexity.HeadProgram.decides_scanP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {d : ℕ} {h hm : Fin K} (hh : ↑h = d) (hhm : ↑hm = d + 1) {F : HeadProgram L K} {P : (Fin K → A) → Prop} (hF : F.Decides A (d + 2) P) (hP : HeadLocal (d + 1) P) : (scanP h hm F).Decides A d fun (x : Fin K → A) => ∀ (a : A), P (Function.update x h a)

What a sweep decides: the body, at every value of the walking head.

theorem DescriptiveComplexity.HeadProgram.deterministic_scanP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {h hm : Fin K} {F : HeadProgram L K} (hF : F.Deterministic A) : (scanP h hm F).Deterministic A

A sweep is deterministic as soon as its body is: it walks, it does not guess.

Atoms as guards

def DescriptiveComplexity.HeadProgram.atomGuard {L : FirstOrder.Language} {K : ℕ} {α : Type} {n : ℕ} (hv : α ⊕ Fin n → Fin K) (ψ : (L.sum FirstOrder.Language.order).BoundedFormula α n) : (L.sum FirstOrder.Language.order).Formula (Fin K)

An atomic formula, read as a guard on the heads: its variables are sent to the heads that hold them.

Equations

• DescriptiveComplexity.HeadProgram.atomGuard hv ψ = FirstOrder.Language.Formula.relabel hv ψ.toFormula

theorem DescriptiveComplexity.HeadProgram.isQF_toFormula {L : FirstOrder.Language} {α : Type} {n : ℕ} {ψ : (L.sum FirstOrder.Language.order).BoundedFormula α n} (hψ : ψ.IsQF) : FirstOrder.Language.BoundedFormula.IsQF ψ.toFormula

Turning the bound variables into free ones keeps a formula quantifier-free.

theorem DescriptiveComplexity.HeadProgram.isQF_atomGuard {L : FirstOrder.Language} {K : ℕ} {α : Type} {n : ℕ} (hv : α ⊕ Fin n → Fin K) {ψ : (L.sum FirstOrder.Language.order).BoundedFormula α n} (hψ : ψ.IsQF) : FirstOrder.Language.BoundedFormula.IsQF (atomGuard hv ψ)

A guard read off a quantifier-free formula is quantifier-free, as a guard must be.

theorem DescriptiveComplexity.HeadProgram.realize_atomGuard {L : FirstOrder.Language} {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (hv : α ⊕ Fin n → Fin K) (ψ : (L.sum FirstOrder.Language.order).BoundedFormula α n) (x : Fin K → A) : (atomGuard hv ψ).Realize x ↔ ψ.Realize (fun (a : α) => x (hv (Sum.inl a))) fun (i : Fin n) => x (hv (Sum.inr i))

The guard holds exactly where the formula does, its variables read off the heads.

theorem DescriptiveComplexity.HeadProgram.headLocal_realize {L : FirstOrder.Language} {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] {n d : ℕ} (hv : α ⊕ Fin n → Fin K) (ψ : (L.sum FirstOrder.Language.order).BoundedFormula α n) (hlow : ∀ (v : α ⊕ Fin n), ↑(hv v) < d) : HeadLocal d fun (x : Fin K → A) => ψ.Realize (fun (a : α) => x (hv (Sum.inl a))) fun (i : Fin n) => x (hv (Sum.inr i))

What a formula says of the heads depends only on the heads its variables live in.

theorem DescriptiveComplexity.HeadProgram.decides_exitP_false {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (m : ℕ) : (exitP false).Decides A m fun (x : Fin K → A) => False

Exiting at once decides falsity.

theorem DescriptiveComplexity.HeadProgram.decides_exitP_true {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (m : ℕ) : (exitP true).Decides A m fun (x : Fin K → A) => True

Exiting at once decides truth.

The evaluator

def DescriptiveComplexity.HeadProgram.qdepth {L : FirstOrder.Language} {α : Type} {n : ℕ} : (L.sum FirstOrder.Language.order).BoundedFormula α n → ℕ

How many heads an evaluation needs: two per nested quantifier, one to walk and one to mark the greatest element.

Equations

• DescriptiveComplexity.HeadProgram.qdepth FirstOrder.Language.BoundedFormula.falsum = 0
• DescriptiveComplexity.HeadProgram.qdepth (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = 0
• DescriptiveComplexity.HeadProgram.qdepth (FirstOrder.Language.BoundedFormula.rel R ts) = 0
• DescriptiveComplexity.HeadProgram.qdepth (φ₁.imp φ₂) = max (DescriptiveComplexity.HeadProgram.qdepth φ₁) (DescriptiveComplexity.HeadProgram.qdepth φ₂)
• DescriptiveComplexity.HeadProgram.qdepth φ.all = DescriptiveComplexity.HeadProgram.qdepth φ + 2

def DescriptiveComplexity.HeadProgram.evalP {L : FirstOrder.Language} {K : ℕ} {α : Type} (sh : ℕ → Fin K) {n : ℕ} : ℕ → (α ⊕ Fin n → Fin K) → (L.sum FirstOrder.Language.order).BoundedFormula α n → HeadProgram L K

The evaluator: a program deciding a fixed first-order formula of the heads. Atoms are guards, implication is a branch, and a quantifier is a sweep of two fresh heads – sh d walking, sh (d + 1) marking the greatest element.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.evalP sh x✝¹ x✝ FirstOrder.Language.BoundedFormula.falsum = DescriptiveComplexity.HeadProgram.exitP false

theorem DescriptiveComplexity.HeadProgram.decides_evalP {L : FirstOrder.Language} {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] [Finite A] (sh : ℕ → Fin K) (hsh : ∀ i < K, ↑(sh i) = i) {n : ℕ} (ψ : (L.sum FirstOrder.Language.order).BoundedFormula α n) (d : ℕ) (hv : α ⊕ Fin n → Fin K) : (∀ (v : α ⊕ Fin n), ↑(hv v) < d) → d + qdepth ψ ≤ K → (evalP sh d hv ψ).Decides A d fun (x : Fin K → A) => ψ.Realize (fun (a : α) => x (hv (Sum.inl a))) fun (i : Fin n) => x (hv (Sum.inr i))

The evaluator is correct: it decides the formula, reading its variables off the heads they live in, and gives those heads back untouched.

theorem DescriptiveComplexity.HeadProgram.deterministic_evalP {L : FirstOrder.Language} {K : ℕ} {α A : Type} [L.Structure A] [LinearOrder A] (sh : ℕ → Fin K) {n : ℕ} (ψ : (L.sum FirstOrder.Language.order).BoundedFormula α n) (d : ℕ) (hv : α ⊕ Fin n → Fin K) : (evalP sh d hv ψ).Deterministic A

The evaluator is deterministic: it sweeps, it does not guess. This is what lets the same programs serve the deterministic capture.