Decision trees from certificates

A certificate for one value of a function and a certificate for another value disagree at some variable (IsCertificate.exists_mem_inter_ne). So querying the variables of a smallest certificate for the value 1 either confirms the value 1, or makes every certificate for the value 0 of the function restricted by the answers shorter. Repeating this computes a Boolean function with at most C₀(f) C₁(f) queries, where C_b(f) is the largest certificate complexity at an input of value b (complexity_le_certificateComplexityFor_mul) [BI87], [Tar89], Jukna, Section 14.2. In particular, decision tree complexity is at most the square of certificate complexity.

Main results

• Cslib.DecisionTree.complexity_le_card_add: querying a set of variables and continuing with trees for the restricted functions.
• Cslib.DecisionTree.complexity_le_certificateComplexityFor_mul: D(f) ≤ C₀(f) C₁(f).
• Cslib.DecisionTree.complexity_le_certificateComplexity_sq: D(f) ≤ C(f) ^ 2.

References

• M. Blum and R. Impagliazzo, Generic oracles and oracle classes
• G. Tardos, Query complexity, or why is it difficult to separate NP^A ∩ coNP^A from P^A by random oracles A?
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.QueryComplexity.IsCertificate.exists_mem_inter_ne {n : ℕ} {f : BooleanFunction n} {x w : BitString n} {S T : Finset (Fin n)} (hS : IsCertificate f x S) (hT : IsCertificate f w T) (hne : f x ≠ f w) : ∃ i ∈ T ∩ S, w i ≠ x i

A certificate for one value and a certificate for another value disagree at a variable that both contain.

theorem Cslib.QueryComplexity.IsCertificate.restrict {n : ℕ} {f : BooleanFunction n} {S T : Finset (Fin n)} {a z : BitString n} (hT : IsCertificate f (S.piecewise a z) T) : IsCertificate (fun (y : BitString n) => f (S.piecewise a y)) z (T \ S)

Fixing the variables of S to the values a turns a certificate T at the filled input into the certificate T \ S of the restricted function.

theorem Cslib.DecisionTree.complexity_le_card_add {ι : Type u_1} {β : Type u_2} [DecidableEq ι] [Finite ι] {f : (ι → Bool) → β} (S : Finset ι) {d : ℕ} (h : ∀ (a : ι → Bool), (complexity fun (y : ι → Bool) => f (S.piecewise a y)) ≤ d) : complexity f ≤ S.card + d

Querying the variables of S and continuing with a tree for the function restricted by the answers computes f with #S more queries.

theorem Cslib.DecisionTree.complexity_le_certificateComplexityFor_mul {n : ℕ} (f : BooleanFunction n) : complexity f ≤ QueryComplexity.certificateComplexityFor f false * QueryComplexity.certificateComplexityFor f true

Certificates give decision trees. A Boolean function is computed by a decision tree of depth at most C₀(f) C₁(f).

theorem Cslib.DecisionTree.complexity_le_certificateComplexity_sq {n : ℕ} (f : BooleanFunction n) : complexity f ≤ QueryComplexity.certificateComplexity f ^ 2

Decision tree complexity is at most the square of certificate complexity.