Evaluating a quantifier prefix by one monotone sweep

The machine-free half of the sweep, and the reason a nondeterministic wide machine can evaluate a first-order kernel at all: an alternating quantifier prefix over a linearly ordered universe is the fold of its matrix along the lexicographic enumeration of its valuations.

DescriptiveComplexity.altQuantFrom (Exponential.AltQuant) is the prefix, with the state a machine would carry – a level j and a valuation v. What a machine sweeping the valuations in order actually holds at each moment is not that value but a partial one:

DescriptiveComplexity.foldFrom pol P le j v is the value of the subtree at level j, with the coordinates below j fixed to those of v, computed over the leaves up to v and no further.

Four facts make it a sweep, and together they are what a program's correctness proof will discharge.

fact	theorem
at the last level the accumulator is the matrix	DescriptiveComplexity.foldFrom_last
at the first valuation it is the matrix	DescriptiveComplexity.foldFrom_bot
at the last valuation it is the whole prefix	DescriptiveComplexity.foldFrom_top
across one step it folds	foldFrom_above, foldFrom_carry, foldFrom_below

The step splits by comparison with the carry level c – the last coordinate that is not maximal, which the enumeration increments. Above c nothing changes but the deeper accumulator; at c the accumulator absorbs the subtree just completed and takes in the new leaf; below c the accumulators reset to the new leaf. That is one ∨ (or ∧) per level and one matrix evaluation per step – k bits of control and no addressing, which is the whole point.

Everything is stated at an arbitrary order relation on the values, and the successor is a hypothesis (∀ a, WMLt le a b' ↔ le a b) rather than a construction, so this file is independent of the address layer; it is DescriptiveComplexity.wmSetLt_iff_of_wmIncr that supplies the hypothesis when the values are addresses.

The partial value of a prefix

def DescriptiveComplexity.foldAux {A : Type} {n : ℕ} (pol : ℕ → Bool) (P : (Fin n → A) → Prop) (le : A → A → Prop) : ℕ → ℕ → (Fin n → A) → Prop

The recursion of DescriptiveComplexity.foldFrom, with the same explicit fuel as DescriptiveComplexity.altQuantAux: the number of levels left.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.foldAux pol P le 0 x✝¹ x✝ = P x✝

def DescriptiveComplexity.foldFrom {A : Type} {n : ℕ} (pol : ℕ → Bool) (P : (Fin n → A) → Prop) (le : A → A → Prop) (j : ℕ) (v : Fin n → A) : Prop

The partial value of a prefix: the value of the subtree at level j, with the coordinates below j read off v, computed over the valuations up to v in the lexicographic order and no further. This is what a machine sweeping the valuations holds in its control.

Equations

• DescriptiveComplexity.foldFrom pol P le j v = DescriptiveComplexity.foldAux pol P le (n - j) j v

theorem DescriptiveComplexity.foldFrom_of_le {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {j : ℕ} (h : n ≤ j) (v : Fin n → A) : foldFrom pol P le j v = P v

Past the last level the accumulator is the matrix.

theorem DescriptiveComplexity.foldFrom_last {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} (v : Fin n → A) : foldFrom pol P le n v = P v

At the last level the accumulator is the matrix.

theorem DescriptiveComplexity.foldFrom_ex {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {j : ℕ} (h : j < n) (hp : pol j = true) (v : Fin n → A) : foldFrom pol P le j v ↔ (∃ (a : A), WMLt le a (v ⟨j, h⟩) ∧ altQuantFrom pol P (j + 1) (Function.update v ⟨j, h⟩ a)) ∨ foldFrom pol P le (j + 1) v

One existential level of the accumulator.

theorem DescriptiveComplexity.foldFrom_all {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {j : ℕ} (h : j < n) (hp : pol j = false) (v : Fin n → A) : foldFrom pol P le j v ↔ (∀ (a : A), WMLt le a (v ⟨j, h⟩) → altQuantFrom pol P (j + 1) (Function.update v ⟨j, h⟩ a)) ∧ foldFrom pol P le (j + 1) v

One universal level of the accumulator.

The two ends of the enumeration

theorem DescriptiveComplexity.foldFrom_bot {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v : Fin n → A} {j₀ : ℕ} (hbot : ∀ (i : Fin n), j₀ ≤ ↑i → ∀ (a : A), le (v i) a) {j : ℕ} (hj : j₀ ≤ j) : foldFrom pol P le j v ↔ P v

At the first valuation the accumulator is the matrix, at every level: no leaf before it has been seen, so nothing has been accumulated yet.

theorem DescriptiveComplexity.foldFrom_top {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v : Fin n → A} {j₀ : ℕ} (h : IsLinOrd le) (htop : ∀ (i : Fin n), j₀ ≤ ↑i → ∀ (a : A), le a (v i)) {j : ℕ} (hj : j₀ ≤ j) : foldFrom pol P le j v ↔ altQuantFrom pol P j v

At the last valuation the accumulator is the whole prefix: every leaf has been seen, so the sweep has finished computing the value of the subtree. This is the half that reads the answer off the machine when it reaches the end of its tape.

One step of the enumeration

The three rules a program's step obligation splits into, by comparison with the carry level – the last coordinate the enumeration increments.

theorem DescriptiveComplexity.levelEx_congr {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v v' : Fin n → A} {j : ℕ} (hj : j < n) (hagree : ∀ (i : Fin n), ↑i ≤ j → v i = v' i) : (∃ (a : A), WMLt le a (v ⟨j, hj⟩) ∧ altQuantFrom pol P (j + 1) (Function.update v ⟨j, hj⟩ a)) ↔ ∃ (a : A), WMLt le a (v' ⟨j, hj⟩) ∧ altQuantFrom pol P (j + 1) (Function.update v' ⟨j, hj⟩ a)

The contribution of a level to its accumulator depends only on the coordinates up to that level, so above the carry it does not change.

theorem DescriptiveComplexity.levelAll_congr {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v v' : Fin n → A} {j : ℕ} (hj : j < n) (hagree : ∀ (i : Fin n), ↑i ≤ j → v i = v' i) : (∀ (a : A), WMLt le a (v ⟨j, hj⟩) → altQuantFrom pol P (j + 1) (Function.update v ⟨j, hj⟩ a)) ↔ ∀ (a : A), WMLt le a (v' ⟨j, hj⟩) → altQuantFrom pol P (j + 1) (Function.update v' ⟨j, hj⟩ a)

The universal reading of DescriptiveComplexity.levelEx_congr.

theorem DescriptiveComplexity.foldFrom_above {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v v' : Fin n → A} {j : ℕ} (hj : j < n) (hagree : ∀ (i : Fin n), ↑i ≤ j → v i = v' i) : foldFrom pol P le j v' ↔ if pol j = true then (∃ (a : A), WMLt le a (v ⟨j, hj⟩) ∧ altQuantFrom pol P (j + 1) (Function.update v ⟨j, hj⟩ a)) ∨ foldFrom pol P le (j + 1) v' else (∀ (a : A), WMLt le a (v ⟨j, hj⟩) → altQuantFrom pol P (j + 1) (Function.update v ⟨j, hj⟩ a)) ∧ foldFrom pol P le (j + 1) v'

Above the carry the accumulator only changes through the deeper one: the level's own contribution is untouched, because the coordinates up to it are.

theorem DescriptiveComplexity.foldFrom_carry {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v v' : Fin n → A} {c : ℕ} (h : IsLinOrd le) (hc : c < n) (hagree : ∀ (i : Fin n), ↑i < c → v i = v' i) (htop : ∀ (i : Fin n), c < ↑i → ∀ (a : A), le a (v i)) (hsucc : ∀ (a : A), WMLt le a (v' ⟨c, hc⟩) ↔ le a (v ⟨c, hc⟩)) : foldFrom pol P le c v' ↔ if pol c = true then foldFrom pol P le c v ∨ foldFrom pol P le (c + 1) v' else foldFrom pol P le c v ∧ foldFrom pol P le (c + 1) v'

At the carry level the accumulator absorbs the subtree just completed. The new accumulator is the old one – which, every deeper coordinate having been maximal, was the whole subtree up to and including the old value – combined with the accumulator one level deeper, which by DescriptiveComplexity.foldFrom_bot is the new leaf. This is the fold, and the only place the successor is used.

theorem DescriptiveComplexity.foldFrom_below {A : Type} {n : ℕ} {pol : ℕ → Bool} {P : (Fin n → A) → Prop} {le : A → A → Prop} {v' : Fin n → A} {c j : ℕ} (hbot : ∀ (i : Fin n), c < ↑i → ∀ (a : A), le (v' i) a) (hj : c < j) : foldFrom pol P le j v' ↔ P v'

Below the carry the accumulators reset to the new leaf, by DescriptiveComplexity.foldFrom_bot: every coordinate below the carry is minimal in the incremented valuation.