Read-once branching programs and the rectangle bound

A layered read-once nondeterministic branching program reads the coordinates of an input x : ι → U a few at a time: ∅ = X 0 ⊆ X 1 ⊆ ... ⊆ X T = ι. Its nodes at each layer are states. An edge of step t joins a state at layer t to a state at layer t + 1 and is labelled by an assignment to the coordinates X (t + 1) \ X t read during the step. An input is accepted when some path from the start state at layer 0 to the accepting state at layer T follows edges whose labels agree with the input. Each coordinate is read at exactly one step. The program is unambiguous when every input has at most one accepting path; the rectangle bound below does not need this.

Concatenation (IsAcceptingPath.splice). If accepting paths for x and y are in the same state at layer t, following the first up to layer t and the second afterwards is an accepting path for the input that agrees with x on X t and with y elsewhere. So the chosen accepting paths form a sweep of the accepted set (ReadOnceNBP.sweep): the inputs whose paths pass through a fixed state at layer t span a rectangle, for the cut X t, inside the accepted set.

The rectangle bound (ncard_accepted_le_of_smallSides). Suppose that at every layer, the inputs whose paths share a state have fewer than K distinct parts on one side of the cut, as when the accepted set is K-rectangle-free (ncard_accepted_le). Then the program has at least |accepted| / (K - 1) ^ 2 edges. This is the charging argument for the sweep of the program (Sweep.ncard_le_mul_transitionCount): the transition an input takes at a step is read off the edge its path takes there.

Peeling (abs_signedCount_accepted_le). In an unambiguous program the inputs whose paths pass through a state are exactly a rectangle (Unambiguous.peers_eq_rectangle), and deleting the state removes exactly them, leaving an unambiguous program (accepted_eraseNode). So while some state has at least K distinct parts on both sides of its cut, its rectangle can be peeled off; what remains has small sides and is counted by the rectangle bound. If S has bias at most b on rectangles with both sides of size at least K, the accepted inputs in S and those outside it then differ in number by at most 2 b |accepted| + (K - 1) ^ 2 · size. The peeling argument is due to Sam McGuire.

Constraint networks laid out along a vertex ordering give such programs, whose states are the values on the edges of a frontier (Cslib.Circuits.Frontier.Network.branchingProgram).

Main definitions

• Cslib.Circuits.Frontier.ReadOnceNBP ι U M: a layered read-once nondeterministic branching program with states in M.
• Cslib.Circuits.Frontier.ReadOnceNBP.accepted: its accepted inputs.
• Cslib.Circuits.Frontier.ReadOnceNBP.Unambiguous: every input has at most one accepting path.
• Cslib.Circuits.Frontier.ReadOnceNBP.size: its number of edges.
• Cslib.Circuits.Frontier.ReadOnceNBP.sweep: its chosen accepting paths, as a sweep of the accepted set.

Main results

• Cslib.Circuits.Frontier.ReadOnceNBP.IsAcceptingPath.splice: concatenation of accepting paths.
• Cslib.Circuits.Frontier.ReadOnceNBP.ncard_accepted_le_of_smallSides, Cslib.Circuits.Frontier.ReadOnceNBP.ncard_accepted_le: the rectangle bound.
• Cslib.Circuits.Frontier.ReadOnceNBP.abs_signedCount_accepted_le: peeling.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Ch. 16

structure Cslib.Circuits.Frontier.ReadOnceNBP (ι : Type u_4) (U : Type u_5) (M : Type u_6) : Type (max (max u_4 u_5) u_6)

A layered read-once nondeterministic branching program over inputs ι → U, with states in M. Step t reads the coordinates in revealed (t + 1) \ revealed t.

• length : ℕ

  The number of steps.

• revealed : ℕ → Set ι

  The coordinates read before layer t.

• revealed_zero : self.revealed 0 = ∅

  Nothing is read before the first layer.

• revealed_length : self.revealed self.length = Set.univ

  Everything is read before the last layer.

• revealed_mono : Monotone self.revealed

  A coordinate once read stays read.

• start : M

  The start state, at layer 0.

• accept : M

  The accepting state, at the last layer.

• Edge (t : ℕ) : M → (↑(self.revealed (t + 1) \ self.revealed t) → U) → M → Prop

  Edge t m a m': an edge of step t joins the state m at layer t to the state m' at layer t + 1, labelled by the values a of the coordinates read during the step.

@[reducible, inline]

abbrev Cslib.Circuits.Frontier.ReadOnceNBP.newly {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) (t : ℕ) : Set ι

The coordinates read during step t, between layers t and t + 1.

structure Cslib.Circuits.Frontier.ReadOnceNBP.IsAcceptingPath {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) (x : ι → U) (γ : ℕ → M) : Prop

γ is an accepting path for the input x: it starts at the start state, ends at the accepting state, and at each step follows an edge labelled by the values of x.

• start : γ 0 = P.start

  The path starts at the start state.

• accept : γ P.length = P.accept

  The path ends at the accepting state.

• edge (t : ℕ) : t < P.length → P.Edge t (γ t) ((P.newly t).domRestrict x) (γ (t + 1))

  Each step follows an edge labelled by the values of x.

def Cslib.Circuits.Frontier.ReadOnceNBP.accepted {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) : Set (ι → U)

The accepted inputs: those with an accepting path.

def Cslib.Circuits.Frontier.ReadOnceNBP.Unambiguous {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) : Prop

The program is unambiguous when every input has at most one accepting path: two accepting paths for the same input agree up to the last layer.

def Cslib.Circuits.Frontier.ReadOnceNBP.edges {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) (t : ℕ) : Set (M × (↑(P.newly t) → U) × M)

The edges of step t, each given by its source state, its label, and its target state.

noncomputable def Cslib.Circuits.Frontier.ReadOnceNBP.size {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) : ℕ

The size of the program: its number of edges.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.newly_subset_revealed {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) {s t : ℕ} (h : s < t) : P.newly s ⊆ P.revealed t

A coordinate read at step s < t was read before layer t.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.newly_subset_compl {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) {s t : ℕ} (h : t ≤ s) : P.newly s ⊆ (P.revealed t)ᶜ

A coordinate read at step s ≥ t was not read before layer t.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.IsAcceptingPath.splice {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} {x y z : ι → U} {γ δ : ℕ → M} (hγ : P.IsAcceptingPath x γ) (hδ : P.IsAcceptingPath y δ) {t : ℕ} (ht : γ t = δ t) (hzx : Set.EqOn z x (P.revealed t)) (hzy : Set.EqOn z y (P.revealed t)ᶜ) : P.IsAcceptingPath z fun (s : ℕ) => if s ≤ t then γ s else δ s

Concatenation. Let the accepting paths γ for x and δ for y be in the same state at layer t. Following γ up to layer t and δ afterwards is an accepting path for any input that agrees with x on the coordinates read before layer t and with y on the others.

noncomputable def Cslib.Circuits.Frontier.ReadOnceNBP.path {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) (x : ι → U) : ℕ → M

An accepting path for each accepted input, chosen once and for all.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.isAcceptingPath_path {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) {x : ι → U} (hx : x ∈ P.accepted) : P.IsAcceptingPath x (P.path x)

The chosen path of an accepted input is an accepting path.

noncomputable def Cslib.Circuits.Frontier.ReadOnceNBP.edgeOf {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) (t : ℕ) (x : ι → U) : M × (↑(P.newly t) → U) × M

The edge that the chosen path of x takes at step t.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.edgeOf_mem_edges {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) {x : ι → U} (hx : x ∈ P.accepted) {t : ℕ} (ht : t < P.length) : P.edgeOf t x ∈ P.edges t

The chosen path of an accepted input follows edges of the program.

noncomputable def Cslib.Circuits.Frontier.ReadOnceNBP.sweep {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) : Sweep P.accepted M

The sweep of a program: the message of an accepted input at time t is the state of its chosen accepting path at layer t. Inputs in the same state splice by concatenation of their paths, and all paths end in the accepting state.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.mem_peers_sweep {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) {t : ℕ} {x y : ι → U} : y ∈ P.sweep.peers t x ↔ y ∈ P.accepted ∧ P.path y t = P.path x t

The peers of x at layer t are the accepted inputs whose chosen paths are in the same state as that of x.

The rectangle bound

def Cslib.Circuits.Frontier.ReadOnceNBP.SmallSides {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) (K : ℕ) : Prop

At every layer, the inputs sharing the state of an accepted input have fewer than K distinct parts on one side of the cut.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.smallSides_of_rectangleFree {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) {K : ℕ} (hS : RectangleFree P.accepted K) : P.SmallSides K

A rectangle-free accepted set has small sides.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.SmallSides.one_lt {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} [Finite ι] [Finite U] {K : ℕ} (hS : P.SmallSides K) (hne : P.accepted.Nonempty) : 1 < K

Small sides force K > 1 once some input is accepted: at the first layer both sides of an accepted input are nonempty.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.one_le_size {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) [Finite ι] [Finite U] [Finite M] (hL : 0 < P.length) (hne : P.accepted.Nonempty) : 1 ≤ P.size

A program that accepts some input and has a step has an edge.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.transitionCount_sweep_le_size {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) [Finite ι] [Finite U] [Finite M] : P.sweep.transitionCount ≤ P.size

The transitions of the sweep of a program are read off the edges taken by the chosen paths, so there are no more of them than edges.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.ncard_accepted_le_of_smallSides {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) [Finite ι] [Finite U] [Finite M] (hL : 0 < P.length) {K : ℕ} (hS : P.SmallSides K) : P.accepted.ncard ≤ (K - 1) ^ 2 * P.size

The rectangle bound. If at every layer the inputs sharing the state of an accepted input have fewer than K distinct parts on one side of the cut, the program has at least |accepted| / (K - 1) ^ 2 edges.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.ncard_accepted_le {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) [Finite ι] [Finite U] [Finite M] (hL : 0 < P.length) {K : ℕ} (hS : RectangleFree P.accepted K) : P.accepted.ncard ≤ (K - 1) ^ 2 * P.size

The rectangle bound for rectangle-free sets. A read-once branching program whose accepted set is K-rectangle-free has at least |accepted| / (K - 1) ^ 2 edges.

Peeling large rectangles

def Cslib.Circuits.Frontier.ReadOnceNBP.eraseNode {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) (t : ℕ) (m : M) : ReadOnceNBP ι U M

The program with the state m deleted from layer t: no edge enters or leaves it.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.IsAcceptingPath.of_eraseNode {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} {t : ℕ} {m : M} {x : ι → U} {γ : ℕ → M} (h : (P.eraseNode t m).IsAcceptingPath x γ) : P.IsAcceptingPath x γ

theorem Cslib.Circuits.Frontier.ReadOnceNBP.isAcceptingPath_eraseNode_iff {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} (hL : 0 < P.length) {t : ℕ} (ht : t ≤ P.length) {m : M} {x : ι → U} {γ : ℕ → M} : (P.eraseNode t m).IsAcceptingPath x γ ↔ P.IsAcceptingPath x γ ∧ γ t ≠ m

The accepting paths of the program with a state deleted are those avoiding it.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.Unambiguous.eraseNode {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} (hP : P.Unambiguous) (t : ℕ) (m : M) : (P.eraseNode t m).Unambiguous

theorem Cslib.Circuits.Frontier.ReadOnceNBP.accepted_eraseNode {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} (hP : P.Unambiguous) (hL : 0 < P.length) {t : ℕ} (ht : t ≤ P.length) (m : M) : (P.eraseNode t m).accepted = {x : ι → U | x ∈ P.accepted ∧ P.path x t ≠ m}

In an unambiguous program, deleting a state removes exactly the inputs whose paths pass through it.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.size_eraseNode_le {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} [Finite ι] [Finite U] [Finite M] (t : ℕ) (m : M) : (P.eraseNode t m).size ≤ P.size

theorem Cslib.Circuits.Frontier.ReadOnceNBP.Unambiguous.peers_eq_rectangle {ι : Type u_1} {U : Type u_2} {M : Type u_3} {P : ReadOnceNBP ι U M} (hP : P.Unambiguous) {t : ℕ} (ht : t ≤ P.length) (x : ι → U) : P.sweep.peers t x = rectangle (P.revealed t) (P.sweep.pastSide t x) (P.sweep.futureSide t x)

In an unambiguous program, the inputs whose paths share a state are exactly the rectangle spanned by their parts.

theorem Cslib.Circuits.Frontier.ReadOnceNBP.abs_signedCount_accepted_le {ι : Type u_1} {U : Type u_2} {M : Type u_3} (P : ReadOnceNBP ι U M) [Finite ι] [Finite U] [Finite M] (hP : P.Unambiguous) (hL : 0 < P.length) {S : Set (ι → U)} {K : ℕ} {b : ℝ} (hb : 0 ≤ b) (hS : RectangleBias S K b) : |signedCount S P.accepted| ≤ 2 * b * ↑P.accepted.ncard + ↑((K - 1) ^ 2 * P.size)

Peeling. Let S have bias at most b ≥ 0 on rectangles with both sides of size at least K. Then the accepted inputs of an unambiguous program that lie in S and those that do not differ in number by at most 2 b |accepted| + (K - 1) ^ 2 · size.

While the inputs sharing some state have at least K distinct parts on both sides of its cut, they form such a rectangle, and deleting the state removes exactly them and leaves an unambiguous program. When no such state is left, the rectangle bound counts the remaining inputs. The argument is due to Sam McGuire.