Circuit-family outputs as formula families -- definitions

These definitions connect typed, length-indexed CircuitFamily semantics to the total-assignment convention used by the Barrington development.

def Complexity.BoolFunFamily.onTotalAssignments (f : BoolFunFamily) : ℕ → (ℕ → Bool) → Bool

View a typed Boolean-function family on total assignments by restricting an assignment to the first n variables at family index n.

Equations

• f.onTotalAssignments n assignment = f n fun (input : Fin n) => assignment ↑input

def Complexity.CircuitFamily.outputFormulaFamily (F : CircuitFamily Basis.andOr2) : FormulaFamily

Unfold the unique output of each positive-length fan-in-two circuit into a formula. The explicit empty-input answer becomes a Boolean constant.

Equations

• F.outputFormulaFamily 0 = if F.emptyOutput = true then Complexity.BoolFormula.tru else Complexity.BoolFormula.fls
• F.outputFormulaFamily n.succ = (F.circuit (n + 1)).outputFormula 0