LeanMachineLearning

3.8. SequentialLearning.Deterministic🔗

Deterministic algorithms and environments

A deterministic algorithm chooses its action in a deterministic way. That is, that action is given by a measurable function of the history instead of a general Markov kernel. Similarly, a deterministic environment gives feedback in a deterministic way.

Main definitions

We introduce two typeclasses IsDeterministicAlg and IsDeterministicEnv to express that an algorithm or an environment is deterministic. We also give definitions for the initial action and the next action of a deterministic algorithm, and for the feedback functions of a deterministic environment. Finally, we give a construction of a deterministic algorithm and environment from measurable functions.

  • IsDeterministicAlg alg: a typeclass expressing that the algorithm alg is deterministic.

  • IsDeterministicEnv env: a typeclass expressing that the environment env is deterministic.

  • actionZero alg: the initial action of a deterministic algorithm alg.

  • nextAction alg n: the function that gives the next action of a deterministic algorithm alg at step n, as a function of the history.

  • feedbackFunZero env: the function that gives the initial feedback of a deterministic environment env.

  • feedbackFun env n: the function that gives the feedback of a deterministic environment env at step n, as a function of the history and the current action.

  • detAlgorithm nextA h_next action0: a deterministic algorithm that chooses its action according to the measurable function nextA (with proof of measurability h_next), with initial action action0.

Module LeanMachineLearning.SequentialLearning.Deterministic contains 39 exposed declarations.