Evaluation paths in Boolean decision trees

The evaluation path of a decision tree on an input records exactly the queries and branch values encountered before reaching a leaf. Its length is at most the tree depth. More importantly, any second input agreeing on every coordinate queried along that path produces the same output.

This is an adversary-facing semantic interface. It does not normalize or optimize decision trees and permits repeated queries.

def Algebraic.AC0.DecisionTree.evaluationPath {n : ℕ} : DecisionTree n → (Fin n → Bool) → List (PathStep n)

Query transcript followed by tree on input.

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.AC0.DecisionTree.leaf value).evaluationPath x✝ = []

theorem Algebraic.AC0.DecisionTree.evaluationPath_length_le_depth {n : ℕ} (tree : DecisionTree n) (input : Fin n → Bool) : (tree.evaluationPath input).length ≤ tree.depth

An evaluation path cannot be longer than the source tree's depth.

theorem Algebraic.AC0.DecisionTree.eval_eq_of_agree_on_evaluationPath {n : ℕ} (tree : DecisionTree n) (source target : Fin n → Bool) (agree : ∀ index ∈ (PathStep.indices (tree.evaluationPath source)).toFinset, target index = source index) : tree.eval target = tree.eval source

Inputs agreeing on all coordinates queried along one evaluation path produce the same tree output.