Khrapchenko's bound for circuits with few shared gates #
A SharedProgram n k is a sequence of k + 1 De Morgan formulas on n inputs in which each
formula also reads the values of the earlier ones: share G P computes the formula G,
appends its value to the inputs as a new last variable, and continues with P, and
output F returns the value of the formula F. A shared value is read through literals of
either sign, any number of times. Unfolded, this is a circuit of fan-in-two AND and OR gates
with negations free on wires in which only the k shared gates can have fan-out at least two.
Conversely, cutting a circuit at its gates of fan-out at least two gives a program with the same
AND and OR gates; KarchmerWigderson.Sharing.Circuit proves this for the library's De Morgan
circuits (exists_sharedProgram_of_circuit) and transfers the bounds below to them.
SharedProgram.gates counts the AND and OR gates and SharedProgram.inputLeaves the literal
leaves that read an input rather than a shared value.
Theorem. If a program with k shared gates is 1 on A and 0 on B, and X is its
number of input leaves, then |edges A B|² ≤ (k + 1) · X · |A| · |B|
(SharedProgram.sq_card_edges_le). For k = 0 this is Khrapchenko's theorem.
The proof extends the inductive proof of Khrapchenko's theorem. Call an edge of A × B
uncut when its endpoints agree on every shared value computed so far. For a single formula,
|uncut edges|² ≤ X · |A| · |B|, where X counts input literals only: a literal on a shared
variable separates only pairs that the shared value cuts, so it contributes no uncut edge
(Formula.sq_card_uncutEdges_le). For share G P, an uncut edge on which G is constant
stays uncut for P, and the others are separated by G or by its De Morgan dual on the
rectangles {G = 1} × {G = 0} and {G = 0} × {G = 1}, which together contain at most
√(X_G · |A| · |B|) of them by the Cauchy–Schwarz inequality. Summing over the k + 1
formulas, Cauchy–Schwarz gives the factor k + 1 (SharedProgram.sq_card_uncutEdges_le).
Through KhrapchenkoBound the theorem inherits Khrapchenko's corollaries. For all n ≥ 1 and
k, every program with k shared gates computing the parity of n bits satisfies
n² ≤ (k + 1) · (gates + k + 1), so it has at least n² / (k + 1) - (k + 1) gates
(SharedProgram.parity_sq_le_gates). If (k + 1) · (C + 1) ≤ n it has at least C · n
gates (SharedProgram.mul_le_gates_of_parity), so parity needs superlinear size whenever
k = o(n) (SharedProgram.isLittleO_gates_of_parity). The threshold and majority bounds
transfer the same way (SharedProgram.threshold_mul_le_gates,
SharedProgram.majority_mul_le_gates).
Counting gates and input leaves of a formula #
The number of literal leaves on the variables 0, …, m - 1. Constants and literals on
later variables are not counted.
Equations
- (Algebraic.KW.Formula.lit i positive).inputLeaves x✝ = if ↑i < x✝ then 1 else 0
- (Algebraic.KW.Formula.const value).inputLeaves x✝ = 0
- (l.and r).inputLeaves x✝ = l.inputLeaves x✝ + r.inputLeaves x✝
- (l.or r).inputLeaves x✝ = l.inputLeaves x✝ + r.inputLeaves x✝
Instances For
Programs with shared gates #
Uncut edges #
The edges of A × B whose endpoints agree, under val, on every variable from n on.
When val appends shared values to the inputs, these are the edges no shared value cuts.
Equations
- Algebraic.KW.uncutEdges val A B = {p ∈ Algebraic.KW.edges A B | ∀ (i : Fin N), n ≤ ↑i → val p.1 i = val p.2 i}
Instances For
Splitting the zero side of a rectangle splits its uncut edges.
Splitting the one side of a rectangle splits its uncut edges.
Khrapchenko's theorem with shared variables. Let val extend each input by further
variables, keeping the first n variables equal to the input. If a formula F over the
extended variables is 1 on val '' A and 0 on val '' B, the edges of A × B that agree
on the extra variables satisfy |uncut edges|² ≤ X · |A| · |B|, where X counts only the
literal leaves on the first n variables.
Superlinearity from a quantitative bound. If k n = o(n) and C · n ≤ s n whenever
(k n + 1) · (C + 1) ≤ n, then n = o(s n).