Savitch's algorithm in the space of its stack

Savitch's algorithm (Cslib.Reachability.savitch) runs the midpoint recursion on an explicit stack, for Cslib.Reachability.Savitch.steps w d steps. This file bounds its time and space in the quantitative calculus (Turing.MultiTapeTM.ComputableInO), charging every stored frame, counter, returned value and copy.

The states are encoded by framed pairs, options and lists, with the levels in unary (Cslib.Reachability.Savitch.encState). The edge test may depend on a parameter, which a round of the iteration keeps in its state together with the width of the midpoints (Cslib.Reachability.Savitch.roundStep). A round takes time quadratic and space linear in its encoded state, plus the cost of the edge test on the endpoints of a call at level 0 (Cslib.Reachability.Savitch.computableInO_roundStep). Every state of a run from a call at level d holds at most d frames of size O(d + w), so iterating the rounds with a binary counter takes space O((d + 1) * (d + w + 1)), plus the parameter and the space of the edge test on the worst endpoints (Cslib.Reachability.edgeMax), and exponential time (Cslib.Reachability.computableInO_savitch). With an edge test and inputs computable in polynomial time, the space is polynomial (Cslib.Reachability.exists_polyBounded_space_savitch).

Main definitions

• Cslib.Reachability.encArgs, Cslib.Reachability.encEdgeArgs: the encodings of the inputs of Savitch's algorithm and of the edge test.
• Cslib.Reachability.edgeMax: the cost of the edge test on the worst endpoints.
• Cslib.Reachability.Savitch.encFrame, Cslib.Reachability.Savitch.encReg, Cslib.Reachability.Savitch.encState: the encoded states of the machine.
• Cslib.Reachability.Savitch.roundStep, Cslib.Reachability.Savitch.encRound: a step carrying the parameter of the edge test and the width, and its encoding.
• Cslib.Reachability.Savitch.Invariant: the states of a run from a call at a given level.

Main results

• Cslib.Reachability.Savitch.computableInO_roundStep: the time and space of a round.
• Cslib.Reachability.Savitch.invariant_iterate, Cslib.Reachability.Savitch.length_encState_le: the states of a run hold at most d frames, so their encodings have length O((d + 1) * (d + w + 1)).
• Cslib.Reachability.computableInO_savitch: the time and space of Savitch's algorithm.
• Cslib.Reachability.exists_polyBounded_space_savitch: Savitch's algorithm in polynomial space.

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

The inputs and the cost of the edge test

@[reducible, inline]

abbrev Cslib.Reachability.encArgs {π : Type} (encP : π ↪ List Bool) : π × ℕ × ℕ × List Bool × List Bool ↪ List Bool

The encoding of the inputs of Savitch's algorithm: the parameter of the edge test, the width and the depth in unary, and the endpoints.

@[reducible, inline]

abbrev Cslib.Reachability.encEdgeArgs {π : Type} (encP : π ↪ List Bool) : π × List Bool × List Bool ↪ List Bool

The encoding of the inputs (p, u, v) of the edge test: the parameter p, framed, then the endpoints u, framed, and v, as themselves.

def Cslib.Reachability.edgeMax {π : Type} (T : π × List Bool × List Bool → ℕ) (p : π) (w : ℕ) : ℕ

The largest value of T on the parameter p and two words of width w.

theorem Cslib.Reachability.le_edgeMax {π : Type} (T : π × List Bool × List Bool → ℕ) (p : π) {w : ℕ} {u v : List Bool} (hu : u.length = w) (hv : v.length = w) : T (p, u, v) ≤ edgeMax T p w

edgeMax bounds T on all words of width w.

Encodings

def Cslib.Reachability.Savitch.Frame.fields (f : Frame) : ℕ × List Bool × List Bool × List Bool × Bool

The fields of a frame.

@[reducible, inline]

abbrev Cslib.Reachability.Savitch.encFrameFields : ℕ × List Bool × List Bool × List Bool × Bool ↪ List Bool

The encoding of the fields of a frame: the level in unary, the words as themselves.

def Cslib.Reachability.Savitch.encFrame : Frame ↪ List Bool

Frames encoded by their fields.

def Cslib.Reachability.Savitch.Reg.toPair : Reg → Option (ℕ × List Bool × List Bool) × Bool

The register as a pending call, if any, and the returned value, false during a call.

@[reducible, inline]

abbrev Cslib.Reachability.Savitch.encCall : ℕ × List Bool × List Bool ↪ List Bool

The encoding of the arguments of a call: the level in unary, the words as themselves.

def Cslib.Reachability.Savitch.encReg : Reg ↪ List Bool

Registers encoded by Reg.toPair.

def Cslib.Reachability.Savitch.encState : State ↪ List Bool

States encoded as the list of their frames followed by their register.

The step in linear time, apart from the edge test

def Cslib.Reachability.Savitch.allT : Turing.MultiTapeTM.Transducer Bool Bool

The transducer testing whether all bits are ones.

@[simp]

theorem Cslib.Reachability.Savitch.allT_step (a b : Bool) : allT.step a b = (a && b, [])

@[simp]

theorem Cslib.Reachability.Savitch.allT_final (a : Bool) : allT.final a = [a]

@[simp]

theorem Cslib.Reachability.Savitch.allT_q₀ : allT.q₀ = true

theorem Cslib.Reachability.Savitch.allT_run (a : Bool) (u : List Bool) : allT.run a u = [a && u.all id]

The transducer allT tests whether all bits are ones.

Sizes of encoded states

theorem Cslib.Reachability.Savitch.length_encFrame (f : Frame) : (encFrame f).length = 2 * f.level + 2 * f.src.length + 2 * f.dst.length + 2 * f.mid.length + 5

The length of an encoded frame.

theorem Cslib.Reachability.Savitch.length_encReg_call (i : ℕ) (u v : List Bool) : (encReg (Reg.call i u v)).length = 4 * i + 4 * u.length + 2 * v.length + 8

The length of an encoded pending call.

theorem Cslib.Reachability.Savitch.length_encReg_ret (b : Bool) : (encReg (Reg.ret b)).length = 2

The length of an encoded returned value.

theorem Cslib.Reachability.Savitch.length_encState (s : State) : (encState s).length = 2 * ((Turing.MultiTapeTM.encList encFrame) s.stack).length + 1 + (encReg s.reg).length

The length of an encoded state.

A step carrying the parameter of the edge test

def Cslib.Reachability.Savitch.roundStep {π : Type} (edge : π → List Bool → List Bool → Bool) (q : (π × ℕ) × State) : (π × ℕ) × State

A round of the iteration of Savitch's algorithm: a step of the machine for the edge test edge q.1.1 and the width q.1.2, keeping both.

@[reducible, inline]

abbrev Cslib.Reachability.Savitch.encRound {π : Type} (encP : π ↪ List Bool) : (π × ℕ) × State ↪ List Bool

The encoding of the states of the iteration, with the width in unary.

def Cslib.Reachability.Savitch.Reg.edgeCost {π : Type} (T : π × List Bool × List Bool → ℕ) (p : π) : Reg → ℕ

The cost T of the edge test, with the parameter p, on the endpoints of the pending call, if any.

theorem Cslib.Reachability.Savitch.computableInO_roundStep {π : Type} {encP : π ↪ List Bool} {edge : π → List Bool → List Bool → Bool} {Te Se : π × List Bool × List Bool → ℕ} (hedge : Turing.MultiTapeTM.ComputableInO (fun (q : π × List Bool × List Bool) => edge q.1 q.2.1 q.2.2) (encEdgeArgs encP) Turing.MultiTapeTM.encBool Te Se) : Turing.MultiTapeTM.ComputableInO (roundStep edge) (encRound encP) (encRound encP) (fun (q : (π × ℕ) × State) => (((encRound encP) q).length + 1) ^ 2 + Reg.edgeCost Te q.1.1 q.2.reg) fun (q : (π × ℕ) × State) => ((encRound encP) q).length + Reg.edgeCost Se q.1.1 q.2.reg

A round within the time and space of the edge test, plus quadratic time and linear space. A call at level 0 compares its endpoints, in quadratic time, and runs the edge test on them; the other cases copy and rearrange the encoded state, in linear time.

The states of a run

theorem Cslib.Reachability.Savitch.roundStep_iterate {π : Type} (edge : π → List Bool → List Bool → Bool) (p : π) (w : ℕ) (s : State) (k : ℕ) : (roundStep edge)^[k] ((p, w), s) = ((p, w), (step (edge p) w)^[k] s)

The rounds keep the parameter and the width, and run the machine.

def Cslib.Reachability.Savitch.StackOk (w d : ℕ) : List Frame → Prop

The frames of a run from a call at level d with words of width w: a frame with n frames below it is at a level below d - n, and its words have width w.

def Cslib.Reachability.Savitch.Invariant (w d : ℕ) (s : State) : Prop

The states of a run from a call at level d with words of width w.

theorem Cslib.Reachability.Savitch.invariant_step (edge : List Bool → List Bool → Bool) {w d : ℕ} {s : State} (h : Invariant w d s) : Invariant w d (step edge w s)

The step keeps the invariant of a run.

theorem Cslib.Reachability.Savitch.invariant_iterate (edge : List Bool → List Bool → Bool) {w d : ℕ} {s : State} (h : Invariant w d s) (k : ℕ) : Invariant w d ((step edge w)^[k] s)

Every state of a run keeps the invariant.

theorem Cslib.Reachability.Savitch.StackOk.length_le {w d : ℕ} {stack : List Frame} : StackOk w d stack → stack.length ≤ d

A run from a call at level d holds at most d frames.

theorem Cslib.Reachability.Savitch.StackOk.mem {w d : ℕ} {stack : List Frame} : StackOk w d stack → ∀ f ∈ stack, f.level < d ∧ f.src.length = w ∧ f.dst.length = w ∧ f.mid.length = w

The frames of a run from a call at level d are below level d, with words of width w.

theorem Cslib.Reachability.Savitch.length_encState_le {w d : ℕ} {s : State} (h : Invariant w d s) : (encState s).length ≤ 24 * (d + 1) * (d + w + 1)

The states of a run from a call at level d, with words of width w, are of size O((d + 1) * (d + w + 1)): at most d frames of size O(d + w), and a call of size O(d + w).

The number of rounds, in binary

The first round and the answer

Savitch's algorithm in the space of its stack

theorem Cslib.Reachability.computableInO_savitch {π : Type} {encP : π ↪ List Bool} {γ : Type} {encIn : γ ↪ List Bool} {edge : π → List Bool → List Bool → Bool} {Te Se : π × List Bool × List Bool → ℕ} (hedge : Turing.MultiTapeTM.ComputableInO (fun (q : π × List Bool × List Bool) => edge q.1 q.2.1 q.2.2) (encEdgeArgs encP) Turing.MultiTapeTM.encBool Te Se) {par : γ → π} {width depth : γ → ℕ} {src dst : γ → List Bool} {Tin Sin : γ → ℕ} (hin : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => (par x, width x, depth x, src x, dst x)) encIn (encArgs encP) Tin Sin) (hsrc : ∀ (x : γ), (src x).length = width x) (hdst : ∀ (x : γ), (dst x).length = width x) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => savitch (edge (par x)) (width x) (depth x) (src x) (dst x)) encIn Turing.MultiTapeTM.encBool (fun (x : γ) => Tin x + 2 ^ ((width x + 2) * (depth x + 1)) * (((depth x + 1) * (depth x + width x + 1) + (encP (par x)).length + 1) ^ 2 + edgeMax Te (par x) (width x))) fun (x : γ) => Sin x + (depth x + 1) * (depth x + width x + 1) + (encP (par x)).length + edgeMax Se (par x) (width x)

Savitch's algorithm in the space of its stack. If the edge test is computable with time Te and space Se, and the parameter, the width and depth in unary, and endpoints of width w are computable from x with time Tin and space Sin, then Savitch's algorithm is computable within space O(Sin + (d + 1) * (d + w + 1) + |par| + edgeMax Se) and exponential time.

theorem Cslib.Reachability.exists_polyBounded_space_savitch {π : Type} {encP : π ↪ List Bool} {γ : Type} {encIn : γ ↪ List Bool} {edge : π → List Bool → List Bool → Bool} (hedge : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : π × List Bool × List Bool) => edge q.1 q.2.1 q.2.2) (encEdgeArgs encP) Turing.MultiTapeTM.encBool) {par : γ → π} {width depth : γ → ℕ} {src dst : γ → List Bool} (hin : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => (par x, width x, depth x, src x, dst x)) encIn (encArgs encP)) (hsrc : ∀ (x : γ), (src x).length = width x) (hdst : ∀ (x : γ), (dst x).length = width x) : ∃ (t : γ → ℕ) (s : γ → ℕ), Turing.MultiTapeTM.PolyBounded (fun (x : γ) => (encIn x).length) s ∧ Turing.MultiTapeTM.ComputableInTimeAndSpace (fun (x : γ) => savitch (edge (par x)) (width x) (depth x) (src x) (dst x)) encIn Turing.MultiTapeTM.encBool t s

Savitch's algorithm in polynomial space. If the edge test is computable in polynomial time, and the parameter, the width and depth in unary, and endpoints of width w are computable from x in polynomial time, then Savitch's algorithm is computable within space polynomial in the length of the encoded input; the time is exponential, see Cslib.Reachability.computableInO_savitch. The width and the depth are polynomial since they are computed in unary Sipser, Theorem 8.5.