Decision Trees

Pure decision tree datatype and evaluator. This is a standalone non-neural baseline, so it does not use the tensor/module APIs.

Why include it here?

• It serves as a non-neural reference baseline for experiments (e.g. mixed pipelines).
• The datatype is direct enough to use in proofs or examples without pulling in tensor machinery.

If you're thinking in the Python ecosystem: this is not an nn.Module-style component. It is closer to a symbolic scikit-learn style decision tree, except we keep it fully pure and explicit.

References / analogies:

• Breiman, Friedman, Olshen, Stone, "Classification and Regression Trees" (CART), 1984.
• Quinlan, "Induction of Decision Trees" (ID3), 1986; and "C4.5: Programs for Machine Learning", 1993.
• scikit-learn user guide (for intuition, not semantics): https://scikit-learn.org/stable/modules/tree.html

inductive DecisionTree (α : Type) : Type

A small decision tree datatype (spec-only baseline).

node feature left right branches on decisionFn feature.

• leaf {α : Type} (value : α) : DecisionTree α
• node {α : Type} (feature : String) (left right : DecisionTree α) : DecisionTree α

def evaluate {α : Type} (tree : DecisionTree α) (decisionFn : String → Bool) : α

Evaluate a decision tree using a Boolean predicate for each feature name.