Relative circuit complexity

The complexity C(f | g) of f relative to g is the least number of gates needed to compute f when the values of g come for free: the circuit reads an input x followed by the values g x. Such a circuit only ever sees inputs of this form, which make up the graph of g, so computing f given g is computing f of the first part of the input, on the graph of g. Relative complexity is defined as this complexity on a support, C(f | g) = C^Γ(f ∘ π) where Γ is the graph of g and π forgets the values of g. The reading in terms of circuits on x and g x is recovered by ecomplexityGiven_le_iff.

The rules of relative complexity follow from the calculus of support complexity. Knowing g never makes f harder, and knowing more never makes it harder either. Computing g and then f from it gives the chain rule C(f) ≤ C(g) + C(f | g), and its variant for computing f and g together. Relative complexity satisfies the triangle inequality C(f | h) ≤ C(g | h) + C(f | g), and every function is free given itself.

def Cslib.Circuits.graph {U : Type u} {n k : ℕ} (g : (Fin n → U) → Fin k → U) : Set (Fin (n + k) → U)

The graph of g: every input followed by the values of g on it.

def Cslib.Circuits.onFirstInputs {U : Type u} {n m : ℕ} (k : ℕ) (f : (Fin n → U) → Fin m → U) : (Fin (n + k) → U) → Fin m → U

Apply f to the first n inputs, ignoring the last k inputs.

noncomputable def Cslib.Circuits.ecomplexityGiven {σ : Signature} {U : Type u} {n m k : ℕ} (I : Interpretation σ U) (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : ℕ∞

The complexity C(f | g) of f relative to g: the least size of a single circuit satisfying c.eval I (Fin.append x (g x)) = f x for every x, or ⊤ if there is none. Each evaluation supplies only x and g x; values of g at other inputs are not provided. graph g specifies the inputs on which the circuit must be correct, and onFirstInputs k f specifies its required output on those inputs.

theorem Cslib.Circuits.Circuit.computesOn_graph_iff {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} {g : (Fin n → U) → Fin k → U} (c : Circuit σ (n + k) m) : c.ComputesOn I (graph g) (onFirstInputs k f) ↔ ∀ (x : Fin n → U), c.eval I (Fin.append x (g x)) = f x

A circuit computes f of the first n inputs on the graph of g exactly when, reading an input followed by the values of g on it, it outputs the values of f on that input.

theorem Cslib.Circuits.ecomplexityGiven_le_of_eval {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) (c : Circuit σ (n + k) m) (hc : ∀ (x : Fin n → U), c.eval I (Fin.append x (g x)) = f x) : ecomplexityGiven I f g ≤ ↑c.size

theorem Cslib.Circuits.ecomplexityGiven_le_iff {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} {s : ℕ} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : ecomplexityGiven I f g ≤ ↑s ↔ ∃ (c : Circuit σ (n + k) m), (∀ (x : Fin n → U), c.eval I (Fin.append x (g x)) = f x) ∧ c.size ≤ s

theorem Cslib.Circuits.ecomplexity_append_self_le {σ : Signature} {U : Type u} {n k : ℕ} {I : Interpretation σ U} (g : (Fin n → U) → Fin k → U) : (ecomplexity I fun (x : Fin n → U) => Fin.append x (g x)) ≤ ecomplexity I g

Computing the graph map x ↦ (x, g x) costs no more than computing g.

@[simp]

theorem Cslib.Circuits.ecomplexityGiven_self {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) : ecomplexityGiven I f f = 0

Every function is free given itself: C(f | f) = 0.

theorem Cslib.Circuits.ecomplexityGiven_le_ecomplexity {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : ecomplexityGiven I f g ≤ ecomplexity I f

Knowing g never makes f harder: C(f | g) ≤ C(f).

theorem Cslib.Circuits.ecomplexity_le_add_ecomplexityGiven {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : ecomplexity I f ≤ ecomplexity I g + ecomplexityGiven I f g

The chain rule: computing g and then f from it gives C(f) ≤ C(g) + C(f | g).

theorem Cslib.Circuits.ecomplexity_append_le_add_ecomplexityGiven {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : (ecomplexity I fun (x : Fin n → U) => Fin.append (f x) (g x)) ≤ ecomplexity I f + ecomplexityGiven I g f

Computing f and g together costs at most computing f and then g given f.

theorem Cslib.Circuits.ecomplexityGiven_le_add {σ : Signature} {U : Type u} {n m k l : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) (h : (Fin n → U) → Fin l → U) : ecomplexityGiven I f h ≤ ecomplexityGiven I g h + ecomplexityGiven I f g

The triangle inequality: C(f | h) ≤ C(g | h) + C(f | g). Given h, compute g, and then f from g.

theorem Cslib.Circuits.ecomplexityGiven_append_le {σ : Signature} {U : Type u} {n m k l : ℕ} {I : Interpretation σ U} (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) (g' : (Fin n → U) → Fin l → U) : (ecomplexityGiven I f fun (x : Fin n → U) => Fin.append (g x) (g' x)) ≤ ecomplexityGiven I f g

Knowing more never makes f harder: C(f | g, g') ≤ C(f | g).

Over a complete basis

theorem Cslib.Circuits.ecomplexityGiven_ne_top {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : ecomplexityGiven I f g ≠ ⊤

noncomputable def Cslib.Circuits.complexityGiven {σ : Signature} {U : Type u} {n m k : ℕ} (I : Interpretation σ U) [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : ℕ

The complexity C(f | g) of f relative to g over a complete basis, as a natural number.

@[simp]

theorem Cslib.Circuits.natCast_complexityGiven {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : ↑(complexityGiven I f g) = ecomplexityGiven I f g

@[simp]

theorem Cslib.Circuits.complexityGiven_self {σ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) : complexityGiven I f f = 0

theorem Cslib.Circuits.complexityGiven_le_complexity {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : complexityGiven I f g ≤ complexity I f

theorem Cslib.Circuits.complexity_le_add_complexityGiven {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : complexity I f ≤ complexity I g + complexityGiven I f g

theorem Cslib.Circuits.complexity_append_le_add_complexityGiven {σ : Signature} {U : Type u} {n m k : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) : (complexity I fun (x : Fin n → U) => Fin.append (f x) (g x)) ≤ complexity I f + complexityGiven I g f

theorem Cslib.Circuits.complexityGiven_le_add {σ : Signature} {U : Type u} {n m k l : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) (h : (Fin n → U) → Fin l → U) : complexityGiven I f h ≤ complexityGiven I g h + complexityGiven I f g

theorem Cslib.Circuits.complexityGiven_append_le {σ : Signature} {U : Type u} {n m k l : ℕ} {I : Interpretation σ U} [I.IsComplete] (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin k → U) (g' : (Fin n → U) → Fin l → U) : (complexityGiven I f fun (x : Fin n → U) => Fin.append (g x) (g' x)) ≤ complexityGiven I f g