124 Complexity — Feed Forward
124.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.TreeCircuit 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.
124.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 number of its non-input nodes, i.e. the total number of nodes lying in layers \(1, \dots , \mathrm{depth}(F)\).
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\).
Let \(C\) be a Boolean circuit on \(n\) variables. Then the size of \(C\) — the total number of literal leaves and internal AND/OR gates — is at least \(1\); that is, \(1 \le \mathrm{size}(C)\).
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.TreeCircuit.
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.
Let \(F\) be a Boolean feedforward circuit whose inputs are indexed by \(\mathrm{Fin}\, n\), and suppose each of its gates has finite arity and computes either the conjunction or the disjunction of its inputs, according to a flag marking every non-input node as an AND node or an OR node. Then for every layer \(m\) with \(m \le \mathrm{depth}(F)\), every node \(v\) of layer \(m\), and every input assignment \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\), the Boolean circuit obtained by tree-unrolling \(v\), evaluated at \(x\), equals the value that \(v\) takes in \(F\) under the assignment \(x\).
Let \(F\) be a Boolean feedforward circuit from the inputs \(\mathrm{Fin}\, n\) to an output type, in which every gate has finitely many input wires, and suppose \(k \in \mathbb {N}\) bounds these arities, so that each gate has at most \(k\) input wires. Then for every layer \(m \le \mathrm{depth}(F)\) and every node \(v\) of layer \(m\), the tree-unrolling of \(v\) is a Boolean circuit of 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.
Let \(F\) be a Boolean feedforward circuit with input variables indexed by \(\mathrm{Fin}\, n\) and output nodes of type \(\mathrm{out}\), equipped with a flag assigning to each non-input node the label AND or OR and a witness that each gate has finite arity. Suppose \(F\) is an AND/OR circuit: every gate computes the conjunction of the values on its input wires when its node is labelled AND, and their disjunction when it is labelled OR. Then for every output node \(o\) and every assignment \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\), the tree-shaped Boolean circuit obtained by unrolling \(o\) from the last layer down to the inputs, evaluated at \(x\), agrees with the value that \(F\) itself assigns to \(o\) under the input assignment \(x\).
Let \(F\) be a layered feedforward circuit over the Boolean alphabet with input type \(\mathrm{Fin}\, n\) and output type \(\mathrm{out}\), of depth \(d\), in which each gate is designated an AND gate or an OR gate. Suppose every gate has finite input arity, and that there is a bound \(k \in \mathbb {N}\) such that every gate reads from at most \(k\) input wires. Then for each output node \(o\), the tree-unrolled Boolean circuit obtained from \(o\) has size (its total number of AND/OR gates and literal leaves) at most \((k+1)^{d}\).
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.
Let \(C\) be a Boolean circuit on \(n\) variables and let \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\) be an assignment of Boolean values to the inputs of \(C\). The feedforward embedding of \(C\) is a layered circuit of depth \(\mathrm{depth}(C) + 1\) whose layer \(0\) carries the \(n\) input variables and each of whose higher layers carries a single node. Then for every layer index \(m\) with \(1 \le m \le \mathrm{depth}(C) + 1\) and every node \(v\) of layer \(m\), the value assigned to \(v\) by the feedforward embedding on input \(x\) equals \(\mathrm{eval}(C, x)\), the value of \(C\) on \(x\).
Let \(C\) be a Boolean circuit on \(n\) variables, and let \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\) be an assignment of Boolean values to those variables. Form the feedforward embedding of \(C\), a layered feedforward circuit with a single output wire, and let its unique output value under \(x\) be the Boolean it computes. Then this value equals \(C(x)\), the value obtained by evaluating the circuit \(C\) directly on the assignment \(x\).
Let \(C\) be a Boolean circuit on \(n\) variables, with depth \(\mathrm{depth}(C)\) equal to the length of the longest root-to-leaf path in \(C\). Embedding \(C\) as a layered feedforward circuit — in which layer \(0\) carries the \(n\) input variables and each higher layer carries a single wire — produces a circuit whose depth equals \(\mathrm{depth}(C) + 1\).
Let \(C\) be a Boolean circuit on \(n\) variables, and let \(\mathrm{size}(C)\) and \(\mathrm{depth}(C)\) denote its total number of nodes and its depth, respectively. Writing \(\widehat{C}\) for the layered feedforward circuit obtained by embedding \(C\), the number of non-input nodes of \(\widehat{C}\) satisfies
124.3 Additional declarations
A single operation in a feedforward circuit over an alphabet \(\alpha \): it consists of an arity type \(\iota \) together with a function \((\iota \to \alpha ) \to \alpha \) that computes the gate’s output value from the values supplied on its input slots.