Towards better understanding of gate elimination, the only method known that can prove complexity lower bounds for explicit functions against unrestricted Boolean circuits, this work contributes: (1) formalizing circuit simplifications as a convergent term graph rewriting system and (2) giving a simple and constructive proof of a classical lower bound using this system. First, we show that circuit simplification is a convergent term graph rewriting system over the DeMorgan and $\{\land, \lor, \oplus\}$ bases. We define local rewriting rules from Boolean identities such that every simplification sequence yields an identical final result (up to circuit isomorphism or bisimulation). Convergence enables rigorous reasoning about structural properties of simplified circuits without dependence on the order of simplification. Then, we show that there is \emph{no similar} convergent formalization of circuit simplification over the $U_2$ and $B_2$ bases. Then, we use our simplification system to give a constructive circuit lower bound, generalizing Schnorr's classical result that the XOR function requires $3(n - 1)$ gates to compute in the DeMorgan basis. A constructive lower bound $f \not\in C$ gives an algorithm (called a "refuter") that efficiently finds counter-examples for every $C$-circuit trying to compute the function $f$. Chen, Jin, Santhanam, and Williams showed that constructivity plays a central role in many longstanding open problems about complexity theory (FOCS 2021), so it is natural to ask for constructive circuit lower bounds from gate elimination arguments. This demonstrates how using convergent simplification can lead to shorter and more modular proofs of circuit lower bounds. Furthermore, until this work, no constructive lower bound had been proved via gate elimination.

翻译：为更好地理解门限消除这一目前已知唯一能针对显式函数在无限制布尔电路上证明复杂度下界的方法，本工作做出以下贡献：(1) 将电路简化形式化为收敛的项图重写系统；(2) 利用该系统给出经典下界的简洁构造性证明。首先，我们证明在DeMorgan基和$\{\land, \lor, \oplus\}$基上，电路简化构成收敛的项图重写系统。我们基于布尔恒等式定义局部重写规则，使得任意简化序列都能产生（在电路同构或互模拟意义下）相同的最终结果。收敛性使得我们能够严格推理简化电路的结构性质，而不依赖于简化顺序。其次，我们证明在$U_2$基和$B_2$基上不存在类似的电路简化收敛形式化方法。随后，我们利用简化系统给出构造性电路下界，推广了Schnorr关于XOR函数在DeMorgan基中计算需要$3(n - 1)$个门限的经典结果。构造性下界$f \not\in C$提供了一个算法（称为“反驳器”），该算法能高效地为每个试图计算函数$f$的$C$电路找到反例。Chen、Jin、Santhanam和Williams的研究表明（FOCS 2021），构造性在复杂性理论许多长期悬而未决的问题中起着核心作用，因此自然需要从门限消除论证中寻求构造性电路下界。本工作展示了如何利用收敛简化获得更简洁、更具模块性的电路下界证明。此外，在本工作之前，尚未有通过门限消除方法证明的构造性下界。