Restricting decision trees

A fixed query can be eliminated by selecting the corresponding branch. A free query remains and recursively restricts both children. This is the structural simplification used when switching-lemma arguments measure decision-tree depth.

Main results

• DecisionTree.eval_restrict -- restriction preserves semantics.
• DecisionTree.depth_restrict_le -- restriction cannot increase query depth.
• DecisionTree.vars_restrict_subset_filter -- surviving queries are free variables from the original tree.
• DecisionTree.restrict_comp -- sequential restriction agrees with left-biased restriction composition.

def Complexity.DecisionTree.restrict (ρ : Restriction) : DecisionTree → DecisionTree

Simplify a decision tree under a restriction.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DecisionTree.restrict ρ (Complexity.DecisionTree.leaf b) = Complexity.DecisionTree.leaf b

@[simp]

theorem Complexity.DecisionTree.restrict_empty (tree : DecisionTree) : restrict Restriction.empty tree = tree

The empty restriction is the identity on decision trees.

theorem Complexity.DecisionTree.eval_restrict (ρ : Restriction) (α : ℕ → Bool) (tree : DecisionTree) : eval α (restrict ρ tree) = eval (ρ.applyTo α) tree

Evaluating a restricted tree agrees with applying the restriction to its assignment before evaluating the original tree.

theorem Complexity.DecisionTree.depth_restrict_le (ρ : Restriction) (tree : DecisionTree) : (restrict ρ tree).depth ≤ tree.depth

Restricting a decision tree cannot increase its query depth.

theorem Complexity.DecisionTree.vars_restrict_subset_filter (ρ : Restriction) (tree : DecisionTree) : (restrict ρ tree).vars ⊆ {i ∈ tree.vars | ρ i = none}

Every variable queried after restriction was queried originally and remains free. Selecting a fixed branch may remove additional variables.

theorem Complexity.DecisionTree.restrict_comp (ρ₁ ρ₂ : Restriction) (tree : DecisionTree) : restrict ρ₂ (restrict ρ₁ tree) = restrict (ρ₁.comp ρ₂) tree

Sequentially restricting a tree agrees with applying the left-biased composition of the two restrictions once.