Learner Properties

Properties that learners may satisfy: iterative, set-driven, consistent, conservative, passive. These are Prop predicates, not separate types. Also includes probabilistic and team learner variants.

Learner Properties

def IsIterative {X : Type u} {Y : Type v} (L : GoldLearner X Y) : Prop

An iterative learner depends only on its previous hypothesis and the new data point.

Equations

• IsIterative L = ∃ (step : Concept X Y → X × Y → Concept X Y), ∀ (data : List (X × Y)) (xy : X × Y), L.conjecture (data ++ [xy]) = step (L.conjecture data) xy

def IsSetDriven {X : Type u} {Y : Type v} [DecidableEq X] [DecidableEq Y] (L : GoldLearner X Y) : Prop

A set-driven learner's output depends only on the SET of data, not the order.

Equations

• IsSetDriven L = ∀ (data₁ data₂ : List (X × Y)), data₁.toFinset = data₂.toFinset → L.conjecture data₁ = L.conjecture data₂

def IsConsistent {X : Type u} {Y : Type v} (L : GoldLearner X Y) : Prop

A consistent learner always outputs a hypothesis consistent with all data seen.

Equations

• IsConsistent L = ∀ (data : List (X × Y)), ∀ p ∈ data, L.conjecture data p.1 = p.2

def IsConservative {X : Type u} {Y : Type v} (L : GoldLearner X Y) : Prop

A conservative learner only changes its hypothesis when forced by inconsistency.

Equations

• IsConservative L = ∀ (data : List (X × Y)) (xy : X × Y), L.conjecture data xy.1 = xy.2 → L.conjecture (data ++ [xy]) = L.conjecture data

structure ProbabilisticLearner (X : Type u) (Y : Type v) : Type (max u v)

A probabilistic learner uses randomness.

• hypotheses : HypothesisSpace X Y

  The hypothesis space

• learn {m : ℕ} : ℕ → (Fin m → X × Y) → Concept X Y

  Randomized learning: seed → sample → hypothesis

structure TeamLearner (X : Type u) (Y : Type v) (n : ℕ) : Type (max u v)

A team learner: multiple learners, at least one of which identifies the target.

• team : Fin n → GoldLearner X Y

  The team members

MeasurableBatchLearner API

theorem MeasurableBatchLearner.learn_measurable {X : Type u} [MeasurableSpace X] (L : BatchLearner X Bool) [h : MeasurableBatchLearner X L] {m : ℕ} (S : Fin m → X × Bool) : Measurable (L.learn S)

Fixed-sample measurability: for fixed training data S, L.learn S is a measurable function X → Bool. This is the most commonly used consequence of MeasurableBatchLearner.