Canonical deepest paths in finite decision trees -- definitions

def Complexity.DecisionTree.On.deepPath {N : ℕ} : On N → List (Fin N × Bool)

A deepest root-to-leaf path, recording each query and chosen branch. Ties are resolved toward the false child.

Equations

• (Complexity.DecisionTree.On.leaf value).deepPath = []
• (Complexity.DecisionTree.On.node index ifFalse ifTrue).deepPath = if ifTrue.depth ≤ ifFalse.depth then (index, false) :: ifFalse.deepPath else (index, true) :: ifTrue.deepPath

def Complexity.DecisionTree.On.deepPathVars {N : ℕ} (tree : On N) : List (Fin N)

The query indices occurring on deepPath.

Equations

• tree.deepPathVars = List.map Prod.fst tree.deepPath

def Complexity.DecisionTree.On.PathReadOnce {N : ℕ} : On N → Prop

No root-to-leaf path repeats a query. This structural predicate is stronger than merely having a duplicate-free chosen deepest path.

Equations

• (Complexity.DecisionTree.On.leaf value).PathReadOnce = True
• (Complexity.DecisionTree.On.node index ifFalse ifTrue).PathReadOnce = (index ∉ ifFalse.vars ∧ index ∉ ifTrue.vars ∧ ifFalse.PathReadOnce ∧ ifTrue.PathReadOnce)