A read machine for undirected connectivity

Cslib.USTCON.Reader.machine decides undirected s–t connectivity (Cslib.Complexity.USTCON) on the encodings Cslib.Complexity.encUSTCON, reading its input by address (Turing.ReadMachine), following Reingold's algorithm Reingold, Theorem 4.1 Arora and Barak, Section 21.4:

1. it counts the unary header 1^n 0 1^s 0 1^t 0 (hdrN, hdrS, hdrT) and halves n until it vanishes, adding 16 to the depth and 4168 to the walk length at each halving (size), so that the depth and the walk length are Cslib.Reachability.Reingold.depth a and Cslib.Reachability.Reingold.walkLength a for a = Nat.size n, with n ≤ 2 ^ a;
2. for each counter c = 0, 1, … it walks in Reingold's graph from the vertex (⋯ ((s, s), 0) ⋯, 0) (start, fill) along the labels given by the digits of c in base |B| = 257 ^ 8 (next), each step evaluating the rotation map in place (eval, by Cslib.RotationMap.reingoldEvalStep) and reading the adjacency matrix at a step of the slot graph;
3. it accepts when a walk ends over a slot of t, and rejects when the counter has more digits than the walk length, all counters having been tried (check).

Its memory is a constant number of numbers bounded by a polynomial in n or by |B| to the power of the walk length, and two lists of O(log n) labels and program counters, so O(log n) bits.

Main definitions

• Cslib.USTCON.Reader.labelOfNat: the label of a digit.
• Cslib.USTCON.Reader.slotRotN: the rotation map of the regular rotation map of the input graph, on the slots as pairs of numbers, given the entry of the adjacency matrix.
• Cslib.USTCON.Reader.Ctl, Cslib.USTCON.Reader.State: the control and the memory.
• Cslib.USTCON.Reader.step, Cslib.USTCON.Reader.addr: the step and the address read.
• Cslib.USTCON.Reader.machine: the read machine.

References

• O. Reingold, Undirected connectivity in log-space
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.USTCON.Reader.numLabels : ℕ

The number of labels, 257 ^ 8.

theorem Cslib.USTCON.Reader.numLabels_pos : 0 < numLabels

There are labels.

theorem Cslib.USTCON.Reader.card_label_eq_numLabels : Fintype.card Reachability.Reingold.Label = numLabels

The number of labels is the cardinality of the label type.

noncomputable def Cslib.USTCON.Reader.labelEquiv : Fin numLabels ≃ Reachability.Reingold.Label

The labels numbered by the residues modulo their number.

noncomputable def Cslib.USTCON.Reader.labelOfNat (x : ℕ) : Reachability.Reingold.Label

The label of the digit x % numLabels.

def Cslib.USTCON.Reader.slotRotN (n : ℕ) (v : ℕ × ℕ) (b : Reachability.Reingold.Label) (bit : Bool) : (ℕ × ℕ) × Reachability.Reingold.Label

The rotation map of the regular rotation map of the input graph, on slots written as pairs of numbers below n, given the entry bit of the adjacency matrix at the slot: the edge of the graph exchanges the ends of an edge if bit is set, the edges of the cycle of the slots move to the next or the previous slot, and every other label is a self-loop.

inductive Cslib.USTCON.Reader.Ctl : Type

The control state of the machine.

• hdrN : Ctl

  Counting the ones of the number of vertices.

• hdrS : Ctl

  Counting the ones of the source.

• hdrT : Ctl

  Counting the ones of the target.

• size : Ctl

  Halving the number of vertices, to compute the depth and the walk length.

• start : Ctl

  Starting the walk of the counter.

• fill : Ctl

  Filling the labels of the start vertex with zeros.

• next : Ctl

  Taking the next step of the walk, or ending it.

• eval : Ctl

  Evaluating the rotation map of Reingold's graph.

• check : Ctl

  Checking the end of the walk.

• done : Ctl

  Halted.

@[instance_reducible]

instance Cslib.USTCON.Reader.instDecidableEqCtl : DecidableEq Ctl

structure Cslib.USTCON.Reader.State : Type

The memory of the machine.

• ctl : Ctl

  The control state.

• cnt : ℕ

  The ones counted in the header, or the number of vertices being halved.

• n : ℕ

  The number of vertices.

• s : ℕ

  The source.

• t : ℕ

  The target.

• depth : ℕ

  The depth of Reingold's graph.

• len : ℕ

  The length of the walks.

• c : ℕ

  The counter of the walks.

• w : ℕ

  The digits of the counter not yet used.

• j : ℕ

  The steps of the walk not yet taken.

• ev : RotationMap.ReingoldEvalState (ℕ × ℕ) Reachability.Reingold.Label

  The state of the evaluation of the rotation map: the slot, the labels and the frames.

def Cslib.USTCON.Reader.slotRot (n : ℕ) (bit : Bool) (p : (ℕ × ℕ) × Reachability.Reingold.Label) : (ℕ × ℕ) × Reachability.Reingold.Label

The step of the evaluation with the entry bit of the adjacency matrix.

noncomputable def Cslib.USTCON.Reader.step (q : State) (b : Bool) : State × List Bool

A step, given the bit read.

def Cslib.USTCON.Reader.addr (q : State) : Option ℕ

The address read by a step: the next bit of the header while counting it, and the entry of the adjacency matrix at the slot at a step of the slot graph.

def Cslib.USTCON.Reader.init : State

The initial state: counting the header.

noncomputable def Cslib.USTCON.Reader.machine : Turing.ReadMachine State

The read machine for undirected connectivity.