feat(Complexity): Query Complexity of Boolean Functions (aka Decision…

[Lsonic233]

Defines three Boolean function complexity measures : sensitivity s(f), block sensitivity bs(f) and certificate complexity C(f) with the inequality chain : s(f) ≤ bs(f) ≤ C(f).

• Defs.lean sets up the boolean hypercube and boolean functions which is defined as a function from {0,1}^n to {0,1}.
• Measures.lean defines the above three measures and proves the inequality chain.
• Deterministic Decision Trees and D(f) : the decision tree complexity of boolean function f will follow in a second PR.

AI usage : Used claude to help me fill in proofs in a few places and refactor my handwritten proofs.

[crei]

I mean it's kind of trivial but maybe you should sync some of the definitions here with #890 ?

[SamuelSchlesinger]

Yeah, I'm working out the right way to do that and I'll include this refactor in a forthcoming PR.

[SamuelSchlesinger]

That is merged now, you can use BooleanFunction and BitString.

[crei]

Do you have a reference for naming this object Cube? Wouldn't "Assignment" be easier to understand?

[Lsonic233]

Cube is short for the boolean hypercube (or hamming cube) which views {0,1}^n as vertices of a graph such that two strings are connected by an edge if their hamming distance is 1. Analysis of Boolean Functions by O'Donnell also calls it that.
If you prefer not to have Cube, then would something like "Input" or "BooleanInput" be better than "Assignment"?
"Assignment" is the term used for partial assignments in the survey by BuhrmanDeWolf. See the section Certificate Complexity.

[crei]

I don't want to argue with O'Donnell but isn't what you define rather a point in the hypercube than the hypercube itself?
I think I would prefer PartialAssignment for partial assignments. The article you link does not formally introduce the concept and only uses it twice.
I'm mostly concerned about the same definition having different names in different directories of cslib and in general creating confusion. If some terms are only used locally thisis fine but I think these definitions could be made more widely available.

Maybe @SamuelSchlesinger also has an opinion.

[Lsonic233]

I think the type here is the hypercube (#eval Fintype.card (Cube 3) gives 8) and x : Cube n is a point of Cube n. I should probably change the docstring above it to say something like "The boolean hypercube whose points are bit strings of length n".
For partial assignments - I agree I'll change Assignment in my code to PartialAssignment.
Yeah I think we should work on some infra for BooleanFunctions ({0,1}^n -> {0,1}) especially now that #890 is merged and it uses it. This would require some coordination on zulip.

[SamuelSchlesinger]

I think we should have global definitions for Boolean strings of known size somewhere. I believe we shouldn't call it Cube but BitString or BitVec is a reasonable name.

[SamuelSchlesinger]

I added these in #943.

[crei]

If you rename Cube to Assignment, then this could be PartialAssignment (and also could be in general)

[Lsonic233]

My bad, my main reference and the place I studied this topic from is the Buhrman and de Wolf survey so most of my naming choices match that rather than Arora-Barak. I've addressed this in my previous comment.

[crei]

Sorry that I have so many remarks about terminology and please push back, but Arora-Bark talks about "bit position". I know it makes sense when talking about hypercubes and so on, but currently, "index" would be equally valid and understandable, right?

[Lsonic233]

I agree, "index" and "coordinate" are interchangeable. I'd keep "coordinate" because thats what most of the definitions about blocks use in the file.

[crei]

Do we really need this definition?

[Lsonic233]

It's there to follow the same pattern as sensitiveCoords and singletonFamily. I could remove it and inline it - don't think it would make much of a difference.

[crei]

Sorry for the many comments! In general, this is a good contribution, it just has so many definitions :)
Feel free to push back and we can also talk about in the chat or in a call.
Another final comment: Shouldn't this be "CommunicationComplexity" instead of "QueryComplexity"?

[Lsonic233]

Sorry for the many comments! In general, this is a good contribution, it just has so many definitions :) Feel free to push back and we can also talk about in the chat or in a call. Another final comment: Shouldn't this be "CommunicationComplexity" instead of "QueryComplexity"?

Sure, I'll send you a zulip dm and make a thread about this topic in a bit.
"Communication Complexity" refers to a completely different model of computation where two parties (where the inputs are distributed between them ) try to compute a boolean function by communicating bits of info.
"Query Complexity" or Decision Tree Complexity is the boolean decision tree model of computation (I have a second PR ready defining boolean decision trees and the decision tree complexity D(f) and proving that C(f) <= D(f)).

[crei]

Sure, I'll send you a zulip dm and make a thread about this topic in a bit. "Communication Complexity" refers to a completely different model of computation where two parties (where the inputs are distributed between them ) try to compute a boolean function by communicating bits of info. "Query Complexity" or Decision Tree Complexity is the boolean decision tree model of computation (I have a second PR ready defining boolean decision trees and the decision tree complexity D(f) and proving that C(f) <= D(f)).

Right, I confused the chapters in Arora-Barak

[SamuelSchlesinger]

This is great. I'm under the impression we can simplify this PR quite a bit and get something basically the right shape, but overall this is the right first direction. Thank you for the contribution! I am working on a more detailed review.

[SamuelSchlesinger]

This is great, I am very close to approval but I just want to see this one change so we can make the proofs a bit tighter. We can do the BitString and BooleanFunction reuse in a followup unless #943 lands first.

[SamuelSchlesinger]

I like keeping PartialAssignment as a general object. At a fixed input x, though, an assignment agreeing with x is determined entirely by its support. Would you consider defining pointwise certificates using a set of coordinates, with a lemma connecting that view to PartialAssignment? I think that would simplify C_x(f) and the bs_x(f) <= C_x(f) proof.

[Lsonic233]

I played around with your idea of defining point certificates using just coordinate sets (instead of appealing to IsCertificate) and here is the definition I am working with (Fixes in the code below).

def Fixes (f : BoolFunc n) (x : Cube n) (S : Finset (Fin n)) : Prop :=
  ∀ y, (∀ i ∈ S, y i = x i) → f y = f x

instance (f : BoolFunc n) (x : Cube n) (S : Finset (Fin n)) : Decidable (Fixes f x S) :=
  inferInstanceAs (Decidable (∀ y, (∀ i ∈ S, y i = x i) → f y = f x))

lemma fixes_univ (f : BoolFunc n) (x : Cube n) : Fixes f x Finset.univ :=
  fun _ hy => congrArg f (funext fun i => hy i (Finset.mem_univ i))

lemma fixes_nonempty (f : BoolFunc n) (x : Cube n) :
    (Finset.univ.filter (Fixes f x)).Nonempty :=
  ⟨Finset.univ, Finset.mem_filter.mpr ⟨Finset.mem_univ _, fixes_univ f x⟩⟩

def pointCertificateComplexity (f : BoolFunc n) (x : Cube n) : ℕ :=
  (Finset.univ.filter (Fixes f x)).inf' (fixes_nonempty f x) Finset.card

I still think we need IsbCertificate for theorems like Theorem10 we need $C^{1}(f)$ and $C^{0}(f)$. Also I just found out that the Barak Arora textbook follows your way of defining $C_x(f)$ which is different from how the Buhrman and de Wolf defines it (this is the one I used for my implementation).
The proofs for $bs_x(f) \leq C_x(f)$ are not significantly shorter (maybe a few lines across the main theorem and supporting lemmas). I could push a demo of these proofs if you'd like.

[Lsonic233]

@SamuelSchlesinger gentle ping in case you have any further comments? I've made the suggested changes - point certificates are defined using subsets of input bit-string, fixes_iff_isCertificate_restrict, isCertificate_iff_fixes_support which are the connecting lemmas to PartialAssignment.

[Lsonic233]

@SamuelSchlesinger I left a reply on your previous comment regarding your suggestion for an alternate path for defining Certificates. Here is a full demo in a separate branch. Wanted to get your thoughts and would like to know if this is what you were talking about. My comparison of the two approaches is in my previous comment.

[SamuelSchlesinger]

Yes, exactly. The only thing missing is if hx : Agrees C x, then Fixes f x (support C) ↔ IsCertificate f C (f x). We also want the converse restricting x to a coordinate set. Could you add that and bring the demo into the PR? The shape looks good.

[SamuelSchlesinger]

Let's also replace Cube with BitString.

[Lsonic233]

Made this change and replaced Cube with BitString. Added to Defs.lean a def restrict (x : BitString n) (S : Finset (Fin n)) : PartialAssignment n (which creates a partial assignment out of a subset of [n]) for the converse of the statement in your previous comment.

[Lsonic233]

@SamuelSchlesinger I've made #925 ready for review which depends on this. We can start discussing that if this looks good.

[SamuelSchlesinger]

Thanks, the set-based Cₓ(f) refactor came out well and the math all looks right. Two doc fixes (stale DecisionTree.lean/D(f) references), one name shadowing, and a handful of nits below, mostly naming; the only ones with any design weight are the Cslib.BitString namespace for flips and sensitivity, which I'm happy to do as a follow-up, and swapping the Fixes/IsCertificate names to match Jukna. None of these block merging as far as I'm concerned.

[SamuelSchlesinger]

DecisionTree.lean is in #925 rather than here. Could the module doc describe only what this PR adds? The follow-up can extend it when the decision tree file lands.

[SamuelSchlesinger]

Nit: flipBlock and sensitivity are basic operations on the cube that other developments will want (subcube arguments on CNF solution sets, isolated inputs for DNF lower bounds, average sensitivity). I'd put them in the Cslib.BitString namespace next to BitString and BooleanFunction, keeping block sensitivity and certificates here. Fine as a follow-up if you'd rather not widen this PR.

[SamuelSchlesinger]

Nit: since this is Function.update x i (!x i) and the docstring wants the update simp set to apply, I'd either use the update expression directly (with flipBlock_singleton as the simp normal form, dropping flipBit_flipBit) or make this an abbrev, so that proofs don't need to unfold it first, as flipBit_flipBit, flipBlock_singleton and flipBlock_erase all do.

[SamuelSchlesinger]

Nit: consider the set-first order flipBlock B x, so flipBlock B is a map on the cube and flipBlock_flipBlock can be stated as Function.Involutive (flipBlock B), which is what bijection arguments on sets of inputs want. Independently, this is definitionally B.piecewise (fun j => !x j) x; a rfl lemma saying so gives access to the Finset.piecewise API.

[SamuelSchlesinger]

Nit on naming, applies to all three pointwise measures: sensitivityAt f x, blockSensitivityAt f x, certificateComplexityAt f x would read as Jukna's s(f, x), bs(f, x), C(f, x) and follow Mathlib's *At convention for "at a point"; point* is not a prefix I've seen elsewhere.

[SamuelSchlesinger]

Nit: this is word for word Jukna's "f-certificate of a" (Section 14.3: a set S of positions such that f(b) = f(a) whenever b agrees with a on S), so IsCertificate f x S would be the recognisable name, and then Cₓ(f) reads as "least size of a certificate for x" like in the book. "Fixes" also already means "fixes coordinate i to b" in the PartialAssignment docstring in Defs.lean, so the verb is doing double duty. The partial-assignment version could then take the name its docstring already uses, Forces f C b.

[SamuelSchlesinger]

Nit: keeping this decidable via inf' is nice (the decide examples are a real plus). One lemma the follow-up will want is attainment, ∃ S, Fixes f x S ∧ S.card = pointCertificateComplexity f x, from Finset.exists_mem_eq_inf'; the D ≤ C₀ C₁ proof starts with "take a smallest certificate for x".

[SamuelSchlesinger]

Nit: the global versions would be good to have alongside this: sensitivity f ≤ n (Finset.card_le_univ), blockSensitivity f ≤ n (from bsₓ ≤ Cₓ ≤ n) and certificateComplexity f ≤ n, each a Finset.sup_le away. They are what an = n result for general n (parity, OR) reduces to: ≤ n plus a lower bound.

[SamuelSchlesinger]

Nit: x and B can be implicit here, since hB determines them (as f already is); the call in card_le_card_of_isSensitiveFamily then shrinks to sensitiveBlock_inter_nonempty (hF.1 B hB) hS.

[SamuelSchlesinger]

The header still describes D(f) and claims the chain s ≤ bs ≤ C ≤ D; same for the D = n remark under OR, D = 3 under MAJ₃ and "the trivial tree" under constants. Could these be trimmed to the three measures in this PR? #925 can put the D remarks back with its own examples.