Minimum circuit complexity #
Complexity is the infimum of the costs of all circuits computing a target,
valued in the extended natural numbers. Nonrepresentable targets therefore
have complexity ⊤, while representable targets recover an ordinary minimum.
noncomputable def
Cslib.Circuits.Circuit.costComplexity
{σ : Signature}
{U : Type u_2}
{n m : ℕ}
(interpretation : Interpretation σ U)
(operationCost : Algebraic.OperationCost σ)
(target : Algebraic.Target U n m)
:
Minimum weighted cost of a target. The value is ⊤ when no circuit
computes the target.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Cslib.Circuits.Circuit.gateComplexity
{σ : Signature}
{U : Type u_2}
{n m : ℕ}
(interpretation : Interpretation σ U)
(target : Algebraic.Target U n m)
:
Minimum gate count of a target.
Equations
- Cslib.Circuits.Circuit.gateComplexity interpretation target = Cslib.Circuits.Circuit.costComplexity interpretation Algebraic.OperationCost.unit target
Instances For
theorem
Cslib.Circuits.Circuit.costComplexity_le
{σ : Signature}
{n m : ℕ}
{U : Type u_2}
{circuit : Circuit σ n m}
{interpretation : Interpretation σ U}
{target : Algebraic.Target U n m}
(operationCost : Algebraic.OperationCost σ)
(computes : circuit.ComputesWith interpretation target)
:
Any concrete implementation upper-bounds minimum weighted complexity.
theorem
Cslib.Circuits.Circuit.le_costComplexity
{σ : Signature}
{U : Type u_2}
{n m : ℕ}
{interpretation : Interpretation σ U}
{target : Algebraic.Target U n m}
(operationCost : Algebraic.OperationCost σ)
(bound : ℕ∞)
(lowerBound :
∀ (circuit : Circuit σ n m), circuit.ComputesWith interpretation target → bound ≤ ↑(circuit.cost operationCost))
:
A uniform lower bound on all implementations lower-bounds minimum weighted complexity.
theorem
Cslib.Circuits.Circuit.le_costComplexity_iff
{σ : Signature}
{U : Type u_2}
{n m : ℕ}
{interpretation : Interpretation σ U}
{target : Algebraic.Target U n m}
(operationCost : Algebraic.OperationCost σ)
(bound : ℕ∞)
:
bound ≤ costComplexity interpretation operationCost target ↔ ∀ (circuit : Circuit σ n m), circuit.ComputesWith interpretation target → bound ≤ ↑(circuit.cost operationCost)
Characterization of a weighted complexity lower bound by all concrete implementations.
theorem
Cslib.Circuits.Circuit.costComplexity_lt_top_iff
{σ : Signature}
{U : Type u_2}
{n m : ℕ}
{interpretation : Interpretation σ U}
{target : Algebraic.Target U n m}
(operationCost : Algebraic.OperationCost σ)
:
costComplexity interpretation operationCost target < ⊤ ↔ ∃ (circuit : Circuit σ n m), circuit.ComputesWith interpretation target
Weighted complexity is finite exactly when the target is representable.
@[simp]
theorem
Cslib.Circuits.Circuit.costComplexity_eq_top_iff
{σ : Signature}
{U : Type u_2}
{n m : ℕ}
{interpretation : Interpretation σ U}
{target : Algebraic.Target U n m}
(operationCost : Algebraic.OperationCost σ)
:
costComplexity interpretation operationCost target = ⊤ ↔ ¬∃ (circuit : Circuit σ n m), circuit.ComputesWith interpretation target
theorem
Cslib.Circuits.Circuit.costComplexity_eq
{σ : Signature}
{n m : ℕ}
{U : Type u_2}
{circuit : Circuit σ n m}
{interpretation : Interpretation σ U}
{target : Algebraic.Target U n m}
(operationCost : Algebraic.OperationCost σ)
(computes : circuit.ComputesWith interpretation target)
(minimal : CostMinimal operationCost circuit interpretation target)
:
A minimum-cost concrete circuit realizes the extended-natural complexity.
theorem
Cslib.Circuits.Circuit.gateComplexity_le
{σ : Signature}
{n m : ℕ}
{U : Type u_2}
{circuit : Circuit σ n m}
{interpretation : Interpretation σ U}
{target : Algebraic.Target U n m}
(computes : circuit.ComputesWith interpretation target)
:
Any concrete implementation upper-bounds minimum gate complexity.
theorem
Algebraic.Translation.costComplexity_le
{σ : Signature}
{τ : Signature}
{U : Type u_3}
{n m : ℕ}
(translation : Translation σ τ)
(interpretation : Interpretation τ U)
(operationCost : OperationCost τ)
(target : Target U n m)
:
Circuit.costComplexity interpretation operationCost target ≤ Circuit.costComplexity (translation.pull interpretation) (translation.pullCost operationCost) target
Compilation makes target-basis weighted complexity no larger than source complexity charged by the exact pulled-back cost.
theorem
Algebraic.Translation.gateComplexity_le_mul
{σ : Signature}
{τ : Signature}
{U : Type u_3}
{n m K : ℕ}
(translation : Translation σ τ)
(interpretation : Interpretation τ U)
(target : Target U n m)
(positive : 1 ≤ K)
(bounded : ∀ (op : σ.Op), (translation.operation op).size ≤ K)
:
Circuit.gateComplexity interpretation target ≤ ↑K * Circuit.gateComplexity (translation.pull interpretation) target
A uniform local K-gate simulation gives the conventional multiplicative
gate-complexity comparison. The positivity assumption avoids the indeterminate
0 * ⊤ case.
theorem
Algebraic.Translation.transport_sizeLowerBound
{σ : Signature}
{τ : Signature}
{U : Type u_3}
{n m L K : ℕ}
(translation : Translation σ τ)
(interpretation : Interpretation τ U)
(target : Target U n m)
(lowerBound :
∀ (targetCircuit : Circuit τ n m), targetCircuit.ComputesWith interpretation target → L ≤ targetCircuit.size)
(bounded : ∀ (op : σ.Op), (translation.operation op).size ≤ K)
(circuit : Circuit σ n m)
(computes : circuit.ComputesWith (translation.pull interpretation) target)
:
Transport a target-basis size lower bound through a uniformly bounded translation, without introducing a global complexity value.
theorem
Algebraic.Translation.transport_sizeLowerBound_ceilDiv
{σ : Signature}
{τ : Signature}
{U : Type u_3}
{n m K L : ℕ}
(translation : Translation σ τ)
(interpretation : Interpretation τ U)
(target : Target U n m)
(positive : 0 < K)
(lowerBound :
∀ (targetCircuit : Circuit τ n m), targetCircuit.ComputesWith interpretation target → L ≤ targetCircuit.size)
(bounded : ∀ (op : σ.Op), (translation.operation op).size ≤ K)
(circuit : Circuit σ n m)
(computes : circuit.ComputesWith (translation.pull interpretation) target)
:
Division form of transport_sizeLowerBound.
theorem
Algebraic.Realization.operation_costComplexity_eq_minimumCost
{σ : Signature}
{U : Type u_2}
{τ : Signature}
{source : Interpretation σ U}
{targetInterpretation : Interpretation τ U}
(realization : Realization σ τ source targetInterpretation)
(operationCost : OperationCost τ)
(op : σ.Op)
:
Circuit.costComplexity targetInterpretation operationCost (source.operationTarget op) = ↑(realization.minimumCost operationCost op)
Intrinsic operation cost is exactly the target-basis complexity of that source operation.
theorem
Algebraic.Realization.costComplexity_le
{σ : Signature}
{U : Type u_2}
{τ : Signature}
{n m : ℕ}
{source : Interpretation σ U}
{targetInterpretation : Interpretation τ U}
(realization : Realization σ τ source targetInterpretation)
(operationCost : OperationCost τ)
(target : Target U n m)
:
Circuit.costComplexity targetInterpretation operationCost target ≤ Circuit.costComplexity source (realization.pullCost operationCost) target
Complexity comparison specialized to a realization of named source and target interpretations.
theorem
Algebraic.Realization.costComplexity_le_minimumCost
{σ : Signature}
{U : Type u_2}
{τ : Signature}
{n m : ℕ}
{source : Interpretation σ U}
{targetInterpretation : Interpretation τ U}
(realization : Realization σ τ source targetInterpretation)
(operationCost : OperationCost τ)
(target : Target U n m)
:
Circuit.costComplexity targetInterpretation operationCost target ≤ Circuit.costComplexity source (realization.minimumCost operationCost) target
The intrinsic, minimum-operation-cost form of complexity transport.
theorem
Algebraic.Realization.gateComplexity_le_mul
{σ : Signature}
{U : Type u_2}
{τ : Signature}
{n m K : ℕ}
{source : Interpretation σ U}
{targetInterpretation : Interpretation τ U}
(realization : Realization σ τ source targetInterpretation)
(target : Target U n m)
(positive : 1 ≤ K)
(bounded : ∀ (op : σ.Op), (realization.operation op).size ≤ K)
:
Uniformly bounded realization gadgets give the conventional multiplicative comparison of gate complexities.
theorem
Algebraic.Realization.gateComplexity_le_mul_overhead
{σ : Signature}
{U : Type u_2}
{τ : Signature}
{n m : ℕ}
[Fintype σ.Op]
{source : Interpretation σ U}
{targetInterpretation : Interpretation τ U}
(realization : Realization σ τ source targetInterpretation)
(target : Target U n m)
:
Circuit.gateComplexity targetInterpretation target ≤ ↑realization.overhead * Circuit.gateComplexity source target
Gate complexity changes by at most the selected realization's normalized local overhead.
theorem
Algebraic.Realization.transport_sizeLowerBound
{σ : Signature}
{U : Type u_2}
{τ : Signature}
{n m L K : ℕ}
{source : Interpretation σ U}
{targetInterpretation : Interpretation τ U}
(realization : Realization σ τ source targetInterpretation)
(target : Target U n m)
(lowerBound :
∀ (targetCircuit : Circuit τ n m), targetCircuit.ComputesWith targetInterpretation target → L ≤ targetCircuit.size)
(bounded : ∀ (op : σ.Op), (realization.operation op).size ≤ K)
(circuit : Circuit σ n m)
(computes : circuit.ComputesWith source target)
:
Per-circuit constant-factor lower-bound transport through a realization.
theorem
Algebraic.Realization.transport_sizeLowerBound_ceilDiv
{σ : Signature}
{U : Type u_2}
{τ : Signature}
{n m K L : ℕ}
{source : Interpretation σ U}
{targetInterpretation : Interpretation τ U}
(realization : Realization σ τ source targetInterpretation)
(target : Target U n m)
(positive : 0 < K)
(lowerBound :
∀ (targetCircuit : Circuit τ n m), targetCircuit.ComputesWith targetInterpretation target → L ≤ targetCircuit.size)
(bounded : ∀ (op : σ.Op), (realization.operation op).size ≤ K)
(circuit : Circuit σ n m)
(computes : circuit.ComputesWith source target)
:
Division form of constant-factor lower-bound transport through a realization.
theorem
Cslib.Circuits.Interpretation.gateComplexity_linearlyEquivalent_of_functionallyComplete
{σ : Signature}
{U : Type u_2}
{τ : Signature}
[Fintype σ.Op]
[Fintype τ.Op]
(first : Interpretation σ U)
(second : Interpretation τ U)
(firstComplete : first.FunctionallyComplete)
(secondComplete : second.FunctionallyComplete)
:
∃ (forward : ℕ) (backward : ℕ),
1 ≤ forward ∧ 1 ≤ backward ∧ (∀ {n m : ℕ} (target : Algebraic.Target U n m),
Circuit.gateComplexity second target ≤ ↑forward * Circuit.gateComplexity first target) ∧ ∀ {n m : ℕ} (target : Algebraic.Target U n m),
Circuit.gateComplexity first target ≤ ↑backward * Circuit.gateComplexity second target
Two finite, functionally complete interpreted signatures have linearly equivalent gate complexities, with explicit constants supplied by realizations of their operation sets.