Reinforcement Learning

Motivation

Reinforcement learning methods estimate the value function $v_\pi$ of a policy $\pi$: the expected discounted sum of future rewards from each state. When the state space is large, $v_\pi$ cannot be stored as a table and is approximated by a parametrized function. The most studied case is linear function approximation, where each state $s$ carries a feature vector $\mathbf x(s) \in \mathbb R^d$ and the estimate is $\hat v(s, \mathbf w) = \mathbf w^\top \mathbf x(s)$. Temporal-difference learning with this approximation, linear semi-gradient TD(0), is one of the basic algorithms of the field, and Chapter 9 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) presents its analysis: where the algorithm can converge, why that point exists, and how good it is.

The history is short. Sutton (1988, doi:10.1007/BF00115009) introduced TD learning and showed positive definiteness of the matrix governing its expected update. Dayan (1992, doi:10.1007/BF00992701) extended convergence to TD(λ). Tsitsiklis and Van Roy (1997, doi:10.1109/9.580874) proved convergence with probability one for linear TD(λ) under on-policy sampling and bounded the error of the limit. Bradtke and Barto (1996) introduced least-squares TD (LSTD), which computes the same limit directly.

Setting

A finite Markov decision process has finite sets of states $\mathcal S$, actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$, the probability of next state $s'$ and reward $r$ after action $a$ in state $s$. A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. It induces a Markov chain on states with transition matrix $\mathbf P$, $\mathbf P(s, s') = p(s' \mid s) = \sum_a \pi(a \mid s) \sum_r p(s', r \mid s, a)$, and expected one-step reward $r_\pi(s)$. For a discount rate $0 \le \gamma < 1$, the true value is $v_\pi(s) = \sum_{k \ge 0} \gamma^k (\mathbf P^k r_\pi)(s)$, the expected discounted return.

A state distribution $\mu$ is stationary if $\mu^\top \mathbf P = \mu^\top$; write $\mathbf D = \mathrm{diag}(\mu)$. The feature matrix $\mathbf X$ is the $|\mathcal S| \times d$ matrix with rows $\mathbf x(s)$. The mean square value error of a weight vector is

$$\overline{\mathrm{VE}}(\mathbf w) = \sum_{s} \mu(s)\,[v_\pi(s) - \mathbf w^\top \mathbf x(s)]^2 .$$

Linear semi-gradient TD(0) updates $\mathbf w_{t+1} = \mathbf w_t + \alpha(R_{t+1} + \gamma \mathbf w_t^\top \mathbf x_{t+1} - \mathbf w_t^\top \mathbf x_t)\mathbf x_t$. In steady state its expected update involves

$$\mathbf b = \mathbb E[R_{t+1}\mathbf x_t], \qquad \mathbf A = \mathbb E[\mathbf x_t(\mathbf x_t - \gamma \mathbf x_{t+1})^\top],$$

and the TD fixed point is $\mathbf w_{\mathrm{TD}} = \mathbf A^{-1}\mathbf b$. A real square matrix $M$, not necessarily symmetric, is positive definite if $y^\top M y > 0$ for every $y \ne 0$. The key matrix is $\mathbf D(\mathbf I - \gamma\mathbf P)$.

Formalization targets

Goal: the TD fixed point exists and its error bound (9.12), (9.14)

Under the hypotheses above, with every $\mu(s) > 0$ and linearly independent feature columns, $\mathbf A$ is invertible, $\mathbf b = \mathbf A \mathbf w_{\mathrm{TD}}$, and

$$\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}}) \le \frac{1}{1-\gamma}\min_{\mathbf w} \overline{\mathrm{VE}}(\mathbf w).$$

Milestones

1. The expected update (9.13): $\mathbb E[\mathbf w_{t+1} \mid \mathbf w_t] = (\mathbf I - \alpha \mathbf A)\mathbf w_t + \alpha \mathbf b$.
2. The matrix form $\mathbf A = \mathbf X^\top \mathbf D(\mathbf I - \gamma \mathbf P)\mathbf X$.
3. The criterion of Sutton (1988): positive diagonal, nonpositive off-diagonal entries, positive row sums and nonnegative column sums give positive definiteness.
4. The column sums of the key matrix, $\mathbf 1^\top \mathbf D(\mathbf I - \gamma \mathbf P) = (1-\gamma)\mu^\top$.
5. The key matrix and $\mathbf A$ are positive definite.
6. A positive definite $\mathbf A$ is invertible and $\mathbf A^{-1}\mathbf b$ is the unique solution of $\mathbf b = \mathbf A \mathbf w$ (9.12).
7. The Sherman–Morrison update (9.22) of the LSTD inverse $\hat{\mathbf A}_t^{-1}$.

Significance

Positive definiteness of $\mathbf A$ is the reason on-policy linear TD(0) is stable: it makes the expected iteration contract toward the fixed point for small step sizes, and it guarantees that the fixed point exists and is unique. The error bound (9.14) quantifies the price of bootstrapping: the limit of TD can be worse than the best linear approximation, but by at most the factor $1/(1-\gamma)$. The same objects $\mathbf A$, $\mathbf b$ and the key matrix reappear in LSTD, in the analysis of off-policy divergence (Chapter 11 of the book, where $\mathbf D$ is no longer the stationary distribution of $\mathbf P$ and positive definiteness fails), and in gradient-TD methods.

All results here are known. The book gives the positive definiteness argument in a box and cites (9.14) without proof. None of them has a machine-checked proof on the platform; the general Woodbury identity (FamousTheorems.woodbury_identity) is available, and (9.22) is its rank-one case written for the LSTD recursion. The mission produces a formal account of the finite-state theory of linear TD(0), with every hypothesis the book leaves implicit stated.

Difficulty

The key matrix $\mathbf D(\mathbf I - \gamma \mathbf P)$ is not symmetric, so the usual tools for symmetric positive definite matrices do not apply directly, and $\mathbf A$ is positive definite only because of the specific interplay between $\mathbf D$ and $\mathbf P$: if $\mu$ is replaced by a non-stationary distribution the claim is false (this is the off-policy counterexample of Chapter 11). The error bound (9.14) is not a consequence of positive definiteness alone. The TD fixed point is not the minimizer of $\overline{\mathrm{VE}}$, and $\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}})$ has to be compared with the error of the $\mu$-weighted projection of $v_\pi$, which requires controlling $\mathbf P$ in the $\mu$-weighted norm. The book gives no argument for this step.

Formalization scope

The Lean development lives in the namespace SuttonBartoRL.LinearTD. The MDP has four-argument dynamics $p(s', r \mid s, a)$ with a finite reward set and one action set for all states; policies are stochastic. $v_\pi$ is defined from expected discounted returns as the series $\sum_k \gamma^k \mathbf P^k r_\pi$, never from a Bellman equation or from $\mathbf w_{\mathrm{TD}}$. $\mathbf A$ and $\mathbf b$ are defined as the book's steady-state expectations (9.11), as finite sums over $\mu$, $\pi$ and $p$; the matrix form is a milestone, not a definition. Features are a matrix Matrix S (Fin d) ℝ with rows $\mathbf x(s)$; linear independence of its columns is LinearIndependent ℝ Xᵀ. Positive definiteness is a custom predicate $\forall y \ne 0,\ 0 < y^\top M y$, not Mathlib's Matrix.PosDef, which requires symmetry. The minimum in (9.14) is expressed by quantifying over every $\mathbf w$. The matrix inverse is Mathlib's, which is zero on singular matrices; the goal therefore asserts invertibility of $\mathbf A$ explicitly.

Hypotheses the book leaves implicit and the statements make explicit: $0 \le \gamma < 1$ (the continuing case); $\mu$ a stationary distribution of the chain induced by $\pi$ with $\mu(s) > 0$ for every $s$ (otherwise the key matrix is only positive semidefinite); linearly independent feature columns (the book's "degenerate cases", p. 205). The box calls the off-diagonal entries of the key matrix "negative"; they are zero wherever $p(s' \mid s) = 0$, so the criterion is stated with nonpositive entries. The book's sentence that $\varepsilon\mathbf I$ "ensures that $\hat{\mathbf A}_t$ is always invertible" (p. 229) is false in general, because the summands $\mathbf x_k(\mathbf x_k - \gamma \mathbf x_{k+1})^\top$ are not positive semidefinite: with $d = 1$, $\varepsilon = 1/10$, $\gamma = 1/2$, $\mathbf x_0 = 1$, $\mathbf x_1 = 11/5$ one gets $\hat{\mathbf A}_1 = 0$. It is not stated; (9.22) carries invertibility of $\hat{\mathbf A}_{t-1}$ and a nonzero denominator as hypotheses.

A statement in which $v_\pi$ is defined as the solution of the projected equation, or in which $\mathbf A$ is assumed invertible or positive definite, would make the goal trivial or empty; neither is done. Convergence of the stochastic algorithm with probability one is not stated, since the book says it needs conditions and a step-size schedule it does not give. The bound for the episodic case and for other bootstrapping methods (p. 208) is stated only by reference in the book and is not a target.

Useful infrastructure: the $\mu$-weighted inner product and orthogonal projection onto the column space of $\mathbf X$, the non-expansiveness of a stochastic matrix in the norm of its stationary distribution, and the positive definiteness criterion for non-symmetric matrices. All of these are reusable in the off-policy and average-reward chapters of the book. Contributions of these lemmas, and of alternative proofs of the milestones, are welcome.

Selected references

• Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§9.2, 9.4, 9.8.
• Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 1988. doi:10.1007/BF00115009
• John N. Tsitsiklis and Benjamin Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 1997. doi:10.1109/9.580874
• Steven J. Bradtke and Andrew G. Barto, Linear least-squares algorithms for temporal difference learning, Machine Learning 22, 1996. doi:10.1007/BF00114723
• Richard S. Varga, Matrix Iterative Analysis, Prentice-Hall, 1962.

Motivation

Reinforcement learning methods must explore in order to find good behaviour, yet the quantity they usually want to evaluate is the value of a different, often deterministic, policy. Off-policy prediction separates the two roles: episodes are generated by a behaviour policy $b$, and the goal is the value function $v_\pi$ of a target policy $\pi$. Almost every off-policy method in Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), and in the literature that follows it, rests on importance sampling: a return observed under $b$ is reweighted by the relative probability of its trajectory under $\pi$ and $b$. Section 5.5 of the book introduces the idea for Monte Carlo prediction, §5.6 gives the incremental form of the weighted estimator, and §§5.8–5.9 refine the weights using the internal structure of the return: discounting-aware importance sampling, after Sutton, Mahmood, Precup and van Hasselt (2014), and per-decision importance sampling, introduced by Precup, Sutton and Singh (2000). The book's remarks on the variance of the two estimators (p. 105) cite Precup, Sutton and Dasgupta (2001). Later chapters (7, 11, 12) reuse the same ratios for $n$-step, gradient-TD and eligibility-trace methods.

This mission is the fifth in a series formalizing the book's central mathematical claims. It covers §§5.5–5.9 (pp. 103–115).

Setting

A finite Markov decision process has finite sets of states $\mathcal S$ (terminal states included), actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$: for each $(s, a)$ a probability distribution over next state and reward. The state-transition probability is $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$. A policy $\mu$ gives a distribution $\mu(\cdot \mid s)$ over actions in every state.

An episode from a start state $s$ is a sequence $S_0 = s, A_0, R_1, S_1, \dots, A_{T-1}, R_T, S_T$ in which $S_0, \dots, S_{T-1}$ are nonterminal and $S_T$ is terminal. Under $\mu$ it has probability $\prod_{k=0}^{T-1} \mu(A_k \mid S_k)\, p(S_{k+1}, R_{k+1} \mid S_k, A_k)$. The return is $G_0 = \sum_{k=0}^{T-1} \gamma^k R_{k+1}$ with discount rate $\gamma \in [0, 1]$, and the value $v_\pi(s)$ is the expected return of an episode generated by $\pi$ from $s$.

The behaviour policy covers the target policy if $\pi(a \mid s) > 0$ implies $b(a \mid s) > 0$. The importance-sampling ratio of decisions $0, \dots, j$ is

$$\rho_{0:j} = \prod_{k=0}^{j} \frac{\pi(A_k \mid S_k)}{b(A_k \mid S_k)},$$

and the per-decision return weights each reward only by the ratio of the decisions that precede it:

$$\tilde G_0 = \rho_{0:0} R_1 + \gamma \rho_{0:1} R_2 + \dots + \gamma^{T-1} \rho_{0:T-1} R_T .$$

The book writes these objects at a general time $t$ and conditions on $S_t = s$; by the Markov property this is the same as starting the episode at $s$, which is what the formal statements do.

Formalization targets

Goal: unbiasedness of ordinary and per-decision importance sampling

For episodes generated by $b$ from $s$,

$$\mathbb E_b\bigl[\rho_{0:T-1} G_0 \mid S_0 = s\bigr] = v_\pi(s) = \mathbb E_b\bigl[\tilde G_0 \mid S_0 = s\bigr].$$

The first equality is Eq. (5.4) (p. 104); the second is the statement $\mathbb E[\rho_{t:T-1}G_t] = \mathbb E[\tilde G_t]$ of §5.9 (p. 114).

Milestones

1. (5.3): the trajectory probability is a product, and the ratio of trajectory probabilities under $\pi$ and $b$ is $\rho_{0:T-1}$, independent of the dynamics.
2. (5.4) alone.
3. (5.13): $\sum_a b(a \mid x)\, \pi(a \mid x)/b(a \mid x) = \sum_a \pi(a \mid x) = 1$ under coverage.
4. (5.14) and its $k$-th form: $\mathbb E_b[\rho_{0:T-1} R_k] = \mathbb E_b[\rho_{0:k-1} R_k]$ for every $k \ge 1$ (Exercise 5.13).
5. Example 5.5: in a one-state MDP with a loop, $v_\pi(s) = 1$ and $\mathbb E_b[\rho_{0:T-1}G_0] = 1$, yet $\mathbb E_b[(\rho_{0:T-1}G_0)^2] = \infty$.
6. (5.7)–(5.8): the incremental rule $V_{n+1} = V_n + (W_n/C_n)(G_n - V_n)$ computes the weighted average $\sum_{k<n} W_k G_k / \sum_{k<n} W_k$ (Exercise 5.10).
7. §5.8: $G_t = (1-\gamma)\sum_{h=t+1}^{T-1}\gamma^{h-t-1}\bar G_{t:h} + \gamma^{T-t-1}\bar G_{t:T}$ with flat partial returns $\bar G_{t:h} = R_{t+1} + \dots + R_h$.

Significance

Eq. (5.4) is the reason the first-visit ordinary importance-sampling estimator (5.5) is unbiased, and it is the template for every importance-sampling correction in the rest of the book. The per-decision identity shows that an estimator with fewer ratio factors per reward, (5.15), has the same expectation, which is the starting point for per-decision and control-variate methods for multi-step off-policy learning (Precup, Sutton and Singh 2000). Example 5.5 shows that unbiasedness says nothing about variance: the ordinary estimator can have infinite variance on a two-action problem, which motivates weighted importance sampling and the incremental weighted update of §5.6.

The results of these sections are classical and proved informally in the book, partly as exercises (5.10, 5.13) left without solution. No machine-checked version exists on the platform: a search for importance sampling, off-policy and per-decision returned no statements. The mission produces a formal trajectory model of an episodic MDP under two policies, which later missions on $n$-step off-policy returns and off-policy traces can reuse.

Difficulty

Eq. (5.4) itself is a termwise identity: for every episode, $\Pr_b(\text{episode})\,\rho_{0:T-1} = \Pr_\pi(\text{episode})$ under coverage. The per-decision identity is not termwise. The later factors of $\rho_{0:T-1}$ multiply a reward that was received before the corresponding decisions, and removing them requires summing over all continuations of an episode prefix, of every remaining length, and using that each factor has conditional expectation one (5.13) and that the continuation terminates with probability one. The obvious attempt, cancelling the factors episode by episode, fails: on a single episode $\rho_{0:T-1}R_1$ and $\rho_{0:0}R_1$ differ.

In Example 5.5 the episodes have no length bound, so the expected square is an infinite series over episode lengths whose divergence must be shown directly.

Formalization scope

• States, actions and rewards are finite types; the terminal states are a finite subset of the state type. Policies are stochastic, one action set is used in every state, and $v_\pi$ is defined as an expected return, never as the solution of a Bellman equation.
• Expectations are series over episode lengths of finite sums over episodes. Lean assigns $0$ to a divergent series, so the goal and milestones 2 and 4 assume that under $b$ every episode from $s$ terminates within a fixed number $H$ of steps with probability one. The book leaves termination implicit; this bounded-horizon hypothesis is a restriction relative to the book's episodic setting and is stated as such. Example 5.5, whose episodes are unbounded, is stated without it, with the expected square in $[0, \infty]$.
• The discount rate is kept general in $[0, 1]$.
• The importance-sampling ratio uses real division; a factor with $b(A_k \mid S_k) = 0$ evaluates to $0$ in Lean, but such episodes have probability $0$ under $b$.
• The flat-partial-return decomposition is an algebraic identity and is stated for every real $\gamma$, which is more general than the book's "for any $\gamma \in [0,1)$".
• The incremental weighted update is stated with nonnegative weights and $W_1 > 0$. The book's $C_0 = 0$ makes (5.8) divide by zero at $n = 1$ when $W_1 = 0$; the hypothesis excludes that case.
• A trivializing formalization is ruled out: $v_\pi$ is the expected return of $\pi$'s own episodes, the ratio is computed from the episode, and the per-decision identity, which carries the chapter's content beyond (5.4), is part of the goal.
• Not stated: the bias and variance comparisons of ordinary and weighted importance sampling (p. 105) and the discounting-aware estimators (5.9)–(5.10) as estimators; these are statistical claims about estimators over a random number of visits that the book does not make precise.

Contributions welcome: proofs of the milestones, a general measure-theoretic version of the trajectory model without the bounded-horizon hypothesis, and variants for action values $q_\pi$ (Exercise 5.6).

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§5.5–5.9, pp. 103–115. http://incompleteideas.net/book/the-book-2nd.html
• D. Precup, R. S. Sutton and S. Singh, Eligibility Traces for Off-Policy Policy Evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (cited in the book's bibliography).
• D. Precup, R. S. Sutton and S. Dasgupta, Off-Policy Temporal-Difference Learning with Function Approximation, Proceedings of the 18th International Conference on Machine Learning (ICML), 2001, pp. 417–424 (cited in the book, p. 105).

Motivation

Policy iteration alternates two steps: evaluate the current policy, then replace it by a policy that is greedy with respect to the evaluated action values. The policy improvement theorem guarantees that each greedy step does not make the policy worse, and that the process stops only at an optimal policy. When the action values are estimated from experience rather than computed from a model, as in Monte Carlo control, a greedy policy is a problem: it never tries the actions it does not currently prefer, so their values are never re-estimated. Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), §5.4, resolve this without the unrealistic assumption of exploring starts by moving the policy only toward a greedy one, to an ε-greedy policy that keeps every action's probability at least ε/|A|.

The question this mission formalizes is whether policy iteration still works under that restriction. The book's answer (pp. 101–102) is yes, in a precise sense: an ε-greedy step never makes an ε-soft policy worse, and it fails to make it strictly better only when the policy is already the best among all ε-soft policies. This is the dynamic-programming fact that justifies on-policy first-visit Monte Carlo control for ε-soft policies, and more broadly every ε-greedy on-policy control scheme that is analysed with exact action values.

Setting

A finite Markov decision process has a finite state set S, a finite nonempty action set A used in every state, a finite reward set R ⊂ ℝ and dynamics p(s′, r | s, a) ≥ 0 with $\sum_{s', r} p(s', r \mid s, a) = 1$. A policy π gives, for each state s, a probability distribution π(· | s) on A. With a discount rate $0 \le \gamma < 1$, the state value $v_\pi(s)$ is the expected discounted return $\mathbb E_\pi[\sum_{k \ge 0} \gamma^k R_{t+k+1} \mid S_t = s]$, and the action value is

$$q_\pi(s, a) = \sum_{s', r} p(s', r \mid s, a)\,[r + \gamma v_\pi(s')].$$

For ε > 0, a policy is ε-soft if $\pi(a \mid s) \ge \varepsilon/|A|$ for all s and a. A policy π′ is ε-greedy with respect to $q_\pi$ if at each state some maximizer $A^*(s)$ of $q_\pi(s, \cdot)$ receives probability $1 - \varepsilon + \varepsilon/|A|$ and every other action receives $\varepsilon/|A|$; ties among maximizers are broken arbitrarily. A policy π is optimal among the ε-soft policies if it is ε-soft and $v_{\pi''}(s) \le v_\pi(s)$ for every ε-soft π″ and every state s.

The book's analysis uses a new environment with the same states, actions and rewards, in which with probability 1 − ε the chosen action is executed and with probability ε a uniformly random action replaces it:

$$\tilde p(s', r \mid s, a) = (1 - \varepsilon)\, p(s', r \mid s, a) + \sum_{a'} \frac{\varepsilon}{|A|}\, p(s', r \mid s, a').$$

Its optimal value function is written $\tilde v_*$.

Formalization targets

Goal: ε-greedy improvement with the equality case

For $0 \le \gamma < 1$, $0 < \varepsilon \le 1$, an ε-soft policy π and any ε-greedy policy π′ with respect to $q_\pi$,

$$v_{\pi'}(s) \ge v_\pi(s) \quad \text{for all } s, \qquad \text{and} \qquad v_{\pi'} = v_\pi \;\Longrightarrow\; \pi, \pi' \text{ are optimal among the ε-soft policies}.$$

The goal is stated in terms of the original MDP and ε-soft policies only; the new environment appears only in the milestones.

Milestones

1. Policy improvement theorem for stochastic policies (4.7)–(4.8), p. 78: $\sum_a \pi'(a \mid s) q_\pi(s, a) \ge v_\pi(s)$ for all s implies $v_{\pi'} \ge v_\pi$, strictly at every state where the hypothesis is strict.
2. Eq. (5.2), pp. 101–102: $\sum_a \pi'(a \mid s) q_\pi(s, a) = \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a) + (1-\varepsilon)\max_a q_\pi(s, a) \ge v_\pi(s)$.
3. Characterization, p. 102: an ε-soft π is optimal among ε-soft policies if and only if $v_\pi = \tilde v_*$.
4. Uniqueness, p. 102: $\tilde v_*$ is the unique solution of the Bellman optimality equation with the altered transition probabilities $\tilde p$, and that equation splits as $(1-\varepsilon)\max_a(\cdot) + \frac{\varepsilon}{|A|}\sum_a(\cdot)$.
5. Fixed-point equation, p. 102: if $v_{\pi'} = v_\pi$, then $v_\pi(s) = (1-\varepsilon)\max_a q_\pi(s, a) + \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a)$.

Significance

The result is what makes ε-greedy on-policy control a form of generalized policy iteration: monotone improvement at every step, and a characterization of where the process can stop. It also locates precisely what is lost by exploring, namely that the fixed point is optimal among ε-soft policies, not among all policies. The value $\tilde v_*$ of the new environment is the benchmark against which ε-greedy methods converge when action values are exact.

The book presents the argument informally and states the stochastic policy improvement theorem without proof ("we will not go through the details", p. 79). A formalization supplies the missing proof of the stochastic case, the identification of the best ε-soft policy value with the optimal value of a modified MDP, and the uniqueness of that value. As far as a search of the platform shows, no statement about ε-soft or ε-greedy policies has been formalized there; existing finite-MDP results (Bellman optimality in the Foundations of Machine Learning and Bertsekas series) use different reward models and do not cover the modified environment.

Difficulty

The improvement half follows from (5.2) and the policy improvement theorem, but both need work in the return-based model: the theorem requires comparing infinite discounted sums under two different Markov chains, and (5.2) uses the identity $v_\pi(s) = \sum_a \pi(a \mid s) q_\pi(s, a)$, which is a theorem about returns, not a definition. The equality half is where the obvious argument fails. The deterministic-policy argument of Chapter 4 shows that an unimproved greedy policy satisfies the ordinary Bellman optimality equation; here the unimproved policy satisfies a different equation, and nothing in the original MDP identifies its solution with the best ε-soft value. That identification needs two further facts: every policy of the new environment corresponds to an ε-soft policy of the original one with the same values, and conversely (at ε = 1 only the uniform policy is ε-soft); and the altered optimality equation has exactly one solution.

Formalization scope

Everything is stated in the namespace SuttonBartoRL.EpsSoft on a finite MDP with four-argument dynamics, one finite nonempty action set for all states (so $|A(s)| = |A|$, the book's footnote 3, p. 48), and a finite reward set. The conventions are:

• $v_\pi$ is defined from expected discounted returns as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ with $0 \le \gamma < 1$; Bellman equations are theorems, never definitions. $q_\pi$ is the one-step lookahead (4.6) on this $v_\pi$.
• $\tilde v_*$ is the supremum of the new environment's policy values over all stochastic policies, a bounded family for $\gamma < 1$.
• ε ranges over (0, 1]: the book requires ε > 0, and for ε > 1 no ε-soft policy exists. The equality in (5.2) is stated without the book's intermediate division by 1 − ε, so the case ε = 1 is included.
• "Any ε-greedy policy" is encoded by quantifying over every choice of maximizer at every state.
• "Optimal among ε-soft policies" means ε-soft and pointwise at least as good as every ε-soft policy.

Defining $v_\pi$ as the solution of the Bellman expectation equation, or $\tilde v_*$ as the solution of the altered optimality equation, would make milestones 3–5 and the goal's equality half hold by definition; the formalization does neither. The goal is not the statement "$v_{\pi'} \ge v_\pi$" alone: the equality case is part of the book's claim and part of the goal.

The finite-MDP definitions duplicate those of other missions in this series and are expected to be merged later. Useful contributions include the Neumann-series identity $v_\pi = (I - \gamma P_\pi)^{-1} r_\pi$, the Bellman expectation equation, the contraction property of Bellman operators, and the correspondence between policies of the new environment and ε-soft policies of the original one; these are reusable for the other finite-MDP missions of the series.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §4.2 (pp. 76–79) and §5.4 (pp. 100–103). http://incompleteideas.net/book/the-book-2nd.html
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (policy iteration).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, doi:10.1002/9780470316887.

Motivation

Policy gradient methods learn a parameterized policy $\pi(a \mid s, \theta)$ directly, by stochastic gradient ascent on a scalar performance measure $J(\theta)$, instead of deriving the policy from learned action values. They are how reinforcement learning handles continuous action spaces, stochastic optimal policies and prior knowledge built into the policy's form, and they underlie REINFORCE (Williams, 1992) and the actor–critic family. Every such method needs an estimate of $\nabla J(\theta)$. The difficulty is that $J$ depends on $\theta$ in two ways: through the action choices in each state, and through the distribution of states those choices produce. The second effect depends on the unknown environment dynamics.

The policy gradient theorem (Sutton, McAllester, Singh and Mansour, 2000; Marbach and Tsitsiklis, 2001) gives $\nabla J(\theta)$ as an expectation over the on-policy state distribution that involves no derivative of that distribution. Chapter 13 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) states it as Eq. (13.5), proves it in a box for the episodic case (p. 325) and in a second box for the continuing case (pp. 334–335), and builds REINFORCE, REINFORCE with baseline and actor–critic methods on it. This mission formalizes that chapter's theorem and the identities around it, in the book's own model.

Setting

A finite episodic MDP has a finite set $\mathcal S$ of nonterminal states, a terminal state, a finite action set $\mathcal A$, a finite reward set $\mathcal R \subset \mathbb R$ and dynamics $p(s', r \mid s, a)$: for each nonterminal $s$ and action $a$, a probability distribution over next state $s' \in \mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$ and reward $r$. The terminal state is absorbing and pays nothing. Write $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ and $r(s, a)$ for the expected reward.

A differentiable policy parameterization assigns to every $\theta \in \mathbb R^{d'}$ and state $s$ a distribution $\pi(\cdot \mid s, \theta)$ over actions, with $\theta \mapsto \pi(a \mid s, \theta)$ differentiable. Under $\pi_\theta$ the nonterminal states form a substochastic chain with matrix $P_\theta(s, s') = \sum_a \pi(a \mid s, \theta) p(s' \mid s, a)$; $\Pr(s \to x, k, \pi) = P_\theta^k(s, x)$. Episodes terminate when $\sum_{k} P_\theta^k(s, s') < \infty$ for all $s, s'$.

There is no discounting ($\gamma = 1$, p. 324). The state value $v_{\pi}(s) = \sum_{k \ge 0} (P_\theta^k r_\theta)(s)$ is the expected total reward from $s$, with $r_\theta(s) = \sum_a \pi(a\mid s,\theta) r(s,a)$; the action value $q_\pi(s,a)$ is the expected total reward after taking $a$ in $s$. The episode starts in a fixed state $s_0$, and the performance is $J(\theta) = v_{\pi_\theta}(s_0)$ (13.4). The expected number of visits to $s$ in an episode is $\eta(s) = \sum_{k \ge 0} \Pr(s_0 \to s, k, \pi)$, and the on-policy distribution is $\mu(s) = \eta(s) / \sum_{s'} \eta(s')$ (9.3).

In the continuing case there is no terminal state, $J(\theta) = r(\pi)$ is the average reward per step (13.15), $\mu$ is the steady-state distribution, and $v_\pi$, $q_\pi$ are differential values, defined from the return $\sum_k (R_{t+k+1} - r(\pi))$ (13.17).

Formalization targets

Goal: the policy gradient theorem, episodic case (13.5)

If episodes terminate under $\pi_{\theta_0}$, then $J$ is differentiable at $\theta_0$ and

$$\nabla J(\theta_0) = \sum_s \eta(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0) = \Big(\sum_{s'} \eta(s')\Big) \sum_s \mu(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0),$$

with $\sum_{s'} \eta(s') \ge 1$. The book writes $\nabla J(\theta) \propto \sum_s \mu(s) \sum_a q_\pi(s,a) \nabla \pi(a \mid s,\theta)$ and names the constant, the average length of an episode, in words (p. 326). The goal states it.

Milestones

1. Exercises 3.18–3.19 with $\gamma = 1$: $v_\pi(s) = \sum_a \pi(a\mid s) q_\pi(s,a)$ and $q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)(r + v_\pi(s'))$.
2. The recursion $\nabla v_\pi(s) = \sum_a [\nabla\pi(a\mid s) q_\pi(s,a) + \pi(a\mid s) \sum_{s'} p(s'\mid s,a) \nabla v_\pi(s')]$, including the differentiability of $v_\pi$.
3. The unrolled gradient $\nabla v_\pi(s) = \sum_{x} \sum_{k=0}^\infty \Pr(s \to x, k, \pi) \sum_a \nabla\pi(a\mid x) q_\pi(x,a)$ for every $s$.
4. The theorem with a baseline (13.10): $\sum_a b(s) \nabla \pi(a\mid s,\theta) = 0$, hence $q_\pi$ may be replaced by $q_\pi - b$.
5. The log form behind REINFORCE: where $\pi(\cdot\mid s,\theta) > 0$, $\sum_a q_\pi(s,a) \nabla\pi(a\mid s,\theta) = \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$, and hence $\nabla J(\theta) = (\sum_{s'}\eta(s')) \sum_s \mu(s) \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$, the exact form of $\nabla J \propto \mathbb E_\pi[q_\pi(S_t,A_t) \nabla\pi(A_t\mid S_t,\theta)/\pi(A_t\mid S_t,\theta)]$.
6. Exercise 13.3, (13.9): for the linear soft-max, $\nabla \ln \pi(a\mid s,\theta) = x(s,a) - \sum_b \pi(b\mid s,\theta) x(s,b)$.
7. Exercise 13.4: the eligibility vectors of the Gaussian policy (13.19)–(13.20).
8. The continuing case: under ergodicity, $\nabla r(\pi_\theta) = \sum_s \mu(s) \sum_a \nabla\pi(a\mid s,\theta) q_\pi(s,a)$ with differential $q_\pi$.

Significance

The theorem turns $\nabla J$ into a quantity that can be sampled by following the policy: weighting states by $\mu$ is what visiting them under $\pi$ does, and the log form makes the action sum an expectation over $A_t \sim \pi$. REINFORCE (13.8), REINFORCE with baseline (13.11) and one-step and eligibility-trace actor–critic methods all rest on it, and so does their claim that the expected update is in the direction of the performance gradient (p. 329). The baseline identity is why a learned state value can reduce variance without introducing bias.

The results are proved, in the book and in the literature. What this mission adds is a machine-checked version in the book's model: random episode lengths with $\gamma = 1$, vector parameters $\theta \in \mathbb R^{d'}$, four-argument dynamics, and values defined from expected returns. The platform already has a proved finite-horizon policy gradient theorem (policy_gradient_finite_horizon, with a baseline and log-form companion) for a fixed horizon $T$, a scalar parameter $\theta \in \mathbb R$ and an expected-reward kernel; it does not cover the book's statement. The mission also makes explicit two points the text leaves informal: that episodes terminate, and what exact constant hides behind "$\propto$".

Difficulty

The book's proof is a formal manipulation: differentiate the Bellman equation, substitute it into itself, and "unroll" infinitely often. Two steps are not justified on the page. First, it presupposes that $\nabla v_\pi(s)$ exists; with $\gamma = 1$ the value is an infinite series whose convergence depends on $\theta$ through termination, so differentiability of $v_\pi$ at $\theta_0$ has to be established, and termination is assumed only at $\theta_0$. Second, "repeated unrolling" is a limit: after $n$ unrollings a remainder $\sum_x P_\theta^{n}(s,x) \nabla v_\pi(x)$ is left over, and it vanishes only because $P_\theta^n \to 0$. Differentiating the series for $v_\pi$ term by term is not an alternative shortcut without a uniform bound on the derivatives of $P_\theta^k$.

In the continuing case the corresponding obstacle is the differentiability of the steady-state distribution and of the differential values, which the book's proof uses without comment; here they are part of what is to be proved, from ergodicity at $\theta_0$ alone.

Formalization scope

• Model. $\mathcal S^+$ is Option S, with none the single terminal state (several terminal states can be merged, all having value 0). One action type for all states. $\theta$ lives in EuclideanSpace ℝ (Fin d), and $\nabla$ is Mathlib's gradient; conclusions are HasGradientAt, so differentiability is asserted, not assumed.
• Values from returns. $v_\pi$, $q_\pi$, $\eta$ are series in powers of $P_\theta$; Bellman equations are theorems (milestone 1). The continuing-case average reward and steady-state distribution are the limits of (13.15), and the differential values are the series of (13.17).
• Implicit hypotheses made explicit. Termination under $\pi_{\theta_0}$ is a hypothesis of every episodic result that involves values; the continuing case assumes the book's ergodicity (the limit of $\Pr\{S_t = s'\}$ exists and does not depend on $S_0$) at $\theta_0$. The positivity of $\pi(a \mid s,\theta_0)$ is assumed where a logarithm is differentiated.
• "∝". The episodic goal states the exact equality with the constant $\sum_{s'} \eta(s')$ and proves it is at least 1. A formalization of the form "$\exists c,\ \nabla J = c \cdot \ldots$" is ruled out: it holds with $c = 0$ and loses the book's constant.
• Fixed start state. $s_0$ is a fixed state, as in the book (p. 324); no start distribution.
• Not included. Convergence of REINFORCE or actor–critic under stochastic-approximation conditions (p. 329) rests on unstated conditions and is not an item. The baseline is a deterministic function of the state, not the random variable the book also allows.

Reusable infrastructure: the episodic value layer (substochastic chains, expected visits, termination) is needed by any undiscounted episodic RL result; the soft-max and Gaussian eligibility computations are needed by every policy-gradient algorithm. Proofs of any milestone, and general lemmas on the differentiability of values and stationary distributions of parameterized finite Markov chains, are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 13. http://incompleteideas.net/book/the-book-2nd.html
• R. S. Sutton, D. McAllester, S. Singh and Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
• P. Marbach and J. N. Tsitsiklis, Simulation-Based Optimization of Markov Reward Processes, IEEE Transactions on Automatic Control 46(2), 2001. https://doi.org/10.1109/9.905687
• R. J. Williams, Simple Statistical Gradient-Following Algorithms for Connectionist Reinforcement Learning, Machine Learning 8, 1992. https://doi.org/10.1007/BF00992696

Motivation

Eligibility traces are one of the basic mechanisms of reinforcement learning. A trace is a short-term memory vector $z_t$ with one component per weight. It records which components contributed to recent value estimates, so that an error observed now can be credited to the right components without storing the past. Chapter 12 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) organizes the topic around two ways of describing an algorithm. A forward view updates each state toward a target built from rewards that arrive later. A backward view makes an update at every step from the current error and the trace.

The chapter proves one exact equivalence between the two views itself, in §12.6: "This is the only equivalence of forward- and backward-views that we explicitly demonstrate in this book" (p. 301). The setting is linear Monte Carlo prediction, and the backward view uses a dutch trace. The same trace appears in true online TD($\lambda$), whose exact equivalence to the online $\lambda$-return algorithm (van Seijen and Sutton, 2014; van Seijen et al., 2016) the book cites without proof. Of that proof, §12.6 "gives some of the flavor ... but is much simpler" (p. 301).

The older equivalence of §§12.1–12.2 goes back to Sutton (1988). If the weights are held fixed during an episode, the summed updates of TD($\lambda$) with accumulating traces equal the summed updates of the off-line $\lambda$-return algorithm. The book leaves it as Exercises 12.3–12.4.

Setting

Fix a dimension $d$, a step size $\alpha$ and an episode of length $T \ge 1$ with feature vectors $x_0, \dots, x_{T-1} \in \mathbb R^d$. The episode ends with a single return $G \in \mathbb R$ ("a single reward received at the end of the episode ... and ... no discounting", p. 301). The forward view is the linear gradient Monte Carlo, or LMS, rule (12.13): from an initial $w_0$,

$$w_{t+1} = w_t + \alpha\,[G - w_t^\top x_t]\,x_t, \qquad 0 \le t < T .$$

Let $F_t = I - \alpha x_t x_t^\top$ be the fading matrix. The backward view keeps two vectors that are updated at each step in $O(d)$ time without knowledge of $G$. The dutch trace is $z_0 = x_0$, $z_t = z_{t-1} + (1 - \alpha z_{t-1}^\top x_t)\,x_t$. The auxiliary vector is $a_t = a_{t-1} - \alpha x_t x_t^\top a_{t-1}$, with $a_0 = F_0 w_0$.

For the second part, an episode $S_0, R_1, S_1, \dots, R_T, S_T$ carries states and rewards, and $\hat v(s, w)$ is a differentiable value function with $\hat v(\text{terminal}, \cdot) = 0$. For one fixed weight vector $w$, define the following, with $\gamma \in [0,1]$ and $\lambda \in [0,1)$:

• the return $G_t$;
• the $n$-step return $G_{t:t+n}$ (12.1), with $G_{t:t+n} = G_t$ once $t + n \ge T$;
• the $\lambda$-return $G^\lambda_t = (1-\lambda)\sum_{n \ge 1}\lambda^{n-1} G_{t:t+n}$ (12.2);
• the TD error $\delta_t = R_{t+1} + \gamma\hat v(S_{t+1}, w) - \hat v(S_t, w)$ (12.6);
• the accumulating trace $z_{-1} = 0$, $z_t = \gamma\lambda z_{t-1} + \nabla\hat v(S_t, w)$ (12.5).

Formalization targets

Goal: the dutch-trace equivalence (12.14), corrected

$$w_T = a_{T-1} + \alpha G\, z_{T-1}.$$

The left side is the forward view after $T$ LMS updates. On the right, $a_{T-1}$ and $z_{T-1}$ are produced by the incremental recursions above. The goal is about the two algorithms, not only about the closed-form product identity.

Milestones on the goal's path (§12.6, p. 302)

1. $w_{t+1} = F_t w_t + \alpha G x_t$.
2. $w_T = F_{T-1}\cdots F_0 w_0 + \alpha G \sum_{k=0}^{T-1} F_{T-1}\cdots F_{k+1} x_k$, the first line of (12.14).
3. $z_t = \sum_{k=0}^{t} F_t \cdots F_{k+1} x_k$ for the dutch-trace recursion.
4. $a_t = F_t \cdots F_0 w_0$ for the auxiliary-vector recursion (corrected initialization).

Milestones on the $\lambda$-return (§§12.1–12.2)

5. (12.3): $G^\lambda_t = (1-\lambda)\sum_{n=1}^{T-t-1}\lambda^{n-1}G_{t:t+n} + \lambda^{T-t-1}G_t$ for $t < T$.
6. Exercise 12.1: $G^\lambda_t = R_{t+1} + \gamma[(1-\lambda)\hat v(S_{t+1}, w) + \lambda G^\lambda_{t+1}]$.
7. Exercise 12.3: $G^\lambda_t - \hat v(S_t, w) = \sum_{k=t}^{T-1}(\gamma\lambda)^{k-t}\delta_k$.
8. Exercise 12.4: $\sum_{t<T}\alpha\delta_t z_t = \sum_{t<T}\alpha[G^\lambda_t - \hat v(S_t, w)]\nabla\hat v(S_t, w)$.

Significance

The goal says that an $O(d)$-per-step algorithm reproduces the Monte Carlo/LMS result exactly. That algorithm never stores the feature vectors or the $T$ intermediate weight vectors. The book draws the conclusion that eligibility traces "are not specific to TD learning at all" (p. 303). The dutch trace in the case $\gamma\lambda = 1$ is the same object that true online TD($\lambda$) (12.11) uses for general $\gamma\lambda$. The fading-matrix products and their incremental forms are therefore the vocabulary of any later formalization of true online TD($\lambda$) and of the online $\lambda$-return algorithm.

Exercises 12.3–12.4 are the fixed-weight equivalence of TD($\lambda$) and the off-line $\lambda$-return algorithm. They are the standard justification for calling TD($\lambda$) an approximation of the $\lambda$-return algorithm. Exercise 12.1 and (12.3) are the identities the rest of the chapter uses to manipulate $\lambda$-returns.

On status: all of these results are known and elementary on paper, and the book prints the derivation of (12.14). To our knowledge none of them has a machine-checked proof, and the platform has no statement about $\lambda$-returns, eligibility traces or TD($\lambda$). What this mission adds is formal statements with every convention fixed, including one correction to the printed text. It also adds reusable definitions of $n$-step returns, $\lambda$-returns and traces.

Difficulty

The algebra is elementary. The difficulty lies in the conventions, and a careless reading of the page produces a false statement. The book initializes $a_0 = w_0$, and taken literally that makes the goal false. The $\lambda$-return is an infinite series, whose tail collapses only because every $n$-step return that reaches past termination equals the full return. That convention has to be built into the definition of $G_{t:t+n}$, together with the terminal value $\hat v(\text{terminal}, \cdot) = 0$. Exercises 12.3 and 12.4 are true only when the weights stay fixed. With the algorithms' changing weights $w_t$ the $n$-step returns (12.1) use $w_{t+n-1}$, and neither identity holds. The boundary indices ($t = T-1$, the empty product at $k = T-1$, $G^\lambda_T = 0$) must come out right.

Formalization scope

Namespace SuttonBartoRL.Traces. Vectors of §12.6 are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $x x^\top$ is Matrix.vecMulVec x x. The ordered product fadeProd α x j t is $F_t \cdots F_j$, the identity when $t < j$. Feature sequences are indexed by $\mathbb N$; only $x_0, \dots, x_{T-1}$ enter. $T \ge 1$ is a hypothesis wherever $T - 1$ appears. The identities of §12.6 are stated for every real $\alpha$ and $G$, a harmless strengthening of the book's positive step size.

For §§12.1–12.2, weights are EuclideanSpace ℝ (Fin d), $\nabla$ is Mathlib's gradient, and each $\hat v(s,\cdot)$ is assumed differentiable in Exercise 12.4. An episode is a length $T$, states and rewards. The value at time $t \ge T$ is $0$. (12.2) is a tsum over $n \ge 0$ of $\lambda^n G_{t:t+n+1}$, and $\lambda \in [0,1)$, the range the book gives with (12.2). Milestone 5 concludes summability, so the junk value of a divergent tsum cannot make it trivial. Exercises 12.3–12.4 take one weight binder w, used in every return, TD error and gradient. That is the book's fixed-$w$ assumption, stated in the binders.

Correction. The printed initialization $a_0 = w_0$ (p. 302) contradicts the printed definition $a_t \doteq F_t\cdots F_0 w_0$ and (12.14). The counterexample is $d = 1$, $T = 1$, $x_0 = 1$, $\alpha = 1/2$, $w_0 = 1$, $G = 0$: the forward view gives $w_1 = 1/2$, while $a_0 + \alpha G z_0 = 1$. The mission states the corrected result with $a_0 = F_0 w_0$, equivalently the same recursion started from $a_{-1} = w_0$. The printed text is kept verbatim in the milestone.

A trivializing formalization is ruled out: the goal is not the closed-form identity with $a_{T-1}$ and $z_{T-1}$ defined as the products and sums. Those vectors are defined by their $G$-free incremental recursions, and the closed forms are separate milestones.

Out of scope: the equivalence of true online TD($\lambda$) and the online $\lambda$-return algorithm (cited, p. 300), the truncated-return identity (12.10), the error bound (12.8), and all convergence claims. Proofs of the milestones, and reuse of the definitions in later missions on true online TD($\lambda$), are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 12, pp. 287–320. http://incompleteideas.net/book/the-book-2nd.html
• R. S. Sutton, "Learning to predict by the methods of temporal differences", Machine Learning 3 (1988), 9–44. https://doi.org/10.1007/BF00115009
• H. van Seijen and R. S. Sutton, "True online TD(λ)", Proceedings of ICML 2014, PMLR 32, 692–700. https://proceedings.mlr.press/v32/seijen14.html
• H. van Seijen, A. R. Mahmood, P. M. Pilarski, M. C. Machado and R. S. Sutton, "True online temporal-difference learning", Journal of Machine Learning Research 17 (2016), 1–40. https://jmlr.org/papers/v17/15-599.html

Motivation

Temporal-difference (TD) learning estimates the value of a policy by moving a current estimate toward a target built from observed rewards and from the estimate itself. Chapter 7 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) interpolates between the two extreme targets of the preceding chapters: the one-step TD target, which uses one reward and then bootstraps, and the Monte Carlo target, which uses every reward until the end of the episode. The intermediate target, the $n$-step return, uses $n$ rewards and then bootstraps from the current estimate. The family underlies $n$-step TD, $n$-step Sarsa, the off-policy per-decision methods and the tree-backup algorithm, and it is the introduction to eligibility traces (Chapter 12).

The book justifies the whole family with one inequality, the error reduction property (7.3), p. 144: the expected $n$-step return is closer to the true value than the estimate it bootstraps from, by a factor $\gamma^n$ in the worst state. It is the reason given for calling $n$-step TD methods "sound". The same chapter states, mostly as exercises without solutions, a series of exact identities that rewrite each kind of $n$-step return as a sum of one-step TD errors.

Setting

A finite Markov decision process has finite state and action sets $\mathcal S$, $\mathcal A$, a finite reward set $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$, the probability of next state $s'$ and reward $r$ after action $a$ in state $s$ (Eqs. (3.2)–(3.3)). A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. Following $\pi$ from $S_t = s$ produces a random trajectory $A_t, R_{t+1}, S_{t+1}, A_{t+1}, R_{t+2}, \dots$ For a discount factor $0 \le \gamma < 1$ the state-value function is the expected discounted return (3.12),

$$v_\pi(s) = \mathbb E_\pi\Big[\sum_{k=0}^{\infty} \gamma^k R_{t+k+1} \,\Big|\, S_t = s\Big].$$

Given any function $V : \mathcal S \to \mathbb R$ (an estimate of $v_\pi$), the $n$-step return (7.1) is

$$G_{t:t+n} = R_{t+1} + \gamma R_{t+2} + \cdots + \gamma^{n-1} R_{t+n} + \gamma^n V(S_{t+n}).$$

In an episode that terminates at time $T$ it is replaced by the complete return $G_t$ when $t + n \ge T$. The TD error (6.5) is $\delta_k = R_{k+1} + \gamma V(S_{k+1}) - V(S_k)$. Off-policy variants use a behavior policy $b$ that generates the data, the per-decision ratio $\rho_t = \pi(A_t \mid S_t)/b(A_t \mid S_t)$, and the return with control variate (7.13), $G_{t:h} = \rho_t(R_{t+1} + \gamma G_{t+1:h}) + (1-\rho_t) V(S_t)$, $G_{h:h} = V(S_h)$. The tree-backup return (7.15)–(7.16) uses action values $Q$ and the expected approximate value $\bar V(s) = \sum_a \pi(a \mid s) Q(s, a)$ (7.8).

Formalization targets

Goal: the error reduction property (7.3)

For a finite MDP, a policy $\pi$, $0 \le \gamma < 1$, any $V : \mathcal S \to \mathbb R$ and every $n \ge 1$,

$$\max_s \big|\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s)\big| \le \gamma^n \max_s \big|V(s) - v_\pi(s)\big|.$$

Milestones, in the book's order

1. Exercise 7.1, p. 143: with $V$ fixed and $V(S_T) = 0$, $G_{t:t+n} - V(S_t) = \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}\delta_k$.
2. Exercise 7.4, Eq. (7.6), p. 148: the $n$-step Sarsa return equals $Q_{t-1}(S_t, A_t) + \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}[R_{k+1} + \gamma Q_k(S_{k+1}, A_{k+1}) - Q_{k-1}(S_k, A_k)]$, with estimates changing from step to step.
3. Eq. (7.12), p. 150: $G_{t:h} = R_{t+1} + \gamma G_{t+1:h}$ for $t < h < T$, $G_{h:h} = V(S_h)$.
4. Exercise 7.6, p. 151, for (7.13): under coverage, $\mathbb E_b$ of the control-variate return equals $\mathbb E_b$ of the same return without the control variate, and both equal $\mathbb E_\pi[G_{t:t+n} \mid S_t = s]$.
5. Exercise 7.8, p. 151: $G_{t:h} - V(S_t) = \sum_{k=t}^{h-1} \gamma^{k-t} \big(\prod_{i=t}^{k}\rho_i\big) \delta_k$ for the return (7.13).
6. Exercise 7.11, p. 153: the tree-backup return equals $Q(S_t, A_t) + \sum_{k=t}^{\min(t+n-1,T-1)} \delta_k \prod_{i=t+1}^{k} \gamma\pi(A_i \mid S_i)$ with the expectation-based TD error $\delta_k = R_{k+1} + \gamma\bar V(S_{k+1}) - Q(S_k, A_k)$.

Significance

The result. The error reduction property makes the expected $n$-step target a $\gamma^n$-contraction toward $v_\pi$ in the sup norm, uniformly over the estimate it starts from. It is the one-line reason the book offers for the soundness of every $n$-step TD method, and the same contraction is what the $\lambda$-return of Chapter 12 averages over $n$. The TD-error identities are the algebra behind implementations that accumulate TD errors instead of storing returns, and behind the forward/backward-view equivalences of Chapter 12. Exercise 7.6 is the unbiasedness of the control-variate return, which is what allows (7.13) to replace plain importance weighting without changing the expected update.

Formalizing it. All results are elementary and well known, but the book gives no proofs: (7.3) is asserted, and the identities are exercises without published solutions. None is formalized on Prove2Me. The mission produces machine-checked versions with every hypothesis explicit (discounting, the fixed estimate, terminal values, coverage), and a trajectory-level expectation for finite MDPs that other chapters of the series can reuse.

Difficulty

The obvious proof of (7.3) is a matrix computation: $\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s) = \gamma^n (P_\pi^n (V - v_\pi))(s)$, and a stochastic matrix does not increase the sup norm. The difficulty lies in the step before it. The left side is an expectation over trajectories, and $v_\pi$ is an infinite discounted series; neither is a matrix power by definition. Connecting them requires a Chapman–Kolmogorov identity for the finite-trajectory distribution induced by $\pi$ and $p(s', r \mid s, a)$, the splitting of $v_\pi$ at time $n$, and summability of the discounted series. Defining the expected $n$-step return as the matrix expression would reduce the goal to the last line and remove its content; that shortcut is ruled out below.

The TD-error identities are telescoping sums, but each has its own boundary: termination inside the $n$ steps, the convention that terminal states have value zero, the index $Q_{-1}$ at $t = 0$ in (7.6), the special case $G_{T-1:t+n} = R_T$ of the tree backup, and ratios with vanishing denominators in (7.13).

Formalization scope

• Model. The finite MDP, policies and $v_\pi$ follow the series conventions: dynamics $p(s', r \mid s, a)$ over a finite reward set, one action set for all states, $v_\pi(s) = \sum_k \gamma^k (P_\pi^k r_\pi)(s)$ computed from expected rewards and never defined as a Bellman solution.
• Expectations are over trajectories. $\mathbb E_\pi[\,\cdot \mid S_t = s]$ is the finite sum over $n$-step segments $(A_{t+k}, S_{t+k+1}, R_{t+k+1})_{k<n}$ weighted by $\prod_k \pi(A_{t+k}\mid S_{t+k})\,p(S_{t+k+1}, R_{t+k+1}\mid S_{t+k}, A_{t+k})$. The expected $n$-step return is not defined as $\sum_{k<n}\gamma^k P_\pi^k r_\pi + \gamma^n P_\pi^n V$, which would make the goal a two-line matrix inequality.
• The estimate is fixed. In the algorithm, $V_{t+n-1}$ is the current random estimate. Every statement takes a fixed function $V$ (or $Q$), which is the book's own reading ("if the value estimates don't change"). The only exception is Exercise 7.4, whose estimates $Q_k$ are indexed by time $k \in \mathbb Z$ exactly as in (7.6).
• Discounting. The goal assumes $0 \le \gamma < 1$ and takes the maximum over all states. Episodic tasks enter through absorbing zero-reward terminal states. The undiscounted episodic case $\gamma = 1$ is not stated.
• Episodes. Sample-path identities use sequences $S_k, A_k, R_k$ and a termination time $T$. The book's convention that terminal states have value $0$ is a hypothesis ($V(S_T) = 0$, $Q(S_T, \cdot) = 0$).
• Exercise 7.6 is stated for the state-value return (7.13) of p. 150, although the exercise follows the action-value return (7.14). Its conclusion includes, besides the literal "does not change the expected value", equality with the on-policy expected return, the property the book states on p. 150. Coverage ($\pi(a\mid s) > 0 \Rightarrow b(a\mid s) > 0$) is assumed.
• Not stated. The convergence of $n$-step TD methods "under appropriate technical conditions" (p. 144), and the programming exercises.

Needed infrastructure: finite sums over function types, Chapman–Kolmogorov for the segment distribution, summability of $\sum_k \gamma^k P_\pi^k r_\pi$. The trajectory layer is reusable for the importance-sampling and eligibility-trace chapters. Alternative proofs of the goal, and proofs of the undiscounted episodic version as a separate theorem, are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 7, pp. 141–158. http://incompleteideas.net/book/the-book-2nd.html
• C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989 (the $n$-step return and its error reduction property, as credited on p. 158 of the book). https://www.cs.rhul.ac.uk/~chrisw/new_thesis.pdf
• D. Precup, R. S. Sutton and S. Singh, Eligibility traces for off-policy policy evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (the tree-backup algorithm, as credited on p. 158 of the book; no DOI).