feat(Circuit): prove Shannon lower bound - #891
SamuelSchlesinger wants to merge 4 commits into
Conversation
|
|
||
| variable {n g s : ℕ} | ||
|
|
||
| /-- Boolean functions computable with at most `s` De Morgan gates. -/ |
There was a problem hiding this comment.
| /-- Boolean functions computable with at most `s` De Morgan gates. -/ | |
| /-- Boolean functions on `n` inputs computable with at most `s` De Morgan gates. -/ |
There was a problem hiding this comment.
Applied the suggested docstring.
| variable {n g s : ℕ} | ||
|
|
||
| /-- Boolean functions computable with at most `s` De Morgan gates. -/ | ||
| noncomputable def computableFunctions (n s : ℕ) : Finset (BooleanFunction n) := by |
There was a problem hiding this comment.
Would it be difficult to give an explicit definition (instead of using a tactic)?
I mean mem_computableFunctions gives a good definition so it's not too bad, but still a bit weird.
There was a problem hiding this comment.
Replaced both tactic blocks with direct Finset.univ.filter definitions using open scoped Classical in.
| classical | ||
| simp [computableFunctions] | ||
|
|
||
| private noncomputable def irredundantFunctions (n g : ℕ) : Finset (BooleanFunction n) := by |
There was a problem hiding this comment.
Can you give some intuition for this definition?
There was a problem hiding this comment.
Added a docstring explaining that the gates compute pairwise distinct functions, giving g! distinct relabelings for the counting bound.
| classical | ||
| simp [irredundantFunctions] | ||
|
|
||
| private instance opFintype : Fintype Op where |
There was a problem hiding this comment.
Maybe move to definition of Op, could be useful in general
There was a problem hiding this comment.
Moved the Fintype Op instance next to Op in Boolean/Basic.lean and made it public.
| intro gate | ||
| simp [Wire.Renaming.ofPermutation, Function.comp_def] | ||
|
|
||
| private noncomputable def representative (f : ↥(irredundantFunctions n g)) : |
There was a problem hiding this comment.
Is it possible to do this without the ↥?
There was a problem hiding this comment.
Removed the explicit ↥ here and in the related declarations; Lean infers the coercion.
| nlinarith | ||
|
|
||
| private theorem eventually_inputs_le_budget : | ||
| ∀ᶠ n : ℕ in atTop, n + 1 ≤ 2 ^ n / n := by |
There was a problem hiding this comment.
∀ᶠ n : ℕ in atTop, n ≤ 2 ^ n / n could also be a generic theorem
There was a problem hiding this comment.
Extracted public Nat.eventually_add_one_le_pow_div into Foundations/Data/Nat/Asymptotics.lean, retaining the stronger n + 1 bound and generalizing to natural bases greater than one.
2badbfa to
85805b8
Compare
| deriving DecidableEq | ||
|
|
||
| instance Op.instFintype : Fintype Op where | ||
| elems := {.const false, .const true, .not, .and, .or} | ||
| complete := by intro op; cases op <;> simp |
There was a problem hiding this comment.
We can save the instance by deriving also Fintype and proving that the cardinality is 5
| deriving DecidableEq | |
| instance Op.instFintype : Fintype Op where | |
| elems := {.const false, .const true, .not, .and, .or} | |
| complete := by intro op; cases op <;> simp | |
| deriving DecidableEq, Fintype | |
| @[simp] theorem Op.card : Fintype.card Op = 5 := rfl |
This needs the imports above swapped as well, and changing the proof in Cslib/Computability/Circuit/Boolean/Counting.lean:84 to just simp
There was a problem hiding this comment.
Fantastic! Thank you.
| classical | ||
| simp [irredundantFunctions] | ||
|
|
||
| private def lineEquiv (n g : ℕ) : |
There was a problem hiding this comment.
the content of lines 64-84 is generic over σ. Only Arity op ≤ 2 and card Op = 5 are actually used.
I think that lineEquiv should be in Program.lean and the Fintype instance
plus the cardinality lemmas into a new standalone file under Circuit/
| left_inv _ := rfl | ||
| right_inv _ := rfl | ||
|
|
||
| private noncomputable instance : Fintype (Line signature n g) := |
There was a problem hiding this comment.
The noncomputable doesn't look needed
There was a problem hiding this comment.
Maybe the file should define
def Program.Irredundant (p : Program σ n g) (i : Interpretation σ U) : Prop := Function.Injective (p.gateFunction i)
and analogously for circuits?
0a41372 to
e5d3371
Compare
Add semantic normalization and counting to prove the worst-case 2^n/n lower bound for De Morgan circuits.
Extract computable finite circuit syntax and factorial-corrected counting over arbitrary interpretations. Name semantic irredundancy and specialize the generic bounds to De Morgan circuits. Extend Shannon to every finite Boolean basis of arity at most two, and cover infinite carriers, empty signatures, nullary operations, and shared outputs in tests. Incorporate barni120400’s review suggestions.
85805b8 to
c387e6c
Compare
Prove the |U|^n/n lower bound for every finite nontrivial carrier and finite operation signature with arities at most two. The Boolean theorem is a specialization; the tests also instantiate a three-valued carrier.
3 participants
Add semantic normalization and counting to prove the worst-case 2^n/n lower bound for De Morgan circuits.
Assisted by Codex, adapted from https://github.com/samuelSchlesinger/algebraic-circuits.