Boolean decision trees

Decision trees over Boolean variables, with evaluation, depth, and leaf-count measures (roadmap track L4). A decision tree queries one variable per internal node and branches on its value; leaves carry the output bit. Decision trees are the combinatorial substrate for restrictions and switching-lemma arguments, and are distinct from the DAG-shaped Circuit.

Main definitions and results

• DecisionTree — the tree syntax
• DecisionTree.eval — evaluation under an assignment
• DecisionTree.depth, DecisionTree.numLeaves — the query-depth and leaf-count measures
• DecisionTree.numLeaves_le_two_pow_depth — a depth-d tree has at most 2 ^ d leaves
• DecisionTree.vars, DecisionTree.eval_eq_of_agree — the queried-variable set and the locality property: a tree's output depends only on the variables it queries (a decision tree is a junta on vars)
• DecisionTree.toFormula, DecisionTree.toFormula_eval — compilation to an equivalent Boolean formula (the decision-tree ⟹ formula direction)

inductive Complexity.DecisionTree : Type

A Boolean decision tree: a leaf carries an output bit; a node i t₀ t₁ queries variable i and continues into t₀ if it is false, t₁ if true.

• leaf (b : Bool) : DecisionTree

  A leaf carrying output bit b.

• node (i : ℕ) (t₀ t₁ : DecisionTree) : DecisionTree

  Query variable i; branch to t₀ on false, t₁ on true.

@[implicit_reducible]

instance Complexity.instReprDecisionTree : Repr DecisionTree

Equations

• Complexity.instReprDecisionTree = { reprPrec := Complexity.instReprDecisionTree.repr }

def Complexity.instReprDecisionTree.repr : DecisionTree → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.instDecidableEqDecisionTree : DecidableEq DecisionTree

Equations

• Complexity.instDecidableEqDecisionTree = Complexity.instDecidableEqDecisionTree.decEq

def Complexity.instDecidableEqDecisionTree.decEq (x✝ x✝¹ : DecisionTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.instDecidableEqDecisionTree.decEq (Complexity.DecisionTree.leaf a) (Complexity.DecisionTree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.instDecidableEqDecisionTree.decEq (Complexity.DecisionTree.leaf b) (Complexity.DecisionTree.node i t₀ t₁) = isFalse ⋯
• Complexity.instDecidableEqDecisionTree.decEq (Complexity.DecisionTree.node i t₀ t₁) (Complexity.DecisionTree.leaf b) = isFalse ⋯

def Complexity.DecisionTree.eval (α : ℕ → Bool) : DecisionTree → Bool

Evaluate a decision tree under an assignment α : ℕ → Bool.

Equations

• Complexity.DecisionTree.eval α (Complexity.DecisionTree.leaf b) = b
• Complexity.DecisionTree.eval α (Complexity.DecisionTree.node i t₀ t₁) = if α i = true then Complexity.DecisionTree.eval α t₁ else Complexity.DecisionTree.eval α t₀

def Complexity.DecisionTree.depth : DecisionTree → ℕ

The query depth of a decision tree (the longest root-to-leaf path).

Equations

• (Complexity.DecisionTree.leaf b).depth = 0
• (Complexity.DecisionTree.node i t₀ t₁).depth = max t₀.depth t₁.depth + 1

def Complexity.DecisionTree.numLeaves : DecisionTree → ℕ

The number of leaves of a decision tree.

Equations

• (Complexity.DecisionTree.leaf b).numLeaves = 1
• (Complexity.DecisionTree.node i t₀ t₁).numLeaves = t₀.numLeaves + t₁.numLeaves

def Complexity.DecisionTree.vars : DecisionTree → Finset ℕ

The set of variables a decision tree queries.

Equations

• (Complexity.DecisionTree.leaf b).vars = ∅
• (Complexity.DecisionTree.node i t₀ t₁).vars = insert i (t₀.vars ∪ t₁.vars)

@[simp]

theorem Complexity.DecisionTree.eval_leaf (α : ℕ → Bool) (b : Bool) : eval α (leaf b) = b

@[simp]

theorem Complexity.DecisionTree.eval_node (α : ℕ → Bool) (i : ℕ) (t₀ t₁ : DecisionTree) : eval α (node i t₀ t₁) = if α i = true then eval α t₁ else eval α t₀

@[simp]

theorem Complexity.DecisionTree.depth_leaf (b : Bool) : (leaf b).depth = 0

@[simp]

theorem Complexity.DecisionTree.numLeaves_leaf (b : Bool) : (leaf b).numLeaves = 1

theorem Complexity.DecisionTree.one_le_numLeaves (t : DecisionTree) : 1 ≤ t.numLeaves

Every decision tree has at least one leaf.

theorem Complexity.DecisionTree.eval_eq_of_agree (t : DecisionTree) {α β : ℕ → Bool} : (∀ i ∈ t.vars, α i = β i) → eval α t = eval β t

Locality (junta property). A decision tree's output depends only on the variables it queries: if two assignments agree on vars t, they yield the same value.

theorem Complexity.DecisionTree.card_vars_lt_two_pow_depth (t : DecisionTree) : t.vars.card < 2 ^ t.depth

A depth-d decision tree queries fewer than 2 ^ d distinct variables (|vars t| < 2 ^ depth t), the branching-count bound behind decision-tree complexity.

theorem Complexity.DecisionTree.numLeaves_le_two_pow_depth (t : DecisionTree) : t.numLeaves ≤ 2 ^ t.depth

A decision tree of depth d has at most 2 ^ d leaves.

def Complexity.DecisionTree.toFormula : DecisionTree → BoolFormula

Compile a decision tree into an equivalent Boolean formula: a leaf becomes a constant, and a query node node i t₀ t₁ becomes (x_i ∧ ⟦t₁⟧) ∨ (¬x_i ∧ ⟦t₀⟧).

Equations

• (Complexity.DecisionTree.leaf b).toFormula = if b = true then Complexity.BoolFormula.tru else Complexity.BoolFormula.fls
• (Complexity.DecisionTree.node i t₀ t₁).toFormula = ((Complexity.BoolFormula.var i).conj t₁.toFormula).disj ((Complexity.BoolFormula.var i).neg.conj t₀.toFormula)

theorem Complexity.DecisionTree.toFormula_eval (α : ℕ → Bool) (t : DecisionTree) : BoolFormula.eval α t.toFormula = eval α t

The compiled formula computes the same function as the tree.

theorem Complexity.DecisionTree.toFormula_depth_le (t : DecisionTree) : t.toFormula.depth ≤ 2 * t.depth + 1

The compiled formula has depth at most 2 · depth t + 1: each query node expands to a two-level ∨-of-∧ gadget, and the negated literal adds one further level.