2.3 Batch learner
Definition
2.4
Batch Learner
Lean: BatchLearner
A batch learner over \((X, Y)\) is a bundled structure carrying a hypothesis set \(\mathcal{H} \subseteq Y^X\), a learning function \(\mathcal{A}\) that takes a finite training sample \(S : \mathrm{Fin}\, m \to X \times Y\) and returns a hypothesis in \(\mathcal{H}\), and a proof that the output lies in \(\mathcal{H}\).
The kernel formalizes the batch learner as a structure rather than as a bare function so that the constraint “output lies in the hypothesis set” travels with the algorithm. Chapter 4 will introduce a sequential learner with its own bundled type; the contrast between batch and sequential learning is the subject of Chapters 3 and 4.