24 Boolean Analysis — Circuit Reindex

24.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.

24.2 Declarations

Definition 24.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 24.2 Re-indexing preserves depth

✓

For every circuit \(c\) on \(m\) variables and every \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\), the re-indexed circuit has the same depth as \(c\), i.e. \(\mathrm{depth}(\mathrm{reidx}(c, f)) = \mathrm{depth}(c)\).

Theorem 24.3 Re-indexing commutes with evaluation

✓

For every circuit \(c\) on \(m\) variables, every \(f : \mathrm{Fin}\, m \to \mathrm{Fin}\, m'\), and every assignment \(g : \mathrm{Fin}\, m' \to \mathrm{Bool}\), evaluating the re-indexed circuit under \(g\) equals evaluating \(c\) under the pulled-back assignment \(g \circ f\), i.e. \(\mathrm{eval}(\mathrm{reidx}(c, f), g) = \mathrm{eval}(c, g \circ f)\).