Decision trees for symmetric functions

A function of n bits is evasive when every decision tree computing it queries all n bits in the worst case, that is, when its decision tree complexity Jukna, Chapter 14 is n. Every nonconstant symmetric function is evasive (DecisionTree.complexity_eq_card_of_isSymmetric), although its sensitivity can be as small as about n / 2, as for majority.

The proof is an adversary argument on subcubes (DecisionTree.card_le_depth_of_eval_eq_comp_card_filter). Suppose that on the inputs agreeing with a off a set S of free coordinates, a tree's output depends only on the number k of true free bits, through a profile g, and that g changes between two consecutive counts m and m + 1 with m + 1 ≤ #S. When the tree queries a free bit, the adversary answers false if the change still fits among the remaining free bits, and true otherwise, shifting the profile by one. Either way the hypotheses persist with one free bit fewer, so a leaf cannot be reached before all free bits are queried.

Main results

• Cslib.DecisionTree.card_le_depth_of_eval_eq_comp_card_filter: the adversary argument.
• Cslib.DecisionTree.complexity_eq_card_of_isSymmetric: nonconstant symmetric functions are evasive.
• Cslib.DecisionTree.complexity_threshold, Cslib.DecisionTree.complexity_majority: threshold functions Th^n_j with 1 ≤ j ≤ n, and majority, are evasive.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.DecisionTree.card_le_depth_of_eval_eq_comp_card_filter {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) (S : Finset ι) (a : ι → Bool) (g : ℕ → β) (m : ℕ) (ht : ∀ (x : ι → Bool), (∀ j ∉ S, x j = a j) → t.eval x = g {j ∈ S | x j = true}.card) (hm : m + 1 ≤ S.card) (hg : g m ≠ g (m + 1)) : S.card ≤ t.depth

Adversary argument for symmetric functions. If, on the inputs agreeing with a off a set S of free coordinates, a tree's output depends only on the number of true free bits, through a profile g that changes between two consecutive counts m, m + 1 ≤ #S, then the tree has depth at least #S. The output type is arbitrary.

theorem Cslib.DecisionTree.complexity_eq_card_of_isSymmetric {n : ℕ} {f : BooleanFunction n} (hf : f.IsSymmetric) (hnc : ¬Function.IsConst f) : complexity f = n

Nonconstant symmetric functions are evasive: every decision tree computing a nonconstant symmetric function of n bits queries all of them in the worst case.

theorem Cslib.DecisionTree.complexity_threshold {n j : ℕ} (hj : 1 ≤ j) (hjn : j ≤ n) : complexity (threshold n j) = n

Threshold functions are evasive: D(Th^n_j) = n for 1 ≤ j ≤ n.

theorem Cslib.DecisionTree.complexity_majority {n : ℕ} (hn : 1 ≤ n) : complexity (majority n) = n

Majority is evasive: D(MAJ_n) = n for n ≥ 1.