Decision trees from finite observations

An output determined by finitely many Boolean observations has a small decision tree whenever each nonconstant finite input domain admits a query for one varying observation. Queries may depend on the current domain. The construction only branches when both answers occur, so its leaf bound counts attained observation vectors rather than all possible Boolean vectors.

Main results

• Cslib.DecisionTree.exists_of_observations: a tree has depth at most the observation count and at most one leaf per attained observation vector.

theorem Cslib.DecisionTree.exists_of_observations {X : Type u_1} {I : Type u_2} {Q : Type u_3} {β : Type u_4} [Fintype I] (S : Finset X) (hS : S.Nonempty) (observe : X → I → Bool) (answer : Q → X → Bool) (output : X → β) (hout : ∀ x ∈ S, ∀ y ∈ S, observe x = observe y → output x = output y) (hquery : ∀ T ⊆ S, T.Nonempty → (∃ x ∈ T, ∃ y ∈ T, observe x ≠ observe y) → ∃ (q : Q) (i : I), (∀ x ∈ T, answer q x = observe x i) ∧ ∀ (b : Bool), {x ∈ T | observe x i = b}.Nonempty) : ∃ (t : DecisionTree Q β), (∀ x ∈ S, (t.eval fun (q : Q) => answer q x) = output x) ∧ t.depth ≤ Fintype.card I ∧ t.leafCount ≤ (Finset.image observe S).card

A domain-dependent query for a varying observation yields a tree with no empty branches. The output need only be constant on observation fibers inside the supplied finite domain.