Savitch's midpoint reachability with an explicit stack

Savitch's theorem rests on the midpoint recursion: v is reachable from u within 2 ^ (i + 1) steps exactly when some midpoint is reachable from u and reaches v within 2 ^ i steps each (Relation.RelatesWithinSteps.two_pow_succ_iff). On the words of a fixed width w, Cslib.Reachability.reach is this recursion, with the midpoints enumerated by Cslib.BitString.enumList, and it decides walks of at most 2 ^ i steps along the edges of an edge test (Cslib.Reachability.reach_iff).

Savitch's algorithm runs the recursion on an explicit stack. A frame records a call in progress: its level, its endpoints, the midpoint being tried, which doubles as the counter of the midpoints, and the half being tried. A register holds the pending call or the value just returned. One total step function (Cslib.Reachability.Savitch.step) handles the five cases: a call at level 0 tests for an edge, a call at a higher level pushes a frame, a value returned into either half of a frame moves to the other half, to the next midpoint or out of the frame, and an empty stack holding a value is a fixed point. The midpoints advance by a binary counter of fixed width (Cslib.Reachability.Savitch.next), which visits the words in the order of Cslib.BitString.enumList. A call at level i returns within Cslib.Reachability.Savitch.callSteps w i steps (Cslib.Reachability.Savitch.exists_iterate_step_call), so Cslib.Reachability.Savitch.steps w d = 2 ^ ((w + 2) * (d + 1)) - 1 steps compute the recursion at level d (Cslib.Reachability.savitch_eq).

The time and space of the algorithm on multi-tape machines are in Cslib.Computability.Machines.Turing.MultiTape.Complexity.Space.Reachability.

Main definitions

• Cslib.Reachability.reach: the midpoint recursion.
• Cslib.Reachability.Savitch.next: the binary counter of fixed width.
• Cslib.Reachability.Savitch.Frame, Cslib.Reachability.Savitch.Reg, Cslib.Reachability.Savitch.State, Cslib.Reachability.Savitch.step: the stack machine.
• Cslib.Reachability.Savitch.callSteps, Cslib.Reachability.Savitch.steps: the number of steps of a call, and of the algorithm.
• Cslib.Reachability.savitch: Savitch's algorithm.

Main results

• Cslib.Reachability.reach_iff: the recursion decides walks of at most 2 ^ i steps.
• Cslib.Reachability.Savitch.next_getElem_enumList: the counter visits the words in the order of Cslib.BitString.enumList.
• Cslib.Reachability.Savitch.exists_iterate_step_call: every call returns its value.
• Cslib.Reachability.savitch_eq, Cslib.Reachability.savitch_iff: the algorithm computes the recursion, and decides walks of at most 2 ^ d steps.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.5
• S. Arora and B. Barak, Computational Complexity: A Modern Approach, Section 4.2

Reachability by midpoints

def Cslib.Reachability.reach (edge : List Bool → List Bool → Bool) (w : ℕ) : ℕ → List Bool → List Bool → Bool

Reachability within 2 ^ i steps, by midpoints. At level 0, v is u or one edge away; at level i + 1, some word m of width w is reachable from u and reaches v at level i. This is the recursion of Savitch's theorem Sipser, Theorem 8.5.

theorem Cslib.Reachability.length_eq_of_relatesWithinSteps {edge : List Bool → List Bool → Bool} {w n : ℕ} {u v : List Bool} (hu : u.length = w) (h : Relation.RelatesWithinSteps (fun (a b : List Bool) => a.length = w ∧ b.length = w ∧ edge a b = true) u v n) : v.length = w

A walk along edges between words of width w stays among the words of width w.

theorem Cslib.Reachability.reach_iff {edge : List Bool → List Bool → Bool} {w i : ℕ} {u v : List Bool} (hu : u.length = w) (hv : v.length = w) : reach edge w i u v = true ↔ Relation.RelatesWithinSteps (fun (a b : List Bool) => a.length = w ∧ b.length = w ∧ edge a b = true) u v (2 ^ i)

The midpoint recursion decides walks of at most 2 ^ i steps between words of width w, along the edges given by edge Sipser, Theorem 8.5.

The binary counter

def Cslib.Reachability.Savitch.next : List Bool → Option (List Bool)

The successor of a word in the binary counter of its width, least significant bit first, or none on the word of all ones, where the counter overflows.

theorem Cslib.Reachability.Savitch.next_getElem_enumList (w k : ℕ) (hk : k < (BitString.enumList w).length) : next (BitString.enumList w)[k] = (BitString.enumList w)[k + 1]?

The counter visits the words in the order of Cslib.BitString.enumList: it moves from each word to the next one, and overflows on the last one.

The stack machine

structure Cslib.Reachability.Savitch.Frame : Type

A frame of the stack: the call at level level + 1 from src to dst, while it tries the midpoint mid with two calls at level level.

• level : ℕ

  The level of the two calls on the halves; the frame answers a call at level level + 1.

• src : List Bool

  The source of the call.

• dst : List Bool

  The target of the call.

• mid : List Bool

  The midpoint being tried, which is also the counter of the midpoints tried so far.

• phase : Bool

  false while the first half, from src to mid, is being tried; true while the second half, from mid to dst, is, once the first half has succeeded.

@[instance_reducible]

instance Cslib.Reachability.Savitch.instInhabitedFrame : Inhabited Frame

inductive Cslib.Reachability.Savitch.Reg : Type

The register of the machine: a pending call, or the value of a call that has returned.

• call (level : ℕ) (src dst : List Bool) : Reg

  A call asking whether dst is reachable from src within 2 ^ level steps.

• ret (value : Bool) : Reg

  A call has returned value.

@[instance_reducible]

instance Cslib.Reachability.Savitch.instInhabitedReg : Inhabited Reg

def Cslib.Reachability.Savitch.Reg.answer : Reg → Bool

The answer held by a register: the returned value, or false while a call is pending.

structure Cslib.Reachability.Savitch.State : Type

The state of the machine: the stack of frames, top frame first, and the register.

• stack : List Frame

  The frames of the calls in progress, the innermost first.

• reg : Reg

  The pending call or the returned value.

@[instance_reducible]

instance Cslib.Reachability.Savitch.instInhabitedState : Inhabited State

def Cslib.Reachability.Savitch.step (edge : List Bool → List Bool → Bool) (w : ℕ) : State → State

One step of Savitch's machine, with the edge test edge and midpoints of width w.

• A call at level 0 returns whether v is u or one edge away.
• A call at level i + 1 pushes a frame and calls the first half with the first midpoint, the word of all zeros.
• An empty stack with a returned value is a fixed point: the value is the answer.
• A value true returned into the first half moves the frame to the second half; returned into the second half, the frame returns true.
• A value false returned into either half advances the midpoint by the binary counter; when the counter overflows, every midpoint has failed and the frame returns false.

def Cslib.Reachability.Savitch.callSteps (w : ℕ) : ℕ → ℕ

The number of steps the machine takes for a call at level i, with midpoints of width w: one step to push the frame, and for each of the 2 ^ w midpoints at most two calls at level i, each followed by one step to take its value.

def Cslib.Reachability.Savitch.steps (w d : ℕ) : ℕ

The number of steps Savitch's algorithm runs the machine for: 2 ^ ((w + 2) * (d + 1)) - 1, at least callSteps w d, and written in binary as (w + 2) * (d + 1) ones.

Every call returns its value

theorem Cslib.Reachability.Savitch.exists_iterate_step_call {edge : List Bool → List Bool → Bool} {w : ℕ} (i : ℕ) (u v : List Bool) (stack : List Frame) : ∃ T ≤ callSteps w i, (step edge w)^[T] { stack := stack, reg := Reg.call i u v } = { stack := stack, reg := Reg.ret (reach edge w i u v) }

Every call returns its value: from a call at level i, the machine returns reach edge w i u v to the same stack within callSteps w i steps.

theorem Cslib.Reachability.Savitch.iterate_step_ret_nil {edge : List Bool → List Bool → Bool} {w : ℕ} (b : Bool) (n : ℕ) : (step edge w)^[n] { stack := [], reg := Reg.ret b } = { stack := [], reg := Reg.ret b }

An empty stack with a returned value is a fixed point.

theorem Cslib.Reachability.Savitch.callSteps_add_one_le (w i : ℕ) : callSteps w i + 1 ≤ 2 ^ ((w + 2) * i + 1)

The number of steps of a call at level i is below 2 ^ ((w + 2) * i + 1).

theorem Cslib.Reachability.Savitch.callSteps_le_steps (w d : ℕ) : callSteps w d ≤ steps w d

Savitch's algorithm runs the machine for long enough to return from the call at level d.

Savitch's algorithm

def Cslib.Reachability.savitch (edge : List Bool → List Bool → Bool) (w d : ℕ) (u v : List Bool) : Bool

Savitch's algorithm: run the machine from the call at level d from u to v on the empty stack for Savitch.steps w d steps, and read the answer off the register.

theorem Cslib.Reachability.savitch_eq (edge : List Bool → List Bool → Bool) (w d : ℕ) (u v : List Bool) : savitch edge w d u v = reach edge w d u v

Savitch's machine computes the midpoint recursion.

theorem Cslib.Reachability.savitch_iff {edge : List Bool → List Bool → Bool} {w d : ℕ} {u v : List Bool} (hu : u.length = w) (hv : v.length = w) : savitch edge w d u v = true ↔ Relation.RelatesWithinSteps (fun (a b : List Bool) => a.length = w ∧ b.length = w ∧ edge a b = true) u v (2 ^ d)

Savitch's algorithm decides walks of at most 2 ^ d steps between words of width w Sipser, Theorem 8.5.