Decision trees in normal form

The paths of a decision tree to leaves labelled true are the terms of a formula in disjunctive normal form computing the same function (DecisionTree.toDNF), and the paths to leaves labelled false, negated, are the clauses of a formula in conjunctive normal form (DecisionTree.toCNF). A path reads each variable at most once, a variable read again following the branch of its first reading, so the terms and clauses have distinct variables and at most depth literals Jukna, Section 14.1. So a function of decision tree depth t is a disjunction of terms and a conjunction of clauses of width at most t.

Main definitions

• Cslib.DecisionTree.map: relabel the leaves of a decision tree.
• Cslib.DecisionTree.toDNF, Cslib.DecisionTree.toCNF: the normal forms of a decision tree.

Main results

• Cslib.DecisionTree.eval_toDNF, Cslib.DecisionTree.eval_toCNF: they compute the tree.
• Cslib.DecisionTree.length_le_depth_of_mem_toDNF, Cslib.DecisionTree.length_le_depth_of_mem_toCNF: their width is at most the depth.

References

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

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

Relabel the leaves of a decision tree.

@[simp]

theorem Cslib.DecisionTree.eval_map {ι : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (t : DecisionTree ι β) (x : ι → Bool) : (map f t).eval x = f (t.eval x)

@[simp]

theorem Cslib.DecisionTree.depth_map {ι : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (t : DecisionTree ι β) : (map f t).depth = t.depth

def Cslib.DecisionTree.toDNFAux {ι : Type u_1} [DecidableEq ι] : DecisionTree ι Bool → Logic.PL.Term ι → Logic.PL.DNF ι

The terms of the paths of a decision tree to leaves labelled true, each extending the term p of the path so far; a variable already in p is not read again.

def Cslib.DecisionTree.toDNF {ι : Type u_1} [DecidableEq ι] (t : DecisionTree ι Bool) : Logic.PL.DNF ι

The formula in disjunctive normal form of the paths of a decision tree to leaves labelled true.

def Cslib.DecisionTree.toCNF {ι : Type u_1} [DecidableEq ι] (t : DecisionTree ι Bool) : Logic.PL.CNF ι

The formula in conjunctive normal form of the negated paths of a decision tree to leaves labelled false.

@[simp]

theorem Cslib.DecisionTree.eval_toDNF {ι : Type u_1} [DecidableEq ι] (t : DecisionTree ι Bool) (x : ι → Bool) : Logic.PL.DNF.eval x t.toDNF = t.eval x

The paths to leaves labelled true compute the tree.

@[simp]

theorem Cslib.DecisionTree.eval_toCNF {ι : Type u_1} [DecidableEq ι] (t : DecisionTree ι Bool) (x : ι → Bool) : Logic.PL.CNF.eval x t.toCNF = t.eval x

The negated paths to leaves labelled false compute the tree.

theorem Cslib.DecisionTree.length_le_depth_of_mem_toDNF {ι : Type u_1} [DecidableEq ι] {t : DecisionTree ι Bool} {q : Logic.PL.Term ι} (hq : q ∈ t.toDNF) : List.length q ≤ t.depth

The terms of the normal form of a tree have at most depth literals.

theorem Cslib.DecisionTree.nodup_of_mem_toDNF {ι : Type u_1} [DecidableEq ι] {t : DecisionTree ι Bool} {q : Logic.PL.Term ι} (hq : q ∈ t.toDNF) : (List.map Prod.fst q).Nodup

The terms of the normal form of a tree read each variable once.

theorem Cslib.DecisionTree.length_le_depth_of_mem_toCNF {ι : Type u_1} [DecidableEq ι] {t : DecisionTree ι Bool} {c : Logic.PL.Clause ι} (hc : c ∈ t.toCNF) : List.length c ≤ t.depth

The clauses of the conjunctive normal form of a tree have at most depth literals.