Bounded normal forms from decision trees

A decision tree of depth d has both an exact width-d DNF and an exact width-d CNF. This module constructs the DNF structurally from accepting paths, then obtains the CNF by De Morgan duality.

Repeated queries require care: conjoining a branch literal keeps an identical literal already present in a term, discards a contradictory term, and inserts the literal only when its coordinate is absent. Thus the construction applies to arbitrary decision trees and does not assume a read-once normal form. It is a symbolic tree traversal, not truth-table enumeration or depth optimization.

def Algebraic.AC0.Term.conjoinLiteral {n : ℕ} (term : Term n) (literal : Literal n) : Option (Term n)

Conjoin one literal with a noncontradictory term. A conflicting repeated literal makes the conjunction false, represented by none.

Equations

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

theorem Algebraic.AC0.Term.conjoinLiteral_sound {n : ℕ} (term : Term n) (literal : Literal n) (input : Fin n → Bool) : ((term.conjoinLiteral literal).elim false fun (result : Term n) => result.eval input) = (term.eval input && literal.eval input)

conjoinLiteral has exactly the semantics of Boolean conjunction.

theorem Algebraic.AC0.Term.width_conjoinLiteral_le {n : ℕ} (term result : Term n) (literal : Literal n) (conjoined : term.conjoinLiteral literal = some result) : LiteralSet.width result ≤ LiteralSet.width term + 1

Conjoining one literal increases term width by at most one.

def Algebraic.AC0.DNF.conjoinLiteral {n : ℕ} (formula : DNF n) (literal : Literal n) : DNF n

Conjoin every term of a DNF with one literal, discarding contradictory terms.

Equations

• formula.conjoinLiteral literal = { terms := List.filterMap (fun (term : Algebraic.AC0.Term n) => term.conjoinLiteral literal) formula.terms }

@[simp]

theorem Algebraic.AC0.DNF.eval_conjoinLiteral {n : ℕ} (formula : DNF n) (literal : Literal n) (input : Fin n → Bool) : (formula.conjoinLiteral literal).eval input = (formula.eval input && literal.eval input)

Formula-level literal conjunction is semantically exact.

theorem Algebraic.AC0.DNF.WidthAtMost.conjoinLiteral {n : ℕ} {formula : DNF n} {bound : ℕ} (bounded : formula.WidthAtMost bound) (literal : Literal n) : (formula.conjoinLiteral literal).WidthAtMost (bound + 1)

Literal conjunction raises a DNF width bound by at most one.

def Algebraic.AC0.DNF.disjoin {n : ℕ} (left right : DNF n) : DNF n

Disjunction of two ordered DNFs by concatenating their term lists.

Equations

• left.disjoin right = { terms := left.terms ++ right.terms }

@[simp]

theorem Algebraic.AC0.DNF.eval_disjoin {n : ℕ} (left right : DNF n) (input : Fin n → Bool) : (left.disjoin right).eval input = (left.eval input || right.eval input)

DNF list concatenation computes Boolean disjunction.

theorem Algebraic.AC0.DNF.WidthAtMost.disjoin {n : ℕ} {left right : DNF n} {bound : ℕ} (leftBounded : left.WidthAtMost bound) (rightBounded : right.WidthAtMost bound) : (left.disjoin right).WidthAtMost bound

Concatenating two DNFs preserves a common width bound.

def Algebraic.AC0.DecisionTree.toDNF {n : ℕ} : DecisionTree n → DNF n

Structural DNF expansion of a decision tree. Each accepting path becomes a term; incompatible repeated queries are discarded while matching repeats do not increase width.

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.AC0.DecisionTree.leaf false).toDNF = Algebraic.AC0.DNF.bottom
• (Algebraic.AC0.DecisionTree.leaf true).toDNF = Algebraic.AC0.DNF.top

@[simp]

theorem Algebraic.AC0.DecisionTree.eval_toDNF {n : ℕ} (tree : DecisionTree n) (input : Fin n → Bool) : tree.toDNF.eval input = tree.eval input

The structural DNF computes exactly the source decision tree.

theorem Algebraic.AC0.DecisionTree.widthAtMost_toDNF {n : ℕ} (tree : DecisionTree n) : tree.toDNF.WidthAtMost tree.depth

Every term in the structural DNF has width at most the tree depth.

def Algebraic.AC0.DecisionTree.toCNF {n : ℕ} (tree : DecisionTree n) : CNF n

De Morgan-derived structural CNF expansion of a decision tree.

Equations

• tree.toCNF = tree.negate.toDNF.negate

@[simp]

theorem Algebraic.AC0.DecisionTree.eval_toCNF {n : ℕ} (tree : DecisionTree n) (input : Fin n → Bool) : tree.toCNF.eval input = tree.eval input

The structural CNF computes exactly the source decision tree.

theorem Algebraic.AC0.DecisionTree.widthAtMost_toCNF {n : ℕ} (tree : DecisionTree n) : tree.toCNF.WidthAtMost tree.depth

Every clause in the structural CNF has width at most the tree depth.

theorem Algebraic.AC0.DecisionTree.exists_dnf_widthAtMost_of_depthAtMost {n : ℕ} {function : ScalarFunction Bool n} {bound : ℕ} (bounded : DepthAtMost function bound) : ∃ (formula : DNF n), formula.WidthAtMost bound ∧ ∀ (input : Fin n → Bool), formula.eval input = function input

Any function of decision-tree depth at most bound has an exact width-bound DNF representation.

theorem Algebraic.AC0.DecisionTree.exists_cnf_widthAtMost_of_depthAtMost {n : ℕ} {function : ScalarFunction Bool n} {bound : ℕ} (bounded : DepthAtMost function bound) : ∃ (formula : CNF n), formula.WidthAtMost bound ∧ ∀ (input : Fin n → Bool), formula.eval input = function input

Any function of decision-tree depth at most bound has an exact width-bound CNF representation.