Transport of relative circuit complexity

Homomorphisms preserve relative computation; injective homomorphisms reflect it as well. A change of carrier along an embedding therefore preserves the relative complexity of the mapped families. Circuit translations transport relative complexity with exactly the compiled operation costs.

Pointwise interpretation on X → U relates computations on whole rows of a table to computations at each column. This generalizes the mechanism of Boyack's Proposition 7.1.4 beyond Boolean matrices and finite domains.

def Cslib.Circuits.Interpretation.pointwise {σ : Signature} {U : Type u_3} (interpretation : Interpretation σ U) (X : Type u_1) : Interpretation σ (X → U)

Apply each operation pointwise to functions on X.

Equations

• interpretation.pointwise X op arguments x = interpretation op fun (i : Fin (σ.Arity op)) => arguments i x

def Cslib.Circuits.Interpretation.evaluationHomomorphism {σ : Signature} {U : Type u_2} {X : Type u_3} (interpretation : Interpretation σ U) (x : X) : Homomorphism (interpretation.pointwise X) interpretation

Evaluation at a point commutes with pointwise operations.

Equations

• interpretation.evaluationHomomorphism x = { map := fun (f : X → U) => f x, homomorphic := ⋯ }

theorem Cslib.Circuits.Circuit.ComputesFrom.map {σ : Signature} {U : Type u_2} {V : Type u_3} {n m : ℕ} {X : Sort u_4} {first : Interpretation σ U} {second : Interpretation σ V} (hom : Homomorphism first second) {circuit : Circuit σ n m} {target : X → Fin m → U} {sources : X → Fin n → U} (computes : circuit.ComputesFrom first target sources) : circuit.ComputesFrom second (fun (x : X) => hom.map ∘ target x) fun (x : X) => hom.map ∘ sources x

Map a relative computation through an operation-preserving carrier map.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_map_le {σ : Signature} {U : Type u_2} {V : Type u_3} {X : Sort u_4} {m n : ℕ} {first : Interpretation σ U} {second : Interpretation σ V} (hom : Homomorphism first second) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : (relativeCostComplexity second operationCost (fun (x : X) => hom.map ∘ target x) fun (x : X) => hom.map ∘ sources x) ≤ relativeCostComplexity first operationCost target sources

An operation-preserving carrier map cannot increase relative complexity.

theorem Cslib.Circuits.Circuit.relativeCostComplexity_map_eq {σ : Signature} {U : Type u_2} {V : Type u_3} {X : Sort u_4} {m n : ℕ} {first : Interpretation σ U} {second : Interpretation σ V} (hom : Homomorphism first second) (injective : Function.Injective hom.map) (operationCost : Algebraic.OperationCost σ) (target : X → Fin m → U) (sources : X → Fin n → U) : (relativeCostComplexity second operationCost (fun (x : X) => hom.map ∘ target x) fun (x : X) => hom.map ∘ sources x) = relativeCostComplexity first operationCost target sources

An embedding of interpretations preserves relative complexity exactly. No assumption of functional completeness or surjectivity is needed.

@[simp]

theorem Cslib.Circuits.Circuit.eval_pointwise_apply {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Type u_3} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → X → U) (output : Fin m) (x : X) : circuit.eval (interpretation.pointwise X) input output x = circuit.eval interpretation (fun (i : Fin n) => input i x) output

A circuit on function-valued inputs evaluates at each point independently.

theorem Cslib.Circuits.Circuit.computesFrom_iff_eval_pointwise {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Type u_3} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (target : X → Fin m → U) (sources : X → Fin n → U) : circuit.ComputesFrom interpretation target sources ↔ (circuit.eval (interpretation.pointwise X) fun (i : Fin n) (x : X) => sources x i) = fun (i : Fin m) (x : X) => target x i

Computing a tuple of functions pointwise is exactly relative computation of the corresponding family on their common domain.

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

Minimum cost is the same whether a circuit acts on whole functions or on their values at every point. For Boolean tables this is the semantic correspondence in Boyack's Proposition 7.1.4, with explicit gate costs.

theorem Algebraic.Translation.relativeCostComplexity_le {σ : Signature} {τ : Signature} {U : Type u_3} {X : Sort u_4} {m n : ℕ} (translation : Translation σ τ) (interpretation : Interpretation τ U) (operationCost : OperationCost τ) (target : X → Fin m → U) (sources : X → Fin n → U) : Circuit.relativeCostComplexity interpretation operationCost target sources ≤ Circuit.relativeCostComplexity (translation.pull interpretation) (translation.pullCost operationCost) target sources

Compilation transports relative complexity with the exact pulled-back operation cost, just as for ordinary complexity.