Circuit complexity relative to a supplied family

For arbitrary sets X and U, a source family sources : X → Fin n → U supplies the formal inputs to a circuit computing target : X → Fin m → U. Circuit.relativeCostComplexity minimizes the weighted cost of such circuits. No coordinates of X are implicitly available.

This is the general framework of Definition 2.1 and Proposition 2.2 in Stephen Wayne Boyack, The Robustness of Combinatorial Measures of Boolean Matrix Complexity, MIT PhD thesis (1985), pp. 29–31. The signature here has arbitrary finite arities and natural-number costs, rather than only binary operations. Constants must be explicitly supplied or implemented by gates; there is no implicit free zero at disconnected outputs.

The extension and section theorems make the domains in Proposition 2.2.1 explicit. A partial function on Set.range sources must be extended before using ordinary circuit complexity. Surjective sources avoid this issue.

Source: https://hdl.handle.net/1721.1/15322.

def Cslib.Circuits.Circuit.ComputesFrom {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Sort u_3} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (target : X → Fin m → U) (sources : X → Fin n → U) : Prop

A circuit computes a target family when its formal inputs are supplied by sources. The common domain need not be a product or a finite type.

Equations

• circuit.ComputesFrom interpretation target sources = ∀ (x : X), circuit.eval interpretation (sources x) = target x

noncomputable def Cslib.Circuits.Circuit.relativeCostComplexity {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : ℕ∞

Minimum cost of computing target from exactly the supplied source family. No implementation of the sources is charged or required.

Equations

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

noncomputable def Cslib.Circuits.Circuit.relativeGateComplexity {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (target : X → Fin m → U) (sources : X → Fin n → U) : ℕ∞

Minimum number of operation gates computing a target from a source family.

Equations

• Cslib.Circuits.Circuit.relativeGateComplexity interpretation target sources = Cslib.Circuits.Circuit.relativeCostComplexity interpretation Algebraic.OperationCost.unit target sources

theorem Cslib.Circuits.Circuit.relativeCostComplexity_le {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Sort u_3} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} (operationCost : Algebraic.OperationCost σ) (computes : circuit.ComputesFrom interpretation target sources) : relativeCostComplexity interpretation operationCost target sources ≤ ↑(circuit.cost operationCost)

A concrete implementation bounds relative complexity.

theorem Cslib.Circuits.Circuit.le_relativeCostComplexity {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} {interpretation : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} (operationCost : Algebraic.OperationCost σ) (bound : ℕ∞) (lowerBound : ∀ (circuit : Circuit σ n m), circuit.ComputesFrom interpretation target sources → bound ≤ ↑(circuit.cost operationCost)) : bound ≤ relativeCostComplexity interpretation operationCost target sources

A lower bound for all implementations bounds relative complexity.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_le_iff {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (budget : ℕ) : relativeCostComplexity interpretation operationCost target sources ≤ ↑budget ↔ ∃ (circuit : Circuit σ n m), circuit.ComputesFrom interpretation target sources ∧ circuit.cost operationCost ≤ budget

A finite relative budget is witnessed by a concrete circuit.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_lt_top_iff {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost target sources < ⊤ ↔ ∃ (circuit : Circuit σ n m), circuit.ComputesFrom interpretation target sources

Finiteness is exactly representability from the supplied family.

@[simp]

theorem Cslib.Circuits.Circuit.relativeCostComplexity_eq_top_iff {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost target sources = ⊤ ↔ ¬∃ (circuit : Circuit σ n m), circuit.ComputesFrom interpretation target sources

Nonrepresentable targets have infinite relative complexity.

theorem Cslib.Circuits.Circuit.relativeGateComplexity_le_iff {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (target : X → Fin m → U) (sources : X → Fin n → U) (budget : ℕ) : relativeGateComplexity interpretation target sources ≤ ↑budget ↔ ∃ (circuit : Circuit σ n m), circuit.size ≤ budget ∧ circuit.ComputesFrom interpretation target sources

A relative gate bound is witnessed by a circuit with at most that many gates.

theorem Cslib.Circuits.Circuit.relativeGateComplexity_eq_zero_iff {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (target : X → Fin m → U) (sources : X → Fin n → U) : relativeGateComplexity interpretation target sources = 0 ↔ ∃ (select : Fin m → Fin n), ∀ (x : X), sources x ∘ select = target x

With unit gate costs, zero complexity means selecting fixed source wires. This characterization need not hold when operations can have zero weight.

@[simp]

theorem Cslib.Circuits.Circuit.relativeCostComplexity_id {σ : Signature} {U : Type u_2} {n m : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : Algebraic.Target U n m) : (relativeCostComplexity interpretation operationCost target fun (x : Fin n → U) => x) = costComplexity interpretation operationCost target

Ordinary complexity is relative complexity with the identity family supplied.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_select {σ : Signature} {U : Type u_2} {X : Sort u_3} {n m : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (sources : X → Fin n → U) (select : Fin m → Fin n) : relativeCostComplexity interpretation operationCost (fun (x : X) (i : Fin m) => sources x (select i)) sources = 0

Selecting, duplicating, or reordering supplied values requires no gates.

@[simp]

theorem Cslib.Circuits.Circuit.relativeCostComplexity_self {σ : Signature} {U : Type u_2} {X : Sort u_3} {m : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) : relativeCostComplexity interpretation operationCost target target = 0

A family is free relative to itself.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_triangle {σ : Signature} {U : Type u_2} {X : Sort u_3} {m l n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (middle : X → Fin l → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost target sources ≤ relativeCostComplexity interpretation operationCost target middle + relativeCostComplexity interpretation operationCost middle sources

Boyack's Proposition 2.2 for arbitrary domains, interpretations, arities, and natural-number operation costs. Compose the two implementing circuits.

theorem Cslib.Circuits.Circuit.relativeGateComplexity_triangle {σ : Signature} {U : Type u_2} {X : Sort u_3} {m l n : ℕ} (interpretation : Interpretation σ U) (target : X → Fin m → U) (middle : X → Fin l → U) (sources : X → Fin n → U) : relativeGateComplexity interpretation target sources ≤ relativeGateComplexity interpretation target middle + relativeGateComplexity interpretation middle sources

The relative triangle inequality for unit gate cost.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_eq_of_mutually_free {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (first : X → Fin n → U) (second : X → Fin k → U) (forward : relativeCostComplexity interpretation operationCost first second = 0) (backward : relativeCostComplexity interpretation operationCost second first = 0) : relativeCostComplexity interpretation operationCost target first = relativeCostComplexity interpretation operationCost target second

Mutually free changes of supplied representation preserve every relative complexity. This includes removing duplicated or redundant source wires.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_pair_le {σ : Signature} {U : Type u_2} {X : Sort u_3} {m l n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (first : X → Fin m → U) (second : X → Fin l → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost (fun (x : X) => Fin.append (first x) (second x)) sources ≤ relativeCostComplexity interpretation operationCost first sources + relativeCostComplexity interpretation operationCost second sources

Compute two target families in parallel from the same supplied values.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_mono_sources {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (more : X → Fin k → U) (select : Fin n → Fin k) (agrees : ∀ (x : X) (i : Fin n), more x (select i) = sources x i) : relativeCostComplexity interpretation operationCost target more ≤ relativeCostComplexity interpretation operationCost target sources

Supplying a family containing all the old sources cannot increase cost.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_map_outputs_le {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n l : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (select : Fin l → Fin m) : relativeCostComplexity interpretation operationCost (fun (x : X) (i : Fin l) => target x (select i)) sources ≤ relativeCostComplexity interpretation operationCost target sources

Selecting some of the target outputs cannot increase cost.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_pair_eq_of_left_eq_zero {σ : Signature} {U : Type u_2} {X : Sort u_3} {m l n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (first : X → Fin m → U) (second : X → Fin l → U) (sources : X → Fin n → U) (free : relativeCostComplexity interpretation operationCost first sources = 0) : relativeCostComplexity interpretation operationCost (fun (x : X) => Fin.append (first x) (second x)) sources = relativeCostComplexity interpretation operationCost second sources

Adding outputs that are free from the sources does not change complexity.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_eq_iInf {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost target sources = ⨅ (h : Algebraic.Target U n m), ⨅ (_ : ∀ (x : X), h (sources x) = target x), costComplexity interpretation operationCost h

Boyack's extension characterization with an explicit total extension: minimize ordinary complexity over functions agreeing on Set.range sources.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_precomp_le {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} {Y : Sort u_4} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (map : Y → X) : relativeCostComplexity interpretation operationCost (target ∘ map) (sources ∘ map) ≤ relativeCostComplexity interpretation operationCost target sources

Restricting the common domain can only remove correctness obligations.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_precomp_triangle {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} {Y : Sort u_4} {k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (map : Y → X) (supplied : Y → Fin k → U) : relativeCostComplexity interpretation operationCost (target ∘ map) supplied ≤ relativeCostComplexity interpretation operationCost target sources + relativeCostComplexity interpretation operationCost (sources ∘ map) supplied

Relative computation after a change of domain can use any implementation of the restricted sources from a new supplied family.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_precomp_eq {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} {Y : Sort u_4} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (map : Y → X) (onto : Function.Surjective map) : relativeCostComplexity interpretation operationCost (target ∘ map) (sources ∘ map) = relativeCostComplexity interpretation operationCost target sources

A surjective reindexing of the common domain preserves complexity. This includes permuting the columns of a finite table of functions.

theorem Cslib.Circuits.Circuit.ComputesFrom.agrees_on_fibers {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Sort u_3} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} (computes : circuit.ComputesFrom interpretation target sources) {x y : X} (equal : sources x = sources y) : target x = target y

Equal supplied values must give equal target values whenever a circuit computes the target. This necessary condition does not assume completeness.

theorem Cslib.Circuits.Circuit.ComputesFrom.factorsThrough {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Sort u_3} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} (computes : circuit.ComputesFrom interpretation target sources) : Function.FactorsThrough target sources

Circuit computation factors through the supplied values.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_eq_top_of_fiber_collision {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) {x y : X} (same : sources x = sources y) (different : target x ≠ target y) : relativeCostComplexity interpretation operationCost target sources = ⊤

If the supplied values identify two inputs that the target distinguishes, no circuit can compute the target from those values, over any interpretation.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_lt_top_iff_factorsThrough {m : ℕ} {U : Type u_1} {σ : Signature} {X : Sort u_3} {n : ℕ} [Nonempty (Fin m → U)] (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (complete : interpretation.FunctionallyComplete) (target : X → Fin m → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost target sources < ⊤ ↔ Function.FactorsThrough target sources

For a functionally complete interpretation, equality on source fibers is also sufficient. A nonempty output space permits total extensions off the image of the supplied family. This generalizes the complete-basis case of Boyack's Theorem 7.1.5 without asserting its algorithmic running time.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_eq_of_rightInverse {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (sectionMap : (Fin n → U) → X) (sectionLaw : Function.RightInverse sectionMap sources) (respects : ∀ (x y : X), sources x = sources y → target x = target y) : relativeCostComplexity interpretation operationCost target sources = costComplexity interpretation operationCost (target ∘ sectionMap)

Boyack's Corollary 2.2.1.2: for surjective sources and a target constant on their fibers, any right inverse reduces relative to ordinary complexity.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_eq_of_equiv {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X ≃ (Fin n → U)) : relativeCostComplexity interpretation operationCost target ⇑sources = costComplexity interpretation operationCost (target ∘ ⇑sources.symm)

Boyack's Corollary 2.2.1.3: an invertible source family converts relative complexity into ordinary complexity after composing with its inverse.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_reindex_sources {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n k : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (indices : Fin k ≃ Fin n) : (relativeCostComplexity interpretation operationCost target fun (x : X) => sources x ∘ ⇑indices) = relativeCostComplexity interpretation operationCost target sources

Permuting the supplied wires preserves relative complexity.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_reindex_outputs {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n l : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) (indices : Fin l ≃ Fin m) : relativeCostComplexity interpretation operationCost (fun (x : X) => target x ∘ ⇑indices) sources = relativeCostComplexity interpretation operationCost target sources

Permuting the target outputs preserves relative complexity. Together with domain reindexing this gives the structural row/column invariance behind Boyack's Proposition 7.1.4.2.

@[simp]

theorem Cslib.Circuits.Circuit.relativeCostComplexity_append_sources {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost (fun (x : X) => Fin.append (sources x) (target x)) sources = relativeCostComplexity interpretation operationCost target sources

Retaining the supplied family as additional outputs is free.

@[simp]

theorem Cslib.Circuits.Circuit.relativeCostComplexity_append_sources_right {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : relativeCostComplexity interpretation operationCost (fun (x : X) => Fin.append (target x) (sources x)) sources = relativeCostComplexity interpretation operationCost target sources

Retaining the sources after the other outputs is also free.