Conditional circuit complexity

For a target f and a finite family supplied of functions of the same input, Circuit.conditionalGateComplexity interpretation f supplied is the minimum number of gates in a circuit h satisfying h(x, supplied(x)) = f(x). The original input coordinates and the supplied values are free; only the gates of h are charged. Correctness is required on these consistent tuples, with no restriction on h(x, y) when y ≠ supplied(x).

The family is represented as supplied : Target U n k, so a list of scalar functions g : Fin k → ScalarFunction U n is supplied as fun x i => g i x. Targets may have multiple outputs and share gates. The weighted version is Circuit.conditionalCostComplexity; both measures take values in ℕ∞, with ⊤ for targets that cannot be computed even with the supplied values.

CSLib's Boolean Synthesis instead bounds additional gates relative to every program already making a source family available, while preserving all of that program's available functions. It is a budget predicate, not this minimum over circuits with formal supplied inputs. The implication from a conditional gate bound to Synthesis is in Algebraic.ConditionalComplexity.Boolean.

References

Stephen Wayne Boyack, The Robustness of Combinatorial Measures of Boolean Matrix Complexity, MIT PhD thesis (1985), p. 30, defines circuit complexity relative to supplied functions and proves the triangle inequality in Proposition 2.2. Here the original coordinates are always supplied as well: our C(f | G) corresponds to supplying (id, G) in that convention. See https://hdl.handle.net/1721.1/15322.

def Cslib.Circuits.Circuit.ComputesGiven {σ : Signature} {n k m : ℕ} {U : Type u_2} (circuit : Circuit σ (n + k) m) (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : Prop

Compute target from the original inputs and the free values of supplied. Only inputs of the form (x, supplied x) constrain the circuit.

Equations

• circuit.ComputesGiven interpretation target supplied = circuit.ComputesFrom interpretation target fun (input : Fin n → U) => Fin.append input (supplied input)

noncomputable def Cslib.Circuits.Circuit.conditionalCostComplexity {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : ℕ∞

Minimum weighted cost of computing target with the values of supplied supplied as free extra inputs. Unrepresentable targets have value ⊤.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Cslib.Circuits.Circuit.conditionalGateComplexity {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : ℕ∞

Minimum number of gates computing target from the original inputs and the free values of supplied.

Equations

• Cslib.Circuits.Circuit.conditionalGateComplexity interpretation target supplied = Cslib.Circuits.Circuit.conditionalCostComplexity interpretation Algebraic.OperationCost.unit target supplied

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_le {σ : Signature} {n k m : ℕ} {U : Type u_2} {circuit : Circuit σ (n + k) m} {interpretation : Interpretation σ U} {target : Algebraic.Target U n m} {supplied : Algebraic.Target U n k} (operationCost : Algebraic.OperationCost σ) (computes : circuit.ComputesGiven interpretation target supplied) : conditionalCostComplexity interpretation operationCost target supplied ≤ ↑(circuit.cost operationCost)

A concrete conditional implementation bounds the minimum weighted cost.

theorem Cslib.Circuits.Circuit.le_conditionalCostComplexity {σ : Signature} {U : Type u_2} {n m k : ℕ} {interpretation : Interpretation σ U} {target : Algebraic.Target U n m} {supplied : Algebraic.Target U n k} (operationCost : Algebraic.OperationCost σ) (bound : ℕ∞) (lowerBound : ∀ (circuit : Circuit σ (n + k) m), circuit.ComputesGiven interpretation target supplied → bound ≤ ↑(circuit.cost operationCost)) : bound ≤ conditionalCostComplexity interpretation operationCost target supplied

A bound holding for every conditional implementation bounds the minimum.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_le_iff {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) (budget : ℕ) : conditionalCostComplexity interpretation operationCost target supplied ≤ ↑budget ↔ ∃ (circuit : Circuit σ (n + k) m), circuit.ComputesGiven interpretation target supplied ∧ circuit.cost operationCost ≤ budget

A finite budget bounds conditional complexity exactly when some circuit meets that budget. In particular, every finite minimum is attained.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_lt_top_iff {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : conditionalCostComplexity interpretation operationCost target supplied < ⊤ ↔ ∃ (circuit : Circuit σ (n + k) m), circuit.ComputesGiven interpretation target supplied

Conditional complexity is finite exactly when some conditional implementation exists; the supplied functions need not be representable.

@[simp]

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_eq_top_iff {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : conditionalCostComplexity interpretation operationCost target supplied = ⊤ ↔ ¬∃ (circuit : Circuit σ (n + k) m), circuit.ComputesGiven interpretation target supplied

An impossible conditional computation has complexity ⊤.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_eq_iInf {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : conditionalCostComplexity interpretation operationCost target supplied = ⨅ (h : Algebraic.Target U (n + k) m), ⨅ (_ : ∀ (input : Fin n → U), h (Fin.append input (supplied input)) = target input), costComplexity interpretation operationCost h

Equivalently, minimize ordinary complexity over all functions h with h(x, supplied(x)) = target(x). Values outside these consistent tuples are free.

theorem Cslib.Circuits.Circuit.conditionalGateComplexity_le {σ : Signature} {n k m : ℕ} {U : Type u_2} {circuit : Circuit σ (n + k) m} {interpretation : Interpretation σ U} {target : Algebraic.Target U n m} {supplied : Algebraic.Target U n k} (computes : circuit.ComputesGiven interpretation target supplied) : conditionalGateComplexity interpretation target supplied ≤ ↑circuit.size

A conditional circuit gives an upper bound on conditional gate count.

theorem Cslib.Circuits.Circuit.conditionalGateComplexity_le_iff {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) (budget : ℕ) : conditionalGateComplexity interpretation target supplied ≤ ↑budget ↔ ∃ (circuit : Circuit σ (n + k) m), circuit.size ≤ budget ∧ circuit.ComputesGiven interpretation target supplied

A conditional gate bound is equivalent to a circuit with that many gates.

theorem Cslib.Circuits.Circuit.conditionalGateComplexity_eq_zero_iff {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : conditionalGateComplexity interpretation target supplied = 0 ↔ ∃ (select : Fin m → Fin (n + k)), ∀ (input : Fin n → U), Fin.append input (supplied input) ∘ select = target input

Zero conditional gate complexity means that each output is a fixed selection from the original input coordinates and the supplied functions. No input-dependent selection is possible without gates.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_le_costComplexity {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : conditionalCostComplexity interpretation operationCost target supplied ≤ costComplexity interpretation operationCost target

Supplying extra values cannot increase the cost: they may be ignored.

@[simp]

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_empty {σ : Signature} {U : Type u_2} {n m : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n 0) : conditionalCostComplexity interpretation operationCost target supplied = costComplexity interpretation operationCost target

Conditioning on the empty family recovers ordinary weighted complexity.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_select {σ : Signature} {U : Type u_2} {n k m : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (supplied : Algebraic.Target U n k) (select : Fin m → Fin k) : conditionalCostComplexity interpretation operationCost (fun (input : Fin n → U) (output : Fin m) => supplied input (select output)) supplied = 0

Selecting any of the supplied outputs needs no gates.

@[simp]

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_self {σ : Signature} {U : Type u_2} {n m : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) : conditionalCostComplexity interpretation operationCost target target = 0

A supplied target has zero conditional cost, whether or not it has an ordinary circuit over the chosen basis.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_mono_given {σ : Signature} {U : Type u_2} {n m k l : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) (more : Algebraic.Target U n l) (select : Fin k → Fin l) (agrees : ∀ (input : Fin n → U) (i : Fin k), more input (select i) = supplied input i) : conditionalCostComplexity interpretation operationCost target more ≤ conditionalCostComplexity interpretation operationCost target supplied

Reordering, duplicating, or extending the supplied family cannot increase conditional complexity if all the old values remain accessible.

theorem Cslib.Circuits.Circuit.conditionalGateComplexity_le_gateComplexity {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : conditionalGateComplexity interpretation target supplied ≤ gateComplexity interpretation target

Free supplied values cannot increase gate complexity.

@[simp]

theorem Cslib.Circuits.Circuit.conditionalGateComplexity_empty {σ : Signature} {U : Type u_2} {n m : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n 0) : conditionalGateComplexity interpretation target supplied = gateComplexity interpretation target

Empty conditioning recovers ordinary gate complexity.

@[simp]

theorem Cslib.Circuits.Circuit.conditionalGateComplexity_self {σ : Signature} {U : Type u_2} {n m : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) : conditionalGateComplexity interpretation target target = 0

A supplied target requires zero gates.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_triangle {σ : Signature} {U : Type u_2} {n m l k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (middle : Algebraic.Target U n l) (supplied : Algebraic.Target U n k) : conditionalCostComplexity interpretation operationCost target supplied ≤ conditionalCostComplexity interpretation operationCost target middle + conditionalCostComplexity interpretation operationCost middle supplied

Boyack's triangle inequality (Proposition 2.2), with the original inputs always available and arbitrary natural-number operation costs: compute the intermediate supplied family, then the target.

theorem Cslib.Circuits.Circuit.conditionalGateComplexity_triangle {σ : Signature} {U : Type u_2} {n m l k : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (middle : Algebraic.Target U n l) (supplied : Algebraic.Target U n k) : conditionalGateComplexity interpretation target supplied ≤ conditionalGateComplexity interpretation target middle + conditionalGateComplexity interpretation middle supplied

Boyack's triangle inequality specialized to unit gate cost.

theorem Cslib.Circuits.Circuit.costComplexity_le_conditional_add {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : costComplexity interpretation operationCost target ≤ conditionalCostComplexity interpretation operationCost target supplied + costComplexity interpretation operationCost supplied

Supplying a family can save at most its ordinary computation cost.

theorem Cslib.Circuits.Circuit.conditionalCostComplexity_eq_of_costComplexity_eq_zero {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) (free : costComplexity interpretation operationCost supplied = 0) : conditionalCostComplexity interpretation operationCost target supplied = costComplexity interpretation operationCost target

A family that is already free to compute gives no complexity advantage.

theorem Cslib.Circuits.Circuit.costComplexity_pair_le {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : (costComplexity interpretation operationCost fun (input : Fin n → U) => Fin.append (target input) (supplied input)) ≤ conditionalCostComplexity interpretation operationCost target supplied + costComplexity interpretation operationCost supplied

The chain upper bound: compute the supplied family, then the target, retaining both as outputs. Equality need not hold because a joint circuit can share intermediate wires that are absent from the supplied output family.

theorem Cslib.Circuits.Circuit.gateComplexity_pair_le {σ : Signature} {U : Type u_2} {n m k : ℕ} (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) (supplied : Algebraic.Target U n k) : (gateComplexity interpretation fun (input : Fin n → U) => Fin.append (target input) (supplied input)) ≤ conditionalGateComplexity interpretation target supplied + gateComplexity interpretation supplied

The chain upper bound for gate complexity.