Tabular Reinforcement Learning

This module implements typed, total update rules for classic finite-state / finite-action RL:

• TD(0) state-value learning,
• SARSA,
• Expected SARSA,
• Q-learning,
• Double Q-learning.

Choose the bootstrap target with the appropriate rule, then apply update to a tensor coordinate. The same update works for state-value vectors, Q-tables, and higher-dimensional value tensors.

Primary references:

• Sutton, "Learning to Predict by the Methods of Temporal Differences" (1988): https://doi.org/10.1023/A:1022633531479
• Rummery and Niranjan, "On-line Q-learning using connectionist systems" (1994) (SARSA precursor): https://mi.eng.cam.ac.uk/reports/svr-ftp/auto-pdf/rummery_tr166.pdf
• Sutton, "Generalization in Reinforcement Learning: Successful Examples Using Sparse Coarse Coding" (1996) (SARSA / function approximation example): http://www.cs.ualberta.ca/~sutton/papers/sutton-96.pdf
• Watkins and Dayan, "Q-learning" (1992): https://doi.org/10.1007/BF00992698
• van Hasselt, "Double Q-learning" (2010): https://proceedings.neurips.cc/paper/2010/hash/091d584fced301b442654dd8c23b3fc9-Abstract.html
• Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed.): http://incompleteideas.net/book/the-book-2nd.html

def Runtime.RL.Tabular.update {α : Type} [TorchLean.Storage α] [TorchLean.Storage.Update α] [Add α] [Sub α] [Mul α] {shape : Spec.Shape} (values : TorchLean.Tensor α shape) (coordinate : shape.Coord) (target stepSize : α) : TorchLean.Tensor α shape

Move one tensor entry toward a supplied target by stepSize.

The target rule determines the algorithm; the update itself is independent of the table's shape. For Double Q-learning, update either table with a target computed using that table as selector and the other as evaluator. Arithmetic keeps the order current + stepSize * (target - current).

def Runtime.RL.Tabular.row {α : Type} [TorchLean.Storage α] {nStates nActions : ℕ} (q : TorchLean.Tensor α [nStates, nActions]) (state : Fin nStates) : TorchLean.Tensor α [nActions]

Extract the action-value row Q[s, :].

def Runtime.RL.Tabular.maximum {α : Type} [TorchLean.Storage α] [Context α] {nStates nActions : ℕ} (q : TorchLean.Tensor α [nStates, nActions]) (state : Fin nStates) : α

Max action value at a state, defaulting to 0 for empty action spaces.

def Runtime.RL.Tabular.greedy? {α : Type} [TorchLean.Storage α] [Context α] {nStates nActions : ℕ} (q : TorchLean.Tensor α [nStates, nActions]) (state : Fin nStates) : Option (Fin nActions)

Greedy action at a state, if the action space is nonempty.

def Runtime.RL.Tabular.expectation {α : Type} [TorchLean.Storage α] [Context α] {nStates nActions : ℕ} (q : TorchLean.Tensor α [nStates, nActions]) (state : Fin nStates) (policy : TorchLean.Tensor α [nActions]) : α

Policy-weighted action value. Weights are used as supplied, without normalization.

def Runtime.RL.Tabular.sarsaTarget {α : Type} [TorchLean.Storage α] [Context α] {nStates nActions : ℕ} (q : TorchLean.Tensor α [nStates, nActions]) (nextState : Fin nStates) (nextAction : Fin nActions) (reward gamma : α) (done : Bool := false) : α

SARSA target r + γ Q(s', a').

def Runtime.RL.Tabular.expectedSarsaTarget {α : Type} [TorchLean.Storage α] [Context α] {nStates nActions : ℕ} (q : TorchLean.Tensor α [nStates, nActions]) (nextState : Fin nStates) (nextPolicy : TorchLean.Tensor α [nActions]) (reward gamma : α) (done : Bool := false) : α

Expected SARSA target r + γ * E_{a' ~ π(.|s')}[Q(s', a')].

def Runtime.RL.Tabular.qLearningTarget {α : Type} [TorchLean.Storage α] [Context α] {nStates nActions : ℕ} (q : TorchLean.Tensor α [nStates, nActions]) (nextState : Fin nStates) (reward gamma : α) (done : Bool := false) : α

Q-learning target r + γ max_a Q(s', a).

def Runtime.RL.Tabular.doubleQTarget {α : Type} [TorchLean.Storage α] [Context α] {nStates nActions : ℕ} (selector evaluator : TorchLean.Tensor α [nStates, nActions]) (nextState : Fin nStates) (reward gamma : α) (done : Bool := false) : α

Double Q-learning / Double DQN-style target: choose the greedy action under selector, evaluate it under evaluator.