Compiling finite decision trees to CNF and DNF -- definitions

Each accepting root-to-leaf path becomes one DNF term. A false branch records the negative query literal and a true branch records the positive literal. The dual CNF is obtained by compiling the leaf-complemented tree and applying De Morgan negation.

def Complexity.DecisionTree.On.toDNFTerms {N : ℕ} : On N → List (List (Literal N))

DNF terms corresponding to the accepting paths of a finite decision tree.

Equations

• One or more equations did not get rendered due to their size.
• (Complexity.DecisionTree.On.leaf false).toDNFTerms = []
• (Complexity.DecisionTree.On.leaf true).toDNFTerms = [[]]

def Complexity.DecisionTree.On.toDNF {N : ℕ} (tree : On N) : DNF N

Compile a finite decision tree to a DNF with one term per accepting path.

Equations

• tree.toDNF = { terms := tree.toDNFTerms }

def Complexity.DecisionTree.On.toCNF {N : ℕ} (tree : On N) : CNF N

Compile a finite decision tree to a CNF by De Morgan duality.

Equations

• tree.toCNF = tree.neg.toDNF.neg

def Complexity.DecisionTree.On.anyDNF {N : ℕ} (trees : List (On N)) : DNF N

Compile a disjunction of decision trees to one DNF.

Equations

• Complexity.DecisionTree.On.anyDNF trees = Complexity.DNF.disjoin (List.map Complexity.DecisionTree.On.toDNF trees)

def Complexity.DecisionTree.On.allCNF {N : ℕ} (trees : List (On N)) : CNF N

Compile a conjunction of decision trees to one CNF.

Equations

• Complexity.DecisionTree.On.allCNF trees = Complexity.CNF.conjoin (List.map Complexity.DecisionTree.On.toCNF trees)