Depths along program lines, and depths with costs

Every wire read by a gate is shallower than the gate (Program.wireDepths_lines_lt), which is what makes induction on depth go through for programs.

The depth with costs (Circuit.depthWith cost) charges cost op for a gate of operation op instead of one, so it is the largest total cost of the gates on a path to an output. Unit costs give Circuit.depth (Circuit.depthWith_one). With free negations it is the largest number of AND and OR gates on a path in a circuit over the unbounded fan-in basis, the depth of AC⁰ circuits with negations at the inputs.

Main definitions

• Cslib.Circuits.Line.depthWith, Cslib.Circuits.Program.depthsWith, Cslib.Circuits.Program.wireDepthsWith, Cslib.Circuits.Circuit.depthWith: depths with costs.

Main results

• Fin.foldl_max_eq_max_sup: folding max is taking the supremum, so depths are suprema (Cslib.Circuits.Line.depthWith_eq_sup, Cslib.Circuits.Circuit.depthWith_eq_sup).
• Cslib.Circuits.Program.depths_eq_depth_lines: the depth of a gate is the depth of its line.
• Cslib.Circuits.Program.wireDepths_lines_lt: the wires a gate reads are shallower than it.
• Cslib.Circuits.Program.depths_pos: gates have positive depth.
• Cslib.Circuits.Program.wireDepthsWith_lines_add_le: with costs, the wires a gate reads are shallower than it by at least its cost.
• Cslib.Circuits.Circuit.depthWith_one: unit costs give the depth.
• Cslib.Circuits.Circuit.depthWith_le_iff, Cslib.Circuits.Circuit.depthWith_mono: bounds, and monotonicity in the costs.
• Cslib.Circuits.Circuit.depthWith_le_depth: costs of at most one never increase the depth.
• Cslib.Circuits.Circuit.depthWith_le_mul_depth: if every gate costs at most b, the depth with costs is at most b times the depth.

theorem Fin.foldl_max_eq_max_sup {α : Type u_1} [LinearOrder α] [OrderBot α] {m : ℕ} (f : Fin m → α) (init : α) : foldl m (fun (acc : α) (i : Fin m) => max acc (f i)) init = max init (Finset.univ.sup f)

Folding max over the values of f, from init, gives the larger of init and their supremum.

theorem Cslib.Circuits.Line.wireDepth_lt_depth {σ : Signature} {n g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ) (a : Fin (σ.Arity line.op)) : depths (line.wires a) < line.depth depths

A gate is deeper than every wire it reads.

theorem Cslib.Circuits.Program.depths_eq_depth_lines {σ : Signature} {n g : ℕ} (p : Program σ n g) (k : Fin g) : p.depths k = (p.lines k).depth p.wireDepths

The depth of a gate of a program is the depth of its line, over the depths of the wires.

theorem Cslib.Circuits.Program.wireDepths_lines_lt {σ : Signature} {n g : ℕ} (p : Program σ n g) (k : Fin g) (a : Fin (σ.Arity (p.lines k).op)) : p.wireDepths ((p.lines k).wires a) < p.depths k

The wires read by a gate of a program are shallower than the gate.

theorem Cslib.Circuits.Program.depths_pos {σ : Signature} {n g : ℕ} (p : Program σ n g) (k : Fin g) : 0 < p.depths k

Every gate of a program has positive depth.

Depth with costs

The depth of a wire when each operation op costs cost op instead of one: the largest total cost of the gates on a path to the wire. With negations costing nothing, it is the largest number of AND and OR gates on a path, the depth of AC⁰ circuits with negations at the inputs.

def Cslib.Circuits.depthInterpretation {σ : Signature} (cost : σ.Op → ℕ) : Interpretation σ ℕ

The depth interpretation takes the largest argument depth and adds the operation's cost. In particular, a nullary gate contributes its own cost.

def Cslib.Circuits.Line.depthWith {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (line : Line σ n g) (wireDepths : Wire n g → ℕ) : ℕ

The depth of a line when its operation costs cost op.

theorem Cslib.Circuits.Line.depthWith_eq_sup {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (line : Line σ n g) (depths : Wire n g → ℕ) : depthWith cost line depths = (Finset.univ.sup fun (a : Fin (σ.Arity line.op)) => depths (line.wires a)) + cost line.op

The depth of a line with costs is the largest depth of the wires it reads plus its cost.

theorem Cslib.Circuits.Line.cost_le_depthWith {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (line : Line σ n g) (depths : Wire n g → ℕ) : cost line.op ≤ depthWith cost line depths

A line is at least as deep as its cost.

theorem Cslib.Circuits.Line.wireDepth_add_le_depthWith {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (line : Line σ n g) (depths : Wire n g → ℕ) (a : Fin (σ.Arity line.op)) : depths (line.wires a) + cost line.op ≤ depthWith cost line depths

A line is at least as deep as every wire it reads plus its cost.

@[simp]

theorem Cslib.Circuits.Line.depthWith_one {σ : Signature} {n g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ) : depthWith 1 line depths = line.depth depths

With unit costs, Line.depthWith is Line.depth.

theorem Cslib.Circuits.depthInterpretation_le_add {σ : Signature} (cost : σ.Op → ℕ) (op : σ.Op) {depths depths' : Fin (σ.Arity op) → ℕ} {D : ℕ} (h : ∀ (a : Fin (σ.Arity op)), depths a ≤ depths' a + D) : depthInterpretation cost op depths ≤ depthInterpretation cost op depths' + D

Raising argument depths by at most D raises an operation's depth by at most D.

theorem Cslib.Circuits.Line.depthWith_le_add {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (line : Line σ n g) {depths depths' : Wire n g → ℕ} {D : ℕ} (h : ∀ (a : Fin (σ.Arity line.op)), depths (line.wires a) ≤ depths' (line.wires a) + D) : depthWith cost line depths ≤ depthWith cost line depths' + D

Raising the depths of the wires by at most D raises the depth of a line by at most D.

theorem Cslib.Circuits.Line.depthWith_eq_cost {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (line : Line σ n g) {depths : Wire n g → ℕ} (h : ∀ (a : Fin (σ.Arity line.op)), depths (line.wires a) = 0) : depthWith cost line depths = cost line.op

A line reading only wires of depth zero has the depth of its cost.

theorem Cslib.Circuits.Line.depthWith_mono {σ : Signature} {n g : ℕ} {cost cost' : σ.Op → ℕ} (hcost : ∀ (op : σ.Op), cost op ≤ cost' op) {depths depths' : Wire n g → ℕ} (hdepths : ∀ (w : Wire n g), depths w ≤ depths' w) (line : Line σ n g) : depthWith cost line depths ≤ depthWith cost' line depths'

Line.depthWith is monotone in the costs and in the depths of the wires.

def Cslib.Circuits.Program.depthsWith {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) : Fin g → ℕ

The depth of every gate is evaluation in the depth interpretation, with zero-depth inputs.

def Cslib.Circuits.Program.wireDepthsWith {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) : Wire n g → ℕ

The depth of every wire of a program when each operation op costs cost op.

@[simp]

theorem Cslib.Circuits.Program.wireDepthsWith_input {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (i : Fin n) : wireDepthsWith cost p (Wire.input i) = 0

@[simp]

theorem Cslib.Circuits.Program.wireDepthsWith_gateWire {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (k : Fin g) : wireDepthsWith cost p (Wire.gate k) = depthsWith cost p k

@[simp]

theorem Cslib.Circuits.Program.depthsWith_gate_last {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (line : Line σ n g) : depthsWith cost (p.gate line) (Fin.last g) = Line.depthWith cost line (wireDepthsWith cost p)

@[simp]

theorem Cslib.Circuits.Program.depthsWith_gate_castSucc {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (line : Line σ n g) (j : Fin g) : depthsWith cost (p.gate line) j.castSucc = depthsWith cost p j

@[simp]

theorem Cslib.Circuits.Program.wireDepthsWith_gate_castSucc {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (line : Line σ n g) (w : Wire n g) : wireDepthsWith cost (p.gate line) w.castSucc = wireDepthsWith cost p w

theorem Cslib.Circuits.Program.depthsWith_eq_depthWith_lines {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (k : Fin g) : depthsWith cost p k = Line.depthWith cost (p.lines k) (wireDepthsWith cost p)

The depth of a gate is the depth of its line over the depths of the wires.

theorem Cslib.Circuits.Program.cost_le_depthsWith {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (k : Fin g) : cost (p.lines k).op ≤ depthsWith cost p k

A gate is at least as deep as its cost.

@[simp]

theorem Cslib.Circuits.Program.depthsWith_one {σ : Signature} {n g : ℕ} (p : Program σ n g) : depthsWith 1 p = p.depths

With unit costs, Program.depthsWith is Program.depths.

@[simp]

theorem Cslib.Circuits.Program.wireDepthsWith_one {σ : Signature} {n g : ℕ} (p : Program σ n g) : wireDepthsWith 1 p = p.wireDepths

With unit costs, Program.wireDepthsWith is Program.wireDepths.

theorem Cslib.Circuits.Program.depthsWith_mono {σ : Signature} {n g : ℕ} {cost cost' : σ.Op → ℕ} (hcost : ∀ (op : σ.Op), cost op ≤ cost' op) (p : Program σ n g) (k : Fin g) : depthsWith cost p k ≤ depthsWith cost' p k

Program.depthsWith is monotone in the costs.

theorem Cslib.Circuits.Program.wireDepthsWith_mono {σ : Signature} {n g : ℕ} {cost cost' : σ.Op → ℕ} (hcost : ∀ (op : σ.Op), cost op ≤ cost' op) (p : Program σ n g) (w : Wire n g) : wireDepthsWith cost p w ≤ wireDepthsWith cost' p w

Program.wireDepthsWith is monotone in the costs.

theorem Cslib.Circuits.Program.wireDepthsWith_lines_add_le {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (k : Fin g) (a : Fin (σ.Arity (p.lines k).op)) : wireDepthsWith cost p ((p.lines k).wires a) + cost (p.lines k).op ≤ depthsWith cost p k

The wires read by a gate are shallower than the gate by at least its cost.

def Cslib.Circuits.Circuit.depthWith {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) {m : ℕ} (c : Circuit σ n m) : ℕ

The largest depth of an output when each operation op costs cost op.

theorem Cslib.Circuits.Circuit.depthWith_eq_sup {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) {m : ℕ} (c : Circuit σ n m) : depthWith cost c = Finset.univ.sup fun (j : Fin m) => Program.wireDepthsWith cost c.program (c.outputs j)

The depth of a circuit with costs is the largest depth of its outputs.

theorem Cslib.Circuits.Circuit.depthWith_le_iff {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) {m : ℕ} (c : Circuit σ n m) {D : ℕ} : depthWith cost c ≤ D ↔ ∀ (j : Fin m), Program.wireDepthsWith cost c.program (c.outputs j) ≤ D

A circuit has depth at most D with costs exactly when all its outputs do.

theorem Cslib.Circuits.Circuit.wireDepthsWith_outputs_le_depthWith {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) {m : ℕ} (c : Circuit σ n m) (j : Fin m) : Program.wireDepthsWith cost c.program (c.outputs j) ≤ depthWith cost c

Every output is at most as deep, with costs, as the circuit.

@[simp]

theorem Cslib.Circuits.Circuit.depthWith_one {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : depthWith 1 c = c.depth

With unit costs, Circuit.depthWith is Circuit.depth.

theorem Cslib.Circuits.Circuit.depthWith_mono {σ : Signature} {n : ℕ} {cost cost' : σ.Op → ℕ} (hcost : ∀ (op : σ.Op), cost op ≤ cost' op) {m : ℕ} (c : Circuit σ n m) : depthWith cost c ≤ depthWith cost' c

Circuit.depthWith is monotone in the costs.

@[simp]

theorem Cslib.Circuits.Circuit.depthWith_wiring {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) {m : ℕ} (select : Fin m → Fin n) : depthWith cost (wiring σ select) = 0

@[simp]

theorem Cslib.Circuits.Circuit.depthWith_zero_outputs {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) (c : Circuit σ n 0) : depthWith cost c = 0

theorem Cslib.Circuits.Circuit.depthWith_le_depth {σ : Signature} {n : ℕ} {cost : σ.Op → ℕ} (hcost : ∀ (op : σ.Op), cost op ≤ 1) {m : ℕ} (c : Circuit σ n m) : depthWith cost c ≤ c.depth

Costs of at most one never increase the depth.

theorem Cslib.Circuits.Program.depthsWith_le_mul_depths {σ : Signature} {n g : ℕ} {cost : σ.Op → ℕ} {b : ℕ} (p : Program σ n g) (h : ∀ (k : Fin g), cost (p.lines k).op ≤ b) (k : Fin g) : depthsWith cost p k ≤ b * p.depths k

If every gate of a program costs at most b, every gate is at most b times as deep with costs as without.

theorem Cslib.Circuits.Program.wireDepthsWith_le_mul_wireDepths {σ : Signature} {n g : ℕ} {cost : σ.Op → ℕ} {b : ℕ} (p : Program σ n g) (h : ∀ (k : Fin g), cost (p.lines k).op ≤ b) (w : Wire n g) : wireDepthsWith cost p w ≤ b * p.wireDepths w

If every gate of a program costs at most b, every wire is at most b times as deep with costs as without.

theorem Cslib.Circuits.Circuit.depthWith_le_mul_depth {σ : Signature} {n : ℕ} {cost : σ.Op → ℕ} {b m : ℕ} (c : Circuit σ n m) (h : ∀ (k : Fin c.size), cost (c.program.lines k).op ≤ b) : depthWith cost c ≤ b * c.depth

If every gate of a circuit costs at most b, its depth with costs is at most b times its depth.