21 Boolean Analysis — Circuit Reindex

21.1 Overview

This module provides infrastructure for re-indexing the gate inputs of a Boolean circuit: it defines an operation that maps the variable indices of a circuit through a function \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\), and proves that this operation preserves circuit depth and commutes with evaluation.

21.2 Declarations

Definition 21.1 Re-indexing a circuit

✓

Given a circuit \(c\) on \(m\) variables and a function \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\), the re-indexed circuit \(\mathrm{reidx}(c, f)\) on \(m'\) variables is obtained by replacing each literal index \(i\) by \(f(i)\) (keeping its sign) and recursing structurally through the \(\mathrm{And}/\mathrm{Or}\) nodes.

Theorem 21.2 Re-indexing preserves circuit depth

✓

Let \(c\) be a Boolean circuit on \(m\) variables and let \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\) be any map of variable indices. Then re-indexing \(c\) along \(f\) leaves its depth unchanged: \(\mathrm{depth}(\mathrm{reidx}(c, f)) = \mathrm{depth}(c)\).

Theorem 21.3 Re-indexing commutes with evaluation

✓

Let \(c\) be a Boolean circuit on \(m\) variables, let \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\) be a re-indexing map, and let \(g : \mathrm{Fin}\, m' \to \mathbb {F}_2\) be an assignment to the \(m'\) variables. Then evaluating the re-indexed circuit \(\mathrm{reidx}(c, f)\) under \(g\) gives the same value as evaluating the original circuit \(c\) under the pulled-back assignment \(g \circ f\):

\[ \mathrm{eval}\big(\mathrm{reidx}(c, f),\, g\big) = \mathrm{eval}\big(c,\, g \circ f\big). \]