129 Boolean Analysis — Feed Forward Circuit
129.1 Overview
This file introduces layered feedforward circuits over an arbitrary alphabet \(\alpha \): gates with explicit input wiring, the evaluation of nodes and of the whole circuit, and the basic complexity measures (depth, size, finiteness, gate set restriction). It then relates feedforward circuits to the tree-shaped BoolCircuit.Circuit in both directions: tree-unrolling a layered AND/OR circuit into a tree (with an exponential-in-depth size bound), and embedding a tree circuit back as a feedforward circuit padded with identity wires.
129.2 Declarations
A gate over alphabet \(\alpha \) with input domain domain consists of a gate operation op (an arity type \(\iota \) together with a function \((\iota \to \alpha ) \to \alpha \)) and a wiring map \(\iota \to \texttt{domain}\) that assigns to each input slot the node it reads from.
A feedforward circuit from inp to out over \(\alpha \) consists of a depth \(d \in \mathbb {N}\), a family of node types indexed by the layers \(\mathrm{Fin}\, (d+1)\), and, for every layer \(i \lt d\), a gate for each node of layer \(i+1\) whose inputs are wired to nodes of layer \(i\). Layer \(0\) is required to be the input type inp and the last layer the output type out.
The gate operation of arity \(\mathrm{PUnit}\) that returns its single input unchanged.
Given a gate \(g\) and an assignment \(xs\) of values to the nodes of its input domain, the value of \(g\) is \(g.\texttt{op}.\texttt{func}\, (xs \circ g.\texttt{inputs})\), i.e. the gate operation applied to the values read along the input wires.
For an input assignment \(xs : \texttt{inp} \to \alpha \), the value of a node at layer \(d\) is defined by recursion on \(d\): a layer-\(0\) node is read off directly from \(xs\), and a node at layer \(n+1\) evaluates its gate on the values of the layer-\(n\) nodes.
The function \(\texttt{out} \to \alpha \) sending each output node to its value in the last layer under the input assignment \(xs\).
When the output type is a Unique type, the single value \(F.\texttt{eval}\, xs\, \texttt{default} \in \alpha \) computed by the circuit.
The size of \(F\) is the cardinality \(\mathrm{Nat.card}\) of the sigma type of all non-input nodes, i.e. the total number of nodes lying in layers \(1,\dots ,\texttt{depth}\).
The proposition that the node type of every layer \(i\) is finite.
For a set \(S\) of gate operations, \(\texttt{onlyUsesGates}\ S\) asserts that the operation of every gate of the circuit belongs to \(S\).
For every Boolean circuit \(C\) on \(n\) inputs, \(1 \le C.\texttt{size}\).
Given a Boolean feedforward circuit \(F\), a flag \(\texttt{isAnd}\) on each non-input node and a finiteness witness \(\texttt{gfin}\) for each gate’s arity, \(F.\texttt{IsAndOrGate}\) asserts that every gate operation is the conjunction of its inputs when the flag is true and their disjunction when it is false, the inputs being enumerated by \(\texttt{gfin}\). This is the gate restriction under which \(F\) can be converted into a BoolCircuit.Circuit.
Recursively expands a node \(v\) of layer \(m\) of a Boolean feedforward circuit into a tree-shaped \(\texttt{Circuit}\ n\): a layer-\(0\) node becomes the positive literal of the corresponding input variable, and a node at a higher layer becomes an AND/OR node whose children are the unrollings of the nodes on its input wires. Nodes feeding several downstream gates are duplicated.
If every gate of \(F\) is an AND or OR gate as recorded by \(\texttt{isAnd}\) and \(\texttt{gfin}\), then for every node \(v\) at layer \(m\) and every input \(x : \mathrm{Fin}\, n \to \{ 0,1\} \),
If every gate of \(F\) has at most \(k\) input wires, i.e. \(\mathrm{card}\, (F.\texttt{gates}\ d\ v).\texttt{op}.\iota \le k\) for all \(d\) and \(v\), then the unrolling of any node at layer \(m\) has size at most \((k+1)^m\).
For an AND/OR feedforward circuit \(F\) and a chosen output node \(o : \texttt{out}\), the tree-shaped \(\texttt{Circuit}\ n\) obtained by tree-unrolling \(o\) from the last layer down to the inputs.
If every gate of \(F\) is an AND or OR gate, then for every output node \(o\) and every input \(x\),
If every gate of \(F\) has at most \(k\) input wires, then for every output node \(o\) the tree-unrolled circuit satisfies \((F.\texttt{toCircuit}\ \texttt{isAnd}\ \texttt{gfin}\ o).\texttt{size} \le (k+1)^{F.\texttt{depth}}\).
Turns a circuit \(C\) on \(n\) inputs into a feedforward circuit \(\texttt{FeedForward}\ \texttt{Bool}\ (\mathrm{Fin}\, n)\ \mathrm{Unit}\) of depth \(C.\texttt{depth} + 1\): layer \(0\) carries the \(n\) input variables and every higher layer carries a single wire. The gate from layer \(0\) to layer \(1\) computes \(C.\texttt{eval}\) from all inputs at once, and all later gates are identity wires that pass the single Boolean value upward.
For every input \(x\), every layer index \(m\) with \(0 \lt m\) and every node \(v\) of layer \(m\) of \(C.\texttt{toFeedForward}\), the value of \(v\) is \(C.\texttt{toFeedForward}.\texttt{evalNode}\ v\ x = C.\texttt{eval}\ x\).
For every circuit \(C\) on \(n\) inputs and every input \(x\), \(C.\texttt{toFeedForward}.\texttt{eval}_1\ x = C.\texttt{eval}\ x\).
The embedding uses one extra layer for the inputs: \(C.\texttt{toFeedForward}.\texttt{depth} = C.\texttt{depth} + 1\).
For every circuit \(C\) on \(n\) inputs, \(C.\texttt{toFeedForward}.\texttt{size} \le C.\texttt{size} \cdot (C.\texttt{depth} + 1)\).