Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.decision-tree

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/decision_tree.clj2 definitions, 4 theorems

AHoF D-family Decision Tree learning (greedy top-down induction): at each node, split on the feature that most improves purity -- i.e. maximizes the impurity reduction (information gain / Gini gain). Choosing between two candidate splits by their gain is: choose-split gain-a feature-a gain-b feature-b = if gain-a <= gain-b then feature-b else feature-a (return the feature index of the higher-gain split), over exact-rational gains. Proved native and axiom-free: the split-selection rule; a worked split picking the higher-gain feature; the certificate that the chosen split's gain is at least the alternative's (native nnrat/at-most); and a stopping decision -- a node is a leaf when the best gain does not exceed the minimum-gain threshold. The impurity measure and candidate enumeration are executable; what is proved is the greedy split selection and the leaf-stopping decision. Requires nat, audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.decision-tree` prints this classification.

decision-tree/choose-split :
  (x₁ : ℚ≥0) (x₂ : ℕ) (x₃ : ℚ≥0) (x₄ : ℕ)
  → ℕ

decision-tree/is-leaf? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

decision-tree/picks-higher-gain :
  → decision-tree/choose-split 2 0 5 1 = 1

decision-tree/chosen-gain-is-best :
  → 2 ≤ 5

decision-tree/becomes-leaf :
  → ce-is/elite? 1 2 = data/true

decision-tree/keeps-splitting :
  → ce-is/elite? 5 2 = data/false