The inductive-counting machine, abstractly

The combinatorial heart of Immerman–Szelepcsényi (Immerman 1988, Szelepcsényi 1988): a nondeterministic walk on configurations that reaches an accepting configuration exactly when no target is reachable from a source in a finite graph.

Everything here is about an abstract finite linearly ordered node type V with an edge relation E and source and target predicates S, T; nothing is first-order yet. DescriptiveComplexity.InductiveCounting.Sound and DescriptiveComplexity.InductiveCounting.Complete prove the two directions, and DescriptiveComplexity.TransitiveClosureCompl runs the whole machine inside a single TC by realizing each configuration as a mode together with a tuple of elements.

The algorithm

Write Rset d for the set of nodes reachable from a source in at most d steps. The counts |Rset d| are computed by inductive counting: knowing |Rset d| exactly, one can certify, for a given node v, whether v ∈ Rset (d+1), by running over all nodes u in order, guessing which belong to Rset d, certifying each guess by a path of length at most d from a source, and checking at the end that exactly |Rset d| of them were certified – which forces the guessed set to be Rset d itself. Counting the v's that pass gives |Rset (d+1)|. The machine accepts when |Rset (d+1)| = |Rset d|, at which point the reachable set is Rset d; since every certified node is checked not to be a target, acceptance means no target is reachable.

The registers

The machine has eight registers, each holding an element of WithBot V: a node, or a count read through DescriptiveComplexity.orank (so ⊥ is the count 0 and the count m is the m-th value of WithBot V). This uniformity is what lets a register be stored, in the first-order realization, as one tuple of elements together with a finite mode.

Layered reachability

def DescriptiveComplexity.InductiveCounting.RInLe {V : Type} (E : V → V → Prop) : ℕ → V → V → Prop

RInLe E n a b: the node b is reachable from a along E in at most n steps.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.InductiveCounting.RInLe E 0 x✝¹ x✝ = (x✝¹ = x✝)

@[simp]

theorem DescriptiveComplexity.InductiveCounting.rInLe_zero {V : Type} {E : V → V → Prop} {a b : V} : RInLe E 0 a b ↔ a = b

theorem DescriptiveComplexity.InductiveCounting.rInLe_succ {V : Type} {E : V → V → Prop} {n : ℕ} {a b : V} : RInLe E (n + 1) a b ↔ RInLe E n a b ∨ ∃ (c : V), RInLe E n a c ∧ E c b

theorem DescriptiveComplexity.InductiveCounting.RInLe.step {V : Type} {E : V → V → Prop} {n : ℕ} {a b : V} (h : RInLe E n a b) : RInLe E (n + 1) a b

theorem DescriptiveComplexity.InductiveCounting.RInLe.mono {V : Type} {E : V → V → Prop} {n m : ℕ} {a b : V} (hnm : n ≤ m) (h : RInLe E n a b) : RInLe E m a b

theorem DescriptiveComplexity.InductiveCounting.RInLe.cons {V : Type} {E : V → V → Prop} {n : ℕ} {a b c : V} (hab : E a b) (h : RInLe E n b c) : RInLe E (n + 1) a c

Prepending an edge to a bounded walk.

def DescriptiveComplexity.InductiveCounting.Rset {V : Type} (E : V → V → Prop) (S : V → Prop) : ℕ → Set V

The set of nodes reachable from a source in at most d steps.

Equations

• DescriptiveComplexity.InductiveCounting.Rset E S 0 = {x : V | S x}
• DescriptiveComplexity.InductiveCounting.Rset E S d.succ = {x : V | ∃ y ∈ DescriptiveComplexity.InductiveCounting.Rset E S d, y = x ∨ E y x}

theorem DescriptiveComplexity.InductiveCounting.rset_zero {V : Type} {E : V → V → Prop} {S : V → Prop} : Rset E S 0 = {x : V | S x}

theorem DescriptiveComplexity.InductiveCounting.mem_rset_succ {V : Type} {E : V → V → Prop} {S : V → Prop} {d : ℕ} {x : V} : x ∈ Rset E S (d + 1) ↔ ∃ y ∈ Rset E S d, y = x ∨ E y x

theorem DescriptiveComplexity.InductiveCounting.Rset.subset_succ {V : Type} {E : V → V → Prop} {S : V → Prop} {d : ℕ} : Rset E S d ⊆ Rset E S (d + 1)

theorem DescriptiveComplexity.InductiveCounting.Rset.mono {V : Type} {E : V → V → Prop} {S : V → Prop} {d e : ℕ} (h : d ≤ e) : Rset E S d ⊆ Rset E S e

theorem DescriptiveComplexity.InductiveCounting.mem_rset_of_rInLe {V : Type} {E : V → V → Prop} {S : V → Prop} {i n : ℕ} {y b : V} (hy : y ∈ Rset E S i) (h : RInLe E n y b) : b ∈ Rset E S (i + n)

Walking on from a layer: a bounded walk out of Rset i lands in a later layer.

theorem DescriptiveComplexity.InductiveCounting.exists_rInLe_of_mem_rset {V : Type} {E : V → V → Prop} {S : V → Prop} {d : ℕ} {x : V} (hx : x ∈ Rset E S d) : ∃ (s : V), S s ∧ RInLe E d s x

Every member of a layer carries a bounded walk from a source.

theorem DescriptiveComplexity.InductiveCounting.exists_mem_rset_of_reflTransGen {V : Type} {E : V → V → Prop} {S : V → Prop} {s x : V} (hs : S s) (h : Relation.ReflTransGen E s x) : ∃ (d : ℕ), x ∈ Rset E S d

The layers exhaust the reachable set.

theorem DescriptiveComplexity.InductiveCounting.reflTransGen_of_mem_rset {V : Type} {E : V → V → Prop} {S : V → Prop} {d : ℕ} {x : V} (hx : x ∈ Rset E S d) : ∃ (s : V), S s ∧ Relation.ReflTransGen E s x

Conversely, every member of a layer is reachable from a source.

theorem DescriptiveComplexity.InductiveCounting.rset_stabilizes {V : Type} {E : V → V → Prop} {S : V → Prop} {d : ℕ} (h : Rset E S (d + 1) = Rset E S d) (e : ℕ) : Rset E S (d + e) = Rset E S d

Once a layer repeats, all later layers agree with it.

theorem DescriptiveComplexity.InductiveCounting.not_reach_target_of_stable {V : Type} {E : V → V → Prop} {S : V → Prop} {d : ℕ} {T : V → Prop} (hstab : Rset E S (d + 1) = Rset E S d) (hT : ∀ y ∈ Rset E S d, ¬T y) : ¬∃ (a : V) (b : V), S a ∧ T b ∧ Relation.ReflTransGen E a b

If no layer contains a target, no target is reachable from a source.

Registers, slots and atomic constraints

@[reducible, inline]

abbrev DescriptiveComplexity.InductiveCounting.Reg : Type

The eight registers of the machine.

Equations

• DescriptiveComplexity.InductiveCounting.Reg = Fin 8

def DescriptiveComplexity.InductiveCounting.Reg.d : Reg

The stage counter: the current layer index d.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.d = 0

def DescriptiveComplexity.InductiveCounting.Reg.c : Reg

The count of the current layer, |Rset d|.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.c = 1

def DescriptiveComplexity.InductiveCounting.Reg.c2 : Reg

The count of the next layer being built, |Rset (d+1)|.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.c2 = 2

def DescriptiveComplexity.InductiveCounting.Reg.v : Reg

The node scanned by the outer loop.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.v = 3

def DescriptiveComplexity.InductiveCounting.Reg.cnt : Reg

The count of nodes certified in the inner loop.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.cnt = 4

def DescriptiveComplexity.InductiveCounting.Reg.u : Reg

The node scanned by the inner loop.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.u = 5

def DescriptiveComplexity.InductiveCounting.Reg.w : Reg

The node walked backwards along a certifying path.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.w = 6

def DescriptiveComplexity.InductiveCounting.Reg.j : Reg

The countdown of the certifying path's remaining length.

Equations

• DescriptiveComplexity.InductiveCounting.Reg.j = 7

@[reducible, inline]

abbrev DescriptiveComplexity.InductiveCounting.Slot : Type

A slot: a register, read either in the current configuration (false) or in the next one (true).

Equations

• DescriptiveComplexity.InductiveCounting.Slot = (Bool × DescriptiveComplexity.InductiveCounting.Reg)

@[reducible, inline]

abbrev DescriptiveComplexity.InductiveCounting.old (r : Reg) : Slot

The slot reading a register in the current configuration.

Equations

• DescriptiveComplexity.InductiveCounting.old r = (false, r)

@[reducible, inline]

abbrev DescriptiveComplexity.InductiveCounting.nxt (r : Reg) : Slot

The slot reading a register in the next configuration.

Equations

• DescriptiveComplexity.InductiveCounting.nxt r = (true, r)

inductive DescriptiveComplexity.InductiveCounting.VAtom : Type

An atomic constraint relating the registers of two consecutive configurations. Each one is realized, in the first-order construction, by one formula over two tuples of variables.

• eqR (a b : Slot) : VAtom

  Two slots hold the same value.

• neqR (a b : Slot) : VAtom

  Two slots hold different values.

• succR (a b : Slot) : VAtom

  The second slot holds the immediate successor of the first.

• edge (a b : Slot) : VAtom

  The two slots hold nodes joined by an edge.

• nedge (a b : Slot) : VAtom

  The two slots do not hold nodes joined by an edge.

• srcR (a : Slot) : VAtom

  The slot holds a source node.

• nsrcR (a : Slot) : VAtom

  The slot does not hold a source node.

• tgtR (a : Slot) : VAtom

  The slot holds a target node.

• ntgtR (a : Slot) : VAtom

  The slot does not hold a target node.

• botNode (a : Slot) : VAtom

  The slot holds the least node.

• topNode (a : Slot) : VAtom

  The slot holds the greatest node.

• isZero (a : Slot) : VAtom

  The slot holds the count zero.

Configurations and the transition table

inductive DescriptiveComplexity.InductiveCounting.Phase : Type

The control phases of the machine.

• initCount : Phase

  Scanning all nodes to count the sources, that is |Rset 0|.

• inner : Phase

  The inner loop: at node u, about to certify it or to skip it.

• walk : Phase

  Walking backwards along a certifying path for u.

• certDone : Phase

  The certifying path is complete: count u in and test it against v.

• check : Phase

  The inner loop is over: check that the count matches |Rset d|.

• stageEnd : Phase

  The outer loop is over: c2 holds |Rset (d+1)|.

• accept : Phase

  The accepting phase.

@[instance_reducible]

instance DescriptiveComplexity.InductiveCounting.instDecidableEqPhase : DecidableEq Phase

Equations

• DescriptiveComplexity.InductiveCounting.instDecidableEqPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.InductiveCounting.instFinitePhase : Finite Phase

structure DescriptiveComplexity.InductiveCounting.Cfg (V : Type) : Type

A configuration: a phase, the flag recording whether the current outer node has been found in the next layer, and the eight registers.

• phase : Phase

  The control phase.

• flag : Bool

  The flag: v has been seen to lie in the next layer.

• regs : Reg → WithBot V

  The registers.

def DescriptiveComplexity.InductiveCounting.table (p q : Phase × Bool) : List (List VAtom)

The transition table: a list of alternatives, each a list of atomic constraints, for every pair of control states (a phase and the flag). The algorithm of the module docstring is entirely contained here.

Equations

• One or more equations did not get rendered due to their size.

The semantics of the machine

def DescriptiveComplexity.InductiveCounting.EW {V : Type} (E : V → V → Prop) (a b : WithBot V) : Prop

Two slots hold nodes joined by an edge.

Equations

• DescriptiveComplexity.InductiveCounting.EW E a b = ∃ (p : V) (q : V), a = ↑p ∧ b = ↑q ∧ E p q

def DescriptiveComplexity.InductiveCounting.PW {V : Type} (S : V → Prop) (a : WithBot V) : Prop

A slot holds a node satisfying a predicate.

Equations

• DescriptiveComplexity.InductiveCounting.PW S a = ∃ (p : V), a = ↑p ∧ S p

def DescriptiveComplexity.InductiveCounting.slotVal {V : Type} (x y : Reg → WithBot V) : Slot → WithBot V

The value a slot reads, from the current and the next register vectors.

Equations

• DescriptiveComplexity.InductiveCounting.slotVal x y (false, r) = x r
• DescriptiveComplexity.InductiveCounting.slotVal x y (true, r) = y r

def DescriptiveComplexity.InductiveCounting.VAtom.Holds {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) (x y : Reg → WithBot V) : VAtom → Prop

What an atomic constraint asserts about two register vectors.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.InductiveCounting.VAtom.Holds E S T x y (DescriptiveComplexity.InductiveCounting.VAtom.isZero a) = (DescriptiveComplexity.InductiveCounting.slotVal x y a = ⊥)

def DescriptiveComplexity.InductiveCounting.Sat {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) (x y : Reg → WithBot V) (l : List VAtom) : Prop

All the constraints of an alternative hold.

Equations

• DescriptiveComplexity.InductiveCounting.Sat E S T x y l = ∀ a ∈ l, DescriptiveComplexity.InductiveCounting.VAtom.Holds E S T x y a

@[simp]

theorem DescriptiveComplexity.InductiveCounting.sat_nil {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) (x y : Reg → WithBot V) : Sat E S T x y []

@[simp]

theorem DescriptiveComplexity.InductiveCounting.sat_cons {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) {a : VAtom} {l : List VAtom} (x y : Reg → WithBot V) : Sat E S T x y (a :: l) ↔ VAtom.Holds E S T x y a ∧ Sat E S T x y l

def DescriptiveComplexity.InductiveCounting.CfgStep {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) (s s' : Cfg V) : Prop

One step of the machine: some alternative of the table entry for the two control states is satisfied by the two register vectors.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DescriptiveComplexity.InductiveCounting.CfgReach {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) : Cfg V → Cfg V → Prop

Reachability between configurations.

Equations

• DescriptiveComplexity.InductiveCounting.CfgReach E S T = Relation.ReflTransGen (DescriptiveComplexity.InductiveCounting.CfgStep E S T)

def DescriptiveComplexity.InductiveCounting.CfgIsSrc {V : Type} [LinearOrder V] (s : Cfg V) : Prop

The initial configurations: the source scan is about to start, with a zero count and the outer register at the least node.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.InductiveCounting.CfgIsTgt {V : Type} (s : Cfg V) : Prop

The accepting configurations.

Equations

• DescriptiveComplexity.InductiveCounting.CfgIsTgt s = (s.phase = DescriptiveComplexity.InductiveCounting.Phase.accept)

def DescriptiveComplexity.InductiveCounting.MachineAccepts {V : Type} [LinearOrder V] (E : V → V → Prop) (S T : V → Prop) : Prop

The machine accepts: an accepting configuration is reachable from an initial one.

Equations

• One or more equations did not get rendered due to their size.