arXiv:2607.19059 · v2
On the completeness of transformation rules in reversible logic synthesis
摘要
Transformation rules play a central role in reversible circuit optimization, template-based rewriting, and equivalence checking, and establishing their completeness is a fundamental problem in reversible logic synthesis. In this work, we investigate the completeness of transformation rules for reversible circuits both with and without ancillary bits and garbage outputs. For reversible circuits without ancillary bits and garbage outputs, we introduce a refined and complete transformation rule set $\mathcal{RC}^{r}$, obtained by replacing one rule in the rule set $\mathcal{RC}$ proposed in the previous work (TCAD, 45, pp. 3711--3724, 2026) with a simpler and widely adopted transformation rule. Since all rules in $\mathcal{RC}^{r}$ are commonly used in reversible logic synthesis, this result reveals that practically adopted transformation rules are already sufficient to establish a complete rewriting framework. Based on this result, we further propose an extended rule set, denoted by $\mathcal{RC}^+$, and prove its completeness for reversible circuits with ancillary bits and garbage outputs. To the best of our knowledge, this work presents the first complete transformation rule set for arbitrary reversible circuits, regardless of whether ancillary bits or garbage outputs are employed. The proposed framework establishes a theoretical foundation for circuit optimization, template generation, and equivalence checking, and may facilitate the development of automated design tools for reversible and quantum circuits.
作者备注：1. In Lemma 2 and Proposition 5, the definitions of the path gates incorrectly include the target among the controls. 2. In Lemma 1, the definition of T_i^n contains q_{i-1} while allowing i=0. Thus T_0^n refers to the undefined bit q_{-1}. Its proof states that the last element of H_k is 10^{k-1}. But it is actually 0^{k-1}1. 3. References [27] and [28] contain bibliographic errors