Decision trees

A decision tree over Boolean variables indexed by ι queries a variable at each internal node and follows the branch for its value; the leaf it reaches is the output (DecisionTree.eval). Its depth is the longest structural root-to-leaf path, an upper bound on the number of queries on any input. Repeated variables can make a longest path unreachable. The variables queried on the way to the leaf of an input x determine the output: every input that agrees with x on them reaches the same leaf (DecisionTree.eval_eq_of_forall_mem_queries).

Querying every variable in turn computes any function, so over finitely many variables every function has a decision tree of depth at most the number of variables (exists_computes). The decision tree complexity DecisionTree.complexity f of f is the least depth of a tree computing it Jukna, Chapter 14.

Main definitions

• Cslib.DecisionTree: decision trees.
• Cslib.DecisionTree.eval, Cslib.DecisionTree.depth, Cslib.DecisionTree.queries.
• Cslib.DecisionTree.mapQueries: relabel queries without changing the tree shape.
• Cslib.DecisionTree.complexity: the decision tree complexity of a function.

Main results

• Cslib.DecisionTree.eval_eq_of_forall_mem_queries: the queried variables certify the output.
• Cslib.DecisionTree.complexity_le_card: decision tree complexity is at most the number of variables.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

inductive Cslib.DecisionTree (ι : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

A decision tree over Boolean variables indexed by ι, with outputs in β: a leaf, or a query of a variable with a subtree for each of its values.

• leaf {ι : Type u_1} {β : Type u_2} (b : β) : DecisionTree ι β

  Output b.

• node {ι : Type u_1} {β : Type u_2} (i : ι) (ifFalse ifTrue : DecisionTree ι β) : DecisionTree ι β

  Query variable i, then continue with ifFalse or ifTrue.

def Cslib.DecisionTree.eval {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → (ι → Bool) → β

The output of a decision tree on an input.

def Cslib.DecisionTree.depth {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → ℕ

The longest structural root-to-leaf path, bounding the queries executed on any input. Repeated variables can make a longest path unreachable.

def Cslib.DecisionTree.Computes {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) (f : (ι → Bool) → β) : Prop

A decision tree computes f when it agrees with f on every input.

theorem Cslib.DecisionTree.computes_iff {ι : Type u_1} {β : Type u_2} {t : DecisionTree ι β} {f : (ι → Bool) → β} : t.Computes f ↔ t.eval = f

@[simp]

theorem Cslib.DecisionTree.eval_leaf {ι : Type u_1} {β : Type u_2} (b : β) (x : ι → Bool) : (leaf b).eval x = b

@[simp]

theorem Cslib.DecisionTree.eval_node {ι : Type u_1} {β : Type u_2} (i : ι) (t₀ t₁ : DecisionTree ι β) (x : ι → Bool) : (node i t₀ t₁).eval x = bif x i then t₁.eval x else t₀.eval x

@[simp]

theorem Cslib.DecisionTree.depth_leaf {ι : Type u_1} {β : Type u_2} (b : β) : (leaf b).depth = 0

@[simp]

theorem Cslib.DecisionTree.depth_node {ι : Type u_1} {β : Type u_2} (i : ι) (t₀ t₁ : DecisionTree ι β) : (node i t₀ t₁).depth = max t₀.depth t₁.depth + 1

def Cslib.DecisionTree.mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) : DecisionTree ι β → DecisionTree κ β

Relabel the queries while preserving every branch and leaf, even when f is not injective.

@[simp]

theorem Cslib.DecisionTree.eval_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) (x : κ → Bool) : (mapQueries f t).eval x = t.eval (x ∘ f)

@[simp]

theorem Cslib.DecisionTree.depth_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) : (mapQueries f t).depth = t.depth

def Cslib.DecisionTree.queries {ι : Type u_1} {β : Type u_2} [DecidableEq ι] : DecisionTree ι β → (ι → Bool) → Finset ι

The variables queried on the way to the leaf of x.

@[simp]

theorem Cslib.DecisionTree.queries_leaf {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (b : β) (x : ι → Bool) : (leaf b).queries x = ∅

@[simp]

theorem Cslib.DecisionTree.queries_node {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (i : ι) (t₀ t₁ : DecisionTree ι β) (x : ι → Bool) : (node i t₀ t₁).queries x = insert i (bif x i then t₁.queries x else t₀.queries x)

theorem Cslib.DecisionTree.card_queries_le_depth {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (t : DecisionTree ι β) (x : ι → Bool) : (t.queries x).card ≤ t.depth

At most depth variables are queried on any input.

theorem Cslib.DecisionTree.eval_eq_of_forall_mem_queries {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (t : DecisionTree ι β) {x y : ι → Bool} (h : ∀ i ∈ t.queries x, y i = x i) : t.eval y = t.eval x

Inputs that agree on the variables queried for x reach the same leaf.

def Cslib.DecisionTree.graft {ι : Type u_1} {β : Type u_2} [DecidableEq ι] : List ι → ((ι → Bool) → DecisionTree ι β) → (ι → Bool) → DecisionTree ι β

Query the variables of l in turn, starting from the assignment a, and continue with the tree k a' for the assignment a' reached.

@[simp]

theorem Cslib.DecisionTree.graft_nil {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (k : (ι → Bool) → DecisionTree ι β) (a : ι → Bool) : graft [] k a = k a

@[simp]

theorem Cslib.DecisionTree.graft_cons {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (i : ι) (l : List ι) (k : (ι → Bool) → DecisionTree ι β) (a : ι → Bool) : graft (i :: l) k a = node i (graft l k (Function.update a i false)) (graft l k (Function.update a i true))

theorem Cslib.DecisionTree.eval_graft {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (l : List ι) (k : (ι → Bool) → DecisionTree ι β) (a x : ι → Bool) : (graft l k a).eval x = (k fun (j : ι) => if j ∈ l then x j else a j).eval x

theorem Cslib.DecisionTree.depth_graft_le {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (l : List ι) (k : (ι → Bool) → DecisionTree ι β) (a : ι → Bool) {d : ℕ} (hk : ∀ (b : ι → Bool), (k b).depth ≤ d) : (graft l k a).depth ≤ l.length + d

Grafting adds at most the number of queried variables to the depth.

def Cslib.DecisionTree.queryAll {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (f : (ι → Bool) → β) (l : List ι) (a : ι → Bool) : DecisionTree ι β

Query the variables of l in turn, starting from the assignment a, and output f of the assignment reached.

theorem Cslib.DecisionTree.eval_queryAll {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (f : (ι → Bool) → β) (l : List ι) (a x : ι → Bool) : (queryAll f l a).eval x = f fun (j : ι) => if j ∈ l then x j else a j

theorem Cslib.DecisionTree.depth_queryAll_le {ι : Type u_1} {β : Type u_2} [DecidableEq ι] (f : (ι → Bool) → β) (l : List ι) (a : ι → Bool) : (queryAll f l a).depth ≤ l.length

theorem Cslib.DecisionTree.exists_computes {ι : Type u_1} {β : Type u_2} [Fintype ι] (f : (ι → Bool) → β) : ∃ (t : DecisionTree ι β), t.Computes f ∧ t.depth ≤ Fintype.card ι

Over finitely many variables, every function has a decision tree that queries each variable once.

noncomputable def Cslib.DecisionTree.complexity {ι : Type u_1} {β : Type u_2} (f : (ι → Bool) → β) : ℕ

The decision tree complexity of f: the least depth of a decision tree computing it. It is 0 when no decision tree computes f, which can only happen over infinitely many variables.

theorem Cslib.DecisionTree.complexity_le_depth {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {t : DecisionTree ι β} (ht : t.Computes f) : complexity f ≤ t.depth

theorem Cslib.DecisionTree.exists_computes_depth_eq_complexity {ι : Type u_1} {β : Type u_2} [Finite ι] (f : (ι → Bool) → β) : ∃ (t : DecisionTree ι β), t.Computes f ∧ t.depth = complexity f

Some decision tree computing f has depth exactly its decision tree complexity.

theorem Cslib.DecisionTree.complexity_le_iff {ι : Type u_1} {β : Type u_2} [Finite ι] {f : (ι → Bool) → β} {d : ℕ} : complexity f ≤ d ↔ ∃ (t : DecisionTree ι β), t.Computes f ∧ t.depth ≤ d

theorem Cslib.DecisionTree.le_complexity_iff {ι : Type u_1} {β : Type u_2} [Finite ι] {f : (ι → Bool) → β} {d : ℕ} : d ≤ complexity f ↔ ∀ (t : DecisionTree ι β), t.Computes f → d ≤ t.depth

Lower bounds on decision tree complexity are lower bounds on the depth of every tree.

theorem Cslib.DecisionTree.complexity_eq_zero_iff {ι : Type u_1} {β : Type u_2} [Finite ι] {f : (ι → Bool) → β} : complexity f = 0 ↔ Function.IsConst f

A function has decision tree complexity zero exactly when it is constant.

theorem Cslib.DecisionTree.complexity_le_card {ι : Type u_1} {β : Type u_2} [Fintype ι] (f : (ι → Bool) → β) : complexity f ≤ Fintype.card ι

Decision tree complexity is at most the number of variables.