Documentation

Cslib.Computability.Circuit.Shannon

Shannon's lower bound for finite carriers and binary bases #

For any fixed finite signature with operation arities at most two, interpreted on a finite carrier U with q ≥ 2 elements, some function on n inputs requires more than qⁿ/n gates for all sufficiently large n. The threshold may depend on the signature and carrier. For the De Morgan basis on Bool, this matches Lupanov's upper bound asymptotically.

The logarithm of the counting bound is at most s log s + O(s) for n + 1 ≤ s. At s = ⌊qⁿ/n⌋, this is smaller than the logarithm of the q^(qⁿ) functions. This extends the Boolean counting argument in the references to finite carriers.

References #

theorem Cslib.Circuits.Shannon.exists_hard_function {σ : Signature} {U : Type u} [Finite σ.Op] [Finite U] [Nontrivial U] (I : Interpretation σ U) (arity_le : ∀ (op : σ.Op), σ.Arity op ≤ 2) :
∃ (N : ℕ), ∀ n ≥ N, ∃ (f : (Fin n → U) → U), ∀ (c : Circuit σ n 1), (c.Computes I fun (x : Fin n → U) (x_1 : Fin 1) => f x) → ↑(Nat.card U) ^ n / ↑n < ↑c.size

For all sufficiently large n, some function on n inputs over U requires more than |U|ⁿ/n gates over the fixed finite signature, whose operations have arity at most two.