Evaluating Reingold's rotation maps in place

The rotation map of the ℓ-th graph G_ℓ of Reingold's transformation can be evaluated with a constant number of labels of extra memory per level, as in the proof of Reingold, Lemma 3.4. Reingold's step takes the eighth power of G ⓩ H and keeps sixteen labels of H in a label of G_ℓ; the step here takes the square and keeps four. A vertex of G_m is a vertex v of G followed by m labels r₀, …, r_{m-1} (Cslib.RotationMap.ReingoldVertex.toList), and its rotation along a label a changes these registers in place: a step of G_m = ((G_{m-1} ⓩ H) ^ 2).relabel e.symm is a step of H from the label r_{m-1}, a recursive rotation of G_{m-1}, and a step of H, twice, and the four labels of H it uses and produces are stored in a itself, which a fixed permutation of these four labels finally turns into the label at the far end (reingoldStep_rot).

Cslib.RotationMap.reingoldEvalStep runs this recursion with an explicit stack. A state holds the vertex v of G, the labels r_{m-1}, …, r₀ below the current level, and a stack of frames, one per level being evaluated, each with a program counter (Cslib.RotationMap.ReingoldPc) and its own label; the level of the top frame is the number of labels below it. Every step is a step of H on two labels, a push or a pop, or a step of G on the vertex and the lowest label, so the memory is the vertex of G and O(1) labels and a program counter for each of the ℓ levels. From a frame for level m at the top, the evaluation reaches the rotated registers and the label at the far end, the frame popped (exists_iterate_reingoldEvalStep).

Main definitions

• Cslib.RotationMap.ReingoldVertex.toList: the vertex of G and the labels of a vertex of G_m.
• Cslib.RotationMap.reingoldHStep, Cslib.RotationMap.reingoldFinish: the steps of H and the final permutation of a step of the transformation, on the labels.
• Cslib.RotationMap.ReingoldPc, Cslib.RotationMap.ReingoldEvalState, Cslib.RotationMap.reingoldEvalStep: the evaluation with an explicit stack.
• Cslib.RotationMap.ReingoldEvalState.mapVertex: renaming the vertex of the original graph in a state of the evaluation.
• Cslib.RotationMap.ReingoldEvalState.atRoot: whether the next step is a step of the original graph.

Main results

• Cslib.RotationMap.reingoldStep_rot: a step of the transformation on the registers.
• Cslib.RotationMap.exists_iterate_reingoldEvalStep: the evaluation computes the rotation map of G_m.
• Cslib.RotationMap.reingoldEvalStep_congr, Cslib.RotationMap.reingoldEvalStep_mapVertex: a step uses the rotation map of the original graph only at a step of the original graph, and commutes with renaming the vertices of the original graph.

References

• O. Reingold, Undirected connectivity in log-space

inductive Cslib.RotationMap.ReingoldPc : Type

The program counter of a frame: the four steps of H (zig₀, zag₀, zig₁, zag₁), the two recursive rotations between them (call₀, call₁) and the final permutation (finish).

• zig₀ : ReingoldPc

  The first step of H, before the first rotation of the level below.

• call₀ : ReingoldPc

  The first rotation of the level below.

• zag₀ : ReingoldPc

  The second step of H, after the first rotation of the level below.

• zig₁ : ReingoldPc

  The third step of H, before the second rotation of the level below.

• call₁ : ReingoldPc

  The second rotation of the level below.

• zag₁ : ReingoldPc

  The fourth step of H, after the second rotation of the level below.

• finish : ReingoldPc

  The final permutation of the labels of H.

@[instance_reducible]

instance Cslib.RotationMap.instDecidableEqReingoldPc : DecidableEq ReingoldPc

@[instance_reducible]

instance Cslib.RotationMap.instFintypeReingoldPc : Fintype ReingoldPc

There are finitely many program counters.

def Cslib.RotationMap.reingoldHStep {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) : ReingoldPc → B × B → B × B

The steps of H on the label b below a frame and the label a of the frame, which packs the four labels e a = ![(i₀, j₀), (i₁, j₁)] of H used by a step of the transformation: each takes the step of H from b along one of them and stores the label at the far end in its place. Other program counters leave the labels unchanged.

def Cslib.RotationMap.reingoldFinish {B : Type u} {E : Type u_1} (e : B ≃ (Fin 2 → E × E)) (a : B) : B

The final permutation: the labels ![(i₀', j₀'), (i₁', j₁')] produced by the steps of H become the label ![(j₁', i₁'), (j₀', i₀')] at the far end of the step of the transformation.

theorem Cslib.RotationMap.reingoldStep_rot {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} (G : RotationMap V B) (y : V) (c a : B) : (H.reingoldStep e G).rot ((y, c), a) = have s₁ := H.reingoldHStep e ReingoldPc.zig₀ (c, a); have r₁ := G.rot (y, s₁.1); have s₂ := H.reingoldHStep e ReingoldPc.zag₀ (r₁.2, s₁.2); have s₃ := H.reingoldHStep e ReingoldPc.zig₁ (s₂.1, s₂.2); have r₂ := G.rot (r₁.1, s₃.1); have s₄ := H.reingoldHStep e ReingoldPc.zag₁ (r₂.2, s₃.2); ((r₂.1, s₄.1), reingoldFinish e s₄.2)

A step of the transformation on the registers, as in the proof of Reingold, Lemma 3.4 (with the square instead of the eighth power): the rotation of ((G ⓩ H) ^ 2).relabel e.symm at the vertex (y, c) along the label a is a step of H from c, a rotation of G at y, two steps of H, a rotation of G and a step of H, with the labels of H kept in a, followed by the final permutation of a.

structure Cslib.RotationMap.ReingoldEvalState (V : Type u_2) (B : Type u_3) : Type (max u_2 u_3)

The memory of the evaluation: the vertex of the original graph, the labels below the current level, the innermost first, and the stack of frames, the innermost first, each with its program counter and its label.

• vertex : V

  The vertex of the original graph.

• lower : List B

  The labels below the current level, the innermost first.

• frames : List (ReingoldPc × B)

  The frames of the levels being evaluated, the innermost first.

def Cslib.RotationMap.reingoldEvalStep {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} (rotG : V × B → V × B) : ReingoldEvalState V B → ReingoldEvalState V B

A step of the evaluation of the rotation maps of the transformation, with rotG the rotation map of the original graph. The level of the top frame is the number of labels below it, and the label b just below it is its last coordinate. A step of H acts on b and the label of the frame; a rotation of the level below is a step of rotG on the vertex and b at level 1, and otherwise pushes a frame for the level below with the label b; the final permutation pops the frame and puts its label below the frame of the level above.

def Cslib.RotationMap.ReingoldEvalState.mapVertex {B : Type u} {V : Type u_2} {W : Type u_3} (φ : V → W) (s : ReingoldEvalState V B) : ReingoldEvalState W B

Rename the vertex of the original graph.

def Cslib.RotationMap.ReingoldEvalState.atRoot {B : Type u} {V : Type u_2} (s : ReingoldEvalState V B) : Bool

Whether the next step of the evaluation is a step of the original graph: a rotation of the level below at level 1.

theorem Cslib.RotationMap.reingoldEvalStep_congr {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} {rotG rotG' : V × B → V × B} {s : ReingoldEvalState V B} (h : s.atRoot = true → ∀ (b : B), s.lower = [b] → rotG (s.vertex, b) = rotG' (s.vertex, b)) : H.reingoldEvalStep e rotG s = H.reingoldEvalStep e rotG' s

A step of the evaluation depends on the rotation map of the original graph only at a step of the original graph, and there only at the vertex and the label below the frame.

theorem Cslib.RotationMap.reingoldEvalStep_mapVertex {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} {W : Type u_3} (φ : V → W) {rotG : V × B → V × B} {rotG' : W × B → W × B} (h : ∀ (v : V) (b : B), rotG' (φ v, b) = Prod.map φ id (rotG (v, b))) (s : ReingoldEvalState V B) : H.reingoldEvalStep e rotG' (ReingoldEvalState.mapVertex φ s) = ReingoldEvalState.mapVertex φ (H.reingoldEvalStep e rotG s)

Renaming the vertices commutes with the evaluation, when the rotation maps agree through the renaming.

theorem Cslib.RotationMap.iterate_reingoldEvalStep_mapVertex {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} {W : Type u_3} (φ : V → W) {rotG : V × B → V × B} {rotG' : W × B → W × B} (h : ∀ (v : V) (b : B), rotG' (φ v, b) = Prod.map φ id (rotG (v, b))) (N : ℕ) (s : ReingoldEvalState V B) : (H.reingoldEvalStep e rotG')^[N] (ReingoldEvalState.mapVertex φ s) = ReingoldEvalState.mapVertex φ ((H.reingoldEvalStep e rotG)^[N] s)

Renaming the vertices commutes with runs of the evaluation.

theorem Cslib.RotationMap.length_lower_add_length_frames_reingoldEvalStep {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} (rotG : V × B → V × B) (s : ReingoldEvalState V B) : (H.reingoldEvalStep e rotG s).lower.length + (H.reingoldEvalStep e rotG s).frames.length = s.lower.length + s.frames.length

A step of the evaluation keeps the total number of labels below and in the frames.

theorem Cslib.RotationMap.reingoldEvalStep_vertex {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} {rotG : V × B → V × B} {P : V → Prop} (hP : ∀ (v : V) (b : B), P v → P (rotG (v, b)).1) {s : ReingoldEvalState V B} (hs : P s.vertex) : P (H.reingoldEvalStep e rotG s).vertex

A step of the evaluation keeps a property of the vertex that the steps of the original graph keep.

theorem Cslib.RotationMap.exists_iterate_reingoldEvalStep {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u} (G : RotationMap V B) {m : ℕ} (hm : m ≠ 0) (x : ReingoldVertex V B m) (a : B) (rest : List (ReingoldPc × B)) : ∃ (N : ℕ), (H.reingoldEvalStep e G.rot)^[N] { vertex := x.toList.1, lower := x.toList.2, frames := (ReingoldPc.zig₀, a) :: rest } = { vertex := ((H.reingold e G m).rot (x, a)).1.toList.1, lower := ((H.reingold e G m).rot (x, a)).2 :: ((H.reingold e G m).rot (x, a)).1.toList.2, frames := rest }

The evaluation computes the rotation map, as in the proof of Reingold, Lemma 3.4: from a frame for level m ≥ 1, freshly pushed with the label a above the registers of a vertex x of G_m, the evaluation reaches the registers of the rotation (x', a') of G_m at (x, a), with the label a' at the far end below the frames, and the frame popped.