Circuit complexity as a distance

Let I interpret a signature over a carrier U with an additive group structure, so that the functions (Fin n → U) → U form a group under pointwise operations. The difference distance Cslib.Circuits.diffDist I c f g is 0 when f = g, and otherwise the circuit complexity of f - g plus a constant c. Two circuit facts make it a distance:

• combining two outputs by an operation costs at most the complexity of that operation on two inputs (Cslib.Circuits.complexity_single_binary_le). Since f - h = (f - g) + (g - h), the triangle inequality holds once c pays for an addition circuit (Cslib.Circuits.diffDist_triangle);
• since g - f = -(f - g), exchanging the arguments costs at most a negation circuit (Cslib.Circuits.diffDist_comm_le).

So diffDist I c is a right-translation-invariant quasi-metric when c is positive and pays for addition. It need not be symmetric: over a complete basis in which negation costs a gate, the projection x ↦ x 0 is computed by no gates while its negation needs one. It is symmetric when negation leaves complexity unchanged, as in a group of exponent two, where -u = u. A negation circuit of cost zero only exists in that case, since circuits without gates compute projections (Cslib.Circuits.one_le_complexity_single).

When c is positive and pays for addition, and negation leaves complexity unchanged, the map sending 0 to 0 and every other f to C(f) + c is a norm on the group of functions (Cslib.Circuits.diffNorm). For commutative groups its distance is the difference distance (Cslib.Circuits.dist_diffNorm). Circuit complexity is then, up to the constant, a norm on a translation-invariant metric group. Boolean functions with the De Morgan basis are the case c = 4, with addition the exclusive or; see Complexity.Computability.Circuit.Boolean.Metric.

Main definitions

• Cslib.Circuits.diffDist: the difference distance.
• Cslib.Circuits.diffNorm: the corresponding norm, under negation invariance.

Main results

• Cslib.Circuits.diffDist_eq_zero_iff, Cslib.Circuits.diffDist_triangle, Cslib.Circuits.diffDist_comm_le: a quasi-metric.
• Cslib.Circuits.diffDist_add_right, Cslib.Circuits.diffDist_add_left: translation invariance.
• Cslib.Circuits.diffDist_comm: symmetry under negation invariance.
• Cslib.Circuits.dist_diffNorm: the norm induces the difference distance.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

The difference distance

noncomputable def Cslib.Circuits.diffDist {σ : Signature} {U : Type u_1} {n : ℕ} [AddGroup U] (I : Interpretation σ U) [I.IsComplete] (c : ℕ) (f g : (Fin n → U) → U) : ℕ

The difference distance between f and g: 0 if they are equal, and otherwise the circuit complexity of f - g plus c.

@[simp]

theorem Cslib.Circuits.diffDist_self {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c : ℕ} (f : (Fin n → U) → U) : diffDist I c f f = 0

theorem Cslib.Circuits.diffDist_of_ne {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c : ℕ} {f g : (Fin n → U) → U} (h : f ≠ g) : diffDist I c f g = complexity I (single (f - g)) + c

theorem Cslib.Circuits.diffDist_eq_zero_iff {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c : ℕ} (hc : 0 < c) {f g : (Fin n → U) → U} : diffDist I c f g = 0 ↔ f = g

The difference distance separates functions when c is positive.

@[simp]

theorem Cslib.Circuits.diffDist_add_right {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c : ℕ} (f g a : (Fin n → U) → U) : diffDist I c (f + a) (g + a) = diffDist I c f g

The difference distance is invariant under translation on the right.

theorem Cslib.Circuits.diffDist_triangle {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c : ℕ} (hadd : complexity I (single fun (y : Fin 2 → U) => y 0 + y 1) ≤ c) (f g h : (Fin n → U) → U) : diffDist I c f h ≤ diffDist I c f g + diffDist I c g h

The triangle inequality, when c pays for a circuit adding two inputs.

theorem Cslib.Circuits.diffDist_comm_le {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c e : ℕ} (hneg : complexity I (single fun (y : Fin 1 → U) => -y 0) ≤ e) (f g : (Fin n → U) → U) : diffDist I c g f ≤ diffDist I c f g + e

Exchanging the arguments costs at most a circuit negating its input.

theorem Cslib.Circuits.diffDist_comm {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c : ℕ} (hneg : ∀ (f : (Fin n → U) → U), complexity I (single (-f)) = complexity I (single f)) (f g : (Fin n → U) → U) : diffDist I c f g = diffDist I c g f

The difference distance is symmetric when negation leaves complexity unchanged.

@[simp]

theorem Cslib.Circuits.diffDist_add_left {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddCommGroup U] {c : ℕ} (a f g : (Fin n → U) → U) : diffDist I c (a + f) (a + g) = diffDist I c f g

The difference distance is invariant under translation on the left, for commutative groups.

The norm

noncomputable def Cslib.Circuits.diffNorm {σ : Signature} {U : Type u_1} {n : ℕ} [AddGroup U] (I : Interpretation σ U) [I.IsComplete] (c : ℕ) (hc : 0 < c) (hadd : complexity I (single fun (y : Fin 2 → U) => y 0 + y 1) ≤ c) (hneg : ∀ (f : (Fin n → U) → U), complexity I (single (-f)) = complexity I (single f)) : AddGroupNorm ((Fin n → U) → U)

Circuit complexity as a norm: 0 at 0, and otherwise the complexity plus c, when c is positive and pays for a circuit adding two inputs, and negation leaves complexity unchanged.

theorem Cslib.Circuits.diffNorm_apply {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddGroup U] {c : ℕ} {hc : 0 < c} {hadd : complexity I (single fun (y : Fin 2 → U) => y 0 + y 1) ≤ c} {hneg : ∀ (f : (Fin n → U) → U), complexity I (single (-f)) = complexity I (single f)} (f : (Fin n → U) → U) : (diffNorm I c hc hadd hneg) f = ↑(diffDist I c f 0)

theorem Cslib.Circuits.dist_diffNorm {σ : Signature} {U : Type u_1} {I : Interpretation σ U} [I.IsComplete] {n : ℕ} [AddCommGroup U] {c : ℕ} (hc : 0 < c) (hadd : complexity I (single fun (y : Fin 2 → U) => y 0 + y 1) ≤ c) (hneg : ∀ (f : (Fin n → U) → U), complexity I (single (-f)) = complexity I (single f)) (f g : (Fin n → U) → U) : dist f g = ↑(diffDist I c f g)

The norm induces the difference distance on the normed group of functions.