Combining circuits along a balanced tree

A circuit op reading two blocks of r inputs and producing r outputs combines circuits with r outputs: op.comp (C.append D) runs C and D side by side and feeds their outputs to op. Combining a list of k circuits in this way along a balanced binary tree (Circuit.balanced, by List.balancedFold) computes the balanced fold of their values under the function of op (Circuit.eval_balanced). It uses k - 1 copies of op (Circuit.size_balanced) and adds at most ⌈log₂ k⌉ times the depth of op to the depth of the deepest circuit (Circuit.depth_balanced_le). This is how a binary operation, such as the minimum, is computed on k arguments in logarithmic depth, and Formula.balanced is its analogue for formulas.

For an empty list the supplied fallback circuit is returned; the nonempty size formula does not charge the fallback. Appending circuits duplicates their programs, even on shared inputs.

Main definitions

• Cslib.Circuits.Circuit.balanced: circuits combined along a balanced binary tree.

Main results

• Cslib.Circuits.Circuit.eval_balanced: it computes the balanced fold of their values.
• Cslib.Circuits.Circuit.size_balanced: its size, for a nonempty list.
• Cslib.Circuits.Circuit.size_balanced_le: a uniform bound including the empty fallback.
• Cslib.Circuits.Circuit.depth_balanced_le: its depth.

References

This construction uses the balanced list folds of Complexity.Foundations.Data.List.BalancedFold.

def Cslib.Circuits.Circuit.balanced {σ : Signature} {n r : ℕ} (op : Circuit σ (r + r) r) (unit : Circuit σ n r) (l : List (Circuit σ n r)) : Circuit σ n r

The circuits of l combined by op along a balanced binary tree, or unit if l is empty: two circuits C and D are combined into op.comp (C.append D).

theorem Cslib.Circuits.Circuit.eval_balanced {σ : Signature} {n r : ℕ} {U : Type u_1} (I : Interpretation σ U) (op : Circuit σ (r + r) r) (unit : Circuit σ n r) (l : List (Circuit σ n r)) (x : Fin n → U) : (op.balanced unit l).eval I x = List.balancedFold (fun (u v : Fin r → U) => op.eval I (Fin.append u v)) (unit.eval I x) (fun (C : Circuit σ n r) => C.eval I x) l

Circuits combined by op along a balanced tree compute the balanced fold of their values under the function of op.

theorem Cslib.Circuits.Circuit.size_balanced {σ : Signature} {n r : ℕ} (op : Circuit σ (r + r) r) (unit : Circuit σ n r) {l : List (Circuit σ n r)} (hl : l ≠ []) : (op.balanced unit l).size = (List.map size l).sum + (l.length - 1) * op.size

A nonempty list of k circuits combined along a balanced tree uses k - 1 copies of op.

theorem Cslib.Circuits.Circuit.size_balanced_le {σ : Signature} {n r : ℕ} (op : Circuit σ (r + r) r) (unit : Circuit σ n r) (l : List (Circuit σ n r)) : (op.balanced unit l).size ≤ unit.size + (List.map size l).sum + l.length * op.size

A uniform gate bound also covering the empty fallback and an unused expensive operator.

theorem Cslib.Circuits.Circuit.depth_balanced_le {σ : Signature} {n r : ℕ} (op : Circuit σ (r + r) r) (unit : Circuit σ n r) {l : List (Circuit σ n r)} {D : ℕ} (hl : ∀ C ∈ l, C.depth ≤ D) (hunit : l = [] → unit.depth ≤ D) : (op.balanced unit l).depth ≤ D + op.depth * Nat.clog 2 l.length

Depth of a balanced tree of circuits. If every circuit of a list of k circuits has depth at most D, then combining them by op along a balanced tree gives depth at most D + depth op * ⌈log₂ k⌉.