Version Space Lattice

The collection of all version spaces of a concept class is a ∩-closed family with top C, the version space lattice of Mitchell (1982).

Main definitions

• VersionSpaces C: the family of all version spaces of C, over samples of every size.

Main results

• versionSpace_append: the version space of an appended sample is the intersection of the version spaces.
• self_mem_versionSpaces, inter_mem_versionSpaces: the family contains C (top) and is closed under intersection.
• versionSpaces_subset_powerset, versionSpaces_finite, versionSpaces_ncard_le: every member is a subset of C and for a finite class the family is finite of size at most 2 ^ C.ncard.

References

• [Mit77]
• [Mit82]
• [Mit97]

theorem Cslib.MachineLearning.PACLearning.versionSpace_append {α : Type u_1} {β : Type u_2} {m n : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) (T : LabeledSample α β n) : VersionSpace C (Fin.append S T) = VersionSpace C S ∩ VersionSpace C T

The version-space meet law. The version space of an appended sample is the intersection of the version spaces of the two parts: constraints accumulate by intersection.

def Cslib.MachineLearning.PACLearning.VersionSpaces {α : Type u_1} {β : Type u_2} (C : ConceptClass α β) : Set (ConceptClass α β)

The family of all version spaces of a concept class, over labeled samples of every size.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.MachineLearning.PACLearning.mem_versionSpaces_iff {α : Type u_1} {β : Type u_2} {C V : ConceptClass α β} : V ∈ VersionSpaces C ↔ ∃ (m : ℕ) (S : LabeledSample α β m), V = VersionSpace C S

Membership in the version-space family unfolds to a witnessing sample.

theorem Cslib.MachineLearning.PACLearning.self_mem_versionSpaces {α : Type u_1} {β : Type u_2} (C : ConceptClass α β) : C ∈ VersionSpaces C

The whole class is a version space (of the empty sample) which means the family has top C.

theorem Cslib.MachineLearning.PACLearning.inter_mem_versionSpaces {α : Type u_1} {β : Type u_2} {C U V : ConceptClass α β} (hU : U ∈ VersionSpaces C) (hV : V ∈ VersionSpaces C) : U ∩ V ∈ VersionSpaces C

The version-space family is closed under intersection (append the witnessing samples).

theorem Cslib.MachineLearning.PACLearning.versionSpaces_subset_powerset {α : Type u_1} {β : Type u_2} (C : ConceptClass α β) : VersionSpaces C ⊆ 𝒫 C

Every version space is a subset of the class: the family lives in the powerset of C.

theorem Cslib.MachineLearning.PACLearning.versionSpaces_finite {α : Type u_1} {β : Type u_2} {C : ConceptClass α β} (hC : Set.Finite C) : (VersionSpaces C).Finite

A finite concept class has finitely many version spaces.

theorem Cslib.MachineLearning.PACLearning.versionSpaces_ncard_le {α : Type u_1} {β : Type u_2} {C : ConceptClass α β} (hC : Set.Finite C) : (VersionSpaces C).ncard ≤ 2 ^ Set.ncard C

A finite concept class has at most 2 ^ C.ncard version spaces: the lattice embeds in the powerset.