Documentation

Complexity.Computability.Circuit.Boolean.Metric

The computational Hamming metric #

Boolean functions on n inputs form a group under the exclusive or, which is the addition of Mathlib's Boolean ring Bool, taken pointwise: (f + g) x = f x ^^ g x. The computational Hamming distance Cslib.Circuits.Boolean.circuitDist f g is 0 when f = g, and otherwise the De Morgan circuit complexity of f + g plus four, the cost of an exclusive or (Cslib.Circuits.Boolean.circuitDist_def). It is the difference distance of Complexity.Computability.Circuit.Metric for the De Morgan interpretation with c = 4, by definition (Cslib.Circuits.Boolean.circuitDist_eq_diffDist), since f - g = f + g and -f = f.

It is a translation-invariant metric: f + h = (f + g) + (g + h) gives the triangle inequality from C(f ⊕ h) ≤ C(f ⊕ g) + C(g ⊕ h) + 4. Circuit complexity is 1-Lipschitz for it, |C(f) - C(g)| ≤ circuitDist f g (Cslib.Circuits.Boolean.dist_complexity_single_le_circuitDist), which is the correction bound |C(f) - C(g)| ≤ C(f ⊕ g) + 4 of Cslib.Circuits.Boolean.dist_complexity_single_le_complexity_xor [Juk12]. Unlike the normalized Hamming distance, it does not separate functions that differ on many inputs but in a simple way: two functions whose exclusive or is a projection are at distance four.

The same quantity is a norm, 0 at 0 and C(f) + 4 otherwise (Cslib.Circuits.Boolean.circuitNorm), and induces the metric (Cslib.Circuits.Boolean.dist_circuitNormedAddCommGroup). The normed group is a definition, not an instance, since BooleanFunction n is a function type. Apart from the zero function and the offset, the minimum circuit size problem asks for membership in balls about zero: C(f) ≤ s exactly when f lies in the closed ball of radius s + 4 about 0 (Cslib.Circuits.Boolean.complexity_single_le_iff_mem_closedBall).

Main definitions #

Main results #

References #

The group operations as circuits #

source
theorem Cslib.Circuits.Boolean.complexity_single_add_le :
complexity interpretation (single fun (y : Fin 2 → Bool) => y 0 + y 1) ≤ 4

Adding two inputs, an exclusive or, costs four De Morgan gates.

source
theorem Cslib.Circuits.Boolean.complexity_single_neg {n : ℕ} (f : BooleanFunction n) :
complexity interpretation (single (-f)) = complexity interpretation (single f)

Negation is the identity on Boolean functions, so it leaves complexity unchanged.

The computational Hamming distance #

source
noncomputable def Cslib.Circuits.Boolean.circuitDist {n : ℕ} (f g : BooleanFunction n) :
ℕ

The computational Hamming distance: 0 if f = g, and otherwise the complexity of f + g, the inputs where f and g differ, plus four.

Instances For
    source
    theorem Cslib.Circuits.Boolean.circuitDist_eq_diffDist {n : ℕ} (f g : BooleanFunction n) :
    circuitDist f g = diffDist interpretation 4 f g

    The computational Hamming distance is the difference distance with c = 4.

    source
    theorem Cslib.Circuits.Boolean.circuitDist_def {n : ℕ} (f g : BooleanFunction n) :
    circuitDist f g = if f = g then 0 else complexity interpretation (single (f + g)) + 4

    The computational Hamming distance is 0 when f = g and C(f + g) + 4 otherwise.

    source
    @[simp]
    theorem Cslib.Circuits.Boolean.circuitDist_self {n : ℕ} (f : BooleanFunction n) :
    circuitDist f f = 0

    The computational Hamming distance from a Boolean function to itself is zero.

    source
    theorem Cslib.Circuits.Boolean.circuitDist_of_ne {n : ℕ} {f g : BooleanFunction n} (h : f ≠ g) :
    circuitDist f g = complexity interpretation (single fun (x : Fin n → Bool) => f x ^^ g x) + 4

    Distinct functions are at distance the complexity of their exclusive or plus four.

    source
    theorem Cslib.Circuits.Boolean.circuitDist_eq_zero_iff {n : ℕ} {f g : BooleanFunction n} :
    circuitDist f g = 0 ↔ f = g

    The computational Hamming distance between f and g is zero if and only if f = g.

    source
    theorem Cslib.Circuits.Boolean.circuitDist_comm {n : ℕ} (f g : BooleanFunction n) :
    circuitDist f g = circuitDist g f

    The computational Hamming distance is symmetric.

    source
    theorem Cslib.Circuits.Boolean.circuitDist_triangle {n : ℕ} (f g h : BooleanFunction n) :
    circuitDist f h ≤ circuitDist f g + circuitDist g h

    The triangle inequality, from the cost of an exclusive or.

    source
    @[simp]
    theorem Cslib.Circuits.Boolean.circuitDist_add_right {n : ℕ} (f g a : BooleanFunction n) :
    circuitDist (f + a) (g + a) = circuitDist f g

    The computational Hamming distance is invariant under right translation.

    source
    @[simp]
    theorem Cslib.Circuits.Boolean.circuitDist_add_left {n : ℕ} (a f g : BooleanFunction n) :
    circuitDist (a + f) (a + g) = circuitDist f g

    The computational Hamming distance is invariant under left translation.

    source
    theorem Cslib.Circuits.Boolean.dist_complexity_single_le_circuitDist {n : ℕ} (f g : BooleanFunction n) :
    (complexity interpretation (single f)).dist (complexity interpretation (single g)) ≤ circuitDist f g

    Circuit complexity is 1-Lipschitz for the computational Hamming distance.

    The norm #

    source
    noncomputable def Cslib.Circuits.Boolean.circuitNorm (n : ℕ) :
    AddGroupNorm (BooleanFunction n)

    The computational Hamming norm: 0 at 0, and otherwise the complexity plus four.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.circuitNorm_apply {n : ℕ} (f : BooleanFunction n) :
      (circuitNorm n) f = ↑(circuitDist f 0)

      The computational Hamming norm of f is its computational Hamming distance from 0.

      source
      @[reducible, inline]
      noncomputable abbrev Cslib.Circuits.Boolean.circuitNormedAddCommGroup (n : ℕ) :
      NormedAddCommGroup (BooleanFunction n)

      The normed group of Boolean functions with the computational Hamming norm. This is a definition, not an instance, since BooleanFunction n is a function type.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.dist_circuitNormedAddCommGroup {n : ℕ} (f g : BooleanFunction n) :
        dist f g = ↑(circuitDist f g)

        The normed group induces the computational Hamming distance.

        Complexity bounds as balls #

        source
        theorem Cslib.Circuits.Boolean.complexity_single_le_iff_circuitDist_le {n : ℕ} {f : BooleanFunction n} (hf : f ≠ 0) (s : ℕ) :
        complexity interpretation (single f) ≤ s ↔ circuitDist f 0 ≤ s + 4

        For f ≠ 0, the minimum circuit size problem is membership in a ball about 0.

        source
        theorem Cslib.Circuits.Boolean.complexity_single_le_iff_mem_closedBall {n : ℕ} {f : BooleanFunction n} (hf : f ≠ 0) (s : ℕ) :
        complexity interpretation (single f) ≤ s ↔ f ∈ Metric.closedBall 0 (↑s + 4)

        For f ≠ 0, the minimum circuit size problem is membership in the closed ball of radius s + 4 about 0 for the computational Hamming norm.