Savitch's recursive doubling

The combinatorial half of Savitch's theorem (Savitch 1970), stated for an arbitrary relation and independent of any logic: reachability in a graph whose vertices are only known up to a classifying map into a finite type.

The setting is a relation R on a type St of presentations, together with a map cls : St → T into a finite type of classes, such that R only depends on its endpoints through their classes (DescriptiveComplexity.SavInv). That extra generality is what the reduction of SUCCINCT-REACH to QSAT needs: a state of a succinctly described transition system is a predicate on the whole universe, but the clauses only read it on the state variables, so the honest vertex set is the (finite) quotient.

Three notions of bounded reachability live here:

• DescriptiveComplexity.SavStep: one move – a step of R, or standing still inside a class;
• DescriptiveComplexity.SavLe n: at most n moves, the linear staging;
• DescriptiveComplexity.SavPow k: Savitch's staging, ψ_{k+1}(X, Y) = ∃Z, ψ_k(X, Z) ∧ ψ_k(Z, Y), which unfolds into a formula of depth k rather than length 2 ^ k.

The two stagings agree, DescriptiveComplexity.savPow_iff_savLe : SavPow k = SavLe (2 ^ k), and the pigeonhole DescriptiveComplexity.savLe_card says that SavLe saturates at Nat.card T moves – a walk that revisits a class can be shortened. Together they give the statement a reduction uses, DescriptiveComplexity.savPow_of_reflTransGen: as soon as 2 ^ k classes are enough, SavPow k is reachability.

Moves, and the two stagings

def DescriptiveComplexity.SavStep {St T : Type} (cls : St → T) (R : St → St → Prop) (X Y : St) : Prop

One move of the walk: a step of R, or standing still inside a class. The reflexive part is cls-equality rather than equality because a class, not a presentation, is what the walk really visits.

Equations

• DescriptiveComplexity.SavStep cls R X Y = (cls X = cls Y ∨ R X Y)

def DescriptiveComplexity.SavLe {St T : Type} (cls : St → T) (R : St → St → Prop) : ℕ → St → St → Prop

Reachability in at most n moves: the linear staging.

Equations

• DescriptiveComplexity.SavLe cls R 0 = fun (X Y : St) => cls X = cls Y
• DescriptiveComplexity.SavLe cls R n.succ = fun (X Y : St) => ∃ (Z : St), DescriptiveComplexity.SavLe cls R n X Z ∧ DescriptiveComplexity.SavStep cls R Z Y

def DescriptiveComplexity.SavPow {St T : Type} (cls : St → T) (R : St → St → Prop) : ℕ → St → St → Prop

Savitch's staging: SavPow k is “reachable through a midpoint, twice at level k - 1”, which is reachability in at most 2 ^ k moves (DescriptiveComplexity.savPow_iff_savLe) written with k nested midpoints.

Equations

• DescriptiveComplexity.SavPow cls R 0 = DescriptiveComplexity.SavStep cls R
• DescriptiveComplexity.SavPow cls R n.succ = fun (X Y : St) => ∃ (Z : St), DescriptiveComplexity.SavPow cls R n X Z ∧ DescriptiveComplexity.SavPow cls R n Z Y

def DescriptiveComplexity.SavInv {St T : Type} (cls : St → T) (R : St → St → Prop) : Prop

The walk only depends on its endpoints through their classes: the hypothesis that makes the classes, rather than the presentations, the vertices.

Equations

• DescriptiveComplexity.SavInv cls R = ∀ (X X' Y Y' : St), cls X = cls X' → cls Y = cls Y' → R X Y → R X' Y'

Class-invariance of the stagings

theorem DescriptiveComplexity.savStep_congr {St T : Type} {cls : St → T} {R : St → St → Prop} (h : SavInv cls R) {X X' Y Y' : St} (hX : cls X = cls X') (hY : cls Y = cls Y') (hs : SavStep cls R X Y) : SavStep cls R X' Y'

theorem DescriptiveComplexity.savLe_congr {St T : Type} {cls : St → T} {R : St → St → Prop} (h : SavInv cls R) (n : ℕ) {X X' Y Y' : St} : cls X = cls X' → cls Y = cls Y' → SavLe cls R n X Y → SavLe cls R n X' Y'

theorem DescriptiveComplexity.savPow_congr {St T : Type} {cls : St → T} {R : St → St → Prop} (h : SavInv cls R) (k : ℕ) {X X' Y Y' : St} : cls X = cls X' → cls Y = cls Y' → SavPow cls R k X Y → SavPow cls R k X' Y'

The linear staging

theorem DescriptiveComplexity.savLe_succ {St T : Type} {cls : St → T} {R : St → St → Prop} {n : ℕ} {X Y : St} (hs : SavLe cls R n X Y) : SavLe cls R (n + 1) X Y

theorem DescriptiveComplexity.savLe_of_le {St T : Type} {cls : St → T} {R : St → St → Prop} {m n : ℕ} (hmn : m ≤ n) {X Y : St} (hs : SavLe cls R m X Y) : SavLe cls R n X Y

theorem DescriptiveComplexity.savLe_of_savStep {St T : Type} {cls : St → T} {R : St → St → Prop} {X Y : St} (hs : SavStep cls R X Y) : SavLe cls R 1 X Y

theorem DescriptiveComplexity.savLe_add {St T : Type} {cls : St → T} {R : St → St → Prop} (h : SavInv cls R) (a b : ℕ) {X Y : St} : SavLe cls R (a + b) X Y ↔ ∃ (Z : St), SavLe cls R a X Z ∧ SavLe cls R b Z Y

The linear staging composes: walking a + b moves is walking a and then b.

The two stagings agree

theorem DescriptiveComplexity.savPow_iff_savLe {St T : Type} {cls : St → T} {R : St → St → Prop} (h : SavInv cls R) (k : ℕ) {X Y : St} : SavPow cls R k X Y ↔ SavLe cls R (2 ^ k) X Y

Savitch's staging is the linear one at 2 ^ k: k nested midpoints describe a walk of exponentially many moves.

Reachability, and the pigeonhole

theorem DescriptiveComplexity.exists_savLe_of_reflTransGen {St T : Type} {cls : St → T} {R : St → St → Prop} {X Y : St} (hr : Relation.ReflTransGen R X Y) : ∃ (n : ℕ), SavLe cls R n X Y

theorem DescriptiveComplexity.reflTransGen_of_savLe {St T : Type} {cls : St → T} {R : St → St → Prop} (h : SavInv cls R) (n : ℕ) {X Y : St} : SavLe cls R n X Y → ∃ (Y' : St), cls Y' = cls Y ∧ Relation.ReflTransGen R X Y'

A bounded walk is a genuine walk, up to the class of its endpoint.

theorem DescriptiveComplexity.savLe_card {St T : Type} {cls : St → T} {R : St → St → Prop} [Finite T] (h : SavInv cls R) (X : St) (n : ℕ) {Y : St} : SavLe cls R n X Y → SavLe cls R (Nat.card T) X Y

The pigeonhole: a walk saturates after as many moves as there are classes. The set of classes reached in at most n moves grows with n, and as soon as it stops growing it stops growing for good, so it is stable by the time n reaches Nat.card T.

theorem DescriptiveComplexity.savPow_of_reflTransGen {St T : Type} {cls : St → T} {R : St → St → Prop} [Finite T] (h : SavInv cls R) {k : ℕ} (hk : Nat.card T ≤ 2 ^ k) {X Y : St} (hr : Relation.ReflTransGen R X Y) : SavPow cls R k X Y

Savitch's staging computes reachability, as soon as it is deep enough for the number of classes.