Restricting decision trees

Fixing some variables can only make a function easier to compute by decision trees: answering the queries fixed by a restriction (partial assignment) ρ in a tree for f gives a tree for the restricted function f ∘ ρ.fill that is no deeper (DecisionTree.restrict, DecisionTree.complexity_comp_fill_le). Post-processing the output does not make it harder either (DecisionTree.complexity_comp_le), and post-processing by an injective map, such as negation, does not change it (DecisionTree.complexity_comp_of_injective).

Main definitions

• Cslib.DecisionTree.restrict: a tree with some queries answered.

Main results

• Cslib.DecisionTree.complexity_comp_fill_le: restricting does not raise decision tree complexity.
• Cslib.DecisionTree.complexity_comp_of_injective: post-processing by an injective map preserves decision tree complexity.

def Cslib.DecisionTree.restrict {ι : Type u_1} {β : Type u_2} (ρ : BitString.PartialAssignment ι) : DecisionTree ι β → DecisionTree ι β

t with the queries fixed by ρ answered: a variable i with ρ i = some b reads b.

theorem Cslib.DecisionTree.eval_restrict {ι : Type u_1} {β : Type u_2} (ρ : BitString.PartialAssignment ι) (t : DecisionTree ι β) (x : ι → Bool) : (restrict ρ t).eval x = t.eval (ρ.fill x)

The restricted tree computes the restricted function.

theorem Cslib.DecisionTree.depth_restrict_le {ι : Type u_1} {β : Type u_2} (ρ : BitString.PartialAssignment ι) (t : DecisionTree ι β) : (restrict ρ t).depth ≤ t.depth

theorem Cslib.DecisionTree.complexity_comp_fill_le {ι : Type u_1} {β : Type u_2} [Finite ι] (ρ : BitString.PartialAssignment ι) (f : (ι → Bool) → β) : complexity (f ∘ ρ.fill) ≤ complexity f

Restricting does not raise decision tree complexity.

theorem Cslib.DecisionTree.complexity_comp_le {ι : Type u_1} {β : Type u_2} {γ : Type u_3} [Finite ι] (g : β → γ) (f : (ι → Bool) → β) : complexity (g ∘ f) ≤ complexity f

Post-processing the output does not raise decision tree complexity.

theorem Cslib.DecisionTree.complexity_comp_of_injective {ι : Type u_1} {β : Type u_2} {γ : Type u_3} [Finite ι] {g : β → γ} (hg : Function.Injective g) (f : (ι → Bool) → β) : complexity (g ∘ f) = complexity f

Post-processing by an injective map preserves decision tree complexity: a left inverse undoes it.

theorem Cslib.DecisionTree.complexity_not {ι : Type u_1} [Finite ι] (f : (ι → Bool) → Bool) : (complexity fun (x : ι → Bool) => !f x) = complexity f

Negation preserves decision tree complexity.