Compiling finite decision trees to CNF and DNF

An accepting path of length at most d becomes a DNF term of width at most d. De Morgan duality gives a CNF with the same bounds. Both normal forms compute exactly the original tree, have at most one component per leaf, and therefore have at most 2 ^ d terms or clauses.

theorem Complexity.DecisionTree.On.eval_toDNF {N : ℕ} (tree : On N) (input : BitString N) : tree.toDNF.eval input = eval input tree

The accepting-path DNF computes exactly the original decision tree.

theorem Complexity.DecisionTree.On.eval_toCNF {N : ℕ} (tree : On N) (input : BitString N) : tree.toCNF.eval input = eval input tree

The dual CNF computes exactly the original decision tree.

theorem Complexity.DecisionTree.On.width_toDNF_le_depth {N : ℕ} (tree : On N) : tree.toDNF.width ≤ tree.depth

The accepting-path DNF has width at most the tree depth.

theorem Complexity.DecisionTree.On.width_toCNF_le_depth {N : ℕ} (tree : On N) : tree.toCNF.width ≤ tree.depth

The dual CNF has width at most the tree depth.

theorem Complexity.DecisionTree.On.complexity_toDNF_le_numLeaves {N : ℕ} (tree : On N) : tree.toDNF.complexity ≤ tree.numLeaves

The accepting-path DNF has at most one term per decision-tree leaf.

theorem Complexity.DecisionTree.On.complexity_toCNF_le_numLeaves {N : ℕ} (tree : On N) : tree.toCNF.complexity ≤ tree.numLeaves

The dual CNF has at most one clause per decision-tree leaf.

theorem Complexity.DecisionTree.On.complexity_toDNF_le_two_pow_depth {N : ℕ} (tree : On N) : tree.toDNF.complexity ≤ 2 ^ tree.depth

A depth-d decision tree compiles to a DNF with at most 2 ^ d terms.

theorem Complexity.DecisionTree.On.complexity_toCNF_le_two_pow_depth {N : ℕ} (tree : On N) : tree.toCNF.complexity ≤ 2 ^ tree.depth

A depth-d decision tree compiles to a CNF with at most 2 ^ d clauses.

theorem Complexity.DecisionTree.On.eval_anyDNF {N : ℕ} (trees : List (On N)) (input : BitString N) : (anyDNF trees).eval input = trees.any fun (tree : On N) => eval input tree

Disjoining a list of trees and compiling to DNF preserves semantics.

theorem Complexity.DecisionTree.On.eval_allCNF {N : ℕ} (trees : List (On N)) (input : BitString N) : (allCNF trees).eval input = trees.all fun (tree : On N) => eval input tree

Conjoining a list of trees and compiling to CNF preserves semantics.

theorem Complexity.DecisionTree.On.width_anyDNF_le {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (anyDNF trees).width ≤ bound

A disjunction of depth-bounded trees compiles to a DNF under the same width bound.

theorem Complexity.DecisionTree.On.width_allCNF_le {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (allCNF trees).width ≤ bound

A conjunction of depth-bounded trees compiles to a CNF under the same width bound.

theorem Complexity.DecisionTree.On.complexity_anyDNF_le {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (anyDNF trees).complexity ≤ trees.length * 2 ^ bound

A disjunction of depth-d trees compiles to at most number of trees * 2 ^ d DNF terms.

theorem Complexity.DecisionTree.On.complexity_allCNF_le {N : ℕ} (trees : List (On N)) (bound : ℕ) (hbound : ∀ tree ∈ trees, tree.depth ≤ bound) : (allCNF trees).complexity ≤ trees.length * 2 ^ bound

A conjunction of depth-d trees compiles to at most number of trees * 2 ^ d CNF clauses.