Circuit semantics

This file contains the small semantic vocabulary used by circuit lower bounds. Circuit.ComputesWith is generic in the interpretation and number of outputs; it agrees definitionally with CSLib's Circuit.Computes.

@[reducible, inline]

abbrev Algebraic.ScalarFunction (U : Type u) (n : ℕ) : Type u

A single-output function on n inputs over U.

Equations

• Algebraic.ScalarFunction U n = ((Fin n → U) → U)

@[reducible, inline]

abbrev Algebraic.Target (U : Type u) (n m : ℕ) : Type u

An m-output function on n inputs over U.

Equations

• Algebraic.Target U n m = ((Fin n → U) → Fin m → U)

def Cslib.Circuits.Circuit.outputFunction {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (output : Fin m) : Algebraic.ScalarFunction U n

The scalar function carried by one designated output wire.

Equations

• circuit.outputFunction interpretation output input = circuit.eval interpretation input output

@[simp]

theorem Cslib.Circuits.Circuit.outputFunction_apply {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (output : Fin m) (input : Fin n → U) : circuit.outputFunction interpretation output input = circuit.eval interpretation input output

def Cslib.Circuits.Circuit.ComputesWith {σ : Signature} {n m : ℕ} {U : Type u_2} (c : Circuit σ n m) (interpretation : Interpretation σ U) (target : Algebraic.Target U n m) : Prop

Exact pointwise computation of a function by a circuit.

Equations

• c.ComputesWith interpretation target = ∀ (input : Fin n → U), c.eval interpretation input = target input

@[reducible, inline]

abbrev Algebraic.Circuit.Computes {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (target : Target U n m) : Prop

Legacy qualified name for generic circuit computation. Use circuit.ComputesWith interpretation target with field notation.

Equations

• Algebraic.Circuit.Computes circuit interpretation target = circuit.ComputesWith interpretation target

theorem Cslib.Circuits.Circuit.ComputesWith.eval_eq {σ : 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) : circuit.eval interpretation = target

Pointwise computation gives equality of the computed and target functions.

theorem Algebraic.Circuit.Computes.eval_eq {σ : Signature} {n m : ℕ} {U : Type u_2} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} {target : Target U n m} (computes : Computes circuit interpretation target) : circuit.eval interpretation = target

Legacy qualified name for equality of the computed and target functions.

def Cslib.Circuits.Circuit.GateHard {σ : Signature} {U : Type u_2} {n m : ℕ} (interpretation : Interpretation σ U) (G : ℕ) (target : Algebraic.Target U n m) : Prop

A target is gate-hard at budget G when no circuit with at most G internal gates computes it.

Equations

• Cslib.Circuits.Circuit.GateHard interpretation G target = ∀ (circuit : Cslib.Circuits.Circuit σ n m), circuit.size ≤ G → ¬circuit.ComputesWith interpretation target

def Cslib.Circuits.Circuit.DepthHard {σ : Signature} {U : Type u_2} {n m : ℕ} (interpretation : Interpretation σ U) (depth : ℕ) (target : Algebraic.Target U n m) : Prop

A target is depth-hard at depth when every circuit computing it has strictly greater depth.

Equations

• Cslib.Circuits.Circuit.DepthHard interpretation depth target = ∀ (circuit : Cslib.Circuits.Circuit σ n m), circuit.ComputesWith interpretation target → depth < circuit.depth

def Cslib.Circuits.Interpretation.FunctionallyComplete {σ : Signature} {U : Type u_2} (interpretation : Interpretation σ U) : Prop

An interpretation is functionally complete if every finite-arity, finite-output target has some circuit.

Equations

• interpretation.FunctionallyComplete = ∀ (n m : ℕ) (target : Algebraic.Target U n m), ∃ (circuit : Cslib.Circuits.Circuit σ n m), circuit.ComputesWith interpretation target

def Algebraic.DependsOnlyOn {n : ℕ} {U : Sort u_1} {V : Sort u_2} (function : (Fin n → U) → V) (support : Finset (Fin n)) : Prop

A function depends only on the input coordinates in support.

Equations

• Algebraic.DependsOnlyOn function support = ∀ (left right : Fin n → U), (∀ k ∈ support, left k = right k) → function left = function right

def Algebraic.EssentialAt {n : ℕ} {U : Sort u_1} {V : Sort u_2} (function : (Fin n → U) → V) (selected : Fin n) : Prop

Changing only coordinate selected can change the function value.

Equations

• Algebraic.EssentialAt function selected = ∃ (left : Fin n → U) (right : Fin n → U), (∀ (k : Fin n), k ≠ selected → left k = right k) ∧ function left ≠ function right

theorem Algebraic.EssentialAt.mem_support {n : ℕ} {U : Sort u_1} {V : Sort u_2} {function : (Fin n → U) → V} {support : Finset (Fin n)} {selected : Fin n} (essential : EssentialAt function selected) (depends : DependsOnlyOn function support) : selected ∈ support

Every essential coordinate belongs to any support of the function.