diff --git a/Complexity.lean b/Complexity.lean index f08f52b9d2..ff3f15e457 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -979,6 +979,7 @@ public import Complexity.Computability.Communication.Lifting.Gadget public import Complexity.Computability.Communication.Lifting.Partition public import Complexity.Computability.Communication.Lifting.Simulation public import Complexity.Computability.Communication.Newman +public import Complexity.Computability.Communication.Nondeterministic.Basic public import Complexity.Computability.Communication.Operations public import Complexity.Computability.Communication.Protocol public import Complexity.Computability.Communication.Randomized diff --git a/Complexity/Computability/Communication/Nondeterministic/Basic.lean b/Complexity/Computability/Communication/Nondeterministic/Basic.lean new file mode 100644 index 0000000000..f259d06532 --- /dev/null +++ b/Complexity/Computability/Communication/Nondeterministic/Basic.lean @@ -0,0 +1,364 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Communication.FoolingSet +public import Complexity.Computability.Communication.Rectangle +public import Complexity.Foundations.Data.BitString.Basic + +/-! +# Nondeterministic communication complexity + +Nondeterministic communication complexity for the answer `z : Bool` is defined by covers +[Kushilevitz and Nisan, Definition 2.3, p. 18][KushilevitzNisan1997]. For a relation +`R : X → Y → Bool → Prop`, a *`z`-cover* of `R` on `A × B` by `2 ^ k` rectangles is a family of +rectangles indexed by the `k`-bit guesses such that `z` is an acceptable answer on the part of each +rectangle inside `A × B`, and every pair of `A × B` on which `!z` is not acceptable lies in some +rectangle (`Nondeterministic.IsCover`). The complexity `Nondeterministic.ecomplexity z R A B` is the +least such `k`, or `⊤` if there is none; in particular it is `⊤` if no answer is acceptable on some +pair of `A × B`, as for `Protocol.ecomplexity`. For a function `f : X → Y → Bool`, +`Nondeterministic.ecomplexityFun z f A B` is the complexity of the relation `f x y = b`; its +`z`-covers are families of rectangles on which `f` is `z` inside `A × B` that contain every pair of +`A × B` on which `f` is `z` (`Nondeterministic.isCover_fun_iff`). Thus `ecomplexityFun true f` and +`ecomplexityFun false f` are `⌈log₂ C^z(f)⌉`, where `C^z(f)` is the least number of rectangles in a +`z`-cover [Kushilevitz and Nisan, Definition 2.1(4), p. 17][KushilevitzNisan1997] (and `0` when `f` +never takes the value `z` on `A × B`). + +Kushilevitz and Nisan define `N^z(f) = log₂ C^z(f)` for a Boolean function `f` on all of `X × Y`, +without rounding. So for such `f`, `ecomplexityFun z f Set.univ Set.univ` is their `N^z(f)` rounded +up to an integer, and for `n ≥ 1` a lower bound `n ≤ ecomplexityFun z f Set.univ Set.univ` says +`C^z(f) > 2 ^ (n - 1)`, that is, `N^z(f) > n - 1` in their convention. + +The model here lies between the total Boolean functions of their Definition 2.1 and the relations +with arbitrary answers of [Kushilevitz and Nisan, Chapter 5][KushilevitzNisan1997]: it covers +partial Boolean functions, which are relations with Boolean answers. For these it is the model NP of +[Göös, Pitassi and Watson, Definition B.1][GoosPitassiWatson2018Landscape] +([author copy](https://par.nsf.gov/servlets/purl/10090758), p. 44): a collection of +`2 ^ k` rectangles indexed by `k`-bit witnesses, whose output is `1` exactly on their union, correct +on the domain of the function, of cost `k`; co-classes are defined by negating the function. A +partial function is a function together with the sets `A` and `B`, or, when its domain is not a +rectangle, a relation that accepts both answers outside its domain; its values there do not matter, +and rectangles are not required to lie inside the domain. Kushilevitz and Nisan remark after +Definition 5.2 that for relations, measures such as `N¹(R)` are less interesting, since the answer +`1` has no special role; with Boolean answers, `N⁰` and `N¹` keep their meaning. + +A relation `R : X → Y → Bool → Prop` is their relation `R ⊆ X × Y × Z` with `Z = Bool` +[Kushilevitz and Nisan, Definition 5.1, p. 71][KushilevitzNisan1997]: `R x y b` holds exactly when +`(x, y, b) ∈ R`. A partial Boolean function `f` with domain `D` is the relation +`fun x y b => (x, y) ∈ D → f x y = b`. Kushilevitz and Nisan require a protocol for a relation to be +correct only on legal inputs, those with some acceptable answer, and define the other measures for +relations "in a similar manner" +[Kushilevitz and Nisan, Definition 5.2, p. 71][KushilevitzNisan1997]. Here, as for +`Protocol.ecomplexity`, which is stated for relations, every pair of `A × B` must get an acceptable +answer, so a pair of `A × B` with no acceptable answer makes the complexity `⊤`. Just before +Definition 5.2 they note the alternative of extending a relation to allow every answer on its +illegal pairs; their convention for `R` is this one for that extension, which is no harder than `R` +(`Nondeterministic.ecomplexity_le_of_imp`). + +## Covers and protocols + +Covers count rectangles; no bits are spent announcing the answer. Protocols must announce it, and +conventions differ on who must learn it. In `Protocol` the answer is a function of the transcript, +so both players know it; for instance, equality on `v`-bit strings has deterministic complexity +`v + 1` for `v ≥ 1` (`Cslib.Communication.ecomplexityFun_equality`). For nondeterministic protocols +in the same convention, where the guessed bits count towards the cost and at the end both players +know whether to accept, the two notions differ by at most two bits: + +* a protocol of cost `c` gives a cover by at most `2 ^ c` rectangles, one for each accepting + transcript, so a lower bound on `ecomplexity` is a lower bound for protocols, whatever the + convention for announcing the answer; +* a cover by `2 ^ k` rectangles gives a protocol of cost `k + 2`: the `k` guessed bits name a + rectangle, and Alice and Bob each send one bit saying whether their input lies in its side. If + only one player needs to learn the answer, Bob need not reply, and the cost is `k + 1`. + +So `ecomplexity z R A B ≤ k` gives a protocol of cost `k + 2`, and a protocol of cost `c`, once +converted to a cover, gives `ecomplexity z R A B ≤ c` (`Nondeterministic.ecomplexity_le_iff`). +Deterministic protocols give covers directly (`Nondeterministic.ecomplexity_le_protocol`). + +## Main definitions + +* `Cslib.Communication.Nondeterministic.IsCover`, `Cslib.Communication.Nondeterministic.HasCover`: + covers of a relation by rectangles. +* `Cslib.Communication.Nondeterministic.ecomplexity`: nondeterministic communication complexity of a + relation on `A × B` for the answer `z`. +* `Cslib.Communication.Nondeterministic.ecomplexityFun`: the same for a function, as the relation + `f x y = b`. + +## Main results + +* `Cslib.Communication.Nondeterministic.ecomplexity_le_iff`, + `Cslib.Communication.Nondeterministic.le_ecomplexity_iff`, + `Cslib.Communication.Nondeterministic.HasCover.ecomplexity_le`: upper and lower bounds through + covers; `Cslib.Communication.Nondeterministic.ecomplexityFun_le_iff` and + `Cslib.Communication.Nondeterministic.le_ecomplexityFun_iff` for functions. +* `Cslib.Communication.Nondeterministic.isCover_fun_iff`: covers of a function. +* `Cslib.Communication.Nondeterministic.HasCover.mono_bits`: more guessed bits do no harm. +* `Cslib.Communication.Nondeterministic.HasCover.mono`, + `Cslib.Communication.Nondeterministic.ecomplexity_mono`, + `Cslib.Communication.Nondeterministic.ecomplexityFun_mono`: monotonicity in the domain. +* `Cslib.Communication.Nondeterministic.HasCover.of_imp`, + `Cslib.Communication.Nondeterministic.ecomplexity_le_of_imp`: a weaker relation is no harder. +* `Cslib.Communication.Nondeterministic.ecomplexity_not`, + `Cslib.Communication.Nondeterministic.ecomplexityFun_not`: `N⁰` is `N¹` of the negation. +* `Cslib.Communication.Nondeterministic.HasCover.card_le`, + `Cslib.Communication.Nondeterministic.le_ecomplexityFun_of_isFoolingSet`: a fooling set of + `2 ^ n` pairs with value `z` forces `n`. +* `Cslib.Communication.Nondeterministic.HasCover.card_le_two_pow_mul`: on a finite domain, if every + `z`-rectangle has at most `K` pairs, then a `z`-cover by `2 ^ k` rectangles covers at most + `2 ^ k * K` pairs. +* `Cslib.Communication.Protocol.Solves.hasCover`, + `Cslib.Communication.Nondeterministic.ecomplexity_le_protocol`, + `Cslib.Communication.Nondeterministic.ecomplexityFun_le_protocol`: nondeterministic complexity is + at most deterministic complexity. + +## References + +* [M. Göös, T. Pitassi, T. Watson, *The Landscape of Communication Complexity + Classes*][GoosPitassiWatson2018Landscape], Appendix B +* [E. Kushilevitz, N. Nisan, *Communication Complexity*][KushilevitzNisan1997] +-/ + +public section + +namespace Cslib.Communication + +namespace Nondeterministic + +open Finset + +variable {X Y : Type*} + +/-- `C` is a `z`-cover of the relation `R` on `A × B` by `2 ^ k` rectangles: `z` is an acceptable +answer on the part of each rectangle inside `A × B`, and every pair of `A × B` on which `!z` is not +acceptable lies in some rectangle. -/ +@[expose] def IsCover (z : Bool) (R : X → Y → Bool → Prop) (A : Set X) (B : Set Y) {k : ℕ} + (C : BitString k → Set X × Set Y) : Prop := + (∀ w, ∀ x ∈ A, x ∈ (C w).1 → ∀ y ∈ B, y ∈ (C w).2 → R x y z) ∧ + ∀ x ∈ A, ∀ y ∈ B, ¬R x y (!z) → ∃ w, x ∈ (C w).1 ∧ y ∈ (C w).2 + +/-- The relation `R` has a `z`-cover on `A × B` by `2 ^ k` rectangles. -/ +@[expose] def HasCover (z : Bool) (R : X → Y → Bool → Prop) (A : Set X) (B : Set Y) (k : ℕ) : + Prop := + ∃ C : BitString k → Set X × Set Y, IsCover z R A B C + +/-- The nondeterministic communication complexity of the relation `R` on `A × B` for the answer +`z`: the least `k` such that `R` has a `z`-cover on `A × B` by `2 ^ k` rectangles, or `⊤` if there +is none. -/ +noncomputable def ecomplexity (z : Bool) (R : X → Y → Bool → Prop) (A : Set X) (B : Set Y) : ℕ∞ := + ⨅ k : {k : ℕ // HasCover z R A B k}, (k.1 : ℕ∞) + +/-- The nondeterministic communication complexity of `f` on `A × B` for the value `z`: +`ecomplexity` of the relation `f x y = b`. `N¹` is `z = true`, and `N⁰` is `z = false`. -/ +@[expose] noncomputable def ecomplexityFun (z : Bool) (f : X → Y → Bool) (A : Set X) (B : Set Y) : + ℕ∞ := + ecomplexity z (fun x y b => f x y = b) A B + +variable {R R' : X → Y → Bool → Prop} {f : X → Y → Bool} {z : Bool} {A A' : Set X} {B B' : Set Y} + {j k : ℕ} + +/-- A `z`-cover of a function: `f` is `z` on the part of each rectangle inside `A × B`, and every +pair of `A × B` on which `f` is `z` lies in some rectangle. -/ +theorem isCover_fun_iff {C : BitString k → Set X × Set Y} : + IsCover z (fun x y b => f x y = b) A B C ↔ + (∀ w, ∀ x ∈ A, x ∈ (C w).1 → ∀ y ∈ B, y ∈ (C w).2 → f x y = z) ∧ + ∀ x ∈ A, ∀ y ∈ B, f x y = z → ∃ w, x ∈ (C w).1 ∧ y ∈ (C w).2 := by + simp only [IsCover, Bool.eq_not, not_not] + +/-! ### Upper and lower bounds -/ + +/-- A cover by `2 ^ k` rectangles bounds the complexity by `k`. -/ +theorem HasCover.ecomplexity_le (h : HasCover z R A B k) : ecomplexity z R A B ≤ k := + iInf_le (fun k : {k : ℕ // HasCover z R A B k} => (k.1 : ℕ∞)) ⟨k, h⟩ + +/-- A cover by `2 ^ j` rectangles gives one by `2 ^ k` rectangles for `j ≤ k`: ignore the extra +guessed bits. -/ +theorem HasCover.mono_bits (hjk : j ≤ k) (h : HasCover z R A B j) : HasCover z R A B k := by + obtain ⟨C, hmem, hcov⟩ := h + refine ⟨fun w => C fun i => w (Fin.castLE hjk i), fun w => hmem _, fun x hx y hy hR => ?_⟩ + obtain ⟨w, hw⟩ := hcov x hx y hy hR + refine ⟨fun i => if hi : (i : ℕ) < j then w ⟨i, hi⟩ else false, ?_⟩ + simpa using hw + +/-- Lower bounds on nondeterministic complexity are lower bounds on the number of guessed bits of +every cover. -/ +theorem le_ecomplexity_iff {c : ℕ∞} : + c ≤ ecomplexity z R A B ↔ ∀ k, HasCover z R A B k → c ≤ k := by + simp [ecomplexity, le_iInf_iff, Subtype.forall] + +/-- `R` has nondeterministic complexity at most `k` exactly when it has a `z`-cover by `2 ^ k` +rectangles. -/ +theorem ecomplexity_le_iff : ecomplexity z R A B ≤ k ↔ HasCover z R A B k := by + refine ⟨fun h => ?_, HasCover.ecomplexity_le⟩ + have : Nonempty {k : ℕ // HasCover z R A B k} := by + rw [← ENat.iInf_natCast_ne_top] + exact ne_top_of_le_ne_top (ENat.natCast_ne_top k) h + obtain ⟨⟨j, hj⟩, hmin⟩ := ENat.exists_eq_iInf + (fun k : {k : ℕ // HasCover z R A B k} => (k.1 : ℕ∞)) + exact hj.mono_bits (by exact_mod_cast (hmin.trans_le h : (j : ℕ∞) ≤ k)) + +/-- `ecomplexity_le_iff` for functions. -/ +theorem ecomplexityFun_le_iff : + ecomplexityFun z f A B ≤ k ↔ HasCover z (fun x y b => f x y = b) A B k := + ecomplexity_le_iff + +/-- `le_ecomplexity_iff` for functions. -/ +theorem le_ecomplexityFun_iff {c : ℕ∞} : + c ≤ ecomplexityFun z f A B ↔ ∀ k, HasCover z (fun x y b => f x y = b) A B k → c ≤ k := + le_ecomplexity_iff + +/-! ### Monotonicity -/ + +/-- A cover on `A × B` is a cover on any smaller domain. -/ +theorem HasCover.mono (hA : A' ⊆ A) (hB : B' ⊆ B) (h : HasCover z R A B k) : + HasCover z R A' B' k := by + obtain ⟨C, hmem, hcov⟩ := h + exact ⟨C, fun w x hx hxC y hy hyC => hmem w x (hA hx) hxC y (hB hy) hyC, + fun x hx y hy hR => hcov x (hA hx) y (hB hy) hR⟩ + +/-- A cover of `R` is a cover of every weaker relation. -/ +theorem HasCover.of_imp (hR : ∀ x y b, R x y b → R' x y b) (h : HasCover z R A B k) : + HasCover z R' A B k := by + obtain ⟨C, hmem, hcov⟩ := h + exact ⟨C, fun w x hx hxC y hy hyC => hR x y z (hmem w x hx hxC y hy hyC), + fun x hx y hy hR' => hcov x hx y hy fun h => hR' (hR x y _ h)⟩ + +/-- Nondeterministic complexity is monotone in the domain. -/ +theorem ecomplexity_mono (hA : A' ⊆ A) (hB : B' ⊆ B) : + ecomplexity z R A' B' ≤ ecomplexity z R A B := + le_ecomplexity_iff.mpr fun _ hk => (hk.mono hA hB).ecomplexity_le + +/-- `ecomplexity_mono` for functions. -/ +theorem ecomplexityFun_mono (hA : A' ⊆ A) (hB : B' ⊆ B) : + ecomplexityFun z f A' B' ≤ ecomplexityFun z f A B := + ecomplexity_mono hA hB + +/-- A weaker relation is no harder. -/ +theorem ecomplexity_le_of_imp (hR : ∀ x y b, R x y b → R' x y b) : + ecomplexity z R' A B ≤ ecomplexity z R A B := + le_ecomplexity_iff.mpr fun _ hk => (hk.of_imp hR).ecomplexity_le + +/-! ### Negation -/ + +/-- Exchanging the answers exchanges `N⁰` and `N¹`. -/ +theorem ecomplexity_not : + ecomplexity z (fun x y b => R x y (!b)) A B = ecomplexity (!z) R A B := by + have hiff : ∀ k, HasCover z (fun x y b => R x y (!b)) A B k ↔ HasCover (!z) R A B k := fun k => by + simp only [HasCover, IsCover, Bool.not_not] + exact le_antisymm (le_ecomplexity_iff.mpr fun k hk => ((hiff k).mpr hk).ecomplexity_le) + (le_ecomplexity_iff.mpr fun k hk => ((hiff k).mp hk).ecomplexity_le) + +/-- `N⁰` of `f` is `N¹` of its negation, and conversely. -/ +@[simp] theorem ecomplexityFun_not : + ecomplexityFun z (fun x y => !f x y) A B = ecomplexityFun (!z) f A B := by + rw [ecomplexityFun, ecomplexityFun, ← ecomplexity_not] + simp only [Bool.not_eq_eq_eq_not] + +/-! ### Lower bounds -/ + +/-- **The fooling-set bound, for covers.** A fooling set for `f` with value `z` inside `A × B` +has at most `2 ^ k` pairs if `f` has a `z`-cover on `A × B` by `2 ^ k` rectangles: no rectangle +contains two of its pairs. -/ +theorem HasCover.card_le {S : Finset (X × Y)} (hS : IsFoolingSet f z S) + (hSAB : ∀ q ∈ S, q.1 ∈ A ∧ q.2 ∈ B) (h : HasCover z (fun x y b => f x y = b) A B k) : + #S ≤ 2 ^ k := by + classical + obtain ⟨C, hC⟩ := h + obtain ⟨hmem, hcov⟩ := isCover_fun_iff.mp hC + have hw : ∀ q ∈ S, ∃ w, q.1 ∈ (C w).1 ∧ q.2 ∈ (C w).2 := fun q hq => + hcov _ (hSAB q hq).1 _ (hSAB q hq).2 (hS.1 q hq) + choose! g hg using hw + calc #S ≤ #(univ : Finset (BitString k)) := by + refine card_le_card_of_injOn g (by intro _ _; exact mem_univ _) ?_ + intro q hq q' hq' hqq + refine hS.2 q hq q' hq' ?_ ?_ + · exact hmem (g q) _ (hSAB q hq).1 (hg q hq).1 _ (hSAB q' hq').2 + (by rw [hqq]; exact (hg q' hq').2) + · exact hmem (g q) _ (hSAB q' hq').1 (by rw [hqq]; exact (hg q' hq').1) _ + (hSAB q hq).2 (hg q hq).2 + _ = 2 ^ k := by rw [card_univ, BitString.card] + +/-- **The fooling-set bound on nondeterministic complexity.** A fooling set of at least `2 ^ n` +pairs for `f` with value `z` inside `A × B` forces `n`. -/ +theorem le_ecomplexityFun_of_isFoolingSet {S : Finset (X × Y)} (hS : IsFoolingSet f z S) + (hSAB : ∀ q ∈ S, q.1 ∈ A ∧ q.2 ∈ B) {n : ℕ} (hn : 2 ^ n ≤ #S) : + (n : ℕ∞) ≤ ecomplexityFun z f A B := + le_ecomplexityFun_iff.mpr fun _ hk => by + have := hn.trans (hk.card_le hS hSAB) + exact_mod_cast (Nat.pow_le_pow_iff_right (by norm_num)).mp this + +/-- **The rectangle-size bound.** Let `s` and `t` be finite. If every rectangle inside `s × t` on +which `f` is constantly `z` has at most `K` pairs, then a `z`-cover of `f` on `s × t` by `2 ^ k` +rectangles covers at most `2 ^ k * K` pairs, so `f` is `z` on at most `2 ^ k * K` pairs of +`s × t`. -/ +theorem HasCover.card_le_two_pow_mul {s : Finset X} {t : Finset Y} {K : ℕ} + (hK : ∀ S ⊆ s, ∀ T ⊆ t, (∀ x ∈ S, ∀ y ∈ T, f x y = z) → #S * #T ≤ K) + (h : HasCover z (fun x y b => f x y = b) s t k) : + #{q ∈ s ×ˢ t | f q.1 q.2 = z} ≤ 2 ^ k * K := by + classical + obtain ⟨C, hC⟩ := h + obtain ⟨hmem, hcov⟩ := isCover_fun_iff.mp hC + let S : BitString k → Finset X := fun w => {x ∈ s | x ∈ (C w).1} + let T : BitString k → Finset Y := fun w => {y ∈ t | y ∈ (C w).2} + have hsub : {q ∈ s ×ˢ t | f q.1 q.2 = z} ⊆ univ.biUnion fun w => S w ×ˢ T w := by + intro q hq + simp only [mem_filter, mem_product] at hq + obtain ⟨w, hx, hy⟩ := hcov q.1 hq.1.1 q.2 hq.1.2 hq.2 + simp only [mem_biUnion, mem_univ, true_and, mem_product, mem_filter, S, T] + exact ⟨w, ⟨hq.1.1, hx⟩, hq.1.2, hy⟩ + calc #{q ∈ s ×ˢ t | f q.1 q.2 = z} ≤ #(univ.biUnion fun w => S w ×ˢ T w) := card_le_card hsub + _ ≤ ∑ w, #(S w ×ˢ T w) := card_biUnion_le + _ ≤ ∑ _w : BitString k, K := by + refine sum_le_sum fun w _ => ?_ + rw [card_product] + refine hK _ (filter_subset _ _) _ (filter_subset _ _) fun x hx y hy => ?_ + simp only [mem_filter, T] at hx hy + exact hmem w x hx.1 hx.2 y hy.1 hy.2 + _ = 2 ^ k * K := by rw [sum_const, card_univ, BitString.card, smul_eq_mul] + +/-! ### Comparison with deterministic complexity -/ + +/-- The leaves with output `z` of a deterministic protocol solving `R` on `A × B` form a `z`-cover +of `R` by `2 ^ depth` rectangles. -/ +theorem _root_.Cslib.Communication.Protocol.Solves.hasCover {p : Protocol X Y Bool} + (hp : p.Solves R A B) (z : Bool) : + HasCover z R A B p.depth := by + classical + let e := BitString.equivFin p.depth + refine ⟨fun w => if h : (e w : ℕ) < p.leafCount then + if p.leafOutput ⟨e w, h⟩ = z then (p.leafAlice ⟨e w, h⟩, p.leafBob ⟨e w, h⟩) else (∅, ∅) + else (∅, ∅), fun w x hxA hx y hyB hy => ?_, fun x hxA y hyB hR => ?_⟩ + · by_cases h : (e w : ℕ) < p.leafCount + · by_cases hz : p.leafOutput ⟨e w, h⟩ = z + · simp only [h, hz, dite_true, ite_true] at hx hy + have := hp x hxA y hyB + rwa [Protocol.run_eq_leafOutput hx hy, hz] at this + · simp [h, hz] at hx + · simp [h] at hx + · have hlt : (p.leaf x y : ℕ) < 2 ^ p.depth := + (p.leaf x y).2.trans_le p.leafCount_le_two_pow_depth + refine ⟨e.symm ⟨p.leaf x y, hlt⟩, ?_⟩ + have hrun : p.run x y = z := by + have := hp x hxA y hyB + cases hb : p.run x y <;> cases z <;> simp_all + have hz : p.leafOutput (p.leaf x y) = z := by rw [← Protocol.run_eq_leafOutput_leaf, hrun] + simp only [Equiv.apply_symm_apply, (p.leaf x y).2, dite_true, Fin.eta, hz, ite_true] + exact ⟨Protocol.mem_leafAlice_leaf, Protocol.mem_leafBob_leaf⟩ + +/-- **Nondeterministic complexity is at most deterministic complexity.** -/ +theorem ecomplexity_le_protocol (z : Bool) : + ecomplexity z R A B ≤ Protocol.ecomplexity R A B := + le_iInf fun p => (p.2.hasCover z).ecomplexity_le + +/-- `ecomplexity_le_protocol` for functions on all inputs. -/ +theorem ecomplexityFun_le_protocol (z : Bool) : + ecomplexityFun z f Set.univ Set.univ ≤ Protocol.ecomplexityFun f := + ecomplexity_le_protocol z + +end Nondeterministic + +end Cslib.Communication diff --git a/ComplexityTests/NondeterministicCommunication.lean b/ComplexityTests/NondeterministicCommunication.lean new file mode 100644 index 0000000000..27b4af61eb --- /dev/null +++ b/ComplexityTests/NondeterministicCommunication.lean @@ -0,0 +1,152 @@ +/- +Copyright (c) 2026 András Z. Salamon. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: András Z. Salamon +-/ + +import Complexity.Computability.Communication.Functions +import Complexity.Computability.Communication.Nondeterministic.Basic + +/-! Tests for nondeterministic communication complexity by covers: exact values for equality on +three values (`N¹ = 2 = ⌈log₂ 3⌉`, by an explicit cover and the rectangle-size bound) and on `Bool` +(`N⁰ = 1`, by an explicit cover and a fooling set, and `N¹` of inequality by negation); smaller +domains that make equality trivial, and the fooling-set and rectangle-size bounds on a proper +subdomain; a relation with several acceptable answers, which is easier than the function it relaxes, +with its answers exchanged, and one with none, which has no cover; and bounds by deterministic +protocols, for a function and for a relation. -/ + +namespace ComplexityTests.NondeterministicCommunication + +open Finset Cslib Cslib.Communication Cslib.Communication.Nondeterministic + +/-! ### Equality on three values -/ + +/-- The rectangles of equality on `Fin 3` on which it is `true` have at most one pair. -/ +private theorem card_mul_le_one_of_equality (S T : Finset (Fin 3)) + (h : ∀ x ∈ S, ∀ y ∈ T, equality x y = true) : #S * #T ≤ 1 := by + revert h + decide +revert + +-- `N¹(EQ)` on `Fin 3` is `2`: three diagonal pairs need more than `2 ^ 1` rectangles, and the +-- diagonal singletons indexed by two bits are a cover. +example : ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) Set.univ Set.univ = 2 := by + refine le_antisymm (ecomplexityFun_le_iff.mpr ?_) (le_ecomplexityFun_iff.mpr fun k hk => ?_) + · let e := BitString.equivFin 2 + refine ⟨fun w => ({x | (x : ℕ) = e w}, {y | (y : ℕ) = e w}), isCover_fun_iff.mpr ⟨?_, ?_⟩⟩ + · intro w x _ hx y _ hy + simp only [Set.mem_ofPred_eq] at hx hy + simp [equality, Fin.ext_iff, hx, hy] + · intro x _ y _ h + simp only [equality, decide_eq_true_eq] at h + exact ⟨e.symm ⟨x, by omega⟩, by simp, by simp [h]⟩ + · have : #{q ∈ (univ : Finset (Fin 3)) ×ˢ univ | equality q.1 q.2 = true} ≤ 2 ^ k * 1 := + HasCover.card_le_two_pow_mul (fun S _ T _ h => card_mul_le_one_of_equality S T h) + (by simpa only [coe_univ] using hk) + have h3 : #{q ∈ (univ : Finset (Fin 3)) ×ˢ univ | equality q.1 q.2 = true} = 3 := by decide + rw [h3, mul_one] at this + have : 2 ≤ k := by + by_contra! hk + interval_cases k <;> simp at this + exact_mod_cast this + +/-- On the smaller domain `{0} × Fin 3` one rectangle suffices. -/ +private theorem ecomplexityFun_equality_zero_univ : + ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0} Set.univ = 0 := + nonpos_iff_eq_zero.mp <| ecomplexityFun_le_iff.mpr ⟨fun _ => ({0}, {0}), isCover_fun_iff.mpr + ⟨fun _ x hx _ y _ hy => by simp_all [equality], + fun x hx y _ h => ⟨0, hx, by simp_all [equality]⟩⟩⟩ + +-- So it does on any smaller domain. +example : ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0} {0, 1} = 0 := + nonpos_iff_eq_zero.mp <| (ecomplexityFun_mono le_rfl (Set.subset_univ _)).trans + ecomplexityFun_equality_zero_univ.le + +-- On `{0, 1} × {0, 1}` the fooling set `{(0, 0), (1, 1)}` lies inside the domain, so `N¹ ≥ 1`. +example : (1 : ℕ∞) ≤ ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0, 1} {0, 1} := + le_ecomplexityFun_of_isFoolingSet (isFoolingSet_equality {0, 1}) (by decide) (by decide) + +-- The rectangle-size bound on the finite domain `{0, 1} × {0, 1}`: two diagonal pairs and one pair +-- per rectangle need two rectangles. +example : (1 : ℕ∞) ≤ ecomplexityFun true (equality : Fin 3 → Fin 3 → Bool) {0, 1} {0, 1} := by + refine le_ecomplexityFun_iff.mpr fun k hk => ?_ + have : #{q ∈ ({0, 1} : Finset (Fin 3)) ×ˢ {0, 1} | equality q.1 q.2 = true} ≤ 2 ^ k * 1 := + HasCover.card_le_two_pow_mul (fun S _ T _ h => card_mul_le_one_of_equality S T h) + (by simpa only [coe_insert, coe_singleton] using hk) + have h2 : #{q ∈ ({0, 1} : Finset (Fin 3)) ×ˢ {0, 1} | equality q.1 q.2 = true} = 2 := by decide + rw [h2, mul_one] at this + have : 1 ≤ k := by + by_contra! hk + interval_cases k + simp at this + exact_mod_cast this + +/-! ### Equality on `Bool` -/ + +/-- `N⁰(EQ)` on `Bool` is `1`: `(false, true)` and `(true, false)` form a fooling set with value +`false`, and `{b} × {!b}` for the two bits `b` are a cover. -/ +private theorem ecomplexityFun_false_equality_bool : + ecomplexityFun false (equality : Bool → Bool → Bool) Set.univ Set.univ = 1 := by + refine le_antisymm (ecomplexityFun_le_iff.mpr ?_) ?_ + · refine ⟨fun w => ({w 0}, {!w 0}), isCover_fun_iff.mpr ⟨?_, ?_⟩⟩ + · intro w x _ hx y _ hy + simp only [Set.mem_singleton_iff] at hx hy + simp [equality, hx, hy] + · intro x _ y _ h + refine ⟨fun _ => x, rfl, ?_⟩ + cases x <;> cases y <;> simp_all [equality] + · refine le_ecomplexityFun_of_isFoolingSet (S := {(false, true), (true, false)}) ?_ (by simp) + (by decide) + simp [IsFoolingSet, equality] + +example : ecomplexityFun false (equality : Bool → Bool → Bool) Set.univ Set.univ = 1 := + ecomplexityFun_false_equality_bool + +-- Negation exchanges the answers: `N¹` of inequality is `N⁰` of equality. +example : ecomplexityFun true (fun x y : Bool => !equality x y) Set.univ Set.univ = 1 := by + rw [ecomplexityFun_not, Bool.not_true, ecomplexityFun_false_equality_bool] + +/-! ### Relations -/ + +/-- Equality under the promise `x = y`: off the diagonal every answer is acceptable. -/ +private def promiseEq (x y : Bool) (b : Bool) : Prop := x = y → b = true + +/-- No pair must be covered with `false`, since `true` is acceptable everywhere: one empty +rectangle is a `0`-cover, although `N⁰` of equality itself is `1`. -/ +private theorem ecomplexity_false_promiseEq : ecomplexity false promiseEq Set.univ Set.univ = 0 := + nonpos_iff_eq_zero.mp <| ecomplexity_le_iff.mpr + ⟨fun _ => (∅, ∅), fun _ _ _ hx => hx.elim, fun _ _ _ _ h => (h fun _ => rfl).elim⟩ + +-- Exchanging the answers of the relation exchanges `N⁰` and `N¹`. +example : ecomplexity true (fun x y b => promiseEq x y (!b)) Set.univ Set.univ = 0 := by + rw [ecomplexity_not, Bool.not_true, ecomplexity_false_promiseEq] + +-- The relation is weaker than equality, so it is no harder. +example : ecomplexity false promiseEq Set.univ Set.univ ≤ + ecomplexityFun false (equality : Bool → Bool → Bool) Set.univ Set.univ := + ecomplexity_le_of_imp fun _ _ b h hxy => by simp_all [equality] + +-- A relation with no acceptable answer has no cover, as it has no protocol. +example : ecomplexity true (fun (_ _ _ : Bool) => False) Set.univ Set.univ = ⊤ := + top_le_iff.mp <| le_ecomplexity_iff.mpr fun _ ⟨C, hmem, hcov⟩ => by + obtain ⟨w, hx, hy⟩ := hcov false trivial false trivial id + exact (hmem w _ trivial hx _ trivial hy).elim + +/-! ### Deterministic protocols -/ + +/-- Alice sends her bit, then Bob sends whether his bit is equal. -/ +private def eqProtocol : Protocol Bool Bool Bool := + .alice id (.bob id (.output true) (.output false)) (.bob id (.output false) (.output true)) + +-- The protocol computes equality with two bits, so `N¹(EQ) ≤ 2` on `Bool`. +example : ecomplexityFun true (equality : Bool → Bool → Bool) Set.univ Set.univ ≤ 2 := + (ecomplexityFun_le_protocol true).trans <| + (Protocol.ecomplexityFun_le_depth (p := eqProtocol) + (funext₂ fun x y => by cases x <;> cases y <;> rfl)).trans (by decide) + +-- The relation `promiseEq` is solved without communication, so its `N¹` is `0`. +example : ecomplexity true promiseEq Set.univ Set.univ = 0 := + nonpos_iff_eq_zero.mp <| (ecomplexity_le_protocol true).trans <| + (Protocol.ecomplexity_le_depth (p := .output true) (R := promiseEq) (A := Set.univ) + (B := Set.univ) fun _ _ _ _ _ => rfl).trans (by simp) + +end ComplexityTests.NondeterministicCommunication diff --git a/references.bib b/references.bib index cc6369c43d..d521aefddb 100644 --- a/references.bib +++ b/references.bib @@ -2043,6 +2043,18 @@ @article{GoosPitassiWatson2018 doi = {10.1137/16M1059369} } +@article{GoosPitassiWatson2018Landscape, + author = {G{\"o}{\"o}s, Mika and Pitassi, Toniann and Watson, Thomas}, + title = {The Landscape of Communication Complexity Classes}, + journal = {Computational Complexity}, + volume = {27}, + number = {2}, + pages = {245--304}, + year = {2018}, + doi = {10.1007/s00037-018-0166-6}, + note = {Preprint: ECCC TR15-049, revision 1} +} + @article{GotsmanLinial1992, author = {Gotsman, Craig and Linial, Nathan}, title = {The Equivalence of Two Problems on the Cube},