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

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

Sweeping a head along the order

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.

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.

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_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.

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.