25 Boolean Analysis — Circuit Tree Manip
25.1 Overview
This module provides infrastructure for navigating and transforming the Circuit tree type used in the LMN layer-reduction argument. It supplies De Morgan dual conversions between DNF and CNF, structural facts about circuit depth, and the core “absorb one level” operation that folds the top level of a circuit into the Layer 2 gates, lowering the circuit depth by at least one while keeping every gate representable by a width-\(l\) DNF and CNF.
25.2 Declarations
The De Morgan dual of a DNF \(\varphi \) on \(n\) variables, obtained by negating every literal of every term and reading the result as a CNF. Concretely \(\neg \big(\bigvee _i \bigwedge _j \ell _{ij}\big) = \bigwedge _i \bigvee _j \neg \ell _{ij}\).
The dual CNF \(\mathrm{dnfToDualCNF}\, \varphi \) has the same width as \(\varphi \), since flipping the sign of each literal leaves the number of literals per term (and hence per clause) unchanged.
For every input \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), the dual CNF evaluates to the negation of the original DNF: \(\mathrm{CNF.eval}\, (\mathrm{dnfToDualCNF}\, \varphi )\, x = \neg (\mathrm{DNF.eval}\, \varphi \, x)\).
A circuit \(c\) with \(\mathrm{depth}\, c \geq 1\) is not a literal: there exist a Boolean flag \(\mathit{isAnd}\) and a child list \(cs\) with \(c = \mathrm{Circuit.node}\, \mathit{isAnd}\, cs\).
If a node \(\mathrm{Circuit.node}\, \mathit{isAnd}\, cs\) has depth at most \(1\), then every child \(c \in cs\) has depth \(0\).
A circuit \(c\) with \(\mathrm{depth}\, c = 0\) is a literal: there exists \(lr : \mathrm{Lit}\, m\) with \(c = \mathrm{Circuit.lit}\, lr\).
If a node \(\mathrm{Circuit.node}\, \mathit{isAnd}\, cs\) has depth at most \(1\), then every child \(c \in cs\) is a literal, i.e. \(c = \mathrm{Circuit.lit}\, lr\) for some \(lr\).
The Boolean function on \(\mathrm{Fin}\, n \to \mathrm{Bool}\) computed by a subcircuit \(c_{\mathrm{sub}}\) when each of its inputs \(i\) is replaced by the gate function \(\mathrm{gates}\, i\), namely \(x \mapsto c_{\mathrm{sub}}.\mathrm{eval}\, (\lambda i,\ \mathrm{gates}\, i\, x)\).
If, after applying a restriction \(\rho \), every gate function \(\mathrm{restrictFn}\, (\mathrm{gates}\, i).\mathrm{eval}\, \rho \) has decision-tree depth at most \(l\), then each gate admits both a width-\(l\) DNF representation (whose terms are duplicate-free and contain no two literals on the same variable) and a width-\(l\) CNF representation, each computing the same function.
Consider an OR node \(\mathrm{Circuit.node}\, \mathrm{false}\, cs\) whose children are all literals, where each gate function has a width-\(l\) DNF and a width-\(l\) CNF representation. Then the function computed by the node also has a width-\(l\) DNF \(\varphi \) with \(\varphi .\mathrm{eval}\, x = (\mathrm{Circuit.node}\, \mathrm{false}\, cs).\mathrm{eval}\, (\lambda i,\ \mathrm{gates}\, i\, x)\) for all \(x\).
Consider an AND node \(\mathrm{Circuit.node}\, \mathrm{true}\, cs\) whose children are all literals, where each gate function has a width-\(l\) DNF and a width-\(l\) CNF representation. Then the function computed by the node has a width-\(l\) CNF \(\psi \) with \(\mathrm{CNF.eval}\, \psi \, x = (\mathrm{Circuit.node}\, \mathrm{true}\, cs).\mathrm{eval}\, (\lambda i,\ \mathrm{gates}\, i\, x)\) for all \(x\).
Let \(c_{\mathrm{top}}\) have depth exactly \(1\) over the gates of some \(\mathrm{Layer2Data}\), where (with \(0 \lt l\)) each gate has a width-\(l\) DNF and CNF representation. Then there is a new \(\mathrm{Layer2Data}'\) of width at most \(l\) and a circuit \(c_{\mathrm{top}}'\) of depth \(0\) over it computing the same function as \(c_{\mathrm{top}}\) over the original gates.
A circuit \(c_j\) of depth at most \(1\) over gates that each have a width-\(l\) DNF and CNF representation admits a width-\(l\) DNF \(\varphi \) together with a sign bit such that, for all \(x\), the signed evaluation \(\big(\mathrm{if}\ \mathit{sign}\ \mathrm{then} \varphi .\mathrm{eval}\, x\ \mathrm{else}\ \neg \varphi .\mathrm{eval}\, x\big)\) equals \(c_j.\mathrm{eval}\, (\lambda i,\ \mathrm{gates}\, i\, x)\); moreover the terms of \(\varphi \) are duplicate-free with no repeated variable.
Given a list \(cs\) of circuits each of depth at most \(1\), over gates with width-\(l\) DNF and CNF representations, there are families \(\varphi _s\) of width-\(l\) DNFs (with duplicate-free, non-repeating-variable terms) and signs indexed by \(\mathrm{Fin}\, cs.\mathrm{length}\) such that, for each index \(j\), the signed evaluation of \(\varphi _s\, j\) matches \((cs.\mathrm{get}\, j).\mathrm{eval}\, (\lambda i,\ \mathrm{gates}\, i\, x)\) on every \(x\).
For any flag \(\mathit{isAnd}\), arity \(k\), and sign family \(\mathit{signs} : \mathrm{Fin}\, k \to \mathrm{Bool}\), there is a circuit \(c'\) of depth at most \(1\) that equals the node \(\mathrm{Circuit.node}\, \mathit{isAnd}\) over the literals \(\mathrm{Circuit.lit}\, \langle j, \mathit{signs}\, j\rangle \), evaluating identically on every input assignment \(g\).
A circuit \(c\) of depth exactly \(1\) over gates with width-\(l\) DNF and CNF representations collapses to a single signed gate: there exist a width-\(l\) DNF \(\varphi \) (with duplicate-free, non-repeating-variable terms) and a sign bit whose signed evaluation equals \(c.\mathrm{eval}\, (\lambda i,\ \mathrm{gates}\, i\, x)\) for all \(x\).
A circuit \(c\) of depth exactly \(2\) over gates with width-\(l\) DNF and CNF representations reduces to a circuit \(c'\) of depth at most \(1\) over a fresh gate family \(\mathrm{gates}'\) of width-\(l\) DNFs (with duplicate-free, non-repeating-variable terms), so that \(c\) and \(c'\) compute the same function on every \(x\).
Given a list \(cs\) of circuits where each child \(cs.\mathrm{get}\, j\) has been reduced to a circuit \(c_j\) of depth at most \(\mathrm{bound}\, j\) over its own width-\(l\) DNF gate family, this combines all the per-child gate families into a single merged family \(\mathrm{merged}\) indexed by \(\mathrm{Fin}\, M\), with re-indexed circuits \(\mathrm{new\_ cs}\, j\) of depth at most \(\mathrm{bound}\, j\) that reproduce each child’s function.
If each re-indexed child \(\mathrm{new\_ cs}\, j\) evaluated at \(g'\) agrees with the original child \(cs.\mathrm{get}\, j\) evaluated at \(g\), then the node over \(cs\) at \(g\) equals the node over \((\mathrm{List.finRange}\, cs.\mathrm{length}).\mathrm{map}\, \mathrm{new\_ cs}\) at \(g'\), for the same flag \(\mathit{isAnd}\).
For a circuit \(c\) of depth at least \(1\) (with \(0 \lt l\)) over gates that each have a width-\(l\) DNF representation with duplicate-free, non-repeating-variable terms and a width-\(l\) CNF representation, there exist a fresh gate family \(\mathrm{gates}'\) of such width-\(l\) DNFs and a circuit \(c'\) of depth at most \(\mathrm{depth}\, c - 1\) computing the same function as \(c\).
The \(\mathrm{Layer2Data}\) wrapper of the general depth reduction: for \(c_{\mathrm{top}}\) of depth at least \(2\) (with \(0 \lt l\)) over gates having width-\(l\) DNF and CNF representations, there are a new \(\mathrm{Layer2Data}'\) of width at most \(l\) and a circuit \(c_{\mathrm{top}}'\) of depth at most \(\mathrm{depth}\, c_{\mathrm{top}} - 1\) computing the same function.
The combined absorption step: for \(c_{\mathrm{top}}\) of depth at least \(1\) (with \(0 \lt l\)) over \(\mathrm{Layer2Data}\) gates having width-\(l\) DNF and CNF representations, there are a new \(\mathrm{Layer2Data}'\) of width at most \(l\) and a circuit \(c_{\mathrm{top}}'\) of depth at most \(\mathrm{depth}\, c_{\mathrm{top}} - 1\) computing the same function. This dispatches to the depth-1 case (giving depth \(0\)) and the general case (giving depth at most \(1\)).