Decision trees for parity

Flipping any bit flips the parity, so parity is sensitive to every bit at every input (BitString.sensitivityAt_parity), and every decision tree for it queries all of its bits in the worst case (DecisionTree.complexity_parity) Jukna, Chapter 14. More generally, restricted parity queries every free bit (DecisionTree.card_free_le_complexity_parity_fill).

Main results

• Cslib.DecisionTree.complexity_parity: the decision tree complexity of the parity of n bits is n.
• Cslib.DecisionTree.card_free_le_complexity_parity_fill: restricted parity still needs to query every free bit.

References

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

theorem Cslib.DecisionTree.complexity_parity {n : ℕ} : complexity (parity n) = n

Every decision tree for the parity of n bits queries all of them in the worst case.

theorem Cslib.DecisionTree.card_free_le_complexity_parity_fill {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) : ρ.free.card ≤ complexity fun (x : Fin n → Bool) => parity n (ρ.fill x)

Restricted parity is the parity of the free bits, up to a constant, so every decision tree for it queries all free bits in the worst case.