LeanMachineLearning

3.3. SequentialLearning.Algorithm🔗

Algorithms and environments

We define structures for stochastic, sequential algorithms and environments, and the notion of an algorithm-environment sequence, which is a sequence of actions and feedbacks generated by an algorithm interacting with an environment.

At time n, the algorithm has observed the n action-feedback pairs at times 0, ..., n - 1. That history is an element of Fin n → 𝓐 × 𝓨. The algorithm then chooses an action A n according to its policy, and the environment returns a feedback Y n given the history and A n. In particular, the first action is chosen according to the policy at time 0, applied to the empty history (the unique element of Fin 0 → 𝓐 × 𝓨).

Main definitions

  • Algorithm 𝓐 𝓨: a stochastic, sequential algorithm.

  • Environment 𝓐 𝓨: a stochastic environment.

  • history A Y n: the history before time n, a random variable with values in Fin n → 𝓐 × 𝓨.

  • IsAlgEnvSeq A 𝓨 alg env P: an algorithm-environment sequence. That is, a sequence of actions A and feedback Y that have the correct conditional distributions to be generated by an algorithm alg interacting with an environment env, defined on a probability space (Ω, P).

  • IsAlgEnvSeqUntil A Y alg env P N: A and Y form an algorithm-environment sequence for the times n < N.

  • prod_left alg: an Algorithm 𝓐 (𝓧 × 𝓨) obtained from an algorithm alg : Algorithm 𝓐 𝓨 by ignoring the 𝓧 component of each observation.

Laws at time 0

At time 0 the history is the unique element of Fin 0 → 𝓐 × 𝓨: conditioning on it is the same as not conditioning. Note that those results need P to be a probability measure.

Module LeanMachineLearning.SequentialLearning.Algorithm contains 72 exposed declarations.