Randomized decision trees

A randomized decision tree tosses coins, uses them to pick a deterministic decision tree, and runs it. We represent it by the distribution over decision trees that it draws from, a finitely supported probability distribution Convexity.StdSimplex ℝ (DecisionTree ι β) (RandomizedDecisionTree). Its depth is the largest depth of a tree it can draw: the number of queries it makes in the worst case over the inputs and the coins (RandomizedDecisionTree.depth). It computes f with error ε when on every input the tree it draws outputs a wrong value with probability at most ε (RandomizedDecisionTree.errorProb, RandomizedDecisionTree.Computes). The randomized decision tree complexity R_ε(f) is the least depth of a randomized decision tree computing f with error ε (QueryComplexity.randomizedComplexity) [BdW02]; the bounded-error complexity R(f) of the literature is R_{1/3}(f).

Deterministic trees are randomized trees that draw one tree, so R_ε(f) ≤ D(f) for ε ≥ 0 (DecisionTree.randomizedComplexity_le_complexity). With error 0 every tree that can be drawn computes f, so R_0(f) = D(f) (QueryComplexity.randomizedComplexity_zero); zero-error complexity in the literature usually counts the expected number of queries instead, which can be smaller. A fair coin guesses a Boolean value correctly with probability 1/2, so R_ε(f) = 0 for Boolean-valued f and ε ≥ 1/2 (QueryComplexity.randomizedComplexity_eq_zero_of_le).

If a randomized tree computes f with error ε, then for every distribution ν on the inputs some tree that it can draw errs with probability at most ε on inputs drawn from ν (RandomizedDecisionTree.Computes.exists_distributionalError_le, from Convexity.StdSimplex.exists_mem_support_le_sum_mul in Complexity.Probability.Minimax). This averaging argument is the easy direction of Yao's principle [Yao77]; the converse follows from the minimax theorem (QueryComplexity.exists_computes_of_forall_exists_distributionalError_le).

Main definitions

• Cslib.RandomizedDecisionTree: randomized decision trees, as finitely supported distributions over decision trees, with RandomizedDecisionTree.depth, RandomizedDecisionTree.errorProb and RandomizedDecisionTree.Computes.
• Cslib.DecisionTree.distributionalError: the error of a decision tree on inputs drawn from a distribution.
• Cslib.QueryComplexity.randomizedComplexity: the randomized decision tree complexity R_ε(f).

Main results

• Cslib.RandomizedDecisionTree.Computes.exists_distributionalError_le: the averaging argument.
• Cslib.DecisionTree.randomizedComplexity_le_complexity: R_ε(f) ≤ D(f) for ε ≥ 0.
• Cslib.QueryComplexity.randomizedComplexity_zero: R_0(f) = D(f).
• Cslib.QueryComplexity.randomizedComplexity_antitone: R_ε(f) decreases as ε grows.
• Cslib.QueryComplexity.randomizedComplexity_eq_zero_of_le: R_ε(f) = 0 for Boolean-valued f and ε ≥ 1/2.

References

• H. Buhrman, R. de Wolf, Complexity measures and decision tree complexity: a survey
• A. C.-C. Yao, Probabilistic computations: toward a unified measure of complexity

@[reducible, inline]

abbrev Cslib.RandomizedDecisionTree (ι : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

A randomized decision tree over Boolean variables indexed by ι, with outputs in β: a finitely supported probability distribution over decision trees. It draws a tree from this distribution and runs it.

noncomputable def Cslib.DecisionTree.distributionalError {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) (ν : Convexity.StdSimplex ℝ (ι → Bool)) (f : (ι → Bool) → β) : ℝ

The error of a decision tree t on inputs drawn from ν: the probability that on an input x drawn from ν it outputs a value other than f x.

theorem Cslib.DecisionTree.distributionalError_eq_sum {ι : Type u_1} {β : Type u_2} [DecidableEq β] (t : DecisionTree ι β) (ν : Convexity.StdSimplex ℝ (ι → Bool)) (f : (ι → Bool) → β) : t.distributionalError ν f = ν.weights.sum fun (x : ι → Bool) (w : ℝ) => w * if t.eval x = f x then 0 else 1

distributionalError with any decidable equality on the outputs.

theorem Cslib.DecisionTree.distributionalError_nonneg {ι : Type u_1} {β : Type u_2} {t : DecisionTree ι β} {ν : Convexity.StdSimplex ℝ (ι → Bool)} {f : (ι → Bool) → β} : 0 ≤ t.distributionalError ν f

theorem Cslib.DecisionTree.Computes.distributionalError_eq_zero {ι : Type u_1} {β : Type u_2} {t : DecisionTree ι β} {ν : Convexity.StdSimplex ℝ (ι → Bool)} {f : (ι → Bool) → β} (ht : t.Computes f) : t.distributionalError ν f = 0

A decision tree computing f has error 0 on every distribution.

def Cslib.RandomizedDecisionTree.depth {ι : Type u_1} {β : Type u_2} (μ : RandomizedDecisionTree ι β) : ℕ

The depth of a randomized decision tree: the largest depth of a tree that it can draw, so the number of queries it makes in the worst case over the inputs and the coins.

noncomputable def Cslib.RandomizedDecisionTree.errorProb {ι : Type u_1} {β : Type u_2} (μ : RandomizedDecisionTree ι β) (f : (ι → Bool) → β) (x : ι → Bool) : ℝ

The probability that the tree drawn from μ outputs on x a value other than f x.

def Cslib.RandomizedDecisionTree.Computes {ι : Type u_1} {β : Type u_2} (μ : RandomizedDecisionTree ι β) (ε : ℝ) (f : (ι → Bool) → β) : Prop

A randomized decision tree μ computes f with error ε when on every input the tree drawn from μ outputs a wrong value with probability at most ε.

theorem Cslib.RandomizedDecisionTree.errorProb_eq_sum {ι : Type u_1} {β : Type u_2} [DecidableEq β] (μ : RandomizedDecisionTree ι β) (f : (ι → Bool) → β) (x : ι → Bool) : μ.errorProb f x = μ.weights.sum fun (t : DecisionTree ι β) (w : ℝ) => w * if t.eval x = f x then 0 else 1

errorProb with any decidable equality on the outputs.

theorem Cslib.RandomizedDecisionTree.depth_le_iff {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {d : ℕ} : μ.depth ≤ d ↔ ∀ t ∈ μ.weights.support, t.depth ≤ d

theorem Cslib.RandomizedDecisionTree.depth_le_depth {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {t : DecisionTree ι β} (ht : t ∈ μ.weights.support) : t.depth ≤ μ.depth

@[simp]

theorem Cslib.RandomizedDecisionTree.depth_single {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : depth (Convexity.StdSimplex.single t) = t.depth

theorem Cslib.RandomizedDecisionTree.errorProb_nonneg {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {f : (ι → Bool) → β} {x : ι → Bool} : 0 ≤ μ.errorProb f x

theorem Cslib.RandomizedDecisionTree.errorProb_le_one {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {f : (ι → Bool) → β} {x : ι → Bool} : μ.errorProb f x ≤ 1

theorem Cslib.RandomizedDecisionTree.errorProb_eq_zero_iff {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {f : (ι → Bool) → β} {x : ι → Bool} : μ.errorProb f x = 0 ↔ ∀ t ∈ μ.weights.support, t.eval x = f x

theorem Cslib.RandomizedDecisionTree.errorProb_single_of_eq {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {t : DecisionTree ι β} {x : ι → Bool} (h : t.eval x = f x) : errorProb (Convexity.StdSimplex.single t) f x = 0

theorem Cslib.RandomizedDecisionTree.errorProb_single_of_ne {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {t : DecisionTree ι β} {x : ι → Bool} (h : t.eval x ≠ f x) : errorProb (Convexity.StdSimplex.single t) f x = 1

theorem Cslib.RandomizedDecisionTree.Computes.mono {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {f : (ι → Bool) → β} {ε ε' : ℝ} (h : μ.Computes ε f) (hε : ε ≤ ε') : μ.Computes ε' f

theorem Cslib.RandomizedDecisionTree.Computes.nonneg {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {f : (ι → Bool) → β} {ε : ℝ} (h : μ.Computes ε f) : 0 ≤ ε

A randomized decision tree can only compute with nonnegative error.

theorem Cslib.RandomizedDecisionTree.computes_single {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {t : DecisionTree ι β} {ε : ℝ} (ht : t.Computes f) (hε : 0 ≤ ε) : Computes (Convexity.StdSimplex.single t) ε f

A deterministic decision tree computing f computes it with any nonnegative error.

theorem Cslib.RandomizedDecisionTree.computes_zero_iff {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {f : (ι → Bool) → β} : μ.Computes 0 f ↔ ∀ t ∈ μ.weights.support, t.Computes f

A randomized decision tree computes f with error 0 exactly when every tree it can draw computes f.

theorem Cslib.RandomizedDecisionTree.Computes.exists_distributionalError_le {ι : Type u_1} {β : Type u_2} {μ : RandomizedDecisionTree ι β} {f : (ι → Bool) → β} {ε : ℝ} (h : μ.Computes ε f) (ν : Convexity.StdSimplex ℝ (ι → Bool)) : ∃ t ∈ μ.weights.support, t.distributionalError ν f ≤ ε

The averaging argument, the easy direction of Yao's principle: if μ computes f with error ε, then for every distribution ν on the inputs some tree that μ can draw errs with probability at most ε on inputs drawn from ν.

noncomputable def Cslib.QueryComplexity.randomizedComplexity {ι : Type u_1} {β : Type u_2} (ε : ℝ) (f : (ι → Bool) → β) : ℕ

The randomized decision tree complexity R_ε(f): the least depth of a randomized decision tree computing f with error ε. It is 0 when no randomized decision tree computes f with error ε, which over finitely many variables happens exactly for ε < 0.

theorem Cslib.QueryComplexity.randomizedComplexity_le_depth {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {μ : RandomizedDecisionTree ι β} {ε : ℝ} (h : μ.Computes ε f) : randomizedComplexity ε f ≤ μ.depth

theorem Cslib.QueryComplexity.randomizedComplexity_of_neg {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ε : ℝ} (hε : ε < 0) : randomizedComplexity ε f = 0

R_ε(f) = 0 for ε < 0, where no randomized decision tree qualifies.

theorem Cslib.QueryComplexity.exists_computes_depth_eq_randomizedComplexity {ι : Type u_1} {β : Type u_2} {ε : ℝ} [Finite ι] (hε : 0 ≤ ε) (f : (ι → Bool) → β) : ∃ (μ : RandomizedDecisionTree ι β), μ.Computes ε f ∧ μ.depth = randomizedComplexity ε f

For ε ≥ 0 the randomized complexity is attained: some randomized decision tree of depth R_ε(f) computes f with error ε.

theorem Cslib.QueryComplexity.randomizedComplexity_le_iff {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ε : ℝ} {d : ℕ} [Finite ι] (hε : 0 ≤ ε) : randomizedComplexity ε f ≤ d ↔ ∃ (μ : RandomizedDecisionTree ι β), μ.Computes ε f ∧ μ.depth ≤ d

theorem Cslib.QueryComplexity.le_randomizedComplexity_iff {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ε : ℝ} {d : ℕ} [Finite ι] (hε : 0 ≤ ε) : d ≤ randomizedComplexity ε f ↔ ∀ (μ : RandomizedDecisionTree ι β), μ.Computes ε f → d ≤ μ.depth

Lower bounds on R_ε(f) are lower bounds on the depth of every randomized decision tree computing f with error ε.

theorem Cslib.QueryComplexity.randomizedComplexity_antitone {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ε ε' : ℝ} [Finite ι] (hε : 0 ≤ ε) (hεε' : ε ≤ ε') : randomizedComplexity ε' f ≤ randomizedComplexity ε f

R_ε(f) decreases as ε grows.

theorem Cslib.QueryComplexity.randomizedComplexity_zero {ι : Type u_1} {β : Type u_2} [Finite ι] (f : (ι → Bool) → β) : randomizedComplexity 0 f = DecisionTree.complexity f

With error 0 randomness does not help: R_0(f) = D(f). The cost here is the worst case over the coins, unlike the expected number of queries of zero-error (Las Vegas) complexity.

theorem Cslib.QueryComplexity.randomizedComplexity_eq_zero_of_le {ι : Type u_1} {ε : ℝ} (hε : 1 / 2 ≤ ε) (f : (ι → Bool) → Bool) : randomizedComplexity ε f = 0

From ε = 1/2 on, a fair coin computes every Boolean-valued function: R_ε(f) = 0.

theorem Cslib.DecisionTree.randomizedComplexity_le_complexity {ι : Type u_1} {β : Type u_2} [Finite ι] {ε : ℝ} (hε : 0 ≤ ε) (f : (ι → Bool) → β) : QueryComplexity.randomizedComplexity ε f ≤ complexity f

Randomness does not hurt: R_ε(f) ≤ D(f) for ε ≥ 0.

theorem Cslib.DecisionTree.randomizedComplexity_le_card {ι : Type u_1} {β : Type u_2} [Fintype ι] {ε : ℝ} (hε : 0 ≤ ε) (f : (ι → Bool) → β) : QueryComplexity.randomizedComplexity ε f ≤ Fintype.card ι

R_ε(f) is at most the number of variables for ε ≥ 0.