Alternating layers for constructing shallow circuits

Layer n d is construction syntax: a signed input at depth zero, or a list of children at the preceding depth. Evaluation alternates AND and OR, starting with the supplied root operation. Its compiler produces an ordinary CSLib circuit, with exactly the counted AND/OR gates and no extra literal layer. Empty lists supply constants without introducing special constant gates.

This syntax records formulas, so duplicating a subtree duplicates its gates. It supplies upper-bound witnesses in CSLib's shared circuit model.

@[reducible, inline]

abbrev Complexity.Shallow.Layer (n : ℕ) : ℕ → Type

Alternating unbounded layers, with signed primary inputs at depth zero.

Equations

• Complexity.Shallow.Layer n 0 = (Fin n × Bool)
• Complexity.Shallow.Layer n d.succ = List (Complexity.Shallow.Layer n d)

def Complexity.Shallow.Layer.size {n d : ℕ} : Layer n d → ℕ

The number of AND/OR gates; literal occurrences are free.

Equations

• x_2.size = 0
• fs.size = 1 + (List.map Complexity.Shallow.Layer.size fs).sum

def Complexity.Shallow.Layer.eval {n d : ℕ} : AndOrOp → Layer n d → BitString n → Bool

Evaluate alternating layers, with op at the root.

Equations

• Complexity.Shallow.Layer.eval x✝¹ l x✝ = (l.2 ^^ x✝ l.1)
• Complexity.Shallow.Layer.eval Complexity.AndOrOp.and fs x✝ = List.all fs fun (f : Complexity.Shallow.Layer n n_1) => Complexity.Shallow.Layer.eval Complexity.AndOrOp.or f x✝
• Complexity.Shallow.Layer.eval Complexity.AndOrOp.or fs x✝ = List.any fs fun (f : Complexity.Shallow.Layer n n_1) => Complexity.Shallow.Layer.eval Complexity.AndOrOp.and f x✝

def Complexity.Shallow.Layer.mapInputs {n m : ℕ} (ρ : Fin n → Fin m × Bool) {d : ℕ} : Layer n d → Layer m d

Substitute signed inputs. This changes no gates or layers.

Equations

• Complexity.Shallow.Layer.mapInputs ρ x_2 = ((ρ x_2.1).1, x_2.2 ^^ (ρ x_2.1).2)
• Complexity.Shallow.Layer.mapInputs ρ fs = List.map (Complexity.Shallow.Layer.mapInputs ρ) fs

def Complexity.Shallow.Layer.neg {n d : ℕ} (f : Layer n d) : Layer n d

De Morgan negation flips the root operation and every input sign.

Equations

• f.neg = Complexity.Shallow.Layer.mapInputs (fun (i : Fin n) => (i, true)) f