Internals of the monotone Boolean matrix product bound #
This file proves that every De Morgan circuit without NOT gates (AND, OR,
constants and identity gates) computing a partial Boolean product
z i j = ⋁ {x i k ∧ y k j | (i, k, j) ∈ T} of an I × K matrix and a K × J
matrix has at least |T| AND gates (Pratt; Paterson; Mehlhorn--Galil; Wegener,
The Complexity of Boolean Functions, Theorem 6.8.1, whose argument never uses
the shape of T). Compiling the binary AND/OR basis into the De Morgan basis
(ofAndOr) gives the full product bound I * J * K for AND/OR circuits. The
surface statements are in Complexitylib.Algebraic.LowerBound.Monotone.MatrixProduct
and Complexitylib.Algebraic.LowerBound.Monotone.MatrixProduct.Partial.
Proof #
Call x i k and y k j the variables of type k. The argument runs in
stages k = 0, 1, …, K - 1 and never edits the circuit: each stage is a new
evaluation of the same program, carried by a single interpretation whose
carrier holds the gate functions of every stage at once
(stageInterpretation). Stage k is sem p (k + 1); sem p 0 is the
ordinary Boolean evaluation.
- Stage
kfixes the variables of type< k(xto one,yto zero), so the outputs become the product over the triples ofTof type≥ k. - A gate is forced to the constant one at stage
kwhen it was constant one under this restriction at the previous stage, or when its function has two distinct variables of typekamong its one-variable implicants (Bad). Wegener's Lemma 6.8.1 and replacement rule (Theorem 6.5.2) show that forcing such gates does not change the outputs. Here this is proved for all forced gates of a stage at once (StepHyp.agree): below a negative input of an output there is a negative input that sets at most one type-kvariable to zero (cover), and on it every forced gate already evaluates to one. - The creator of a triple
(i, k, j) ∈ Tis a gate whose stage-kfunction hasx i k ∧ y k jas a prime implicant while none of its arguments has. Every output has that implicant, so a creator exists. Constants, identities and OR gates cannot create a prime implicant (creator_shape), so a creator is an AND gate one of whose arguments has the implicantx i kand the othery k j. - Within a stage, two triples cannot share a creator, since an argument of it
would have two type-
kimplicants of length one and would have been forced. Across stages, the argument with implicantx i kis constant one at every later stage (x i kis then fixed to one), so the gate is not a creator there.
The creators therefore form |T| distinct AND gates.
The Boolean core of creator_shape for an AND gate with arguments taking the
values a, b, c on the pair and the two singletons.
A Boolean function is monotone.
Equations
- Algebraic.Monotone.MatrixProduct.Internal.IsMonotone f = ∀ (a b : Fin N → Bool), Algebraic.Monotone.MatrixProduct.Internal.AssignmentLE a b → f a = true → f b = true
Instances For
The assignment whose only true variable is u.
Equations
Instances For
The De Morgan basis without negation #
Every De Morgan operation other than negation is monotone.
The local shape of a creator. A gate other than NOT whose function has the
prime implicant u ∧ w while none of its arguments has it is an AND gate, one
argument of which accepts u alone and the other w alone, and no argument of
which is constant one.
The NOT-gate count of a program vanishes only when it has no NOT gate.
An injective layout of an I × K matrix x and a K × J matrix y among
N circuit inputs.
The input carrying entry
(i, k)of the left matrix.The input carrying entry
(k, j)of the right matrix.- x_inj {i : Fin I} {k : Fin K} {i' : Fin I} {k' : Fin K} : self.x i k = self.x i' k' → i = i' ∧ k = k'
Distinct left entries use distinct inputs.
- y_inj {k : Fin K} {j : Fin J} {k' : Fin K} {j' : Fin J} : self.y k j = self.y k' j' → k = k' ∧ j = j'
Distinct right entries use distinct inputs.
Left and right entries use distinct inputs.
Instances For
The layout of an injective placement of the entries of both matrices.
Equations
- Algebraic.Monotone.MatrixProduct.Internal.Layout.ofInjective x y distinct = { x := x, y := y, x_inj := ⋯, y_inj := ⋯, x_ne_y := ⋯ }
Instances For
The restriction #
Programs #
Induction over the wires of a program in topological order.
A gate wire carries the gate operation applied to its argument wires.
The staged evaluation #
The functions of one gate at every index, from the functions of its
arguments. Index 0 is the ordinary evaluation. Index s + 1 (stage s)
forces the gate to one when its function at index s is constant one under
the restriction fix s, or when the gate operation applied to the arguments
has two type-s implicants of length one (Bad).
Equations
- One or more equations did not get rendered due to their size.
- L.stageValue op u 0 = fun (c : Fin N → Bool) => Algebraic.DeMorgan.interpretation op fun (m : Fin (Algebraic.DeMorgan.arity op)) => u m 0 c
Instances For
The interpretation evaluating all stages at once.
Equations
- L.stageInterpretation op args = L.stageValue op args
Instances For
Input v at every index: index 0 reads it, index s + 1 reads it through
fix s (and fix 0 changes nothing).
Equations
- L.inputValue v t c = L.fix (t - 1) c v
Instances For
The function carried by a wire at index t.
Equations
- L.sem p t w = p.trace L.stageInterpretation L.inputValue w t
Instances For
The function of a gate at index s + 1 before forcing.
Equations
Instances For
One stage #
Hypotheses relating the previous stage, restricted by fix s (prev), to
the next stage (next) of a program without NOT gates.
- next_gate (G : Fin g) : next (Wire.gate G) = if (prev (Wire.gate G) fun (x : Fin N) => false) = true ∨ L.Bad s fun (c : Fin N → Bool) => DeMorgan.interpretation (p.lines G).op fun (m : Fin (DeMorgan.arity (p.lines G).op)) => next ((p.lines G).wires m) c then fun (x : Fin N → Bool) => true else fun (c : Fin N → Bool) => DeMorgan.interpretation (p.lines G).op fun (m : Fin (DeMorgan.arity (p.lines G).op)) => next ((p.lines G).wires m) c
- prev_mono (w : Wire N g) : IsMonotone (prev w)
Instances For
Covering assignments #
Forcing preserves every output that computes a restricted product entry.
All stages #
Index 0 is the ordinary Boolean evaluation.
At index t, the outputs compute the product over the triples of type
≥ t - 1.
A wire that is one at index s + 1 on the restriction fix s' c is one at
the later index s' + 1 on c.
At index s + 1 every wire is constant one or has at most one type-s
implicant of length one.
Creators #
f accepts {x i k, y k j} but neither {x i k} nor {y k j}; for a
monotone f this says that x i k ∧ y k j is a prime implicant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A gate whose function at index k + 1 has the prime implicant x i k ∧ y k j
while none of its arguments has it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A creator is an AND gate; one argument has the implicant x i k, another
y k j, and no argument is constant one.
Two triples of the same type have distinct creators.
A creator at one stage is not a creator at any later stage.
Distinct AND gates indexed by the triples of T bound the AND-gate count.
Every De Morgan circuit without NOT gates computing the partial Boolean
product over the triples of T, laid out injectively among its inputs, has at
least |T| AND gates.
AND/OR circuits #
The binary AND/OR basis as the negation-free binary part of the De Morgan basis: each operation becomes the single De Morgan gate of the same name.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every AND/OR circuit computing the Boolean product of an I × K matrix and a
K × J matrix, laid out injectively among its inputs, has at least I * J * K
AND gates.