Midpoint formulas

Reachability in 2 ^ i steps is expressed by a quantified Boolean formula of size linear in i, by the midpoint recursion of Savitch's theorem with a universal quantifier folding the two halves into one copy of the formula of the level below Sipser, Theorem 8.9 Arora and Barak, Theorem 4.13: Φ_{i+1}(a, b) = ∃ m, ∀ x y, ((x = a ∧ y = m) ∨ (x = m ∧ y = b)) → Φ_i(x, y).

The words are held by blocks of w variables (Cslib.Complexity.TQBF.blockVars): at level i the source, the target and the midpoint blocks, numbered by even numbers (Cslib.Complexity.TQBF.blockVar), so that the odd numbers are free for the formula of level 0. Given a formula of level 0 whose value is that of Cslib.Reachability.reach e w 0 on the words held by the source and target blocks of level 0, the midpoint formula of level i (Cslib.Complexity.TQBF.midpoint) has, under every assignment, the value of Cslib.Reachability.reach e w i on the words held by the blocks of level i (Cslib.Complexity.TQBF.eval_midpoint). Fixing the blocks of level d to two words of width w gives a closed formula (Cslib.Complexity.TQBF.savitchFormula) whose value is Cslib.Reachability.reach e w d u v (Cslib.Complexity.TQBF.eval_savitchFormula), as soon as the free variables of the formula of level 0 lie in its two blocks (Cslib.Complexity.TQBF.closed_savitchFormula).

The formulas use the derived connectives of Cslib.Logic.PL.QBF: blocks of quantifiers (Cslib.Logic.PL.QBF.exs, Cslib.Logic.PL.QBF.alls), conjunctions of lists (Cslib.Logic.PL.QBF.conj), implication, equivalence, literals, and formulas in conjunctive normal form (Cslib.Logic.PL.QBF.ofCNF). Their tokens are given here explicitly (Cslib.Logic.PL.QBF.tokens_exs, …), for the polynomial-time construction of the formulas.

Main definitions

• Cslib.Complexity.TQBF.blockVar, Cslib.Complexity.TQBF.blockVars: the variables of the blocks.
• Cslib.Complexity.TQBF.midpoint, Cslib.Complexity.TQBF.savitchFormula: the midpoint formulas.

Main results

• Cslib.Logic.PL.QBF.tokens_exs, Cslib.Logic.PL.QBF.tokens_alls, Cslib.Logic.PL.QBF.tokens_ofCNF, …: the tokens of the derived connectives.
• Cslib.Complexity.TQBF.eval_midpoint, Cslib.Complexity.TQBF.eval_savitchFormula: the midpoint formulas express reachability by midpoints.
• Cslib.Complexity.TQBF.closed_savitchFormula: they are closed.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.9
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Theorem 4.13

Tokens of the derived connectives

theorem Cslib.Logic.PL.QBF.tokens_exs (vs : List ℕ) (φ : QBF ℕ) : (exs vs φ).tokens = List.map (fun (v : ℕ) => (Kind.ex, v)) vs ++ φ.tokens

theorem Cslib.Logic.PL.QBF.tokens_alls (vs : List ℕ) (φ : QBF ℕ) : (alls vs φ).tokens = List.map (fun (v : ℕ) => (Kind.all, v)) vs ++ φ.tokens

theorem Cslib.Logic.PL.QBF.tokens_conj (l : List (QBF ℕ)) : (conj l).tokens = List.flatMap (fun (φ : QBF ℕ) => (Kind.and, 0) :: φ.tokens) l ++ [(Kind.top, 0)]

theorem Cslib.Logic.PL.QBF.tokens_iff (φ ψ : QBF ℕ) : (φ.iff ψ).tokens = (Kind.or, 0) :: (Kind.and, 0) :: (φ.tokens ++ ψ.tokens ++ (Kind.and, 0) :: (Kind.not, 0) :: (φ.tokens ++ (Kind.not, 0) :: ψ.tokens))

theorem Cslib.Logic.PL.QBF.tokens_lit (v : ℕ) (b : Bool) : (lit v b).tokens = if b = true then [(Kind.var, v)] else [(Kind.not, 0), (Kind.var, v)]

theorem Cslib.Logic.PL.QBF.tokens_ofCNF (φ : CNF ℕ) : (ofCNF φ).tokens = List.flatMap (fun (c : Clause ℕ) => (Kind.and, 0) :: (List.flatMap (fun (l : Literal ℕ) => (Kind.or, 0) :: (lit l.1 l.2).tokens) c ++ [(Kind.bot, 0)])) φ ++ [(Kind.top, 0)]

Blocks of variables

def Cslib.Complexity.TQBF.blockVar (kind i j : ℕ) : ℕ

The j-th variable of the source (kind = 0), target (kind = 1) or midpoint (kind = 2) block of level i. The variables of the blocks are even.

def Cslib.Complexity.TQBF.blockVars (w kind i : ℕ) : List ℕ

The variables of the block kind of level i, for words of width w.

def Cslib.Complexity.TQBF.block (σ : ℕ → Bool) (w kind i : ℕ) : List Bool

The word held by a block under an assignment.

theorem Cslib.Complexity.TQBF.length_block (σ : ℕ → Bool) (w kind i : ℕ) : (block σ w kind i).length = w

theorem Cslib.Complexity.TQBF.blockVar_mod_two (kind i j : ℕ) : blockVar kind i j % 2 = 0

Block variables are even.

theorem Cslib.Complexity.TQBF.blockVar_inj {k k' i i' j j' : ℕ} (hk : k < 3) (hk' : k' < 3) (h : blockVar k i j = blockVar k' i' j') : k = k' ∧ i = i' ∧ j = j'

theorem Cslib.Complexity.TQBF.nodup_blockVars_append (w i : ℕ) : (blockVars w 0 i ++ blockVars w 1 i).Nodup

The source and target blocks of a level are disjoint.

Formulas on blocks

def Cslib.Complexity.TQBF.eqBlock (w k i k' i' : ℕ) : Logic.PL.QBF ℕ

The block k of level i holds the same word as the block k' of level i'.

def Cslib.Complexity.TQBF.isBlock (w k i : ℕ) (u : List Bool) : Logic.PL.QBF ℕ

The block k of level i holds the word u.

theorem Cslib.Complexity.TQBF.eval_eqBlock (σ : ℕ → Bool) (w k i k' i' : ℕ) : Logic.PL.QBF.eval σ (eqBlock w k i k' i') = decide (block σ w k i = block σ w k' i')

theorem Cslib.Complexity.TQBF.mem_freeVars_eqBlock {w k i k' i' x : ℕ} (hx : x ∈ (eqBlock w k i k' i').freeVars) : x ∈ blockVars w k i ∨ x ∈ blockVars w k' i'

The midpoint formulas

def Cslib.Complexity.TQBF.halves (w i : ℕ) : Logic.PL.QBF ℕ

The hypothesis of level i + 1: the source and target blocks of level i hold the source of level i + 1 and the midpoint, or the midpoint and the target of level i + 1.

def Cslib.Complexity.TQBF.midpoint (w : ℕ) (base : Logic.PL.QBF ℕ) : ℕ → Logic.PL.QBF ℕ

The midpoint formula of level i: the formula base at level 0, and at level i + 1, some midpoint such that, for all words held by the source and target blocks of level i that form one of the two halves, the formula of level i holds.

theorem Cslib.Complexity.TQBF.eval_midpoint {e : List Bool → List Bool → Bool} {w : ℕ} {base : Logic.PL.QBF ℕ} (hbase : ∀ (σ : ℕ → Bool), Logic.PL.QBF.eval σ base = Reachability.reach e w 0 (block σ w 0 0) (block σ w 1 0)) (i : ℕ) (σ : ℕ → Bool) : Logic.PL.QBF.eval σ (midpoint w base i) = Reachability.reach e w i (block σ w 0 i) (block σ w 1 i)

The midpoint formulas express reachability by midpoints. If, under every assignment, the formula of level 0 has the value of reach e w 0 on the words held by the source and target blocks of level 0, then so does the formula of every level i, with reach e w i.

def Cslib.Complexity.TQBF.savitchFormula (w d : ℕ) (base : Logic.PL.QBF ℕ) (u v : List Bool) : Logic.PL.QBF ℕ

Savitch's formula: the midpoint formula of level d, with its source and target blocks fixed to the words u and v.

theorem Cslib.Complexity.TQBF.eval_savitchFormula {e : List Bool → List Bool → Bool} {w : ℕ} {base : Logic.PL.QBF ℕ} (hbase : ∀ (σ : ℕ → Bool), Logic.PL.QBF.eval σ base = Reachability.reach e w 0 (block σ w 0 0) (block σ w 1 0)) (d : ℕ) {u v : List Bool} (hu : u.length = w) (hv : v.length = w) (σ : ℕ → Bool) : Logic.PL.QBF.eval σ (savitchFormula w d base u v) = Reachability.reach e w d u v

Savitch's formula expresses reachability by midpoints, for words of width w.

theorem Cslib.Complexity.TQBF.closed_savitchFormula {w : ℕ} {base : Logic.PL.QBF ℕ} (hbase : ∀ x ∈ base.freeVars, x ∈ blockVars w 0 0 ∨ x ∈ blockVars w 1 0) (d : ℕ) (u v : List Bool) : (savitchFormula w d base u v).Closed

Savitch's formula is closed, as soon as the free variables of the formula of level 0 lie in the source and target blocks of level 0.

Tokens of the midpoint formulas

def Cslib.Complexity.TQBF.iffTokens (x y : ℕ) : List (Logic.PL.QBF.Kind × ℕ)

The tokens of an equivalence of two variables.

theorem Cslib.Complexity.TQBF.tokens_eqBlock (w k i k' i' : ℕ) : (eqBlock w k i k' i').tokens = List.flatMap (fun (j : ℕ) => (Logic.PL.QBF.Kind.and, 0) :: iffTokens (blockVar k i j) (blockVar k' i' j)) (List.range w) ++ [(Logic.PL.QBF.Kind.top, 0)]

theorem Cslib.Complexity.TQBF.tokens_isBlock (w k i : ℕ) (u : List Bool) : (isBlock w k i u).tokens = List.flatMap (fun (j : ℕ) => (Logic.PL.QBF.Kind.and, 0) :: (Logic.PL.QBF.lit (blockVar k i j) (u.getD j false)).tokens) (List.range w) ++ [(Logic.PL.QBF.Kind.top, 0)]

def Cslib.Complexity.TQBF.levelTokens (w i : ℕ) : List (Logic.PL.QBF.Kind × ℕ)

The tokens the level i + 1 adds in front of the midpoint formula of level i.

theorem Cslib.Complexity.TQBF.tokens_midpoint (w : ℕ) (base : Logic.PL.QBF ℕ) (d : ℕ) : (midpoint w base d).tokens = List.flatMap (levelTokens w) (List.range d).reverse ++ base.tokens

The tokens of the midpoint formula of level d: the levels from d down to 1, then the formula of level 0.