Canonical decision trees for DNF formulas #
This module formalizes the dynamic canonical decision tree used in the
decision-tree form of Hastad's switching lemma. At each partial assignment it
restricts the whole DNF, selects the first surviving term, and queries every
remaining variable of that term in input-coordinate order. A satisfying
branch returns true; every other branch repeats the construction after the
new assignments have simplified the entire formula.
The recursion is structural in the number of live variables. It is not an optimal-tree search. The distinguished tree makes the eventual switching event concrete and decidable while its correctness gives an ordinary existential decision-tree depth bound as a corollary.
The support of a literal set in the canonical input-coordinate order.
Equations
- set.orderedSupport = List.filter (fun (index : Fin n) => decide (index ∈ set.support)) (List.finRange n)
Instances For
Canonical support lists contain no repeated coordinate.
The first source term not already falsified by a partial assignment.
Equations
- Algebraic.AC0.DNF.firstSurvivingIn rho [] = none
- Algebraic.AC0.DNF.firstSurvivingIn rho (term :: rest) = if Algebraic.AC0.LiteralSet.ConflictsWith term rho then Algebraic.AC0.DNF.firstSurvivingIn rho rest else some term
Instances For
The first term of an ordered DNF not falsified by the assignment.
Equations
- formula.firstSurviving rho = Algebraic.AC0.DNF.firstSurvivingIn rho formula.terms
Instances For
Failure to find a surviving term means that every source term conflicts with the assignment.
A term returned by firstSurvivingIn occurs in the source list.
A term returned by firstSurvivingIn is not falsified.
A first surviving term remains first after refinement whenever that term itself remains nonconflicting.
Variables of term still live under rho, retained in canonical input
order.
Equations
- Algebraic.AC0.DNF.liveSupport term rho = List.filter (fun (index : Fin n) => decide (rho index = none)) (Algebraic.AC0.LiteralSet.orderedSupport term)
Instances For
Live-support lists contain no repeated coordinate.
Computing live support from the source term agrees with first taking its residual literal set.
A first surviving source term remains first after a refinement whenever that term itself remains nonconflicting.
If no source term survives, the restricted DNF is constantly false.
A surviving term with no live variable makes the restricted DNF constantly true.
Every term returned by DNF restriction uses only variables left live by the restriction.
Query the listed variables in order, then continue with recurse on the
refined restriction, whose number of live variables stays below bound.
Equations
- One or more equations did not get rendered due to their size.
- Algebraic.AC0.DNF.queryRemainingBelow [] rho bound below recurse = recurse rho below
Instances For
One step of the canonical decision tree at a surviving term: query the term's
live variables, answer true if the term is satisfied, and otherwise recurse on
the refined restriction.
Equations
- One or more equations did not get rendered due to their size.
- _formula.canonicalSupportStep rho recurse [] allLive_2 = Algebraic.AC0.DecisionTree.leaf true
Instances For
One step of the canonical decision tree of a DNF under restriction rho:
answer false if no term survives, and otherwise query the first surviving
term's live variables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical decision tree of formula below a partial assignment.
The whole formula is freshly restricted between queried terms. Hence later term selection incorporates every assignment made along the current branch.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A canonical path transcript partitioned into the successive source terms selected by the canonical procedure.
- nil
{n : ℕ}
{formula : DNF n}
(rho : PartialAssignment n)
: formula.CanonicalTrace rho []
The empty path prefix is valid at every canonical state.
- start
{n : ℕ}
{formula : DNF n}
{rho : PartialAssignment n}
{term : Term n}
{indices : List (Fin n)}
{steps : List (DecisionTree.PathStep n)}
(found : formula.firstSurviving rho = some term)
(support_eq : liveSupport term rho = indices)
(nonempty : indices ≠ [])
(block : formula.CanonicalBlockTrace term rho indices steps)
: formula.CanonicalTrace rho steps
Begin the next nonempty query block at the first surviving source term.
Instances For
The part of a canonical transcript currently querying one source term.
The final constructor returns to CanonicalTrace, which selects the next
source term after the completed block assignment.
- nil
{n : ℕ}
{formula : DNF n}
{term : Term n}
(rho : PartialAssignment n)
(index : Fin n)
(rest : List (Fin n))
: formula.CanonicalBlockTrace term rho (index :: rest) []
A requested path prefix may stop in the middle of a query block.
- takeMore
{n : ℕ}
{formula : DNF n}
{term : Term n}
{rho : PartialAssignment n}
{index next : Fin n}
{rest : List (Fin n)}
{value : Bool}
{steps : List (DecisionTree.PathStep n)}
(tail : formula.CanonicalBlockTrace term (rho.refine (PartialAssignment.fix index value)) (next :: rest) steps)
: formula.CanonicalBlockTrace term rho (index :: next :: rest) ({ index := index, value := value } :: steps)
Consume a query when more variables remain in the current term.
- takeLast
{n : ℕ}
{formula : DNF n}
{term : Term n}
{rho : PartialAssignment n}
{index : Fin n}
{value : Bool}
{steps : List (DecisionTree.PathStep n)}
(tail : formula.CanonicalTrace (rho.refine (PartialAssignment.fix index value)) steps)
: formula.CanonicalBlockTrace term rho [index] ({ index := index, value := value } :: steps)
Consume the last query of a block and restart canonical term selection.
Instances For
Every path through the canonical decision tree carries a source-term block trace matching the canonical selection procedure.
The canonical tree computes exactly the DNF under the supplied partial assignment.
The canonical tree never queries more coordinates than remain live.
Every canonical root-to-leaf path queries each initially live coordinate at most once.
Every finite canonical path has distinct queried coordinates, all of which were live before the path began.
The numeric depth of the distinguished canonical tree.
Equations
- formula.canonicalDepth rho = (formula.canonicalDecisionTree rho).depth
Instances For
Canonical depth is bounded by the number of live variables.
The concrete bad event counted by the canonical switching argument.
Equations
- formula.CanonicalDepthAtLeast rho threshold = (threshold ≤ formula.canonicalDepth rho)
Instances For
An exact-length prefix of a path through a canonical DNF decision tree.
- steps : List (DecisionTree.PathStep n)
Query-and-answer transcript.
- endpoint : DecisionTree n
Subtree reached after the transcript.
- follows : (formula.canonicalDecisionTree rho).Path self.steps self.endpoint
The transcript follows the canonical tree.
The transcript has the requested exact length.
Instances For
A canonical-depth event supplies an exact-length canonical path prefix.
Canonical path coordinates contain no duplicates.
Every canonical path coordinate was live at the path's initial restriction.
The assignment carried by an exact canonical path fixes exactly the path length.
The assignment carried by a canonical path fixes only variables live at the path's initial restriction.
Equations
- formula.canonicalDepthAtLeastDecidable rho threshold = id (id inferInstance)
The canonical tree also computes the syntactically restricted DNF.
The canonical tree witnesses an ordinary decision-tree upper bound for the restricted DNF.
If every tree for the restricted function has depth at least threshold,
then the canonical tree does too. This relates the concrete switching event to
the representation-independent lower-depth predicate.
At the empty restriction, the canonical tree computes the original DNF.