Mind Change Complexity (Gold Paradigm)

Counts how often a Gold learner changes its conjecture before converging.

def DataStream.prefix {X : Type u} {Y : Type v} (T : DataStream X Y) (t : ℕ) : List (X × Y)

The data prefix: the first t examples from a data stream, as a list.

Equations

• T.prefix t = List.map T.observe (List.range t)

noncomputable def MindChangeCount (X : Type u) (L : GoldLearner X Bool) (_c : Concept X Bool) (T : DataStream X Bool) : ℕ

Mind change count: the number of times a Gold learner changes its conjecture. Counts time steps t where L's conjecture on the first t examples differs from its conjecture on the first t+1 examples. Note: parameter c (target concept) is not used in the definition - it is carried for the type-level specification (theorems bounding mind changes reference c).

Equations

• MindChangeCount X L _c T = {t : ℕ | L.conjecture (T.prefix t) ≠ L.conjecture (T.prefix (t + 1))}.ncard

noncomputable def MindChangeOrdinal (X : Type u) (L : GoldLearner X Bool) (c : Concept X Bool) (T : DataStream X Bool) : Ordinal.{u_1}

Mind change ordinal: ordinal-valued complexity measure encoding both convergence and correctness. Returns a finite ordinal (< ω) when the learner converges correctly to concept c with finitely many mind changes. Returns ω otherwise (non-convergent, or convergent to wrong concept). This encoding makes MindChangeOrdinal < ω equivalent to correct convergence with finite mind changes - the key property for the mind change characterization theorem.

Design rationale: encoding correctness at the definition level makes the backward direction of mind_change_characterization provable - MindChangeOrdinal < ω directly entails both convergence and correctness without needing to extract them separately.

Equations

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