Dynamic Programming

Motivation

Approximate dynamic programming replaces the exact value functions of a Markov decision process by approximations, typically produced by a regression algorithm. The classical guarantees for the resulting policies are stated in the max norm: if every state-action value is estimated to within $\varepsilon$ uniformly over the state space, the greedy policy loses at most a multiple of $\varepsilon$ (Williams and Baird 1993; Bertsekas and Tsitsiklis 1996). Regression algorithms, however, control an average error under the distribution on which they are trained, not a worst-case error, so these guarantees rarely apply to the approximations actually computed.

Chapter 5 of S. M. Kakade's PhD thesis (On the Sample Complexity of Reinforcement Learning, UCL 2003, pp. 57–66) identifies the distribution under which the error of an approximate policy iteration algorithm should be measured. For the finite-horizon, non-stationary approximate policy iteration algorithm (NAPI), the loss relative to any competitor policy is bounded by twice the horizon times the regression error averaged under the future state-time distribution of that competitor. Taking the competitor optimal, the relevant "test" distribution is the one visited by an optimal policy, generally not the distribution on which the regressor was trained; the thesis calls this the "mismeasure" of reinforcement learning. The key tool, the performance difference lemma, was proved for the discounted case by Kakade and Langford (ICML 2002) and is used throughout the conservative policy iteration and policy search literature.

Setting

A $T$-epoch MDP has a finite state set $S$, a finite nonempty action set $A$, decision epochs $t\in\{0,\dots,T-1\}$, a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$. A policy $\pi$ is a sequence of decision rules $\pi(\cdot\mid s,t)$, distributions on $A$; it may be stochastic and non-stationary. A deterministic policy $h$ chooses the action $h(s,t)$.

Values are normalized. The $t$-value is $V_{\pi,t}(s)=\frac1T\mathbb E\big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\mid s_t=s\big]$, so $V_{\pi,t}=0$ for $t\ge T$ and

$$V_{\pi,t}(s)=\sum_a\pi(a\mid s,t)\Big(\tfrac1T r(s,a)+\sum_{s'}P(s'\mid s,a)V_{\pi,t+1}(s')\Big),\qquad V_\pi=V_{\pi,0}.$$

The state-action value is $Q_{\pi,t}(s,a)=\frac1T r(s,a)+\mathbb E_{s'\sim P(\cdot\mid s,a)}V_{\pi,t+1}(s')$, the advantage is $A_{\pi,t}=Q_{\pi,t}-V_{\pi,t}$, and the optimal value is $V^*(s)=\sup_\pi V_\pi(s)$. The future state-time distribution of $\pi$ from $s_0$ is

$$d_{\pi,s_0}(s,t)=\tfrac1T\Pr(s_t=s\mid\pi,s_0)\quad\text{on } S\times\{0,\dots,T-1\}.$$

NAPI (Algorithm 6) starts from an arbitrary deterministic policy and updates its decision rules backwards, $t=T-1,\dots,0$: at update $t$ a PolicyChooser receives the current policy $\pi$ and returns a decision rule $h_t$, which replaces the rule at time $t$. The output is $(h_0,\dots,h_{T-1})$. With RegressionPolicyChooser (Algorithm 7), a regressor returns an approximation $\tilde Q_{\pi,t}$ of $Q_{\pi,t}$ and $h_t$ is greedy for it. The per state error and per state regression error at update $t$ are

$$\varepsilon_t(s)=\max_aQ_{\pi,t}(s,a)-Q_{\pi,t}(s,h_t(s)),\qquad \tilde\varepsilon_t(s)=\max_a|Q_{\pi,t}(s,a)-\tilde Q_{\pi,t}(s,a)|,$$

both measured against the input policy $\pi$ of update $t$.

The discounted companions use the normalized discounted value $V_{\pi,\gamma}=(1-\gamma)\mathbb E[\sum_t\gamma^tr(s_t,a_t)]$, its advantage $A_{\pi,\gamma}$, and the Bellman error $B_J=\sup_{s,a}|Q_J(s,a)-J(s)|$ of a state vector $J$, where $Q_J(s,a)=(1-\gamma)r(s,a)+\gamma\mathbb E_{s'}J(s')$.

Formalization targets

Goal: Theorem 5.3.2 (p. 64)

For the policy $\pi$ returned by NAPI with RegressionPolicyChooser, every policy $\pi'$ and every state $s_0$,

$$V_\pi(s_0)\ \ge\ V_{\pi'}(s_0)-2T\,\mathbb E_{(s,t)\sim d_{\pi',s_0}}\big[\tilde\varepsilon_t(s)\big].$$

The regression outputs are arbitrary; the statement holds for every regressor and every tie-breaking rule.

Milestones

• Lemma 5.2.1, undiscounted (p. 59): $V_{\pi'}(s_0)-V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi',s_0}}\mathbb E_{a\sim\pi'(\cdot\mid s,t)}[A_{\pi,t}(s,a)]$.
• Lemma 5.3.1 (p. 63): for NAPI's output $\tilde\pi$ and the input policy $\pi$ of update $t$, $Q_{\tilde\pi,t}=Q_{\pi,t}$ and $A_{\tilde\pi,t}(s,a)\le\varepsilon_t(s)$.
• Display in the proof of Theorem 5.3.2 (p. 64): $\varepsilon_t(s)\le2\tilde\varepsilon_t(s)$ when $h_t$ is greedy for $\tilde Q_{\pi,t}$.
• Corollary 5.2.2 (p. 61): $V_\pi(s_0)\ge V^*(s_0)-T\|A_{\pi,t}\|_\infty$ and $V_{\pi,\gamma}(s_0)\ge V^*_\gamma(s_0)-\frac{1}{1-\gamma}\|A_{\pi,\gamma}\|_\infty$.
• Theorem 5.1.3 (Williams–Baird, p. 59): a policy greedy for $Q_J$ satisfies $V_{\pi,\gamma}(s)\ge V^*_\gamma(s)-\frac{2B_J}{1-\gamma}$.

The discounted half of Lemma 5.2.1 is already on the platform as ApproxOptRL.CPI.performance_difference and is referenced, not restated.

Significance

The goal replaces a max-norm hypothesis by an average one, under an explicit distribution. Its consequences: the approximation error only matters on the state-time pairs an optimal (or any good) policy visits; a regressor trained under a distribution $\mu$ over state-times performs well when $\mu$ resembles the state-time distribution of a good policy; and only one factor of the horizon $T$ appears, against two factors of $1/(1-\gamma)$ in the max-norm bounds for discounted approximate value and policy iteration (Chapter 3 of the thesis). The same chain, Lemma 5.2.1 and Lemma 5.3.1, underlies the μ-policy search analysis of Chapter 6 and, in the discounted case, conservative policy iteration.

All statements are proved in the thesis; none of the finite-horizon ones is formalized on the platform. A related performance difference identity, FoundationsRL.RLBasics.performance_difference, is proved on the platform for episodic MDPs with layer-dependent kernels and unnormalized values, with roll-in by one policy; it is the same mathematics up to the $1/T$ normalization but a different object, and is not reused. The mission produces a reusable normalized $T$-epoch layer (values, advantages, state-time distributions) and machine-checked proofs of the chapter's results.

Difficulty

The obvious approach to Theorem 5.3.2 compares $V_\pi$ with $V_{\pi'}$ through max-norm contraction arguments, as in the discounted analysis of Chapter 3; that route only yields a bound in terms of $\max_{s,t}\tilde\varepsilon_t(s)$ and loses the averaging under $d_{\pi',s_0}$. The averaged bound needs an exact identity between value differences and advantages along the competitor's trajectory distribution, which for non-stationary stochastic competitors requires a careful telescoping over epochs of the state distribution recursion. The second difficulty is bookkeeping in the algorithm: the regression error at update $t$ is measured against the input policy of that update, whose decision rules at later times have already been replaced, while the bound concerns the returned policy; relating the two requires showing that later updates do not change $Q_{\cdot,t}$.

Formalization scope

• Model. S, A are Fintypes with decidable equality, A nonempty; P s a s' is $P(s'\mid s,a)$ with IsTransitionKernel P; rewards satisfy 0 ≤ r s a ≤ 1 in every statement (the thesis's standing assumption, p. 22). The thesis also allows infinite state spaces; here S is finite.
• Epochs and normalization. Epochs are 0-based, $t\in\{0,\dots,T-1\}$, with 0 < T. All values carry the factor $1/T$ (discounted: $1-\gamma$), and $d_{\pi,s_0}$ carries $1/T$; the constants $T$ and $2T$ are right only in this normalization.
• Policies. A policy is ℕ → S → A → ℝ, valid when every rule at a time $t<T$ is a distribution. Deterministic policies ℕ → S → A enter through their indicator policies. $V^*$ is the supremum over the subtype of valid policies. Discounted statements use the published ApproxOptRL.Shared.Model; $V^*_\gamma$ is the value of an optimal stationary policy.
• The NAPI run is an explicit recursion (napiPolicy): the policy after updates $T-1,\dots,t$, so the input of update $t$ is the policy at stage $t+1$ and the output is the policy at stage $0$. The printed loop "For $t=T-1,\dots,1$" omits the update at $t=0$, which would leave the time-0 rule random and make the theorem false; the loop here runs to $t=0$, as in the proof and in Algorithms 8–9.
• Ruled out. A "run" whose returned policy is unconstrained, or regression errors measured against the returned policy instead of the input policy of each update, would trivialize or alter the goal; both are excluded by the explicit recursion. That the two measurements agree is Lemma 5.3.1, a milestone, not a definition.
• Maxima. Maxima over actions are Finset.sup'; $\|\cdot\|_\infty$ on state-action functions is Mathlib's sup norm on S → A → ℝ. $B_J$ is a single number, as printed in Definition 5.1.2.

Welcome contributions: proofs of the milestones, general lemmas about the $T$-epoch layer (values in $[0,1]$, normalization of $d_{\pi,s_0}$, the path-expectation form of $V_{\pi,t}$), and links to the platform's discounted performance difference results.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
• S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. J. Williams and L. C. Baird, Tight Performance Bounds on Greedy Policies Based on Imperfect Value Functions, Technical Report NU-CCS-93-14, Northeastern University, 1993.
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Policy iteration replaces the current policy by the greedy policy with respect to its state-action values. With exact values this improves the policy at every state. When the improvement step is only approximate, or is restricted to a class of policies, a greedy replacement can make the policy worse, and the resulting error bounds are stated in max norm over all states, a quantity that sampling cannot control in large state spaces.

Conservative policy iteration (CPI), introduced by Kakade and Langford (ICML 2002) and developed in Chapter 7 of Kakade's PhD thesis (UCL, 2003), takes a different route. Instead of switching to a new policy, it mixes the current policy with a small amount of a better one, and it measures progress by an average over states visited under the current policy rather than by a maximum over all states. The thesis proves that the exact form of the algorithm improves its objective at every step, halts after a number of updates polynomial in the horizon and the accuracy, and returns a policy whose average advantages against an entire policy class are small. The approach underlies later trust-region and conservative update methods in reinforcement learning.

Setting

A finite Markov decision process has a finite state set $S$, a finite action set $A$, transition probabilities $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$. A stationary policy $\pi$ chooses action $a$ in state $s$ with probability $\pi(a\mid s)$. For a discount factor $0\le\gamma<1$ the normalized value of $\pi$ is

$$V_\pi(s)=(1-\gamma)\,\mathbb E\Big[\sum_{t\ge0}\gamma^t r(s_t,a_t)\,\Big|\,\pi,\ s_0=s\Big],$$

which lies in $[0,1]$. The state-action value is $Q_\pi(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$. The horizon time is $H=1/(1-\gamma)$.

Fix a reset distribution $\mu$ on $S$. The value of $\mu$ is $V_\pi(\mu)=\mathbb E_{s\sim\mu}V_\pi(s)$. The discounted future state distribution is

$$d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,\ s_0\sim\mu),$$

and $d_{\pi,s_0}$ is the case where $\mu$ is the point mass at $s_0$. For another policy $h$:

• the advantage under a distribution $\nu$ is $A_\pi(\nu,h)=\mathbb E_{s\sim\nu}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$;
• the future state-action value is $\mathbb Q_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}Q_\pi(s,a)$;
• the future advantage is $\mathbb A_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$.

The conservative update with mixing weight $\alpha\in[0,1]$ is $\pi_{\rm new}=(1-\alpha)\pi+\alpha\pi'$.

Exact CPI (Algorithm 11) works with a class $\Pi$ of stationary policies and an accuracy $\varepsilon>0$. Starting from any stationary policy, it repeats three steps:

1. The ExactPolicyChooser returns $\pi'\in\arg\max_{h\in\Pi}\mathbb Q_\pi(\mu,h)$.
2. If $\mathbb A_\pi(\mu,\pi')>\varepsilon/H$, the algorithm sets $\alpha=\mathbb A_\pi(\mu,\pi')/(4H)$ and replaces $\pi$ by $(1-\alpha)\pi+\alpha\pi'$.
3. Otherwise it halts and returns $\pi$.

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

Every run $\pi_0,\pi_1,\dots$ of Exact CPI has a halting round $K$ with

$$K<\frac{8H^2}{\varepsilon^2},\qquad V_{\pi_{k+1}}(\mu)-V_{\pi_k}(\mu)>\frac{\varepsilon^2}{8H^2}\ \ (k<K),\qquad \mathbb A_{\pi_K}(\mu,h)\le\frac{\varepsilon}{H}\ \ (h\in\Pi).$$

The returned $\pi_K$ is a stationary policy. The thesis states the halting bound as $O(H^2/\varepsilon^2)$ calls to the chooser. The constant $8$ is the one the thesis's own Corollary 7.2.3 supplies, and the mission states it explicitly.

Milestones

1. Lemma 7.2.2. For every $\alpha\in[0,1]$, with $\epsilon_\infty=\max_s|\mathbb E_{a\sim\pi'(\cdot\mid s)}A_\pi(s,a)|$,

$$V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A_\pi(\mu,\pi')-\frac{2\gamma\alpha}{1-\gamma(1-\alpha)}\epsilon_\infty\Big).$$

2. Corollary 7.2.3. If $\mathbb A_\pi(\mu,\pi')\ge0$, the step $\alpha=\frac{1-\gamma}{4}\mathbb A_\pi(\mu,\pi')$ gives $V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\mathbb A_\pi(\mu,\pi')^2/8$.
3. Domination of the start distribution (p. 88): $d_{\pi,\mu}\ge\mu/H$.
4. Lemma 5.2.1, discounted half: $V_{\pi'}(s_0)-V_\pi(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d_{\pi',s_0}}\mathbb E_{a\sim\pi'(\cdot\mid s)}A_\pi(s,a)$.
5. Theorem 7.3.1. If $A_\pi(\nu,h)\le\varepsilon/H$ for all $h\in\Pi$, then for every $\pi'\in\Pi$ and every state $s_0$,

$$V_\pi(s_0)\ge V_{\pi'}(s_0)-\varepsilon-H\|d_{\pi',s_0}-\nu\|_1.$$

6. Example 7.4.1. A two-state MDP on which the bound of Lemma 7.2.2 holds with equality for all $\alpha$ and $\gamma$.

Milestones 1, 2 and 4 are already stated on the platform from Kakade–Langford (2002), in the same normalized model. They are included here as references and are not posed again.

Significance

The result. Theorem 7.3.2 is the exact-oracle core of CPI's sample-complexity analysis: the sample-based version later in the chapter replaces the exact chooser and the exact future advantage by estimates. The guarantee is stated through future advantages, so it does not depend on a max-norm accuracy over all states. Through Theorem 7.3.1 it translates into a value guarantee against every policy of the class whose future state distribution is close to the measure the algorithm was trained on. The output need not lie in $\Pi$: even for a deterministic class the returned policy is in general stochastic.

Formalizing it. All results here are proved in the thesis, and the three referenced statements are proved on the platform. None of the new statements has a machine-checked proof. The mission adds a fully specified Exact CPI run as a Lean object, an explicit constant in place of the $O(\cdot)$, and checked versions of the μ-optimality bound and of the tightness example. Its layer is shared with the Kakade–Langford missions, so later work on sample-based CPI can build on it directly.

Difficulty

The halting bound needs two ingredients that are easy to separate and easy to get wrong. The improvement guarantee of Corollary 7.2.3 holds only for a policy and a mixture weight in $[0,1]$, so every iterate of the run must be shown to remain a policy and every step size to stay in range. The count of updates then rests on the normalized values being bounded in $[0,1]$, a property of the model rather than of the algorithm. The output condition is stated for every $h\in\Pi$, while the algorithm only tests the one policy the chooser returned, and the chooser maximizes future state-action values rather than future advantages.

A tempting shortcut is the thesis's remark on p. 88 that $\mathbb A_\pi(\mu,h)\le\varepsilon/H$ implies $A_\pi(\mu,h)\le\varepsilon$. This is false in general: it would need $\mathbb E_{a\sim h}A_\pi(s,a)\ge0$ at every state. The mission formalizes only the true ingredient, $d_{\pi,\mu}\ge\mu/H$.

Formalization scope

The layer is the published normalized model ApproxOptRL.Shared.Model: value, qValue, advantage, futureStateDist, and eta for $V_\pi(\mu)$. The future advantage is ApproxOptRL.CPI.policyAdvantage and the conservative update is ApproxOptRL.CPI.mixPolicy. The model makes these commitments:

• $S$ and $A$ are finite nonempty types.
• Policies are maps $\pi:S\to A\to\mathbb R$ with IsPolicy, and deterministic policies are indicator policies.
• Values carry the factor $1-\gamma$, so all constants are the thesis's normalized ones. The thesis's statements for infinite state spaces are taken for finite $S$, where $\|\cdot\|_1$ is a finite sum.
• In Lean the policy class is called Pi because Π is reserved.

The run is the explicit predicate IsExactCPIRun: up to the round where the algorithm halts, the chooser output lies in $\Pi$ and maximizes $\mathbb Q_{\pi_k}(\mu,\cdot)$ over $\Pi$, and the update uses exactly $\alpha_k=\mathbb A/(4H)$. The halting round is part of the conclusion, never a hypothesis. A formalization in which the halting test or the step size is a free variable, or in which $\Pi$ is empty, would make "halts" an assumption or the run hypothesis unsatisfiable; the goal fixes both and requires $\Pi$ nonempty. The chooser's argmax is assumed to be attained, as in the thesis.

Contributions that would help: bounds $0\le V_\pi\le1$ and $|A_\pi|\le1$ for the normalized model, summability facts for futureStateDist, and a proof that a mixture of policies is a policy. These are reusable across every mission built on the same model.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003, Chapter 7. https://discovery.ucl.ac.uk/id/eprint/10100726/
• S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002, pp. 267–274. https://dl.acm.org/doi/10.5555/645531.656005

Motivation

Negative dynamic programming is the study of infinite-horizon sequential decision problems in which every one-stage reward is non-positive and nothing is discounted. Equivalently, a non-negative cost accumulates forever and the controller minimizes its expected total. Stochastic shortest-path problems, optimal stopping with a cost per step, and inventory or replacement models without discounting all have this form. The total cost of a policy can be infinite, and none of the contraction arguments of discounted dynamic programming apply.

Blackwell settled the discounted case on Borel state and action spaces (Blackwell 1965). There the optimal return is Borel measurable and is the unique bounded solution of the optimality equation. Strauch's paper (Strauch 1966) treats the negative case on the same Borel model. One of its main results is that the optimal return still satisfies the optimality equation, even though it need not be Borel measurable.

Timeline. Blackwell (1965): discounted case, Borel spaces. Blackwell (1967, Positive dynamic programming): positive bounded case. Strauch (1966): negative case on Borel spaces. The optimal return is absolutely measurable, $(p,\varepsilon)$-optimal Markov policies exist, and the optimality equation holds. Bertsekas and Shreve (1978, Stochastic Optimal Control: The Discrete-Time Case) later recast the theory with universally measurable policies, a lower semianalytic optimal cost, and Bellman's equation $J^* = T(J^*)$ under (P), (N) and (D).

Setting

The states $S$ and actions $A$ are non-empty Borel sets. A law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$. The return $r(s,a,t)$ is a Borel function with $-\infty < r \le 0$ whose expectation $\int r(s,a,t)\,dq(t\mid s,a)$ is finite for every $(s,a)$. A policy $\pi = (\pi_1,\pi_2,\dots)$ draws the $n$th action from a kernel $\pi_n(\cdot\mid s_1,a_1,\dots,s_n)$ that may depend on the whole history. A Markov policy $(f_1,f_2,\dots)$ uses measurable maps $f_n:S\to A$, and a stationary policy $f^{(\infty)}$ uses one map at every stage. The expected return from the initial state $s$ is

$$I(\pi)(s) = \sum_{n\ge1} E^\pi_s\, r(s_n,a_n,s_{n+1}) \in [-\infty,0],$$

and the optimal return is

$$v^*(s) = \sup_\pi I(\pi)(s),$$

the supremum over all policies. Write $M(S)$ for the non-positive, extended real-valued Borel functions on $S$. For $u\in M(S)$ and an action $a$,

$$T_a u(s) = \int \big[r(s,a,t) + u(t)\big]\,dq(t\mid s,a).$$

$T$ denotes the same operator for a measurable rule $f$ in place of $a$, and $U = \sup_n T_n$ for a Markov policy $(f_1,f_2,\dots)$. A policy $\pi^*$ is $(p,\varepsilon)$-optimal, for a probability $p$ on $S$, if $p\{I(\pi^*) \ge v^* - \varepsilon\} = 1$. The Lean development uses the same names: Problem, I, In, vstar, T, Ta, U, IsPEOptimal, Conserves.

Formalization targets

Goal: the optimality equation (Theorem 8.2, negative case)

$$v^*(s) = \sup_{a\in A} T_a v^*(s) \qquad\text{for all } s\in S.$$

The equation involves no constants and no regularity hypotheses on $v^*$.

Milestones

1. Theorem 5.2 (a)–(g): monotonicity, translation, sup-, limit- and selection properties of $U$.
2. Theorem 6.1: if $Uv\ge v$ for $v\in M(S)$, some Markov policy generated from $\hat\pi$ has $I(\pi)\ge v-\varepsilon$.
3. Lemma 6.2: $U$ conserves $\sup_n I({}^n\pi)$ and $\lim_n U^n \sup_n I({}^n\pi)$.
4. Theorem 6.2: one Markov policy comes within $\varepsilon$ of the supremum of the returns of countably many Markov policies.
5. Lemma 7.1, Lemma 7.2: measurability of $(s,\nu)\mapsto\int u(s,x)\,d\nu(x)$, and Borel measurability of the set of pairs $(s, e_\pi(s))$, where $e_\pi(s)$ is the law of the future under $\pi$.
6. Theorem 7.1: $v^*$ is absolutely measurable.
7. Theorem 8.1: for every $p$ and $\varepsilon>0$ a $(p,\varepsilon)$-optimal Markov policy exists.

Optional extras: Corollary 6.1 and Theorems 6.3, 6.4, 6.5 and 8.4 (bounds and characterizations for Markov policies).

Significance

The result. The optimality equation is the entry point to every structural statement about optimal policies in the negative case. With it, a stationary policy whose rule attains the supremum in $\sup_a T_a v^*$ can be tested for optimality. Value iteration and policy improvement can be compared with $v^*$. The gap between the negative case and the discounted and positive cases can be located precisely: in the negative case $v^*$ satisfies the equation, but it need not be its unique or extremal solution. Along the way the paper proves that $v^*$ is absolutely measurable and that nearly optimal Markov policies exist for every initial distribution. These two facts are used repeatedly in later Borel-space dynamic programming.

Formalizing it. The results are proved; none is machine-checked. A formal development would contain the first Lean treatment of a total-reward Markov decision process on Borel spaces with possibly infinite returns. It would include the policy-dependent law of the future via Ionescu-Tulcea, the measurability of the optimal return over all randomized history-dependent policies, and the Bellman equation for a non-measurable value function. Bertsekas–Shreve's version of the optimality equation (universally measurable policies) appears on the platform as a separate open statement. It concerns a different policy class and is not the statement posed here.

Difficulty

Two steps of the obvious argument fail. First, the classical proof of the optimality equation picks, at each next state $t$, a policy that is $\varepsilon$-optimal from $t$ and concatenates. Without measurable selection this concatenation is not a policy. The set of $t$ where a given policy is $\varepsilon$-optimal need not be Borel, and $v^*$ itself need not be Borel measurable, so even $\int v^*\,dq$ needs justification. Second, the contraction argument of the discounted case is unavailable. $U$ does not contract, it conserves $v+c$ along with $v$, and value iteration from $0$ can converge to a function strictly above $v^*$. The paper's Example 6.1 shows that the limit of $U^n0$, the best return of generated Markov policies, and the best stationary return can all differ. Any argument has to work with policies that are only nearly optimal, and only outside sets of measure zero that depend on the initial distribution.

Formalization scope

• States and actions are non-empty standard Borel types. Policies are the published Blackwell plans (DiscountedDP.Stationary.Plan): randomized and history-dependent, one Markov kernel per decision, with decisions numbered from $0$ (Lean's π.κ n is the paper's $\pi_{n+1}$). Markov policies are MarkovPlan; "$\pi$-generated" and $G(\hat\pi)$ are the published IsGenerated and IsGeneratedPlan.
• Only the negative case is formalized: $r\le0$ real-valued, $qr$ integrable, $\beta=1$. The discounted and positive parts of Theorems 5.2, 7.1, 8.1 and 8.2, including the uniqueness and minimality clauses of Theorem 8.2, are not stated.
• Returns take values in EReal and are computed as minus a lower Lebesgue integral (lintegral) of the non-negative loss. A Bochner integral is never used for a return: it would map $-\infty$ to $0$ and make the goal false or vacuous.
• $v^*$ is the supremum over all plans. It is not assumed measurable and is never replaced by a measurable modification. $T_a v^*$ is a lintegral of a possibly non-measurable function, which equals the completion integral because $v^*$ is absolutely measurable (Theorem 7.1).
• Explicit readings of the page: the hypothesis $u\in M(S)$ of each operator statement is IsNegM u. Theorem 5.2(b) assumes $u+c\in M(S)$. "$U$ conserves $v$" includes $v\in M(S)$. Lemma 6.2 asserts that the limit defining $v_\pi$ exists. Theorem 6.2 states $\ge$ everywhere and $>$ where $\sup_j I(\pi^j) > -\infty$ (the printed $>$ fails where the supremum is $-\infty$). $(p,\varepsilon)$-optimality is "$p$-almost everywhere". Absolute measurability is NullMeasurable for every probability measure. $P(X)$ carries the Giry σ-field. The extra Theorem 8.4 reads the printed "$I(\pi) < u$" as "$\le$" (the strict reading is false).
• Reusable infrastructure: the negative model, the Ionescu-Tulcea law of the future (futureLaw), and the measurability lemmas for integrals against random measures. Contributions of measurable-selection and analytic-set results (projections of Borel sets are universally measurable; von Neumann selection) are welcome and needed.

Selected references

• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• D. Blackwell, Positive Dynamic Programming, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
• L. E. Dubins and L. J. Savage, How to Gamble If You Must, McGraw-Hill, 1965.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

Temporal-difference learning, TD($\lambda$), is the basic algorithm of reinforcement learning for estimating the expected discounted cost of a Markov chain from observed transitions (Sutton, 1988). On large or infinite state spaces it is run with a linear function approximator: the cost-to-go is represented as a weighted sum of $K$ fixed basis functions, and the algorithm updates the weights. With a lookup table (one basis function per state) its convergence follows from general results on contraction mappings. With function approximation that argument breaks down. Before 1996 there were only results on convergence in the mean (Dayan, 1992), sketches restricted to linearly independent feature vectors $\phi(i)$, and counterexamples in which related algorithms diverge.

Tsitsiklis and Van Roy (MIT report LIDS-P-2322, 1996; IEEE Trans. Automatic Control 42(5), 1997) proved that on-line TD($\lambda$) with linear function approximation converges with probability 1 on finite or countably infinite ergodic chains. They identified the limit as the fixed point of a projected Bellman-type operator $\Pi T^{(\lambda)}$ and bounded its error. This analysis is the reference point for later results: finite-time bounds for linear TD, the off-policy divergence examples, and the gradient-TD family.

Timeline:

• 1988: Sutton introduces TD($\lambda$) and proves convergence in the mean for TD(0) on absorbing chains with linearly independent features.
• 1992: Dayan extends convergence in the mean to general $\lambda$.
• 1994: Jaakkola, Jordan and Singh, and Tsitsiklis, prove almost-sure convergence for lookup tables, using maximum-norm contraction.
• 1996: Tsitsiklis and Van Roy prove almost-sure convergence with linear function approximation and the error bound below.

Setting

A Markov chain $i_0, i_1, \dots$ lives on a finite or countably infinite state space $S$, with transition matrix $P = (p_{ij})$. A transition from $i$ to $j$ costs $g(i,j)$, and $\alpha \in (0,1)$ is a discount factor. The cost-to-go is

$$J^*(i) = E\Big[\sum_{t=0}^\infty \alpha^t g(i_t,i_{t+1}) \,\Big|\, i_0 = i\Big].$$

Basis functions $\phi_1,\dots,\phi_K : S \to \mathbb R$ give the feature vector $\phi(i) \in \mathbb R^K$ and the approximation $\tilde J(i,r) = r'\phi(i)$, written $\Phi' r$ as a vector over $S$.

Starting from an arbitrary $r_0$, TD($\lambda$) with $\lambda \in [0,1]$ and step sizes $\gamma_t$ forms the eligibility vector $z_t = \sum_{k=0}^t (\alpha\lambda)^{t-k}\phi(i_k)$ and the temporal difference $d_t = g(i_t,i_{t+1}) + \alpha\phi(i_{t+1})'r_t - \phi(i_t)'r_t$, and updates $r_{t+1} = r_t + \gamma_t d_t z_t$.

Let $\pi$ be the invariant distribution, $D = \mathrm{diag}(\pi)$, $\|J\|_D^2 = \sum_i \pi(i)J(i)^2$, and $L_2(S,D) = \{J : \|J\|_D < \infty\}$. Write $\Pi = \Phi'(\Phi D\Phi')^{-1}\Phi D$ for the $D$-orthogonal projection onto $\{\Phi'r\}$. The operator $T^{(\lambda)}$ averages $m$-stage truncated costs:

$$(T^{(\lambda)}J)(i) = (1-\lambda)\sum_{m=0}^\infty \lambda^m E\Big[\sum_{t=0}^m \alpha^t g(i_t,i_{t+1}) + \alpha^{m+1}J(i_{m+1}) \,\Big|\, i_0 = i\Big],$$

for $\lambda < 1$, and $T^{(1)}J = J^*$. The paper makes four assumptions:

1. the chain has a unique invariant distribution with $\pi(i) > 0$, $E_0[g^2] < \infty$, and finite $J^*$;
2. the $\phi_k$ are linearly independent with $E_0[\phi_k^2] < \infty$;
3. polynomial moment growth and summable mixing conditions, relative to coordinates $\sigma(i) \in \mathbb R^N$ of the states;
4. nonnegative, nonincreasing step sizes with $\sum\gamma_t = \infty$ and $\sum\gamma_t^2 < \infty$.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumptions 1–4: $J^* \in L_2(S,D)$; for every $\lambda \in [0,1]$, TD($\lambda$) converges with probability 1, from every initial state and every $r_0$, to a vector $r^*$; $r^*$ is the unique solution of

$$\Pi T^{(\lambda)}(\Phi' r^*) = \Phi' r^*;$$

and

$$\|\Phi' r^* - J^*\|_D \le \frac{\|\Pi J^* - J^*\|_D}{1 - \alpha(1-\lambda)/(1-\lambda\alpha)}.$$

Milestones

• Lemma 1: $\|PJ\|_D \le \|J\|_D$.
• Lemma 2: $J^*$ is finite, lies in $L_2(S,D)$, and $J^* = \sum_t(\alpha P)^t\bar g$.
• Lemma 3: $T^{(\lambda)}$ maps $L_2(S,D)$ into itself and has a closed-form series.
• Lemma 4: $T^{(\lambda)}$ is a $\|\cdot\|_D$-contraction with modulus $\alpha(1-\lambda)/(1-\alpha\lambda)$.
• Lemma 5: $\Pi T^{(\lambda)}$ has a unique fixed point $\Phi'r^*$, with the error bound above.
• Lemma 6: steady-state moments of $\phi$ and $z_t$.
• Lemma 7: the steady-state mean step is $E_0[s(r,X_t)] = \Phi D(T^{(\lambda)}(\Phi'r) - \Phi'r)$.
• Lemma 8: $(r - r^*)'E_0[s(r,X_t)] < 0$ for $r \neq r^*$.
• Theorem 2: a stochastic approximation theorem with Markov noise.
• §6: $A = E_0[A(X_t)]$ is negative definite and $Ar^* + b = 0$.

Significance

Theorem 1 says that TD($\lambda$), run on-line along a single trajectory, converges for every $\lambda$, and that its limit has a precise meaning: the fixed point of the projected operator. The error bound shows that as $\lambda \to 1$ the limit approaches the best approximation $\Pi J^*$, and that for smaller $\lambda$ the error can grow by at most a factor $(1-\alpha\lambda)/(1-\alpha)$. The analysis also explains the failures of related schemes: the projection and the contraction must use the same norm, $\|\cdot\|_D$, which holds only when states are sampled along the chain.

The result is proved on paper. To our knowledge no part of it has been machine-checked; it is not in Mathlib or on this platform. This mission produces:

• a Lean model of countable-state Markov chains with costs, their path law, the weighted space $L_2(S,D)$ and the projection $\Pi$, which is reusable for later work on linear TD, LSTD and approximate policy evaluation;
• the deterministic layer (Lemmas 1–5, 7, 8), which is self-contained functional analysis on $L_2(S,D)$;
• Theorem 2, a stochastic approximation theorem with Markov noise, which the paper quotes from Benveniste, Métivier and Priouret (1987) without proof. A formal proof of it would be a library result in its own right.

Difficulty

The obvious approach treats TD($\lambda$) as a noisy version of the deterministic iteration $\bar r_{t+1} = \bar r_t + \gamma_t\Phi D(T^{(\lambda)}(\Phi'\bar r_t) - \Phi'\bar r_t)$. It fails at the noise. The increments $s(r_t,X_t)$ are driven by the Markov process $X_t = (i_t,i_{t+1},z_t)$, not by independent samples. They are not martingale differences, and on an infinite state space they are unbounded. The standard ODE method with martingale-difference noise therefore does not apply, and the bias from Markov dependence must be controlled through the mixing and growth conditions of Assumption 3. The algorithm also starts with $z_{-1} = 0$ rather than in steady state, so the steady-state identities of Lemmas 6–8 must be transferred to the actual trajectory. The contraction argument needs care for a different reason: $\Pi$ is a nonexpansion of $\|\cdot\|_D$ only because $D$ is the invariant distribution of the same chain that defines $T^{(\lambda)}$.

Formalization scope

$S$ is a countable type with the discrete $\sigma$-algebra, $P$ a Markov kernel ($p_{ij} = P(i)(\{j\})$, $P^m$ the kernel power), and the path law of the chain is Mathlib's Ionescu–Tulcea measure Kernel.trajMeasure. Standing conventions:

• $\alpha \in (0,1)$ and $\lambda \in [0,1]$;
• "with probability 1" is almost-sure convergence under the path law from each deterministic initial state;
• $J^*$ and $T^{(\lambda)}$ are defined by the page's path expectations, not by the series of Lemmas 2 and 3;
• $L_2(S,D)$ membership is summability of $\pi(i)J(i)^2$;
• Assumption 1(c) means absolute integrability of the discounted cost series;
• vector norms are Euclidean and matrix norms Frobenius (equivalent to the induced norm and used only under existential constants);
• $(\Phi D\Phi')^{-1}$ is Lean's matrix inverse, invertible under Assumptions 1(a) and 2;
• the steady-state process of Lemmas 6–8 is any two-sided chain on a probability space with the stationary finite-dimensional distributions.

Lean's integral of a non-integrable function and sum of a non-summable series are $0$. A trivializing formalization is excluded by stating every expectation and series with its integrability or summability: "well defined and finite" is always a conjunct or a hypothesis, never left to junk values.

The development needs the following:

• Markov-chain path measures and stationary two-sided chains;
• Bochner integrals of vector-valued functions;
• the Cauchy–Schwarz inequality on $L_2(S,D)$;
• a Markov-noise stochastic approximation theorem.

Contributions are welcome at every level: proofs of the deterministic lemmas, a construction of the stationary chain from $\pi$ and $P$ (showing that the steady-state hypotheses are satisfiable), and a proof of Theorem 2 or a stronger stochastic approximation result that implies it.

Selected references

• J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, MIT LIDS report LIDS-P-2322, 1996; IEEE Transactions on Automatic Control 42(5):674–690, 1997. https://doi.org/10.1109/9.580874
• A. Benveniste, M. Métivier and P. Priouret, Adaptive Algorithms and Stochastic Approximations, Springer, 1990 (French original 1987). https://doi.org/10.1007/978-3-642-75894-2
• R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3:9–44, 1988. https://doi.org/10.1007/BF00115009
• P. Dayan, The convergence of TD(λ) for general λ, Machine Learning 8:341–362, 1992. https://doi.org/10.1007/BF00992701
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the convergence of stochastic iterative dynamic programming algorithms, Neural Computation 6(6):1185–1201, 1994. https://doi.org/10.1162/neco.1994.6.6.1185
• J. N. Tsitsiklis, Asynchronous stochastic approximation and Q-learning, Machine Learning 16:185–202, 1994. https://doi.org/10.1007/BF00993306

Motivation

A finite Markov decision process may have several recurrent classes under one policy. In that setting, its long-run reward depends on the initial state, and a single stationary distribution does not describe the whole decision problem. Hordijk and Kallenberg developed a linear program with two families of variables to handle this multichain case. Their Theorem 8 relates policies to feasible points of that program in both directions: optimal stationary policies give optimal dual solutions, and every optimal dual solution gives an average optimal stationary policy. This relationship explains why the dual program represents the original sequential decision problem rather than merely bounding its value. Hordijk and Kallenberg (1979)

An earlier frequency formulation associated stationary randomized policies with one family of occupation variables in a more restricted Markov-chain setting. The present theorem uses both $x$ and $y$ variables, and its policy comparison covers history-dependent randomized decisions. The corresponding formalization therefore addresses the finite multichain model of the 1979 paper, with its own dual equations and representative map. Hordijk and Kallenberg (1979), §§1 and 3.3

Setting

Let $E$ be a nonempty finite set of states. At state $i$, an action $a$ is chosen from a nonempty finite set $A(i)$. It earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}$. The transition probabilities are nonnegative and sum to one over $j$. A general policy $R$ may randomize and use the complete past history. Its average reward $\phi_i(R)$ is the liminf, as the horizon grows, of expected total reward divided by the horizon when the initial state is $i$. The optimal value $\phi_i$ is the supremum of $\phi_i(R)$ over all such policies. A policy is average optimal when it attains that value at every state. These are the conventions of §2.1 of the paper. Hordijk and Kallenberg (1979), p. 353

A stationary randomized policy $\pi^\infty$ chooses each admissible action $a$ at state $i$ with a fixed probability $\pi_{ia}$, independently of the epoch and history. Its transition matrix is $P(\pi)_{ij}=\sum_{a\in A(i)}\pi_{ia}p_{iaj}$, and its reward vector is $r(\pi)_i=\sum_{a\in A(i)}\pi_{ia}r_{ia}$. The Cesàro limit matrix $P^*(\pi)$ and deviation matrix $D(\pi)$ describe the recurrent and transient behavior of this finite chain. In particular, $\phi(\pi^\infty)=P^*(\pi)r(\pi)$. Hordijk and Kallenberg (1979), p. 359

Fix positive state weights $\beta_j$ summing to one. The primal linear program minimizes $\sum_j\beta_j\widetilde\phi_j$ over pairs $(\widetilde\phi,\widetilde u)$ that are superharmonic: for every $i$ and $a\in A(i)$, the first vector dominates its one-step expected continuation, and the sum of the two vectors dominates one-step reward plus the continuation of the second. The dual linear program maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative $x_{ia}$ and $y_{ia}$ satisfying the two flow equations (3) and (4). Variables are present only for admissible state-action pairs. The set $E_x$ consists of states where $\sum_a x_{ia}>0$. Hordijk and Kallenberg (1979), pp. 356–357

For a feasible dual point $(x,y)$, the associated policy $\pi(x,y)$ normalizes the $x$ row at states in $E_x$ and the $y$ row at other states. Conversely, equation (6) constructs a representative $(x(\pi),y(\pi))$ of a stationary randomized policy. Its $x$ coordinates use $\beta^TP^*(\pi)$. Its $y$ coordinates use $\beta^TD(\pi)+\gamma^TP^*(\pi)$, where $\gamma$ is zero at transient states and is chosen separately on each recurrent class by a maximum formula. The formalization restricts that formula's denominator to the recurrent class, as required by the subsequent nonnegativity calculation; the printed unrestricted denominator has a two-state counterexample. Hordijk and Kallenberg (1979), pp. 359–360

Formalization targets

Optimality correspondence

The goal is Theorem 8, with both directions in one statement:

$$\pi^\infty\text{ average optimal}\ \Longrightarrow\ (x(\pi),y(\pi))\text{ dual optimal}, \qquad (x,y)\text{ dual optimal}\ \Longrightarrow\ \pi^\infty(x,y)\text{ average optimal}.$$

The second implication applies to every optimal dual point. It produces the stationary randomized policy given by the printed normalization rule, including its existence as a valid policy. The first implication uses the particular representative defined by equation (6). Neither direction imposes an extreme-point condition. Hordijk and Kallenberg (1979), Theorem 8, p. 360

Supporting results

The milestones state the least-superharmonic characterization of $\phi$; the positivity that makes the dual-to-policy normalization meaningful; the stationary gain identity; feasibility and objective value of the representative; and Propositions 4 and 5, which describe tight actions and identify $E_x$ with the recurrent states of $P(\pi(x,y))$. Each is a statement about the same finite model and the same primal–dual pair. Hordijk and Kallenberg (1979), pp. 356–361

Significance

The theorem establishes an exact relation between two ways of expressing average optimality. The LP direction turns an optimal stationary policy into a dual optimum with a concrete state-action representation. The converse says an arbitrary optimal dual point can be read as an average optimal policy, even when its $x$ coordinates vanish at some states. Proposition 5 specifies what those vanishing coordinates mean for the induced chain: those states are transient. These statements permit optimization over a finite LP while preserving the policy interpretation of its solutions. Hordijk and Kallenberg (1979), Theorem 8 and Proposition 5

The result was proved in 1979; this mission asks for a machine-checked proof of its precise finite-state statement. The shared MDP model and the limit and deviation matrix definitions already exist as published formal objects. The new work is the correspondence for Hordijk and Kallenberg's dual equations, with the representative, its class-wise correction, and the connection to liminf average reward. The definitions of stationary policy mixtures, admissible-pair LP coordinates, and finite-chain recurrence can support later results about average-reward optimization.

Difficulty

Normalizing $x$ alone does not define a policy at every state: its row sum can be zero. The dual program's second variable $y$ supplies the action weights there, and the feasibility equations must ensure its row sum is positive. In the other direction, the natural $\beta^TD(\pi)$ term in $y(\pi)$ need not be nonnegative. The correction $\gamma$ is chosen by a maximum over each recurrent class, while transient states require a different case. These issues remain in a multichain process even though the state and action sets are finite. Hordijk and Kallenberg (1979), pp. 359–361

Formalization scope

Lean uses finite types for states and actions, a nonempty state type, and a nonempty admissible action set at every state. The published StationaryMDP definition provides real rewards and stochastic transition rows. General policies are its history-dependent randomized AvgHRPolicy values; average reward is its liminf reward, and optimal gain is the supremum over that entire policy class. The mission defines its own average-optimality predicate because the published Puterman predicate uses a stronger limsup comparison. For finite rewards, the liminf gains and their supremum are bounded real numbers.

Stationary randomized weights are nonnegative, sum to one on each $A(i)$, and vanish outside $A(i)$. The dual variables are functions on the subtype of admissible state-action pairs. The primal and dual optima mean feasible points attaining the relevant objective against every other feasible point. The paper's positive, normalized $\beta$ remains explicit. The raw formula for $\pi(x,y)$ is used only with a feasible dual point, and the policy-well-definedness milestone supplies its nonzero denominators. The representative uses a maximum over the ergodic class of each recurrent state, with the class-restricted denominator needed by the paper's proof; replacing $\gamma$ by zero or by one global maximum would change the target.

The known matrix objects $P^*$ and $D$ are imported from the published Blackwell development. Their convergence and identities are theorem obligations, not assumptions hidden in definitions. Contributions proving the finite-chain identities, representative feasibility, complementary slackness, and the final policy comparison are within scope. A statement restricted to a unichain model, an extreme dual point, or a pure selected action would not establish this theorem.

Selected references

• A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. DOI: 10.1287/mnsc.25.4.352.

Motivation

A partially observable Markov decision process (POMDP) models an agent that acts in a stochastic world whose state it cannot see directly. The agent sees only noisy observations. POMDPs are the standard model for planning under uncertainty in robotics, dialogue systems, medical decision making and machine maintenance. The exact finite-horizon theory goes back to Smallwood and Sondik (1973), who showed that the optimal value function is piecewise linear and convex in the agent's belief, so that it can be represented by a finite set of vectors.

Kaelbling, Littman and Cassandra (1998) brought this theory to artificial intelligence. Their paper introduces policy trees as the objects behind those vectors and presents the witness algorithm, an exact value-iteration method. It is one of the most cited papers on POMDPs. The correctness of the witness algorithm rests on a single statement, Theorem A.1 of the paper's appendix, the witness theorem. This mission formalizes that theorem together with the lemmas its proof uses.

Timeline:

• 1965: Åström reduces control with incomplete state information to control of the conditional state distribution.
• 1973: Smallwood and Sondik prove that the finite-horizon value function is piecewise linear and convex and give the first exact algorithm.
• 1980s: Cheng's linear support method. Lark and White's pruning.
• 1994–1996: Littman, Cassandra and Kaelbling give the witness algorithm and its theorem (Littman's thesis, 1996).
• 1998: the journal version studied here.

Setting

A POMDP is a tuple $\langle S, A, T, R, \Omega, O\rangle$ with finite sets $S$ of states, $A$ of actions and $\Omega$ of observations. Taking action $a$ in state $s$ leads to state $s'$ with probability $T(s, a, s')$ and earns expected reward $R(s, a)$. The agent then observes $o$ with probability $O(s', a, o)$. Rewards are discounted by a factor $\gamma$ with $0 < \gamma \le 1$; $\gamma = 1$ is the plain finite-horizon problem.

A belief state $b$ is a probability vector on $S$; $B$ denotes the set of all of them. After action $a$ and observation $o$, the belief is updated by Bayes' rule to $SE(b, a, o)$. The normalizing constant of this update is $\Pr(o \mid a, b)$.

A $t$-step policy tree $p$ is a single action when $t = 1$. For $t \ge 2$ it is a root action $a(p)$ together with one $(t-1)$-step subtree $o(p)$ for each observation $o$. Its value is defined by the recursion

$$V_p(s) = R(s, a(p)) + \gamma \sum_{s'} T(s, a(p), s') \sum_{o} O(s', a(p), o)\, V_{o(p)}(s'),$$

and at a belief state it is $V_p(b) = \sum_s b(s) V_p(s) = b \cdot \alpha_p$. The optimal $t$-step value is $V_t(b) = \max_p V_p(b)$ over all $t$-step trees.

A tree $p$ in a finite set $\tilde V$ is useful if some belief state gives it a strictly larger value than every tree of $\tilde V$ with a different value function. The useful trees form the parsimonious representation of $\tilde V$. Let $\mathcal V_{t-1}$ be the useful $(t-1)$-step trees. The candidates $C^a_t$ are the $t$-step trees with root $a$ and all subtrees in $\mathcal V_{t-1}$, and $\mathcal Q^a_t$ is the set of trees useful in $C^a_t$. The Q-function is

$$Q^a_t(b) = \sum_s b(s) R(s, a) + \gamma \sum_o \Pr(o \mid a, b)\, V_{t-1}(SE(b, a, o)).$$

For a set $U_a$ of candidates, $\hat Q^a_t(b) = \max_{p \in U_a} V_p(b)$ is the current approximation. For $p \in U_a$, an observation $o$ and $p' \in \mathcal V_{t-1}$, the tree $p_{\mathrm{new}}$ is $p$ with its subtree for $o$ replaced by $p'$.

Formalization targets

Goal: Theorem A.1

For a nonempty $U_a \subseteq \mathcal Q^a_t$,

$$U_a \ne \mathcal Q^a_t \iff \exists\, p \in U_a,\ o^* \in \Omega,\ p' \in \mathcal V_{t-1},\ b \in B:\quad V_{p_{\mathrm{new}}}(b) > V_{\tilde p}(b) \ \text{ for all } \tilde p \in U_a .$$

Trees with the same value function are identified, as in the paper. The statement is exact, with no constants.

Milestones

1. §3.3: $\Pr(\cdot \mid a, b)$ is a distribution and $SE(b, a, o) \in B$ when $\Pr(o \mid a, b) \ne 0$.
2. §4.1: $V_t$ is convex on $B$.
3. §4.2: the useful trees represent the same upper surface and are contained, up to identification, in every representing subset.
4. §4.3: for every belief and subtree there is a useful subtree that is at least as good.
5. §4.4: $Q^a_t(b)$ is the maximum of $V_p(b)$ over all $a$-rooted trees and over $C^a_t$, and $V_t(b) = \max_a Q^a_t(b)$.
6. §4.4.1: $\hat Q^a_t \le Q^a_t$ on $B$.
7. Appendix A: if $V_{p^*}(b) > V_p(b)$ for trees with the same root, one subtree swap already improves on $p$ at $b$.
8. §4.4.2: the witness theorem in Q-function form: $\hat Q^a_t \ne Q^a_t$ somewhere on $B$ iff a single-subtree replacement beats all of $U_a$ at some belief.

Significance

The witness theorem is the stopping and growth criterion of the witness algorithm. If no single-subtree modification of the current trees beats all of them at some belief state, the current set represents the Q-function exactly. Otherwise the belief found is a witness and yields a new useful tree. Because each test is one linear program, the theorem turns an infinite search over belief space into finitely many linear programs. It is also the basis of the paper's complexity claim, polynomial time in $|S|$, $|A|$, $|\Omega|$, $|\mathcal V_{t-1}|$ and $|\mathcal Q^a_t|$. Incremental pruning and later exact POMDP solvers rely on the same parsimonious-set machinery.

The theorem is proved in the paper; it has not been machine-checked. A formal development would also provide reusable infrastructure: policy trees, their value recursion, belief updates, and the existence and minimality of parsimonious representations of finite sets of linear functions on the simplex. That infrastructure is needed for any formal treatment of exact POMDP value iteration.

Difficulty

Most steps are finite algebra. The part that needs care is the "if" direction of the goal. A belief at which a new tree beats all of $U_a$ shows that the true Q-function exceeds the approximation. It does not directly show that a useful tree is missing, because the maximizing tree at that belief may tie with other trees there. One needs the representation property of the parsimonious set (milestone 3): at every belief, the maximum over all candidates is attained by a useful one. Proving this means moving from a belief where several value functions tie to a nearby belief, inside the simplex, where exactly one of them is strictly largest. The proof on p. 131 also needs the Q-function to be attained on the candidate set, so that the improving subtree lies in $\mathcal V_{t-1}$ (milestones 4 and 5).

Formalization scope

• $S$, $A$ and $\Omega$ are finite, nonempty types with decidable equality. $T$ and $O$ are stochastic and $0 < \gamma \le 1$; these are bundled in POMDP.IsValid.
• PolicyTree A Ω n is the type of $(n+1)$-step trees, so statements about $t$-step trees with subtrees use $t = n + 2$. The type is finite, and the set of all trees of a given depth is Finset.univ.
• Values are defined by the recursion of p. 109, not by expectations over trajectories; everything is a finite sum.
• Belief states are the points of stdSimplex ℝ S. Every "there is some belief state" ranges over the simplex, not over $\mathbb R^S$.
• Usefulness is relative to a named finite set: all trees of a depth for $\mathcal V_{t-1}$, and the candidates for $\mathcal Q^a_t$. $\mathcal Q^a_t$ is constructed from $\mathcal V_{t-1}$, not quantified over.
• Maxima are Finset.sup' over nonempty finite sets, or IsGreatest.
• $SE(b, a, o)$ is the zero vector when $\Pr(o \mid a, b) = 0$ (division by zero). Every use either assumes $\Pr \ne 0$ or multiplies by $\Pr$.

The following encodings would make the theorem trivial or false, and are excluded: comparing trees by equality instead of by value function, letting $b$ range over all of $\mathbb R^S$, taking $\mathcal Q^a_t$ to be an arbitrary set, allowing $U_a = \emptyset$, and defining the true Q-function as $\hat Q^a_t$ itself.

Contributions are welcome at every level. The parsimonious-representation lemma (milestone 3) is the reusable geometric core. The subtree-swap lemma and the Q-function identity are the algebraic core.

Selected references

• L. P. Kaelbling, M. L. Littman, A. R. Cassandra, Planning and acting in partially observable stochastic domains, Artificial Intelligence 101(1–2):99–134, 1998. https://doi.org/10.1016/S0004-3702(98)00023-X
• R. D. Smallwood, E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10:174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X
• A. R. Cassandra, M. L. Littman, N. L. Zhang, Incremental pruning: a simple, fast, exact method for partially observable Markov decision processes, UAI 1997. https://arxiv.org/abs/1302.1525