Gold-Style Success Criteria (Identification in the Limit)

Seven success criteria for Gold-style learning: EX, BC, Finite, Vacillatory, Anomalous, Monotonic, TrialAndError.

All share the quantifier pattern: ∃ L, ∀ c ∈ C, ∀ T (text/informant for c), ∃ t₀, ∀ t ≥ t₀, ...

The variation is in what "..." requires.

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

Helper: the data seen up to time t from a data stream.

Equations

• dataUpTo T t = List.map T.observe (List.range (t + 1))

def EXLearnable (X : Type u) (C : ConceptClass X Bool) : Prop

EX-learning (explanatory learning, identification in the limit): The learner eventually converges to a hypothesis extensionally equal to c. Gold's original definition (1967).

Equations

• EXLearnable X C = ∃ (L : GoldLearner X Bool), ∀ c ∈ C, ∀ (T : TextPresentation X c), ∃ (t₀ : ℕ), ∀ t ≥ t₀, L.conjecture (dataUpTo T.toDataStream t) = c

def BCLearnable (X : Type u) (C : ConceptClass X Bool) : Prop

BC-learning (behaviorally correct): the learner need only output a hypothesis EXTENSIONALLY equal to c (not syntactically). May oscillate between representations.

Equations

• BCLearnable X C = ∃ (L : GoldLearner X Bool), ∀ c ∈ C, ∀ (T : TextPresentation X c), ∃ (t₀ : ℕ), ∀ t ≥ t₀, ∀ (x : X), L.conjecture (dataUpTo T.toDataStream t) x = c x

def FiniteLearnable (X : Type u) (C : ConceptClass X Bool) : Prop

Finite learning: EX-learning where the learner makes at most finitely many mind changes and eventually outputs a CORRECT hypothesis. Stronger than EX.

Equations

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

def VacillatoryLearnable (X : Type u) (C : ConceptClass X Bool) : Prop

Vacillatory learning: BC-learning where the learner may oscillate between finitely many correct hypotheses.

Equations

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

def AnomalousLearnable (X : Type u) [Fintype X] (C : ConceptClass X Bool) (a : ℕ) : Prop

Anomalous learning: EX-learning where the final hypothesis may have finitely many errors (anomalies).

Equations

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

def MonotonicLearnable (X : Type u) (C : ConceptClass X Bool) : Prop

Monotonic learning: a Gold learner that never RETRACTS a positive claim.

Equations

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

def TrialAndErrorLearnable (X : Type u) (C : ConceptClass X Bool) : Prop

Trial and error learning: point-wise convergence. Characterizes limiting recursion.

Equations

• TrialAndErrorLearnable X C = ∃ (L : GoldLearner X Bool), ∀ c ∈ C, ∀ (T : TextPresentation X c) (x : X), ∃ (t₀ : ℕ), ∀ t ≥ t₀, L.conjecture (dataUpTo T.toDataStream t) x = c x