38 Boolean Analysis — Circuit
38.1 Overview
This module sets up the basic combinatorial data of Boolean circuits used in the switching lemma development: literals, general AND/OR circuit trees and their size/depth/fanin measures, normal-form alternating circuits (\(\mathsf{NAnd}\) and \(\mathsf{NOr}\)) with their normalization maps and semantics/size/literal-count preservation results, as well as the auxiliary types (literals, terms, DNF/CNF, and decision trees) needed elsewhere in the switching-lemma proof.
38.2 Declarations
For a literal \(l\) on \(n\) variables and an assignment \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\), the value \(l.\mathrm{eval}\, x\) is \(x_{l.\mathrm{idx}}\) when \(l\) is positive (\(l.\mathrm{sign} = \mathrm{true}\)) and \(\lnot x_{l.\mathrm{idx}}\) when \(l\) is negated.
A Boolean circuit on \(n\) variables is a tree whose leaves are literals (lit \(l\)) and whose internal nodes (node \(isAnd\) \(children\)) are AND gates when \(isAnd = \mathrm{true}\) and OR gates when \(isAnd = \mathrm{false}\), applied to a list of child circuits. No alternation or deduplication constraint is imposed.
An induction principle for Circuit stating that to prove a predicate \(\mathrm{motive}\) holds for every circuit it suffices to prove it for every literal and, in the node case, to prove \(\mathrm{motive}(\texttt{node}\, isAnd\, cs)\) assuming \(\mathrm{motive}\, c\) for every child \(c \in cs\). This works around the lack of native support for nested inductives.
Evaluates a circuit under an assignment \(x\): a literal evaluates via \(\mathrm{Lit.eval}\), an AND node is the conjunction (foldr with &&, unit true) of its children’s values, and an OR node is the disjunction (foldr with ||, unit false).
The number of literal occurrences in a circuit: a literal contributes \(1\) and a node contributes the sum of the literal counts of its children.
The depth of a circuit (longest root-to-leaf path): a literal has depth \(0\) and a node has depth \(1\) plus the maximum depth among its children.
The total number of nodes of a circuit (internal gates plus literal leaves): a literal has size \(1\) and a node has size \(1\) plus the sum of the sizes of its children.
The maximum depth over a list \(cs\) of circuits (with \(0\) for the empty list), used to compute the depth at a node.
The sum of the sizes over a list \(cs\) of circuits, used to compute the size at a node.
The maximum fanin of a circuit: a literal has fanin \(0\), and a node’s value is the maximum of the number of its children and the maximal fanin occurring recursively among its children.
A normal-form AND circuit on \(n\) variables: either a base clause given by a list of literals whose variable indices are pairwise distinct (a Nodup proof on \(lits.\mathrm{map}\; \mathrm{Lit.idx}\)), or a node that ANDs together a list of normal-form OR circuits. Together with \(\mathrm{NOrCircuit}\) this forms a strictly alternating AND/OR normal form.
Evaluates a normal-form AND circuit under an assignment \(x\): a clause is the conjunction of its literals’ values (unit true), and a node is the conjunction of its child OR circuits’ values.
Evaluates a normal-form OR circuit under an assignment \(x\): a clause is the disjunction of its literals’ values (unit false), and a node is the disjunction of its child AND circuits’ values.
The number of literal occurrences in a normal-form AND circuit: a clause contributes the length of its literal list, and a node contributes the sum over its child OR circuits.
The number of literal occurrences in a normal-form OR circuit: a clause contributes the length of its literal list, and a node contributes the sum over its child AND circuits.
The total node count of a normal-form AND circuit: a clause has size \(1\), and a node has size \(1\) plus the sum of the sizes of its child OR circuits.
The total node count of a normal-form OR circuit: a clause has size \(1\), and a node has size \(1\) plus the sum of the sizes of its child AND circuits.
The depth of a normal-form AND circuit: a clause has depth \(0\), and a node has depth \(1\) plus the maximum depth among its child OR circuits.
The depth of a normal-form OR circuit: a clause has depth \(0\), and a node has depth \(1\) plus the maximum depth among its child AND circuits.
If a normal-form AND circuit \(c\) equals a clause built from literals \(lits\) with a duplication-free proof \(h\), then the variable indices \(lits.\mathrm{map}\; \mathrm{Lit.idx}\) are pairwise distinct.
If a normal-form OR circuit \(c\) equals a clause built from literals \(lits\) with a duplication-free proof \(h\), then the variable indices \(lits.\mathrm{map}\; \mathrm{Lit.idx}\) are pairwise distinct.
In a clause whose variable indices are pairwise distinct, any two literals \(l_1, l_2 \in lits\) that share the same index (\(l_1.\mathrm{idx} = l_2.\mathrm{idx}\)) are in fact equal, \(l_1 = l_2\).
Converts a general circuit into a normal-form AND circuit: a literal becomes a singleton clause; an AND node maps its children through \(\mathrm{toNOr}\); and an OR node is wrapped as a single OR node built from the children’s \(\mathrm{toNAnd}\) images, enforcing alternation.
Converts a general circuit into a normal-form OR circuit: a literal becomes a singleton clause; an OR node maps its children through \(\mathrm{toNAnd}\); and an AND node is wrapped as a single AND node built from the children’s \(\mathrm{toNOr}\) images, enforcing alternation.
A technical lemma: if \(g(h\, c) = f\, c\) for all \(c \in cs\), then the conjunctive foldr of \(g\) over \(cs.\mathrm{map}\; h\) equals the conjunctive foldr of \(f\) over \(cs\).
A technical lemma: if \(g(h\, c) = f\, c\) for all \(c \in cs\), then the disjunctive foldr of \(g\) over \(cs.\mathrm{map}\; h\) equals the disjunctive foldr of \(f\) over \(cs\).
A technical lemma: if \(g(h\, c) = f\, c\) for all \(c \in cs\), then the additive foldr of \(g\) over \(cs.\mathrm{map}\; h\) equals the additive foldr of \(f\) over \(cs\).
A technical lemma: if \(g(h\, c) \le k \cdot f\, c\) for all \(c \in cs\), then the additive foldr of \(g\) over \(cs.\mathrm{map}\; h\) is at most \(k\) times the additive foldr of \(f\) over \(cs\).
For every circuit \(c\) and assignment \(x\), both normalizations agree with the original on values: \((c.\mathrm{toNAnd}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\) and \((c.\mathrm{toNOr}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\).
For every circuit \(c\) and assignment \(x\), \((c.\mathrm{toNAnd}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\).
For every circuit \(c\) and assignment \(x\), \((c.\mathrm{toNOr}).\mathrm{eval}\, x = c.\mathrm{eval}\, x\).
For every circuit \(c\), both normalizations preserve the literal count: \((c.\mathrm{toNAnd}).\mathrm{litCount} = c.\mathrm{litCount}\) and \((c.\mathrm{toNOr}).\mathrm{litCount} = c.\mathrm{litCount}\).
For every circuit \(c\), \((c.\mathrm{toNAnd}).\mathrm{litCount} = c.\mathrm{litCount}\).
For every circuit \(c\), \((c.\mathrm{toNOr}).\mathrm{litCount} = c.\mathrm{litCount}\).
For every circuit \(c\), both normalizations have size at most twice the original: \((c.\mathrm{toNAnd}).\mathrm{size} \le 2\, c.\mathrm{size}\) and \((c.\mathrm{toNOr}).\mathrm{size} \le 2\, c.\mathrm{size}\).
For every circuit \(c\), \((c.\mathrm{toNAnd}).\mathrm{size} \le 2\, c.\mathrm{size}\).
For every circuit \(c\), \((c.\mathrm{toNOr}).\mathrm{size} \le 2\, c.\mathrm{size}\).
The forgetful map turning a normal-form AND circuit into a general circuit: a clause becomes an AND node over its literals, and a node becomes an AND node over the circuit images of its child OR circuits.
The forgetful map turning a normal-form OR circuit into a general circuit: a clause becomes an OR node over its literals, and a node becomes an OR node over the circuit images of its child AND circuits.
The normal-form AND circuit consisting of the single positive literal on variable \(i\).
The normal-form OR circuit consisting of the single positive literal on variable \(i\).
The constant-true AND circuit, given by the empty clause (an empty conjunction).
The constant-false OR circuit, given by the empty clause (an empty disjunction).
For a literal \(l\) with variable \(l.\mathrm{var}\) and polarity \(l.\mathrm{neg}\) and an assignment \(x\), the value is \(x_{l.\mathrm{var}}\) for a positive literal and \(\lnot x_{l.\mathrm{var}}\) for a negated one.
The width of a CNF formula \(c\), defined as the maximum width over its clauses (and \(0\) for the empty formula).
Evaluates a decision tree on an input \(x\): a leaf returns its stored bit, and a branch on variable \(i\) follows the high subtree when \(x_i\) is true and the low subtree otherwise.
The depth of a decision tree (maximum path length to a leaf): a leaf has depth \(0\) and a branch has depth \(1\) plus the maximum of its two subtrees’ depths.
Extracts a deepest root-to-leaf path from a decision tree, at each branch descending into the deeper subtree (ties broken toward the high subtree). It returns the list of \((\text{queried variable}, \text{branch direction})\) pairs along that path.
For every decision tree \(T\), the length of its deepest path equals its depth: \(T.\mathrm{deepPath}.\mathrm{length} = T.\mathrm{depth}\).
For a function \(f\), an index \(k \le n\), and an accumulator assignment \(acc\), the complete decision tree \(\mathrm{buildFullDTree}\, f\, k\, acc\) that queries variables \(k, k+1, \dots , n-1\) in order has depth at most \(n - k\).
For a function \(f\), an index \(k \le n\), and assignments \(acc, x\) agreeing on all coordinates below \(k\) (i.e. \(acc\, i = x\, i\) whenever \(i.\mathrm{val} \lt k\)), the complete decision tree \(\mathrm{buildFullDTree}\, f\, k\, acc\) evaluates to \(f\, x\) on \(x\).
38.3 Base literal, formula, and decision-tree definitions
A literal for Boolean circuits: a variable index \(\mathtt{idx} : \mathrm{Fin}\, n\) together with a polarity \(\mathtt{sign} : \mathrm{Bool}\) (true = positive occurrence).
A literal for switching-lemma formulas: a variable \(\mathtt{var} : \mathrm{Fin}\, n\) with a negation flag \(\mathtt{neg} : \mathrm{Bool}\) (true = negated literal).
A term is a conjunction of literals, represented as a list: \(\mathtt{Term}\, n = \mathtt{List}\, (\mathtt{Literal}\, n)\).
The width of a term is its number of literals (the list length).
A term evaluates to true on input \(x\) iff every literal in it holds under \(x\) (conjunction semantics).
A DNF formula is a disjunction of terms, represented as a list: \(\mathtt{DNF}\, n = \mathtt{List}\, (\mathtt{Term}\, n)\).
The width of a DNF formula is the maximum width of its terms (\(0\) for the empty formula).
A DNF formula evaluates to true on input \(x\) iff at least one of its terms holds under \(x\) (disjunction of conjunctions).
A CNF formula is a conjunction of clauses, each clause a disjunction of literals; it is represented as \(\mathtt{CNF}\, n = \mathtt{List}\, (\mathtt{Term}\, n)\) with dual evaluation semantics.
A single CNF clause evaluates to true on input \(x\) iff some literal in it holds under \(x\) (disjunction semantics).
A CNF formula evaluates to true on input \(x\) iff every clause holds under \(x\).
A decision tree on \(n\) Boolean variables: a leaf \(\mathtt{leaf}\, b\) outputs \(b\), and a branch \(\mathtt{branch}\, i\, lo\, hi\) queries variable \(i\), following \(lo\) on false and \(hi\) on true.
The complete decision tree for a function \(f\) that queries variables \(k, k+1, \dots , n-1\) in order, starting from accumulator assignment \(acc\), and outputs \(f\) applied to the completed assignment at each leaf.
The decision-tree depth of \(f : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) is the least \(d\) such that some decision tree of depth at most \(d\) computes \(f\); it is well defined since the full tree computes \(f\) at depth \(n\).