Dynamic Programming

Markov Chain Operations Research Optimization·Captain: mikedeng1

Optimality of (s, S) Policies in Inventory Models with Markovian Demand II: In the Nonstationary Discounted Infinite-Horizon Problem, a State-Dependent (s, S) Policy Is OptimalResearch Paper

Motivation

Periodic-review inventory models with a fixed ordering cost are the setting in which the $(s,S)$ policy is optimal: when the stock falls below a reorder point $s$ , order up to a level $S$ , otherwise order nothing. Scarf (1960) proved this for independent demands over a finite horizon by introducing $K$ -convexity, and Iglehart (1963) extended it to the discounted infinite horizon. In practice the demand distribution changes with an exogenous environment: the economy, the season, the stage of a product's life cycle. Song and Zipkin (Oper. Res. 41(2), 1993) modelled this environment as a Markov chain of demand states in continuous time with Poisson demand.

Sethi and Cheng (Oper. Res. 45(6), 1997) treat the discrete-time version with general demand densities, nonstationary costs and convex surplus costs of linear growth. The companion mission (I) covers their finite-horizon result, Theorem 4.1. This mission covers the nonstationary discounted infinite-horizon result, Theorem 6.2, together with the existence theory (Theorem 6.1, proved in the paper's Appendix) on which it rests.

Setting

Demand states form the finite set $I = \{1,\dots,L\}$ and follow a Markov chain with transition matrix $P = (p_{ij})$ . In period $k = 0,1,2,\dots$ the demand $\xi_k \ge 0$ has the conditional density $\varphi_{i,k}$ given $i_k = i$ , with mean at most $M$ . Orders are placed at the start of a period and delivered at once, and unmet demand is backlogged, so the surplus evolves by $x_{k+1} = x_k + u_k - \xi_k$ (2.4). Ordering $u \ge 0$ costs $c_k(i,u) = K^i_k\,\delta(u) + c^i_k u$ with $K^i_k, c^i_k \ge 0$ (2.1), where $\delta(z) = 1$ for $z > 0$ and $0$ otherwise. The surplus cost $f_k(i,\cdot)$ is convex and nonnegative, vanishes at $0$ , and satisfies $f_k(i,x) \le C(1+|x|)$ (2.2).

An admissible policy $U$ chooses each order $u_k \ge 0$ as a measurable function of the past demand states and demands. With a discount factor $\alpha$ , the objective from period $n$ , state $i$ and surplus $x$ is

J_n(i,x;U) = \sum_{k=n}^{\infty} \alpha^{k-n}\,E\big[c_k(i_k,u_k) + f_k(i_k,x_k)\big], \tag{6.1}

and the value function is $v_n(i,x) = \inf_U J_n(i,x;U)$ . With $F_{n+1}(b)(i,y) = \sum_j p_{ij}\int_0^\infty b(j,y-z)\,\varphi_{i,n}(z)\,dz$ (3.1), the dynamic programming equations are

v_n(i,x) = f_n(i,x) + \inf_{u\ge0}\big\{c_n(i,u) + \alpha F_{n+1}(v_{n+1})(i,x+u)\big\}, \qquad n = 0,1,2,\dots \tag{6.2}

The truncations $J_{n,k}$ keep the first $k$ periods of (6.1) (6.3), their values are $v_{n,k}$ (6.4), and $w_n = J_n(\cdot;\mathbf 0)$ is the cost of never ordering (6.6). The function classes are $B_0$ (nonnegative pointwise limits of continuous functions), $B_1$ (those of linear growth) and $C_1$ (those also uniformly continuous in $x$ ). A function $g$ is $K$ -convex if $K + g(z+y) \ge g(y) + z\,(g(y)-g(y-b))/b$ for all $z \ge 0$ , $b > 0$ (4.3). Assumption (4.1) asks $K^i_n \ge \sum_j p_{ij}K^j_{n+1} \ge 0$ , and (4.2) asks $c^i_n x + F_{n+1}(f_{n+1})(i,x) \to +\infty$ as $x \to \infty$ .

Formalization targets

Goal: Theorem 6.2

Under (2.1), (2.2), (4.1), (4.2) and $0 < \alpha < 1$ , there are $s^i_n \le S^i_n$ in $[-\infty,\infty)$ such that

\hat u_n(i,x) = (S^i_n - x)\,\delta(s^i_n - x)

attains the infimum in (6.2) at every $(n,i,x)$ , and its feedback policy, started at any period $n$ and surplus $x$ , has cost $J_n(i,x;\hat U) = v_n(i,x)$ : it is optimal among all history-dependent policies.

Milestones

The order-nothing cost $w_n$ is finite, lies in $C_1$ , and is the unique $C_1$ solution of $w_n = f_n + \alpha F_{n+1}(w_{n+1})$ (6.7).
The truncated values solve the dynamic programming equations (6.5), $v_{n,0} = 0$ , $v_{n,k} \in C_1$ , and under (4.2) the infimum in (6.4) is attained.
Theorem 6.1, (6.8): $0 = v_{n,0} \le v_{n,1} \le \cdots \le v_{n,k} \le w_n$ .
Appendix: $|v_{n,k}(i,x') - v_{n,k}(i,x)| \le C|x'-x|/(1-\alpha)$ , and the same for $v_n = \lim_k v_{n,k}$ .
Theorem 6.1, (6.9): $v_{n,k} \uparrow v_n$ , a solution of (6.2) in $B_1$ .
Theorem 6.1, (6.10): $v_n \in C_1$ , a $B_0$ minimizer $\hat U$ of (6.2) exists, and every such $\hat U$ is optimal: $v_n(i,x) = \min_U J_n(i,x;U) = J_n(i,x;\hat U)$ .
Proof of Theorem 6.2: $v_{n,k}(i,\cdot)$ is $K^i_n$ -convex.
Proof of Theorem 6.2: $v_n(i,\cdot)$ is $K^i_n$ -convex.

The structural lemma behind the step from $K$ -convexity to the $(s,S)$ form, Proposition 4.2 of the paper (an extension of Bertsekas' lemma to lower semicontinuous functions coercive only at $+\infty$ , with possibly infinite $s$ , $S$ ), is posed in the companion finite-horizon mission and is not repeated here.

Significance

Theorem 6.2 says that the classical $(s,S)$ structure survives two generalizations at once: demand driven by a Markov environment, and nonstationary data over an infinite horizon. The two levels may depend on the period and on the current demand state, so only $2L$ numbers per period describe an optimal policy, and with cyclic demand only $L$ pairs are needed (Corollary 7.1 of the paper). Theorem 6.1 is a self-contained existence result for a positive-cost, unbounded-state dynamic program: value iteration from zero converges to the value function, which solves the optimality equation, and any measurable minimizer is optimal among history-dependent policies.

The results are proved in the paper, with the finite-horizon existence theory delegated to Beyer, Sethi and Taksar (1998). No machine-checked proof of any of them is known. The platform has $K$ -convexity (BertsekasKConvex) and the $(s,S)$ structure lemma of Bertsekas for continuous functions coercive at both ends; it has no discounted infinite-horizon $(s,S)$ theorem with Markov-modulated demand. The related posed items SongZipkinFluct.FixedCost.theorem5e_theorem6 and theorem5ab concern the Song–Zipkin model (continuous time, Poisson demand, integer levels, stationary data), a different model.

Difficulty

The obvious argument is "the finite-horizon value functions are $K$ -convex, so their limit is, and a minimizer of a $K$ -convex optimality equation is $(s,S)$ ". Three steps of it fail as stated.

First, the limit of value iteration need not be the value function, nor solve (6.2), in a positive-cost problem with unbounded actions: exchanging $\lim_k$ with $\inf_u$ requires the minimizers of the truncated problems to stay in a compact set uniformly in $k$ , and that bound is where the coercivity assumption (4.2) enters. Second, optimality against history-dependent policies, not only Markov ones, requires a verification argument along histories of states and demands. Third, the functions $z_n(i,y) = c^i_n y + \alpha F_{n+1}(v_{n+1})(i,y)$ may be unbounded below, in which case the reorder level is $s = -\infty$ and the order-up-to level does not exist; the goal allows this case.

Formalization scope

The Lean development (namespace SethiChengSS.Infinite) commits to the following.

Demand states are Fin L; periods are natural numbers with the paper's base $0$ .
Expectations are sums over state paths of Lebesgue integrals against the product weight $\prod_t p_{i_t i_{t+1}}\varphi_{i_t,t}(\xi_t)$ , valued in $[0,\infty]$ . This builds in the conditional independence of $\xi_k$ and $i_{k+1}$ given $i_k$ that (3.1) uses.
A policy is a function of the state history and the past demands; admissible means nonnegative and measurable in the demands. The comparison class is never restricted to Markov policies.
$J_n$ (6.1) is the supremum over $k$ of the truncations $J_{n,k}$ (6.3), which equals the series because all costs are nonnegative.
$F_{n+1}$ uses the Bochner integral, which is $0$ on non-integrable integrands; the $C_1$ conclusions are what make it genuine.
The levels $s$ , $S$ are extended reals with $s \le S$ , $S \ne +\infty$ , and $S$ real whenever $s$ is (Remark 4.4).

Pins. The paper prints $0 < \alpha \le 1$ ; the mission assumes $0 < \alpha < 1$ , since $w_n$ is infinite at $\alpha = 1$ and the Appendix divides by $1-\alpha$ . Theorem 6.2 is printed without (4.1), which its proof uses through the induction of Section 4; (4.1) is assumed for every period. Theorem 6.1 is printed under (2.1)–(2.2) only, but attainment in (6.2) can fail without coercivity and the Appendix bound (A.3) divides by $c^i_n$ ; (4.2) is added to (6.9), (6.10) and to the attainment clause of (6.5). "In class $C_1$ " for the sequence $w_n$ is read with one growth constant for all periods. The boundary condition " $v_{n+k,0} = 0$ " of (6.5) is read as $v_{n,0} = 0$ , as the next sentence of the paper states.

The goal cannot be met by a degenerate encoding: the value function is the infimum over all admissible history-dependent policies (not the solution of (6.2) by definition), the demand data must be genuine probability densities with bounded mean, and the levels may not be $S = +\infty$ .

A complete development needs: monotone convergence for the path-measure costs, measurable selection of minimizers, the $K$ -convexity closure properties (Proposition 4.1 of the paper; several are proved on the platform as BertsekasDP.kconvex_*), and Proposition 4.2. The model file and the infinite-horizon verification argument are reusable for other Markov-modulated inventory models. Contributions toward any milestone, or toward general lemmas on positive-cost dynamic programs, are welcome.

Selected references

S. P. Sethi and F. Cheng, Optimality of (s, S) policies in inventory models with Markovian demand, Operations Research 45(6), 931–939, 1997. https://doi.org/10.1287/opre.45.6.931
J.-S. Song and P. Zipkin, Inventory control in a fluctuating demand environment, Operations Research 41(2), 351–370, 1993. https://doi.org/10.1287/opre.41.2.351
H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
D. L. Iglehart, Optimality of (s, S) policies in the infinite horizon dynamic inventory problem, Management Science 9(2), 259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press, 1976.
A. Bensoussan, M. Crouhy and J.-M. Proth, Mathematical Theory of Production Planning, North-Holland, 1983.
D. Beyer, S. P. Sethi and M. Taksar, Inventory models with Markovian demands and cost functions of polynomial growth, Journal of Optimization Theory and Applications 98, 1998 (cited by Sethi and Cheng as forthcoming).

11 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Robust Dynamic Programming 2: The Discounted Robust Value Function Is the Unique Fixed Point of the Robust Bellman OperatorResearch Paper

Motivation

Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.

Timeline:

1968, 1973. Satia (PhD thesis) and Satia and Lave (Operations Research 21) treat finite-state, finite-action Markov decision processes with uncertain transition probabilities. They state the max–min optimality equation and the optimality of stationary policies, assuming convex uncertainty sets, and do not prove that the solution of the equation is the robust value function.
2001. Bagnell, Ng and Schneider analyse robust policies when the decision maker is restricted to stationary policies.
2002–2005. Iyengar (this paper) and Nilim and El Ghaoui (Operations Research 53, 2005) give the rectangular theory. Iyengar proves the discounted robust Bellman equation for countable state spaces, against history-dependent randomized policies and an adversary that may change the law at every visit.

Setting

A discounted ambiguous Markov decision process has a countable state set $\mathcal S$ , for each state $s$ a nonempty set $\mathcal A(s)$ of admissible actions, for each admissible pair $(s,a)$ a nonempty set $\mathcal P(s,a)$ of probability measures on $\mathcal S$ (the ambiguity set), a bounded reward $r(s,a,s')$ and a discount factor $\lambda\in(0,1)$ . Decisions are made at epochs $t=0,1,2,\dots$ .

A policy $\pi=(d_0,d_1,\dots)$ maps each history $h_t=(s_0,a_0,\dots,s_t)$ to a probability measure on $\mathcal A(s_t)$ . $\Pi$ is the set of all such policies. A deterministic Markov policy plays $d_t(s_t)$ for maps $d_t:\mathcal S\to\mathcal A$ with $d_t(s)\in\mathcal A(s)$ . A stationary policy uses one such rule $d$ at every epoch.

Under Rectangularity, the adversary picks a law $p\in\mathcal P(s_t,a_t)$ separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is $\mathcal T^\pi$ . In the static model the adversary fixes one $\bar p_{sa}\in\mathcal P(s,a)$ per pair. The robust value of a policy and the robust value function are

V^\pi_\lambda(s)=\inf_{\mathbf P\in\mathcal T^\pi}\mathbf E^{\mathbf P}\Big[\sum_{t=0}^\infty\lambda^t r(s_t,d_t(h_t),s_{t+1})\Big],\qquad V^*_\lambda(s)=\sup_{\pi\in\Pi}V^\pi_\lambda(s).

Let $\mathbf V$ be the bounded functions on $\mathcal S$ with $\|V\|=\sup_s|V(s)|$ . For a set $\mathcal D$ of deterministic Markov rules, the robust Bellman operator is

\mathcal L_{\mathcal D}V(s)=\sup_{d\in\mathcal D}\ \inf_{p\in\mathcal P(s,d(s))}\mathbf E^p\big[r(s,d(s),s')+\lambda V(s')\big].

Formalization targets

Goal: Corollary 2(b)

V^*_\lambda(s)=\sup_{a\in\mathcal A(s)}\ \inf_{p\in\mathcal P(s,a)}\mathbf E^p\big[r(s,a,s')+\lambda V^*_\lambda(s')\big],\qquad s\in\mathcal S,

$V^*_\lambda$ is the only bounded solution of this equation, and for every $\epsilon>0$ some stationary deterministic policy $\pi^\epsilon$ has $V^{\pi^\epsilon}_\lambda\ge V^*_\lambda-\epsilon$ .

Milestones

Theorem 5(a). $\mathcal L_{\mathcal D}$ maps $\mathbf V$ to $\mathbf V$ and $\|\mathcal L_{\mathcal D}U-\mathcal L_{\mathcal D}V\|\le\lambda\|U-V\|$ .
Theorem 5(b). For $\mathcal D=\prod_s\mathcal D(s)$ , the equation $\mathcal L_{\mathcal D}V=V$ has a unique bounded solution, equal to the robust value over deterministic Markov policies with rules in $\mathcal D$ .
Corollary 2(a). The robust value of a stationary policy $(d,d,\dots)$ is the unique bounded solution of $V(s)=\inf_{p\in\mathcal P(s,d(s))}\mathbf E^p[r(s,d(s),s')+\lambda V(s')]$ .
Theorem 4. $V^*_\lambda(s)=\sup_{\pi\in\Pi_{MD}}V^\pi_\lambda(s)$ .
Lemma 3. For a stationary policy, the dynamic and static models give the same value.
Lemma 2. The value of a stationary policy is the optimal solution of the robust program (31).
Lemma 1, first claim. The output of robust value iteration is within $\epsilon/4$ of $V^*_\lambda$ .

Significance

Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most $\epsilon$ by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.

The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.

Difficulty

The contraction property is a state-by-state $\epsilon$ -argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an $\epsilon$ slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.

Formalization scope

States and actions are countable Lean types; $\mathcal A(s)$ and $\mathcal P(s,a)$ are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and $\mathbf E^p[f]=\sum_x p(x)f(x)$ as a tsum. The rewards satisfy $|r(s,a,s')|\le R$ on admissible actions. This is the reading of the page's " $\sup r=R<\infty$ ", which its bounds $\pm R/(1-\lambda)$ require. The discount factor satisfies $0<\lambda<1$ . Epochs start at $0$ , so the first reward is undiscounted.

A policy maps $(n, h_n)$ to a PMF supported on $\mathcal A(s_n)$ . The dynamic adversary maps $(n,h_n,a)$ to a law in $\mathcal P(s_n,a)$ . The path law is built by PMF.bind, and the discounted reward is $\sum_t\lambda^t\mathbf E[r(s_t,a_t,s_{t+1})]$ , which converges absolutely. Values are real infima and suprema over nonempty families bounded by $R/(1-\lambda)$ , so no junk value arises. $\mathbf V$ is the predicate "bounded", and $\|\cdot\|$ is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.

$V^*_\lambda$ is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in $V^\pi_\lambda$ is the dynamic one; the static adversary appears only in Lemma 3.

The mission deviates from the page in three places:

Theorem 5(b) is stated for product sets $\mathcal D=\prod_s\mathcal D(s)$ . For an arbitrary $\mathcal D$ the printed statement fails, because its proof pastes $\epsilon$ -greedy actions state by state. Both uses in Corollary 2 are products.
Lemma 3 is stated for randomized Markov rules, which is the page's "any decision rule". The page proves it for deterministic rules.
Lemma 2 adds $\sum_s\alpha(s)<\infty$ and restricts the program to bounded $V$ .

Only the first claim of Lemma 1 is posed. Its second claim, that an $\epsilon/2$ -greedy rule is $\epsilon$ -optimal, is false as printed.

A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform $\epsilon$ -optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.

Selected references

G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, 2002 (rev. May 4, 2004); published in Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
J. A. Bagnell, A. Y. Ng and J. Schneider, Solving uncertain Markov decision problems, Tech. Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-problems/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

12 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Robust Dynamic Programming 1: The Robust Bellman Recursion and Optimality of Deterministic Markov Policies in Finite HorizonResearch Paper

Motivation

Markov decision processes assume that the transition law is known exactly. In practice it is estimated from data, and the optimal policy computed for the point estimate can perform badly when the true law differs. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. The worst case is taken against an adversary (nature) who may choose a law from the set at every step.

For this worst case to be computable by backward induction, the set of path measures of a policy has to decompose epoch by epoch. Garud Iyengar named this property Rectangularity and proved that under it the classical finite horizon theory carries over: a robust Bellman equation holds, and deterministic Markov policies are optimal among all history dependent randomized policies, with state and action sets that may be countably infinite and ambiguity sets that need not be convex (Iyengar, CORC Tech Report TR-2002-07, rev. 2004; published in Math. Oper. Res. 30(2), 2005).

Timeline:

1973: Satia and Lave study Markov decision processes with uncertain transition probabilities, finite states and actions (Oper. Res. 21(3)).
2001: Epstein and Schneider axiomatize recursive multiple priors, the decision-theoretic origin of rectangular ambiguity (J. Econ. Theory 113, working paper 2001).
2002–2005: Nilim and El Ghaoui give a robust counterpart of the Bellman recursion for finite state and action spaces and convex ambiguity sets, against Markov controllers (Oper. Res. 53(5)).
2002–2005: Iyengar proves the robust Bellman equation and Markov optimality for countable spaces, arbitrary ambiguity sets and all history dependent randomized policies, under Rectangularity.

Setting

A finite horizon ambiguous Markov decision process (AMDP) has decision epochs $t \in T = \{0,\dots,N-1\}$ , $N\ge 1$ , and a terminal epoch $N$ . States lie in a countable set $\mathcal S$ and actions in a countable set $\mathcal A$ . In state $s$ at epoch $t$ the admissible actions form a nonempty set $\mathcal A_t(s)$ . For each admissible action $a$ , the next state is drawn from some probability measure $p \in \mathcal P_t(s,a)$ , where $\mathcal P_t(s,a)$ is a nonempty set of probability measures on $\mathcal S$ , the ambiguity set. The decision maker receives $r_t(s,a,s')$ when $a$ is taken in $s$ and the next state is $s'$ , and $r_N(s)$ at the terminal epoch.

A history at epoch $n$ is $h_n=(s_0,a_0,\dots,s_{n-1},a_{n-1},s_n)$ . A policy $\pi=(d_t)$ assigns to each history $h_t$ a probability measure $d_t(h_t)$ on $\mathcal A_t(s_t)$ . It is deterministic ( $\Pi_D$ ) if every $d_t(h_t)$ is a point mass, and deterministic Markov ( $\Pi_{MD}$ ) if moreover the chosen action depends on the current state $s_t$ alone. $\Pi$ denotes all history dependent randomized policies.

Under Rectangularity (Assumption 1), the set $\mathcal T^\pi$ of path measures consistent with $\pi$ is a product of one-epoch sets: nature chooses, for every epoch $t$ , every history $h_t$ and every admissible action $a$ , a measure $p_{h_t,a}\in\mathcal P_t(s_t,a)$ , and the path measure is $\mathbf P(h_N)=\prod_t d_t(h_t)(a_t)\,p_{h_t,a_t}(s_{t+1})$ . The robust value of $\pi$ from $h_n$ and the robust value function are

V^\pi_n(h_n)=\inf_{\mathbf P\in\mathcal T^\pi_n}E^{\mathbf P}\Big[\sum_{t=n}^{N-1}r_t(s_t,a_t,s_{t+1})+r_N(s_N)\Big],\qquad V^*_n(h_n)=\sup_{\pi\in\Pi}V^\pi_n(h_n).

The optimistic values $\bar V^\pi_n$ , $\bar V^*_n$ replace the infimum over $\mathcal T^\pi_n$ by a supremum.

Formalization targets

Goal: Theorem 2 (Markov optimality)

For $n=0,\dots,N$ , $V^*_n(h_n)$ depends on $h_n$ only through $s_n$ ; for $n\in T$ , $V^*_n(s_n)=\sup_{\pi\in\Pi_{MD}}V^\pi_n(s_n)$ ; and

V^*_n(s)=\sup_{a\in\mathcal A_n(s)}\ \inf_{p\in\mathcal P_n(s,a)}E^p\big[r_n(s,a,s')+V^*_{n+1}(s')\big],\qquad n\in T. \tag{16}

Milestones

Proof of Theorem 1, eq. (15): at one epoch, randomizing over actions does not raise the worst-case value, and the adversary may choose its measure separately per action.
Theorem 1 (Bellman equation): $V^*_N(h_N)=r_N(s_N)$ and $V^*_n(h_n)=\sup_{a}\inf_{p\in\mathcal P_n(s_n,a)}E^p[r_n(s_n,a,s)+V^*_{n+1}(h_n,a,s)]$ (11).
Corollary 1: $V^*_n(h_n)=\sup_{\pi\in\Pi_D}V^\pi_n(h_n)$ for $n\in T$ .
Theorem 3: the optimistic analogue of Theorem 2, with recursion (18) in which both the outer and the inner optimizations are suprema.

The mission also contains, as a draft theorem that is not a milestone, the per-policy identity of the proof of Theorem 1, eq. (12): for each policy, $V^\pi_n(h_n)=\inf_{p\in\mathcal T^{d_n}}E^p[r_n+V^\pi_{n+1}(h_n,a_n,s_{n+1})]$ .

Significance

Theorem 2 is the basis of robust dynamic programming in finite horizon: computing an optimal robust policy reduces to $N$ backward passes, each a family of one-stage problems $\inf_{p\in\mathcal P_n(s,a)}E^p[v]$ . It also justifies restricting attention to deterministic Markov policies, which is what every algorithm in the robust MDP literature computes. Theorem 1 isolates the role of Rectangularity: without it the worst case over path measures does not decompose and the recursion characterizes nothing.

The results are proved on paper; no machine-checked proof is known. The platform holds the finite-state, Markov-controller special case (the Nilim–El Ghaoui RobustMDP series, posed, not proved), whose comparison class is too small to express the claim $\Pi_{MD}$ suffices against $\Pi$ . A formal proof here supplies the history dependent policy and adversary machinery on countable spaces that the discounted robust theory and the robust MDP literature reuse.

Difficulty

The obvious argument writes the robust value as an inf–sup over path measures and pushes the infimum inside the expectation epoch by epoch. That step is the content of (12): the infimum of an expectation equals the expectation of an infimum only because nature's continuation choice may depend on the realized action and next state, so near-worst continuations for different branches can be glued into one admissible adversary. Infima need not be attained (the ambiguity sets are arbitrary, the state set countable), so the gluing is an $\epsilon$ -argument over countably many branches. The supremum over policies needs a matching splicing of $\epsilon$ -optimal continuation policies (13)–(14). Finally, randomized decision rules must be eliminated (15), which uses Rectangularity again, now per action. Restricting either the policies or the adversary to Markov ones from the start is not allowed: it changes the comparison class and makes the goal circular.

Formalization scope

One countable state type S and one countable action type A serve all epochs; the page's epoch-dependent sets $\mathcal S_t$ embed into their disjoint union. Epochs are 0-based natural numbers, with terminal epoch M.N and 1 ≤ N.
A history at epoch $n$ is (Fin n → S × A) × S. Probability measures are PMF; $E^p[f]=\sum_s p(s)f(s)$ as a tsum. The expected reward under a policy and an adversary is computed by backward iterated sums, which is the expectation under the product path measure (3).
A policy is a decision rule for every epoch, admissible for t < N; the supremum over $\Pi$ equals that over the page's $\Pi_n$ because $V^\pi_n$ uses only $d_n,\dots,d_{N-1}$ . An adversary chooses $p_{h_t,a}\in\mathcal P_t(s_t,a)$ for every epoch, history and admissible action.
Added and implicit hypotheses: $\mathcal A_t(s)\neq\emptyset$ and $\mathcal P_t(s,a)\neq\emptyset$ (implicit on the page), and a uniform bound $|r_t|\le R$ , $|r_N|\le R$ (added: Section 2 states none, but with countable states the expectations and the real suprema and infima need it). All values then lie in a bounded interval, so no supremum or infimum is a junk value.
Ambiguity sets are arbitrary nonempty sets of measures: no convexity, closedness or attainment is assumed anywhere.
" $V^*_n$ is a function of the current state alone" is stated as the existence of $W(n,s)$ with $V^*_n(h_n)=W(n,s_n)$ ; the value is not defined on states, which would hide the claim. The notation $V^\pi_n(s_n)$ for Markov policies is made explicit as a clause.
Ruled out: restricting $\Pi$ or the adversary to Markov or stationary objects, a static adversary that fixes one $p$ per $(s,a)$ for the whole horizon, and suprema over unbounded or empty families; each makes some target false or trivial.

Definitions: AMDP, History, History.extend, IsPolicy, Policy, IsDeterministic, IsDetMarkov, Adversary, Selection, expect, expTail, expectedReward, V, Vstar, Vbar, VbarStar, all in RobustDP.FiniteHorizon. Lemmas about gluing adversaries along history prefixes and about suprema of bounded families indexed by subtypes are reusable. Contributions to any milestone are welcome, in any order; (15) is a one-epoch statement independent of the rest.

Selected references

G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, revised May 4, 2004; Math. Oper. Res. 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Oper. Res. 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
L. G. Epstein and M. Schneider, Recursive multiple-priors, J. Econ. Theory 113(1):1–31, 2003. https://doi.org/10.1016/S0022-0531(03)00097-8
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

7 thms2 active usersReviewed

Completed

Machine Learning Probability Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning VI: In a Deterministic MDP an Algorithm Acts T-Step Optimally at All but NAT TimestepsTextbook

Motivation

A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon $T$ ? Kakade calls this number the sample complexity of exploration.

The question builds on two algorithms. $E^3$ (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. $R_{max}$ (Brafman and Tennenholtz 2002) replaced $E^3$ 's explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of $R_{max}$ . For deterministic MDPs it shows that the number of non-optimal steps is at most $NAT$ , which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on $N$ , $A$ and $T$ made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.

Setting

An MDP $M$ has a finite set $S$ of $N$ states, a finite nonempty set of $A$ actions, a transition model $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ . A deterministic MDP has a next-state map $f$ , with $P(s'\mid s,a)=1$ exactly when $s'=f(s,a)$ .

Online model. An algorithm $\mathcal A$ is a deterministic function that maps the path observed so far, $(s_0,a_0,r_0,\dots,s_t)$ , to the next action $a_t$ . Started at $s_0$ , it produces one path $c=(s_0,a_0,s_1,a_1,\dots)$ ; $c_t$ is the subpath up to $s_t$ . The $T$ -step end time $t'$ of $t$ is the smallest multiple of $T$ larger than $t$ . The $T$ -step value of the algorithm on $c_t$ is the normalized reward it collects until $t'$ ,

U_{\mathcal A}(c_t)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{t'-1}r(s_\tau,a_\tau)\Big],

and $U^*(c_t)$ is the supremum of this quantity over all algorithms continuing from $c_t$ .

$T$ -step policies. A $T$ -step policy $\pi$ is a sequence of deterministic decision rules $\pi(\cdot,0),\dots,\pi(\cdot,T-1)$ . Its $t$ -value is $U_{\pi,t,M}(s)=\frac1T\mathbb E[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\mid s_t=s]$ , and $U^*_{t,M}(s)$ is the supremum over $T$ -step policies. For a set of states $K$ , the induced MDP $M_K$ agrees with $M$ on $K$ and makes every state outside $K$ absorbing with reward $1$ . The escape probability $\Pr(\text{escape from }K\mid\pi,M,s_t=s)$ is the probability that the path $(s_t,\dots,s_{T-1})$ of $\pi$ in $M$ leaves $K$ . A transition model $\hat P$ is an $\varepsilon$ -approximation to $P$ if $\sum_{s'}|\hat P(s'\mid s,a)-P(s'\mid s,a)|<\varepsilon$ for every $(s,a)$ .

Formalization targets

Goal: Theorem 8.3.5 (deterministic sample complexity)

For every $N$ , $A$ and $T\ge1$ there is one algorithm $\mathcal A$ such that, for every deterministic MDP with rewards in $[0,1]$ , every start state and every $L$ ,

\#\{\,t<L:\ U_{\mathcal A}(c_t)\neq U^*(c_t)\,\}\ \le\ NAT .

Milestones

Lemma 8.4.4 (induced inequalities). For every $T$ -step policy, every $t<T$ and every state $s$ ,

U_{\pi,t,M_K}(s)\ge U_{\pi,t,M}(s)\ge U_{\pi,t,M_K}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).

Corollary 8.4.5 (implicit explore or exploit). If $\pi$ is $T$ -step optimal in $M_K$ , then for every $t<T$ and every state $s$ ,

U_{\pi,t,M}(s)\ge U^*_{t,M}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).

Deterministic escapes (p. 114). In a deterministic MDP every escape probability is $0$ or $1$ .
Non-escaping steps are optimal (p. 114). In a deterministic MDP, an optimal policy of $M_K$ that does not escape from $(s,t)$ satisfies $U_{\pi,t,M}(s)=U^*_{t,M}(s)$ .
Lemma 8.5.4 ( $\varepsilon$ -approximation condition). If $\hat P$ is an $\varepsilon$ -approximation to $P$ and the rewards agree, then $|U_{\pi,t,\hat M}(s)-U_{\pi,t,M}(s)|<\varepsilon T$ for all $\pi$ , $s$ and $t<T$ .
Lemma 8.5.5, pinned. If $m\ge\frac{8N}{\varepsilon^2}\log\frac{2N}\delta$ with $\varepsilon>0$ , $0<\delta<1$ , then the empirical distribution of $m$ independent samples from a distribution $p$ on $N$ points satisfies $\sum_i|\hat p(i)-p(i)|\le\varepsilon$ with probability greater than $1-\delta$ .

Significance

The result. The bound $NAT$ does not depend on $L$ . However long the agent runs, only a fixed number of its steps fail to be $T$ -step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has $\Omega(NAT)$ such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.

Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:

a verified finite-horizon dynamic-programming layer (backward recursions, optimal $T$ -step values as suprema);
a simulation lemma in $\ell_1$ ;
a concentration bound for empirical distributions whose sample size is linear in $N$ ;
an explicit construction of an online exploration algorithm, with a counting argument about its run.

The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form $P(|\hat p_i-p_i|>\alpha p_i)\le2e^{-\alpha^2p_im/2}$ . This form fails for the upper tail when $\alpha>1$ , so the pinned statement needs a different argument.

Difficulty

The algorithm must be fixed before the MDP. It knows nothing about $f$ or $r$ beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full $T$ -step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most $T$ steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that $U^*_{t,M}$ is a supremum over all $T$ -step policies, so the comparison has to go through $M_K$ for every competing policy, not only the planner's.

Formalization scope

Model. $S$ and $A$ are finite types, $A$ nonempty; $N=|S|$ and $A=|A|$ . Rewards are deterministic, with $0\le r\le1$ a hypothesis of every statement. Transition models are IsTransitionKernel functions $P(s'\mid s,a)$ .
Normalization and time. Values carry the factor $1/T$ , so they lie in $[0,1]$ ; epochs are 0-based. $T$ -step policies are functions $\mathbb N\to S\to A$ , entered into the canonical stochastic $T$ -epoch layer as indicator policies. $U^*_{t,M}$ is the supremum over these policies, which is bounded under the hypotheses.
Online model. In the online model the algorithm has type List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. $U_{\mathcal A}(c_t)$ is the realised normalized sum up to the end time, and $U^*(c_t)$ is the backward recursion $W_{t'-t}(s_t)$ , which is the supremum over algorithms by the Markov property. The count runs over $t<L$ for every $L$ .
Corrections to the printed text. Corollary 8.4.5 is stated for $t<T$ , where its quantities are defined; the printed range is $t\le T$ . Lemma 8.5.5 carries an explicit sample size in place of $O(\cdot)$ .

Four formalizations would make the goal trivial or false, and each is excluded:

quantifying the algorithm after the MDP, which lets it read $f$ and $r$ ;
giving the algorithm a type that takes $f$ or $r$ as an argument;
defining $U^*$ as a junk real supremum;
hiding rewards from the observed path, which makes the statement false.

Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the $\ell_1$ concentration bound. Contributions to any of these are useful independently of the goal.

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/
R. I. Brafman and M. Tennenholtz, R-max — a general polynomial time algorithm for near-optimal reinforcement learning, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/brafman02a.html
M. Kearns and S. Singh, Near-optimal reinforcement learning in polynomial time, Machine Learning 49, 2002. https://doi.org/10.1023/A:1017984413808
A. L. Strehl, L. Li and M. L. Littman, Reinforcement learning in finite MDPs: PAC analysis, Journal of Machine Learning Research 10, 2009. https://jmlr.org/papers/v10/strehl09a.html

14 thms2 active usersReviewed

Machine Learning Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning III: Non-Stationary Approximate Policy Iteration Is Within 2T Times the Regression Error Averaged over Any Competitor's State-Time DistributionTextbook

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

16 thms2 active usersReviewed

Completed

Machine Learning Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning II: The Gradient of the Normalized Discounted Value Is the Sum over Actions of ∇π·Q under the Discounted Future State DistributionTextbook

Why the gradient of the value matters

Policy gradient methods search a parameterized family of stochastic policies $\pi(a\mid s,\theta)$ , $\theta\in\mathbb R^k$ , by following the gradient of the policy's performance. They are the standard tool when the state space is too large for tabular dynamic programming and when a compact policy class (a neural network, a linear softmax) is easier to represent than a value function. Every such method rests on one identity: a formula for the gradient of the value with respect to $\theta$ that involves only quantities of the current policy, so that it can be estimated from the policy's own trajectories.

Chapter 4 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), states this identity in two settings, the $T$ -epoch undiscounted setting and the $\gamma$ -discounted setting, both in the thesis's normalized convention, in which values lie in $[0,1]$ . The thesis then uses the formula to analyse how many samples a gradient estimate needs (§4.2.3), and in §5.4.2 rewrites it in terms of advantages to explain why gradient methods can stall far from optimal: the gradient weights advantages by the current policy's state distribution, not by the distribution of an optimal policy.

Timeline:

1992: R. J. Williams introduces the likelihood-ratio (REINFORCE) estimator for episodic tasks.
2000: Sutton, McAllester, Singh and Mansour state the policy gradient theorem with function approximation, for discounted and average-reward criteria (NeurIPS 1999 proceedings, 2000); Konda and Tsitsiklis give actor-critic counterparts.
2001: Baxter and Bartlett analyse biased gradient estimation in the infinite-horizon setting.
2003: Kakade's thesis restates both theorems for normalized values, introduces the future state-time distribution $d_{\pi,s_0}$ for non-stationary $T$ -epoch policies, and draws the "mismeasure" consequence.

Setting

A finite MDP has a finite state set $S$ , a finite nonempty action set $A$ , a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ .

$T$ -epoch case. Epochs are $t\in\{0,\dots,T-1\}$ , $T\ge1$ . A non-stationary policy chooses $a$ at epoch $t$ in state $s$ with probability $\pi(a\mid s,t)$ . Starting from $s_0$ , $\Pr(s_t=s\mid\pi,s_0)$ is the probability of being in $s$ at epoch $t$ . The normalized $t$ -value is

V_{\pi,t}(s)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\,\Big|\,\pi,s_t=s\Big],\qquad V_\pi=V_{\pi,0},

the $t$ 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')]$ with $V_{\pi,T}=0$ , and the future state-time distribution on $S\times\{0,\dots,T-1\}$ is $d_{\pi,s_0}(s,t)=\frac1T\Pr(s_t=s\mid\pi,s_0)$ .

Discounted case. For a stationary policy $\pi(a\mid s)$ and $0\le\gamma<1$ , the normalized value, state-action value, advantage and discounted future state distribution are

V_{\pi,\gamma}(s)=(1-\gamma)\,\mathbb E\Big[\sum_{\tau\ge0}\gamma^\tau r(s_\tau,a_\tau)\,\Big|\,\pi,s_0=s\Big],\qquad Q_{\pi,\gamma}(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[V_{\pi,\gamma}(s')],

A_\pi(s,a)=Q_{\pi,\gamma}(s,a)-V_{\pi,\gamma}(s),\qquad d_{\pi,s_0,\gamma}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,s_0).

A parameterized policy is a family $\pi(a\mid s,\theta)$ (resp. $\pi(a\mid s,t,\theta)$ ) of policies indexed by $\theta\in\mathbb R^k$ , each entry differentiable in $\theta$ ; $\nabla$ is the gradient in $\theta$ .

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

\nabla V_{\pi,\gamma}(s_0)=\frac1{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\Big[\sum_a\nabla\pi(a\mid s,\theta)\,Q_{\pi,\gamma}(s,a)\Big].

The statement asserts that $\theta\mapsto V_{\pi_\theta,\gamma}(s_0)$ is differentiable at the given parameter and that its derivative is the right-hand side. It is the thesis's version of the Sutton–McAllester–Singh–Mansour theorem, and the result the rest of the thesis's discussion of gradient methods builds on.

Milestones

Value representations (p. 47): $V_\pi(s_0)=\mathbb E_{(s,t)\sim d_{\pi,s_0}}\mathbb E_{a\sim\pi(\cdot\mid s,t)}[r(s,a)]$ and $V_{\pi,\gamma}(s_0)=\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\mathbb E_{a\sim\pi(\cdot\mid s)}[r(s,a)]$ .
Theorem 4.2.3 (p. 48), the $T$ -epoch gradient:

\nabla V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi,s_0}}\Big[\sum_a\nabla\pi(a\mid s,t,\theta)\,Q_{\pi,t}(s,a)\Big].

The advantage form (§5.4.2, p. 66), with $A=|A|$ the number of actions:

\nabla V_\pi(s_0)=\frac{A}{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0}}\,\mathbb E_{a\sim\mathrm{Uniform}}\big[A_\pi(s,a)\,\nabla\pi(a\mid s,\theta)\big].

Significance

The result. The gradient formula contains no derivative of the state distribution: the effect of $\theta$ on which states are visited cancels, and the gradient is an expectation over states drawn from the current policy, weighted by a sum over actions. This is what makes Monte Carlo and actor-critic estimators possible, and it is the reason the thesis's sample-size analysis of §4.2.3 has no dependence on the size of the state space. The advantage form makes the limitation equally explicit: a small gradient certifies small advantages only under $d_{\pi,s_0}$ , while the performance difference lemma (Lemma 5.2.1) shows that closeness to optimal is governed by advantages under $d_{\pi^*,s_0}$ . That gap motivates the conservative policy iteration of Chapter 7.

Formalizing it. The theorems are proved in the thesis and in the cited literature; none of them is machine-checked in this normalized convention. The platform has a proved finite-horizon policy gradient theorem for a scalar parameter, a stationary policy and unnormalized values (policy_gradient_discounted_finite, policy_gradient_finite_horizon), and a posed direct-parameterization gradient for Agarwal et al.'s unnormalized discounted value (PolicyGradTheory.ProjGA.direct_gradient). This mission adds the multi-parameter statements, the non-stationary $T$ -epoch version with its state-time distribution, and the infinite-horizon discounted version, where differentiability of an infinite series must be established rather than computed from a finite recursion.

Difficulty

In the $T$ -epoch case the value is a finite polynomial in the policy entries, and the work is bookkeeping: unrolling the backward recursion for $V_{\pi,t}$ against the forward recursion for $\Pr(s_t=\cdot)$ so that the terms involving $\nabla V_{\pi,t+1}$ telescope. In the discounted case the obvious route, differentiating the recursion $V=(1-\gamma)r_\pi+\gamma P_\pi V$ term by term and recursing forever, presupposes that $\theta\mapsto V_{\pi_\theta,\gamma}(s)$ is differentiable, which the thesis's proof takes for granted. The value is an infinite series in $t$ , so that differentiability is a genuine part of the claim, and the resulting formula must be matched with $d_{\pi,s_0,\gamma}$ and $Q_{\pi,\gamma}$ , which are themselves defined as infinite series.

Formalization scope

Finite $S$ and $A$ (Fintype), $A$ nonempty; transition kernel IsTransitionKernel P; rewards in $[0,1]$ as a standing hypothesis of every statement; $0\le\gamma<1$ ; $T\ge1$ . The thesis's later chapters allow infinite state spaces; this mission is finite.
Normalization exactly as in the thesis: $T$ -epoch values and $d_{\pi,s_0}$ carry $1/T$ , discounted values and $d_{\pi,s_0,\gamma}$ carry $1-\gamma$ . Hence the factors $T$ and $1/(1-\gamma)$ in the gradient formulas.
The discounted layer is the published normalized model ApproxOptRL.Shared.Model (value, qValue, advantage, futureStateDist; $d_{\pi,s_0,\gamma}$ is futureStateDist at the point mass on $s_0$ ). The $T$ -epoch layer is defined in this mission (TEpoch): 0-based epochs, tValue by backward recursion, tQValue, stateDist, stateTimeDist.
Parameters live in EuclideanSpace ℝ (Fin k). Every statement assumes that $\pi(\cdot\mid s,\theta)$ (resp. $\pi(\cdot\mid s,t,\theta)$ for $t<T$ ) is a probability distribution for every $\theta$ , and that each entry is differentiable at the parameter $\theta_0$ ("the derivatives $\nabla\pi$ exist", p. 48). Differentiability of the value is not assumed.
Gradients are stated with HasFDerivAt: the value map has the right-hand side as its Fréchet derivative at $\theta_0$ . A statement with fderiv of the value alone, or with a policy that does not depend on $\theta$ , would reduce to $0=0$ and is ruled out.
Expectations over finite sets are finite sums; the uniform expectation over actions is $\frac1{|A|}\sum_a$ .
Contributions welcome: the forward/backward recursion identity for $T$ -epoch values, summability and differentiability of the discounted series, and the closed form of $V_{\pi,\gamma}$ via $(I-\gamma P_\pi)^{-1}$ ; all are reusable by the other missions of this series.

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/
R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 229–256, 1992. https://doi.org/10.1007/BF00992696
J. Baxter, P. L. Bartlett, Infinite-Horizon Policy-Gradient Estimation, Journal of Artificial Intelligence Research 15, 319–350, 2001. https://doi.org/10.1613/jair.806
V. R. Konda, J. N. Tsitsiklis, Actor-Critic Algorithms, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/6449f44a102fde848669bdd9eb6b76fa-Abstract.html

9 thms2 active usersReviewed

Completed

Machine Learning Optimization Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning I: Approximate Policy Iteration with Max-Norm Evaluation Error ε Is Eventually Within 2ε/(1−γ)² of OptimalTextbook

Motivation

Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.

Setting

A finite discounted Markov decision process consists of a finite set of states $S$ , a finite nonempty set of actions $A$ , a transition kernel $P(s'\mid s,a)$ (for every $(s,a)$ a probability distribution over $S$ ), a deterministic reward $r(s,a)\in[0,1]$ , and a discount factor $0\le\gamma<1$ . A policy $\pi(a\mid s)$ is a probability distribution over actions for every state; a deterministic policy is a map $f:S\to A$ , identified with the policy that plays $f(s)$ with probability one.

Values are normalized: the value of $\pi$ at $s$ 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],

and 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')]$ . With rewards in $[0,1]$ , every value lies in $[0,1]$ . An optimal policy $\pi^*$ has $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and state $s$ ; write $V^*=V_{\pi^*}$ and $Q^*=Q_{\pi^*}$ . The max norm is $\|x\|_\infty=\max_s|x(s)|$ on state vectors and $\max_{s,a}|x(s,a)|$ on state-action arrays.

The backup operator is $[BJ](s)=\max_a\big((1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[J(s')]\big)$ . A deterministic policy $f$ is greedy with respect to $Q$ if $f(s)\in\arg\max_a Q(s,a)$ for every $s$ .

$\gamma$ -approximate value iteration produces vectors $J_0=0,J_1,J_2,\dots$ with $\|J_t-BJ_{t-1}\|_\infty\le\varepsilon$ , and greedy policies $\pi_t$ for the lookahead $(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[J_t(s')]$ .
$\gamma$ -approximate policy iteration starts from any deterministic $\pi_0$ , forms an estimate $\tilde Q_t$ of $Q_{\pi_t}$ with $\|\tilde Q_t-Q_{\pi_t}\|_\infty\le\varepsilon$ , and takes $\pi_{t+1}$ greedy with respect to $\tilde Q_t$ .

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

\limsup_{t\to\infty}\|V^*-V_{\pi_t}\|_\infty\le\frac{2\varepsilon}{(1-\gamma)^2}.

The policies need not converge; the statement bounds where they end up.

Milestones

Theorem 3.1.1: if $\|\tilde Q-Q^*\|_\infty\le\varepsilon$ and $\pi$ is greedy for $\tilde Q$ , then $V_\pi(s)\ge V^*(s)-\frac{2\varepsilon}{1-\gamma}$ for all $s$ .
Lemma 3.2.3: $\|V^*-V_{\pi_{t+1}}\|_\infty\le\gamma\|V^*-V_{\pi_t}\|_\infty+\frac{2\varepsilon}{1-\gamma}$ .
Rate of approximate policy iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\gamma^t+\frac{2\varepsilon}{(1-\gamma)^2}$ .
Contraction of the backup (p. 26): $\|BJ-BJ'\|_\infty\le\gamma\|J-J'\|_\infty$ .
Approximate value iteration (p. 40): $\|V^*-J_t\|_\infty\le\gamma^t+\frac{\varepsilon}{1-\gamma}$ .
Rate of approximate value iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\frac{2\gamma^t}{1-\gamma}+\frac{2\varepsilon}{(1-\gamma)^2}$ .
Theorem 3.2.1: the same lim sup bound $\frac{2\varepsilon}{(1-\gamma)^2}$ for approximate value iteration.

Significance

The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of $\varepsilon$ in max norm costs at most $2\varepsilon/(1-\gamma)^2$ in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor $2\varepsilon/(1-\gamma)$ of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon $1/(1-\gamma)$ in the limit bound are the reason the thesis turns to other error measures in later chapters.

All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor $\gamma$ to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.

Difficulty

Approximate policy iteration is not monotone: with evaluation errors, $V_{\pi_{t+1}}$ can be worse than $V_{\pi_t}$ at some states, so the argument of exact policy iteration, which uses $V_{\pi_{t+1}}\ge V_{\pi_t}$ everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value $V_\pi$ is defined as an infinite series, so its Bellman equation $V_\pi(s)=Q_\pi(s,\pi(s))$ , the optimality equation $V^*=BV^*$ and the bound $0\le V_\pi\le1$ have to be derived from that definition before any of the recursions can be run.

Formalization scope

The model is the published normalized model ApproxOptRL.Shared.Model: value P r γ π is $V_\pi$ (defined as $(1-\gamma)$ times a tsum), qValue is $Q_\pi$ . $S$ and $A$ are finite types, $A$ nonempty; $P$ satisfies IsTransitionKernel; every statement assumes $0\le r\le1$ and $0\le\gamma<1$ .
The optimal policy is a binder $\pi^*$ with IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.
Policies of the runs are deterministic, S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.
The runs are sequences indexed by ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices $t+1$ and $t$ .
$\|\cdot\|_\infty$ is Mathlib's sup norm on S → ℝ and S → A → ℝ.
The lim sup statements are in $\varepsilon$ – $N$ form: for every $\delta>0$ the bound plus $\delta$ holds eventually.
Ruled out: the accuracy hypothesis is stated against $Q_{\pi_t}$ , the value of the current policy, not against $Q^*$ , and the greedy relation genuinely constrains $\pi_{t+1}$ ; with either changed, the hypotheses would be unsatisfiable or the policies unconstrained and the theorem empty.
Infrastructure needed and reusable beyond this mission: the Bellman equation of the normalized value for indicator policies, $V^*=BV^*$ , monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound $0\le V_\pi\le1$ . Contributions of these lemmas are welcome.

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/
D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996. ISBN 1-886529-10-8.
S. P. Singh and R. C. Yee, An upper bound on the loss from approximate optimal-value functions, Machine Learning 16 (1994), 227–233. https://doi.org/10.1007/BF00993104
S. M. Kakade and J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005

13 thms2 active usersReviewed

Machine Learning Optimization Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

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:

The ExactPolicyChooser returns $\pi'\in\arg\max_{h\in\Pi}\mathbb Q_\pi(\mu,h)$ .
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'$ .
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

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).

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$ .
Domination of the start distribution (p. 88): $d_{\pi,\mu}\ge\mu/H$ .
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)$ .
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.

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

12 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Algorithms for Scheduling Runway Operations Under Constrained Position Shifting 1: Dynamic Programming on the CPS Network Gives the Minimum MakespanResearch Paper

Motivation

A busy runway is the bottleneck of an airport, and the order in which arriving or departing aircraft use it determines how many operations fit into an hour. Consecutive aircraft must be spaced by minimum separations that depend on both aircraft (a light aircraft behind a heavy one needs a long gap because of wake turbulence), so reordering the first-come-first-served (FCFS) queue can raise throughput considerably. Unrestricted reordering is unacceptable in practice: it makes the controllers' job harder and can push one aircraft to the back of the queue indefinitely. Following Dear (1976), constrained position shifting (CPS) allows each aircraft to move at most $k$ positions away from its FCFS position, with $k$ between 1 and 3 in practice.

Earlier algorithms for CPS either exploited a small number of aircraft types and ignored time windows and precedence constraints (Psaraftis 1980), or needed exponentially many parallel processors (Trivizas 1998), and Carr (2004) conjectured that runway scheduling under CPS has exponential complexity in general. Balakrishnan and Chandran (Oper. Res. 58(6), 2010) showed that, for fixed $k$ , the problem with time windows and precedence constraints is solved by dynamic programming on a network whose size is linear in the number of aircraft. This mission formalizes the core of that result: the network, its precedence pruning, and the dynamic program for the minimum makespan.

Setting

There are $n\ge 1$ aircraft, labelled $0,\dots,n-1$ in FCFS order, and the landing positions are also $0,\dots,n-1$ . An instance consists of

the maximum position shift $k\in\mathbb N$ ;
separations $\delta_{ab}\ge 0$ , the minimum time between a leading aircraft $a$ and a trailing aircraft $b$ , satisfying the triangle inequality $\delta_{ac}\le\delta_{ab}+\delta_{bc}$ (which holds for wake-vortex separations in arrivals-only or departures-only operation);
a time window $[e(a),l(a)]$ for each aircraft;
a finite set of precedence pairs $(x,y)$ of distinct aircraft, meaning that $x$ lands before $y$ .

A $k$ -CPS sequence is a bijection $\sigma$ from positions to aircraft with $|\sigma(p)-p|\le k$ for all $p$ . A feasible schedule is such a $\sigma$ with landing times $t_p$ such that $e(\sigma(p))\le t_p\le l(\sigma(p))$ , $\delta_{\sigma(p)\sigma(q)}\le t_q-t_p$ for all positions $p<q$ , and every precedence pair is respected. The makespan is $t_{n-1}$ , the landing time of the last aircraft.

The CPS network has stages $p=1,\dots,n$ . A node of stage $p$ is a list of $\min\{2k+1,p\}$ distinct aircraft occupying the positions that end at $p-1$ , each within $k$ of its FCFS position; its last entry is its final aircraft. An arc joins a stage- $p$ node $i$ to a stage- $(p+1)$ node $j$ when the first $\min\{2k,p\}$ entries of $j$ are the last $\min\{2k,p\}$ entries of $i$ . A source-sink path picks one node per stage, joined by arcs, and its sequence puts the final aircraft of the stage- $(q+1)$ node at position $q$ . The pruned network $G$ deletes the nodes that violate a precedence pair $(x,y)$ : those containing $y$ before $x$ , or $y$ at a position less than $x-k$ , or $x$ at a position greater than $y+k$ .

On $G$ , with $e(j),l(j)$ the window of the final aircraft of $j$ , $\delta_i(j)$ the separation between the final aircraft of $i$ and $j$ , and $P(j)$ the predecessors of $j$ , the dynamic program is $T^*(j)=e(j)$ at stage 1 and

T^*(j)=\max\Big\{e(j),\ \min_{i\in P(j):\,T^*(i)\le l(i)}\big(T^*(i)+\delta_i(j)\big)\Big\}\qquad(1)

with $\min\emptyset=+\infty$ .

Formalization targets

Goal: §4.1, the minimum makespan rule

\exists\ \text{feasible schedule}\iff \exists\, j\in G_n:\ T^*(j)\le l(j),

\min\{\text{makespan of a feasible schedule}\}=\min\{T^*(j): j\in G_n,\ T^*(j)\le l(j)\},

where $G_n$ is stage $n$ of $G$ ; the second identity is stated as " $\tau$ is the least makespan iff $\tau$ is the least admissible $T^*(j)$ " for every real $\tau$ .

Milestones

Theorem 1. $\sigma$ is a $k$ -CPS sequence iff it is the sequence of a source-sink path of the CPS network.
Lemma 1 (Case I). For $a<b$ , a path whose sequence puts $a$ after $b$ has a node containing $b$ before $a$ .
Lemma 2 (Case II). For $a<b$ , in the position-constrained network, a path whose sequence puts $a$ before $b$ has a node containing $a$ before $b$ .
§3.1 conclusion. The source-sink paths of $G$ are exactly the $k$ -CPS sequences respecting all precedence pairs.
Lemma 3. For every node $j$ of $G$ , $T^*(j)$ is the earliest landing time of the final aircraft of $j$ over all partial schedules ending at $j$ , and $+\infty$ exactly when there is none.

Significance

The network turns a search over permutations into a shortest-path-like computation over $O(n(2k+1)^{2k+1})$ nodes, so for the small values of $k$ used in practice the minimum makespan with time windows and precedence constraints is computed in time linear in $n$ . The same network underlies the paper's algorithms for total delay (§5.2) and, in a time-expanded form, for arbitrary separable costs without the triangle inequality (§6).

The paper's proofs are short and informal. A formalization pins down exactly what $T^*(j)$ means (the paper describes it only as "arrival time of the final aircraft of node $i$ in an optimal solution"), makes precise which nodes the precedence pruning removes, and checks the correctness of the stage- $n$ rule. The result has not been machine-checked before.

Difficulty

Two features of the model make the correctness of the network nontrivial. First, a node records only a window of at most $2k+1$ consecutive positions, so nothing local prevents a path from using the same aircraft twice or omitting one; Theorem 1 asserts that the global sequence is nevertheless a permutation, and Lemmas 1 and 2 assert that precedence, a global property of the sequence, is detected inside single nodes. Second, the recursion (1) adds the separation only between consecutive aircraft, while feasibility constrains every pair of aircraft; the triangle inequality is what reconciles the two, and without it Lemma 3 fails.

The obvious reading of §4.1 also fails: taking the least $T^*(j)$ over all stage- $n$ nodes, as the paper prints, can select a node whose final aircraft lands after its latest time. The goal filters stage $n$ by $T^*(j)\le l(j)$ .

Formalization scope

All data are real numbers; aircraft and positions are Fin n, 0-based; stages are 1-based natural numbers; [NeZero n] encodes $n\ge 1$ . Separations are pairwise in the definition of feasibility, never only consecutive. The recursion takes values in WithTop ℝ, with $\top=+\infty$ ; optima are stated with IsLeast over sets of makespans, never with a real infimum. Precedence pairs are a Finset of ordered pairs of distinct aircraft, covering both of the paper's cases.

Explicit readings of loose phrases:

"corresponding source-sink path" (Theorem 1) is the path whose final aircraft, stage by stage, form the sequence, as defined in the proof;
"the values of $T^*(\cdot)$ " (Lemma 3) are earliest landing times over partial schedules ending at the node: paths in $G$ with times satisfying the windows of the earlier aircraft, the earliest time of the last one, and all pairwise separations;
"the minimum makespan is the lowest value of $T^*(\cdot)$ among all nodes in stage $n$ " is corrected to the nodes with $T^*(j)\le l(j)$ , which is the paper's own feasibility check;
the Case II position filter uses the printed rule ( $<b-k$ , $>a+k$ ).

Not formalized: running times (Proposition 1 and the $O(k)$ preprocessing remark), the predecessor pointers and tie-breaking that reconstruct an optimal sequence, the removal of nodes unreachable from the source or the sink (it does not change the set of source-sink paths), asymmetric shifts (§3.2) and disjoint time windows.

A formalization that defines feasibility with consecutive separations only, defines $T^*$ by the recursion and states Lemma 3 as an unfolding, or states Theorem 1 as "some CPS sequence exists iff some path exists" would be trivial; the statements here avoid all three.

The definitions (instance, $k$ -CPS sequences, the CPS network and its pruning) are shared with the two other missions of this series (total delay, discrete time) and may be consolidated later. Proofs of the milestones, and lemmas about the window structure of the network, are welcome.

Selected references

H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
H. N. Psaraftis, A Dynamic Programming Approach for Sequencing Groups of Identical Jobs, Operations Research 28(6), 1347–1359, 1980. https://doi.org/10.1287/opre.28.6.1347
R. G. Dear, The Dynamic Scheduling of Aircraft in the Near Terminal Area, MIT Flight Transportation Laboratory Report R76-9, 1976.
D. A. Trivizas, Optimal Scheduling with Maximum Position Shift (MPS) Constraints: A Runway Scheduling Application, Journal of Navigation 51(2), 250–266, 1998.
F. R. Carr, Robust Decision-Support Tools for Airport Surface Traffic, Ph.D. thesis, Massachusetts Institute of Technology, 2004.

8 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Algorithms for Scheduling Runway Operations Under Constrained Position Shifting 2: The Minimum Total Delay Is a Shortest Source-Sink Path in the CPS NetworkResearch Paper

Motivation

Runway capacity is the binding constraint at many busy airports. An aircraft landing or taking off behind another must wait a minimum separation time that depends on the two aircraft's weight classes, because of wake vortices; the US Federal Aviation Administration publishes these spacing requirements. Reordering aircraft changes the sum of the separations incurred and hence the delays, but unrestricted reordering is unacceptable to airlines and controllers: an aircraft that arrived early could be pushed to the end of the queue. Constrained position shifting (CPS), introduced by Psaraftis (1980) and used in the United States and Europe since, allows each aircraft to move at most $k$ positions from its first-come-first-served (FCFS) position.

Balakrishnan and Chandran (Operations Research 58(6), 2010) recast CPS scheduling as dynamic programming on a layered network, the CPS network, whose size is polynomial in the number of aircraft $n$ for fixed $k$ . Their §4 minimizes the makespan (the landing time of the last aircraft). §5.2 minimizes the total delay, equivalently the average delay, which measures passenger and airline cost more directly. This mission formalizes §5.2.

Setting

There are $n$ aircraft labelled $1,\dots,n$ in FCFS order, a maximum position shift $k\in\mathbb N$ , separations $\delta_{ab}\ge 0$ (the minimum time between leading aircraft $a$ and trailing aircraft $b$ ), and a finite set of precedence pairs $(x,y)$ with $x\ne y$ , meaning that $x$ must land before $y$ . The separations satisfy the triangle inequality $\delta_{ac}\le\delta_{ab}+\delta_{bc}$ , as wake-vortex separations do for arrivals-only or departures-only operations.

A $k$ -CPS sequence is a permutation $\sigma$ of the aircraft (position $p$ receives aircraft $\sigma(p)$ ) with $|\sigma(p)-p|\le k$ for every $p$ . A feasible schedule is a $k$ -CPS sequence that places $x$ before $y$ for each precedence pair, together with landing times $t_1,\dots,t_n$ (by position) such that

t_p\ge 0,\qquad t_q-t_p\ge\delta_{\sigma(p)\sigma(q)}\quad(p<q).

There are no time windows. Its total delay is $t_1+\dots+t_n$ , measured from time $0$ , at which all aircraft are available.

The CPS network has stages $1,\dots,n$ . A node of stage $p$ is a sequence of $\min\{2k+1,p\}$ distinct aircraft that can occupy positions $p-\min\{2k+1,p\}+1,\dots,p$ (each within $k$ of its position). Its last aircraft is its final aircraft. An arc joins a stage- $p$ node $i$ to a stage- $(p+1)$ node $j$ when the sequences overlap: the first $\min\{2k,p\}$ aircraft of $j$ are the last $\min\{2k,p\}$ aircraft of $i$ . A source-sink path picks one node per stage, and its sequence assigns position $p$ to the final aircraft of the stage- $p$ node. Precedence is incorporated by deleting every node that places $y$ before $x$ for some pair $(x,y)$ , or that places an aircraft outside the positions a pair allows it (§3.1). The result is the pruned network $G$ . For nodes $i,j$ , $\delta_i(j)$ is the separation between their final aircraft.

For a node $j$ in stage $p$ and times $t_1,\dots,t_p$ along a path to $j$ , the paper uses the partial objective

\theta_j(p)=t_1+\dots+t_{p-1}+(n-p+1)\,t_p .

Formalization targets

Goal: the shortest-path equivalence (§5.2, p. 1656)

Give the arc $(i,j)$ from stage $p-1$ to stage $p$ the distance $(n-p+1)\delta_i(j)$ , and source and sink arcs distance $0$ . Then a feasible schedule exists if and only if $G$ has a source-sink path, and

\min_{(\sigma,t)\ \text{feasible}}\ \sum_{p=1}^{n}t_p\;=\;\min_{v\ \text{source-sink path of }G}\ \sum_{p=2}^{n}(n-p+1)\,\delta_{v_{p-1}}(v_p),

where each minimum exists exactly when the other does.

Milestones

Theorem 1 with Lemmas 1–2 (pp. 1652–1654): the source-sink paths of $G$ are exactly the $k$ -CPS sequences respecting the precedence pairs.
Proposition 2 (p. 1656): in a schedule of minimum total delay, $t_p-t_{p-1}=\delta_{\sigma(p-1)\sigma(p)}$ for every $p\ge 2$ .
Proposition 3 (p. 1656): all paths from the source to a node lying on some source-sink path contain the same set of aircraft.
The recursion of §5.2 (p. 1656): with $\theta^*_j(p)$ the minimum of $\theta_j(p)$ over partial schedules ending at $j$ , $\theta^*_j(1)=0$ and

\theta^*_j(p)=\min_{i\in P(j)}\big(\theta^*_i(p-1)+(n-p+1)\,\delta_i(j)\big),

where $P(j)$ is the set of predecessors of $j$ in $G$ .

Significance

The result turns a sequencing problem over up to $n!$ orders into a shortest-path computation on a directed acyclic graph with $O(n(2k+1)^{2k+1})$ nodes, and it does so while respecting precedence constraints, which earlier CPS algorithms (Psaraftis 1980; Trivizas 1998) could not handle. It is the average-delay counterpart of the makespan algorithm of §4 and shares its network. The same network carries the discrete-time models of §6.

The paper's proof of the equivalence is one sentence ("follows from properties of shortest paths and is omitted here"). Propositions 2 and 3 are proved in a few lines, and Theorem 1 by an argument about windows of $2k+1$ consecutive positions. None of these results has a machine-checked proof. A formal development makes explicit the conventions the prose leaves implicit (the time origin, pairwise separations, which nodes Proposition 3 refers to) and checks that the recursion and the shortest-path value really compute the minimum total delay.

Difficulty

The arc distances weight the separation into stage $p$ by $n-p+1$ , the number of aircraft whose landing it delays. The equivalence needs two directions. A path's length must be the total delay of the schedule that lands each aircraft at its predecessor's time plus the separation, and that schedule must satisfy every pairwise separation, not only the consecutive ones; this is where the triangle inequality enters. Conversely, every feasible schedule must have total delay at least the length of its sequence's path, and every feasible sequence must be a path of $G$ . The last point is Theorem 1 with precedence pruning: a node sees only $2k+1$ consecutive positions, so detecting a violated precedence pair inside one node requires the position filter of §3.1 for pairs that reverse FCFS order. Proposition 3 is false for nodes that lie on no source-sink path, which the printed statement does not exclude.

Formalization scope

Aircraft and positions are Fin n, 0-based, and stages are 0-based natural numbers, so the arc into stage $s$ has distance $(n-s)\delta_i(j)$ . Separations are real, nonnegative and satisfy the triangle inequality; feasibility requires them between every pair of positions. Landing times are real and nonnegative. The paper fixes no time origin, but its path length equals the total delay exactly when delays are measured from $0$ , and without a lower bound on the times the objective has no minimum. Minima are stated with IsLeast on sets of values, never with a real infimum. Feasibility and the existence of a path are stated separately, because the equality of least elements alone does not force them to exist.

The following loose phrases are given explicit readings. "In an optimal solution" (Proposition 2) means a feasible schedule whose total delay is at most that of every feasible schedule. "The CPS network" in Proposition 3 means nodes lying on a source-sink path, stated for the network without precedence pruning, which also covers the pruned one. " $\theta^*$ " means the least element of the set of values of $\theta_j(p)$ over partial schedules ending at $j$ , and the printed $\theta^*_j(s)$ is read as $\theta^*_j(p)$ . The boundary value $\theta^*_j(1)=0$ is not printed and is stated explicitly. Precedence pruning uses the printed Case II rule. Running times (the $O(n(2k+1)^{2k+2})$ bound) are not formalized.

A trivializing formalization would require separations only between consecutive aircraft, define the minimum by the recursion itself, or use a network whose nodes need not be distinct or admissible. Here the minimum is defined directly over feasible schedules, separations are pairwise, and the nodes are checked against the paper's Figure 1 (stage sizes 2, 4, 7, 14, 14, 7 and 13 paths for $n=6$ , $k=1$ ).

The development needs finite sums, permutations of Fin n and lists. The network layer (stages, arcs, precedence pruning, Theorem 1) is shared with the makespan and discrete-time missions of this series and reusable for any CPS objective. Proofs of any milestone, alternative proofs of the goal, and generalizations (asymmetric shifts, §3.2) are welcome.

Selected references

H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
H. N. Psaraftis, A Dynamic Programming Approach for Sequencing Groups of Identical Jobs, Operations Research 28(6), 1347–1359, 1980. https://doi.org/10.1287/opre.28.6.1347
R. G. Dear, Y. S. Sherif, An Algorithm for Computer Assisted Sequencing and Scheduling of Terminal Area Operations, Transportation Research Part A 25(2–3), 129–139, 1991.
D. A. Trivizas, Optimal Scheduling with Maximum Position Shift (MPS) Constraints: A Runway Scheduling Application, Journal of Navigation 51(2), 250–266, 1998.
R. de Neufville, A. Odoni, Airport Systems: Planning, Design, and Management, McGraw-Hill, 2003.

6 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

On the Structure of Lost-Sales Inventory Models 3: If Demand Increases in the Convex Order, the Optimal Lost-Sales Cost f̄_t(v; φ) Is Nondecreasing in φResearch Paper

Motivation

In the periodic-review inventory model with lost sales, demand that cannot be met from stock is lost rather than backordered. With a positive order lead time $L$ the state of the system is a vector of length $L$ : on-hand stock plus the $L-1$ orders still in the pipeline. This model is standard in retail, where a customer facing an empty shelf buys elsewhere. Its optimal policy is not a base-stock policy and depends on the whole pipeline vector, which makes it much harder to analyse than the backorder model.

A basic question for any stochastic inventory model is how its optimal cost responds to uncertainty in demand. For the backorder model it is classical that more variable demand costs more (Song 1994). Zipkin's paper (Oper. Res. 56(4), 2008, 937–944) recasts the lost-sales model in a transformed state in which the optimal cost functions are L $^\natural$ -convex. Its §5 uses this structure to prove the lost-sales analogue: if demand becomes more variable in the convex order, the optimal cost does not decrease. The paper presents this as new in the lost-sales setting.

Timeline of the structural results the mission rests on:

1958: Karlin and Scarf analyse the lost-sales model with lead time one and show that the optimal order decreases in the on-hand stock, with sensitivity less than one.
1969: Morton extends these monotonicity and bounded-sensitivity properties to general lead times and derives bounds on the optimal order.
2008: Zipkin reproves these properties through L $^\natural$ -convexity in the transformed state (Theorem 4) and adds the parametric result of §5 (Theorem 11).

Setting

The order lead time is a positive integer $L$ . The cost factors are the unit procurement cost $c$ , the unit holding cost $\hat h$ , the unit lost-sales penalty $p$ and the discount factor $\gamma$ . Demands in different periods are independent and nonnegative, with a common law. The paper treats states and orders as continuous.

Transformed state. A state is a vector $v=(v_0,\dots,v_{L-1})$ , where $v_l$ is the stock on hand plus all orders due to arrive $l$ or more periods hence, and $v_L=0$ by convention. So $v_0$ is the inventory position and $v_0-v_1$ is the stock on hand. The state space is

V=\{v\in\mathbb R^L:\ v_0\ge v_1\ge\cdots\ge v_{L-1}\ge0\}.

The action is $\zeta=-z\le0$ , where $z\ge0$ is the order quantity, and $e$ is the all-ones vector. After demand $d$ , the next state is

v_+=\big([v_0-v_1-d]^++v_1,\ v_2,\ \dots,\ v_{L-1},\ 0\big)-\zeta e.

Costs and recursion. The end-of-period holding and penalty cost is $\hat q(u)=\hat hu^++pu^-$ , and its expectation given on-hand stock $y$ is $\hat q^0(y)=E[\hat q(y-d)]$ . The optimal cost functions satisfy

\bar g_t(v,\zeta)=-\gamma^Lc\zeta+\hat q^0(v_0-v_1)+\gamma E[\bar f_{t+1}(v_+)],\qquad \bar f_t(v)=\min_{\zeta\le0}\bar g_t(v,\zeta),

with $\bar f_{T+L+1}=0$ . This is the paper's recursion (1)–(2), written in the state $v$ .

Program (4). Fix a demand $d$ . Choosing the next stock level $v_+$ , with $-d\le v_+-v_0\le0$ and $v_+\ge v_1$ , gives

\bar\kappa_t(v,\zeta\mid d)=\min_{v_+}\Big\{\hat h(v_+-v_1)+p(v_+-v_0+d)+\gamma\bar f_{t+1}\big[(v_+,v_2,\dots,v_{L-1},0)-\zeta e\big]\Big\}.

Here $v_+-v_1$ is the leftover stock and $d-(v_0-v_+)$ the unmet demand.

Parametric demand. The demand $d(\phi)$ depends on a real parameter $\phi$ , with law $\mu_\phi$ , and $\bar f_t(v;\phi)$ is the optimal cost under $\mu_\phi$ . A random variable $X$ is smaller than $Y$ in the convex order if $E\,g(X)\le E\,g(Y)$ for every convex $g:\mathbb R\to\mathbb R$ for which both expectations exist. This forces equal means and a variance that does not decrease.

Formalization targets

Goal: Theorem 11 (p. 941)

If $d(\phi)$ is increasing in $\phi$ with respect to the convex order, then for all $t$ and all $v\in V$ ,

\phi\le\phi'\ \Longrightarrow\ \bar f_t(v;\phi)\le\bar f_t(v;\phi').

Milestones, in attack order

Reformulation (proof of Theorem 4, p. 939). For $v\in V$ , $\zeta\le0$ , $d\ge0$ , the stock level $v_+=[v_0-v_1-d]^++v_1$ is optimal in program (4):

\bar\kappa_t(v,\zeta\mid d)=\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+).

Convexity of the optimal cost (Theorem 4, p. 939, with the remark on p. 938). $\bar f_t$ is convex on $V$ for every $t$ .
The key step (proof of Theorem 11, p. 941). If $F$ is convex and nonnegative on $V$ , then program (4) with continuation $F$ is jointly convex in $(v,\zeta,d)$ on $\{v\in V,\ \zeta\le0,\ d\ge0\}$ .
The induction step (proof of Theorem 11, p. 941). If $\bar f_{t+1}(v;\phi)$ is nondecreasing in $\phi$ on $V$ , then so is $\bar g_t(v,\zeta;\phi)$ for every $\zeta\le0$ .

Significance

Theorem 11 is a comparative-statics statement: replacing demand by a mean-preserving spread cannot lower the optimal cost from any starting state, at any horizon. It justifies valuing variance reduction in lost-sales systems, for example forecasting or demand pooling, without solving the high-dimensional dynamic program. The induction pattern of the proof transfers to other parametric questions about the model; §6 of the paper notes that the parametric analysis remains valid in several extensions.

The paper proves Theorem 11 in a few lines on top of Theorem 4. No machine-checked proof of the result or of its structural prerequisites is known: neither the lost-sales recursion in the transformed state nor its convexity is formalized. A complete development checks the measure-theoretic steps the paper leaves implicit: that the optimal costs are finite, the existence of the expectations, and the passage from convexity in $d$ on $[0,\infty)$ to the convex order's test functions on $\mathbb R$ .

Difficulty

The argument looks immediate: the costs are convex, so the convex order should apply directly. It does not. The function to which the convex order must be applied is the end-of-period cost as a function of demand. In recursion (1) that function is $\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+(d))$ , where the next state depends on $d$ through the kink $[v_0-v_1-d]^+$ . Convexity of $\bar f_{t+1}$ alone does not make this composition convex in $d$ . The paper avoids the issue by passing to program (4), where the amount of demand filled is a decision. That requires two facts: that selling as much as possible is optimal (milestone 1), and that the program is jointly convex in state, action and demand (milestone 3), which needs convexity of $\bar f_{t+1}$ on all of $V$ (milestone 2). A second difficulty is analytic: the optimal costs are defined by infima and expectations, and one must show that these are finite and integrable before any order comparison applies.

Formalization scope

Model. States are Fin L → ℝ with 0-based indices matching the paper. $v_L=0$ is the helper vext. $V$ is the set of antitone, nonnegative vectors.
Time. Data are stationary, so the optimal cost is indexed by the number of periods to go $k$ , with $\bar f=0$ at $k=0$ . The paper's "for all $t$ " is "for all $k$ ".
Demand. One-period demand has law $\mu$ , a probability measure on $\mathbb R$ with $\mu((-\infty,0))=0$ and finite mean. The finite mean is not in the paper; it is added so that $\hat q^0$ is finite.
Parametric family. A family $\mu_\phi$ , $\phi\in\mathbb R$ , with every hypothesis imposed for every $\phi$ . Every object depending on demand takes the law as an argument, so $\bar f_t(v;\phi)$ is fbar … (μ φ) k v.
Costs. "Unit cost" and "discount rate" are read as $c,\hat h,p\ge0$ and $0<\gamma\le1$ .
Minima. "Min" over orders is an infimum over $\zeta\le0$ , and program (4) is an infimum over the interval $[\max(v_0-d,v_1),v_0]$ . Lean's infimum is $0$ on sets that are unbounded below or empty. Nonnegative costs and demand keep the infima genuine, and the generic key-step milestone assumes the continuation is nonnegative.
Expectations. Bochner integrals.
Convex order. The platform definition StochasticOrders.Convex.ConvexOrder (Shaked–Shanthikumar (3.A.1)), applied to the identity on $(\mathbb R,\mu_\phi)$ . Equal means are a consequence and are not assumed.
Convexity milestone. Stated for the model's $\bar f$ only, not as "L $^\natural$ -convex implies convex" in general, which fails without regularity.

Ruled out. Value functions that collapse to a junk constant would make Theorem 11 trivially true. This is excluded because the recursion is defined, not assumed, and every cost and demand hypothesis is imposed for every $\phi$ . Replacing the convex order by "variance nondecreasing", by the increasing convex order, or by test functions convex only on $[0,\infty)$ changes the theorem and is not accepted.

Infrastructure and contributions. A complete development needs:

finiteness and integrability of the optimal costs;
convexity of partial infima over convex fibers;
monotone extension of a function convex on $[0,\infty)$ to all of $\mathbb R$ .

The model file is shared in shape with the series' missions 1 (L $^\natural$ -convexity) and 2 (policy bounds), and its convexity lemmas are reusable for other parametric comparisons of the lost-sales model. Proofs of any milestone, and alternative arguments that bypass program (4), are welcome.

Selected references

P. Zipkin, On the structure of lost-sales inventory models, Operations Research 56(4), 937–944, 2008. https://doi.org/10.1287/opre.1070.0482
S. Karlin, H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in Studies in the Mathematical Theory of Inventory and Production, Chapter 10, Stanford University Press, 1958.
T. E. Morton, Bounds on the solution of the lagged optimal inventory equation with no demand backlogging and proportional costs, SIAM Review 11, 572–576, 1969 (as cited in Zipkin 2008).
J.-S. Song, The effect of leadtime uncertainty in a simple stochastic inventory model, Management Science 40(5), 603–613, 1994. https://doi.org/10.1287/mnsc.40.5.603
D. Stoyan, Comparison Methods for Queues and Other Stochastic Models, Wiley, 1983.
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

8 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Old and New Methods for Lost-Sales Inventory Systems 1: Under Any Policy in Z(s) the State Enters X(s) and Never Leaves, So Every State Outside X(s) Is TransientResearch Paper

Why the lost-sales state space matters

The lost-sales inventory system with a positive lead time is one of the basic models of inventory theory. Demand that cannot be met from stock is lost rather than backlogged, and orders arrive a fixed number $L$ of periods after they are placed. Unlike the backlog system, where the inventory position is a sufficient one-dimensional state and a base-stock policy is optimal, the lost-sales system needs the whole pipeline of outstanding orders as its state, and its optimal policy has no simple form. Computing optimal policies by dynamic programming therefore runs into the size of an $L$ -dimensional state space.

Paul Zipkin's paper Old and New Methods for Lost-Sales Inventory Systems (Operations Research 56(5), 2008, doi:10.1287/opre.1070.0471) revisits this model, compares classical and new heuristics against optimal policies, and prepares the computation with a state-reduction result. Morton (1969, SIAM Review 11, Equation (83)) showed that under an optimal policy the state remains in a bounded set; Zipkin's §4 extends the argument to every policy in a class $Z(s)$ that contains the usual heuristics. This mission formalizes that section: the reduced state space $X(s)$ , the policy class $Z(s)$ , and Claim 1, which says that states outside $X(s)$ are transient.

Setting

Fix the lead time $L\ge 1$ . The state is the $L$ -vector $x=(x_0,\dots,x_{L-1})$ : $x_0$ is the stock on hand after this period's delivery, and $x_l$ ( $1\le l\le L-1$ ) is the order that arrives $l$ periods later, so $x_{L-1}$ is the most recent order. Given the state $x$ , an order $z\ge 0$ and a demand $d\ge 0$ , the next state is

x_+ = \bigl([x_0-d]^+ + x_1,\ x_2,\ \dots,\ x_{L-1},\ z\bigr),\qquad [a]^+=\max(a,0).

Demands in successive periods are independent with a common law $D$ on $[0,\infty)$ .

The pipeline partial sums are $v_l=\sum_{m=l}^{L-1}x_m$ for $l=0,\dots,L-1$ and $v_L=0$ ; $v_0$ is the inventory position and $v_{L-1}=x_{L-1}$ the most recent order. A level vector is $s=(s_0,\dots,s_L)$ with $s_0\ge s_1\ge\dots\ge s_L\ge 0$ . For a level vector $s$ ,

X(s)=\{x\ge 0:\ v_l\le s_l,\ l=0,\dots,L-1\},

and $Z(s)$ is the set of stationary policies $z$ (an order $z(x)\ge 0$ in each state $x\ge 0$ ) with $z(x)=0$ for $x\notin X(s)$ and $v_l+z(x)\le s_l$ for $l=0,\dots,L$ and $x\in X(s)$ . The vector base-stock policy with parameter $s$ is

z_s(x)=\bigl[\min\{s_l-v_l,\ l=0,\dots,L\}\bigr]^+,

equation (5) of the paper with a general $s$ in place of Morton's $\bar s$ . Under a stationary policy $z$ , from an initial state $x$ and along a demand path $(d_t)$ , the state process is $x_0=x$ , $x_{t+1}=(x_t)_+$ with order $z(x_t)$ and demand $d_t$ . In Lean these are next, v, IsLevelVector, Xs, Zs, vectorBaseStock and traj in the namespace LostSalesOldNew.StateReduction.

Formalization targets

Goal: Claim 1 (p. 1259)

For a level vector $s$ , a policy $z\in Z(s)$ , i.i.d. demands with law $D$ on $[0,\infty)$ and $P(d>0)>0$ , and any initial state $x\ge 0$ , almost surely

\exists\,T\ \forall\,t\ge T:\quad x_t\in X(s).

The paper's word is "transient"; the statement above says that every state outside $X(s)$ , indeed the whole complement, is visited only finitely often.

Milestones

(5) and §4: for every level vector $s$ , $z_s\in Z(s)$ .
Invariance (proof of Claim 1): $x\in X(s)$ , $z\in Z(s)$ , $d\ge 0$ imply $x_+\in X(s)$ .
Entrance (proof of Claim 1): along a demand path with $d_t\ge 0$ and $\sum_{t<n}d_t\to\infty$ , the process started at any $x\ge 0$ visits $X(s)$ .

A further item records the paper's remark that $X(s)$ and $Z(s)$ are increasing in $s$ .

Significance

Claim 1 lets the dynamic program be solved on the compact set $X(\bar s)$ with policies restricted to $Z(\bar s)$ , which is what makes the paper's exact computations (lead times up to four, §6) feasible. Since $Z(s)$ contains the vector base-stock policies and, for $s$ large enough, any policy that stops ordering in large states, the claim also says that every plausible policy eventually confines the state to a bounded set.

The result has a short proof in the paper and no machine-checked version. Formalizing it produces a reusable encoding of the lost-sales pipeline with general stationary policies, and makes explicit two points the paper leaves implicit: the probabilistic reading of "transient", and the demand condition under which the process must leave the complement of $X(s)$ . Related platform material treats the backlog analogue (VeinottBaseStock.base_stock_level_absorbing, a base-stock level set is absorbing) and lost-sales dynamics under other conventions (CappedBaseStock_Model, from an empty initial state under capped base-stock policies with average cost); those formulations use another state convention and cost criterion and are not imported here.

Difficulty

The invariance step is algebra on partial sums. The content of the claim is the entrance step: outside $X(s)$ the policy orders nothing, so the process can only reach $X(s)$ through demand draining the stock and the pipeline. That requires the cumulative demand to diverge, which fails pathwise (demand identically zero leaves a state with $x_0>s_0$ fixed forever) and holds only almost surely, from independence and $P(d>0)>0$ . The naive reading of "transient" as invariance alone, or as the pathwise statement with divergent demand assumed, misses this step.

Formalization scope

States are Fin L → ℝ with $L\ge 1$ in the goal; theorems quantify over nonnegative states. The vector $(x,z)$ is Fin.snoc x z; $v$ takes a natural-number index and vanishes at $l\ge L$ , so $v_L=0$ .
Level vectors are Fin (L+1) → ℝ, antitone with nonnegative last entry. $X(s)$ constrains $v_0,\dots,v_{L-1}$ ; $Z(s)$ constrains $v_l+z(x)$ for $l=0,\dots,L$ .
Policies are deterministic stationary functions of the state, with no measurability required. The zero condition and the sign condition of $Z(s)$ range over states $x\ge 0$ (the paper's state space); over all of $\mathbb R^L$ the vector base-stock policy would not be in $Z(s)$ .
Demand is a probability measure $D$ on $\mathbb R$ with $D((-\infty,0))=0$ ; the demand sequence is the coordinate process under Measure.infinitePi (fun _ : ℕ => D). The hypothesis $D((0,\infty))>0$ is added to the paper's assumptions; without it the claim is false.
"Transient" is read as: almost surely the state lies in $X(s)$ from some period on.
Ruled out: the goal is neither the invariance statement alone, which says nothing about states outside $X(s)$ , nor the pathwise entrance statement with divergent cumulative demand assumed, which drops the probabilistic content.

A complete development needs the partial-sum algebra of the pipeline, the second Borel–Cantelli lemma or the strong law for i.i.d. nonnegative sequences under Measure.infinitePi, and induction along traj. The pipeline encoding is shared with the second mission of this series (lead-time monotonicity). Proofs of any milestone and of the goal are welcome.

Selected references

P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5):1256–1263, 2008. https://doi.org/10.1287/opre.1070.0471
T. Morton, Bounds on the Solution of the Lagged Optimal Inventory Equation with No Demand Backlogging and Proportional Costs, SIAM Review 11:572–576, 1969 (as cited in Zipkin 2008).
T. Morton, The Near-Myopic Nature of the Lagged-Proportional-Cost Inventory Problem with Lost Sales, Operations Research 19(7):1708–1716, 1971. https://doi.org/10.1287/opre.19.7.1708
R. Levi, G. Janakiraman, M. Nagarajan, Provably Near-Optimal Balancing Policies for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research, 2008 (forthcoming at the time of Zipkin 2008).

5 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

On the Structure of Lost-Sales Inventory Models 1: In the Transformed State v = J⁻¹x, the Optimal Cost Functions f̄_t(v) and ḡ_t(v, ζ) Are L♮-ConvexResearch Paper

Motivation

The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an $L$ -dimensional vector, and no simple policy is optimal.

Its structure has a long history:

Karlin and Scarf (1958) formulated the model and showed, for lead time one and continuous demand, that the optimal order decreases in on-hand inventory with slope bounded by one.
Morton (1969) extended these qualitative properties to general lead times, again by differentiating the optimal cost function, which required smooth demand distributions.
Zipkin (2008), the paper formalized here, recovered and unified both results with a change of state variables and a single structural property, L♮-convexity, from discrete convex analysis (Murota 2003). The argument needs no smoothness and works for discrete as well as continuous demand.

Setting

Time is discrete. In each period the order due arrives, a new order $z\ge0$ is placed, demand $d\ge0$ occurs, and a holding or penalty cost is charged. The lead time $L\ge1$ is an integer. The original state $x=(x_0,\dots,x_{L-1})$ records on-hand inventory $x_0$ followed by the orders in transit. Demands are independent with a common law $\mu$ . The costs are linear and stationary: unit procurement cost $c$ , unit holding cost $\hat h$ , unit lost-sales penalty $p$ , and discount factor $\gamma$ .

The transformed state is the vector of partial sums $v_l=\sum_{k=l}^{L-1}x_k$ , $0\le l<L$ , with the convention $v_L=0$ . It ranges over the cone

V=\{v\in\mathbb R^L : v_0\ge v_1\ge\dots\ge v_{L-1}\ge 0\}.

The transformed order is $\zeta=-z\le0$ . With $e$ the all-ones vector, the state moves to

v_+=\big([v_0-v_1-d]^+ + v_1,\ v_2,\ \dots,\ v_{L-1},\ 0\big)-\zeta e .

The one-period cost is $\hat q(u)=\hat hu^+ + pu^-$ on $u=y-d$ , where $y=v_0-v_1$ is the on-hand stock, and $\hat q^0(y)=E[\hat q(y-d)]$ . With $k$ periods to go, the optimal cost functions are

\bar f_0\equiv0,\qquad \bar g_k(v,\zeta)=-\gamma^Lc\zeta+\hat q^0(v_0-v_1)+\gamma E\big[\bar f_k(v_+)\big],\qquad \bar f_{k+1}(v)=\inf_{\zeta\le0}\bar g_k(v,\zeta).

A function $\varphi$ is submodular on a set $S\subseteq\mathbb R^n$ if $\varphi(x\vee y)+\varphi(x\wedge y)\le\varphi(x)+\varphi(y)$ for all $x,y\in S$ , with $\vee,\wedge$ the componentwise maximum and minimum. A function $f:V\to\mathbb R$ is L♮-convex if $\psi(v,\zeta)=f(v-\zeta e)$ is submodular on $V\times\Re^-$ . A function $g(v,\zeta)$ on $V\times\Re^-$ is L♮-convex if $g\big((v,\zeta)-\xi(e,1)\big)$ is submodular in $(v,\zeta,\xi)$ over $v\in V$ , $\zeta\le\xi\le0$ .

Formalization targets

Goal: Theorem 4 (p. 939)

For every number of periods to go $k$ ,

\bar f_k \text{ is L♮-convex on } V \quad\text{and}\quad \bar g_k \text{ is L♮-convex on } V\times\Re^- .

The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.

Milestones, in the order the proof uses them

Lemma 1 (p. 938): if $f(v)$ is L♮-convex, so is $\psi(v,\zeta)=f(v-\zeta e)$ .
Lemma 2 (p. 939): if $g(v,\zeta)$ is L♮-convex, so is $f(v)=\min_{\zeta\le0}g(v,\zeta)$ .
Optimal filling (proof of Theorem 4): in the end-of-period program (3), filling as much demand as possible is optimal ( $a=\min\{d,v_0-v_1\}$ ). Consequently $\bar\kappa_t(v,\zeta\mid d)=\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+)$ .
$\psi_t$ is L♮-convex: the objective $\psi_t(v_+,v,\zeta)=\hat h(v_+-v_1)+p(v_+-v_0+d)+\gamma\bar f_{t+1}[(v_+,v_2,\dots,v_{L-1},0)-\zeta e]$ of program (4) is L♮-convex on its constraint set.
$\bar\kappa_t$ is L♮-convex: the end-of-period cost $\bar\kappa_t(v,\zeta\mid d)$ is L♮-convex in $(v,\zeta)$ for each $d$ .
$\bar g_t$ is L♮-convex: if $\bar f_{t+1}$ is L♮-convex, so is $\bar g_t=-\gamma^Lc\zeta+E_d[\bar\kappa_t]$ , by (5).

Significance

The result. L♮-convexity of $\bar f_t$ implies that $\bar f_t$ is submodular and convex in the transformed state. L♮-convexity of $\bar g_t$ yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order $\bar z_t(v)$ is nonincreasing in $v$ and changes by at most $\omega$ when every component of $v$ increases by $\omega$ . These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:

a formal L♮-convexity theory on real cones (the shift characterization, its preservation under partial minimization, and its preservation under expectation);
a checked version of the induction behind Theorem 4;
a verified model of the lost-sales recursion in the transformed state, which missions on Corollary 5 and the later sections can import.

Difficulty

The obvious argument works with ordinary convexity and submodularity in the original state $x$ . It stalls: the lost-sales transition $[x_0-d]^+$ is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in $x$ . The paper's structure appears only in the partial sums $v$ . Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over $\zeta$ (Lemma 2). Proving plain submodularity of $\bar f_t$ on $V$ therefore does not close the induction.

A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.

A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of $d\mapsto\bar f_k(v_+)$ , and these come from the model rather than from the definitions.

Formalization scope

Representation. States are functions Fin L → ℝ, indexed $0,\dots,L-1$ as in the paper. A helper returns $v_l$ for $l<L$ and $0$ at $l=L$ . A function $g(v,\zeta)$ is encoded on Fin (L+1) → ℝ with $\zeta$ last. The objective $\psi_t$ of (4) is encoded on Fin (L+2) → ℝ with coordinates $(v_+,v_0,\dots,v_{L-1},\zeta)$ . The order is componentwise.
L♮-convexity on a domain $D$ : $(x,\xi)\mapsto f(x-\xi e)$ is submodular on $\{\xi\le0,\ x\in D,\ x-\xi e\in D\}$ , with $e$ the all-ones vector on every coordinate. For $D=V$ this is the paper's definition verbatim. This is the paper's definition, not Murota's translation-submodularity form, and it is stated on real vectors. The platform's discrete-convexity library (DiscreteConvex.LConvexFunctions.*) works on $\mathbb Z^V$ with values in $\mathbb R\cup\{+\infty\}$ , a different domain and definition, and is not reused.
Time. Data are stationary, so the paper's $\bar f_t$ depends on $t$ only through the number of periods to go $k=T+L+1-t$ , and "for all $t$ " is "for all $k$ ". The minimum over $z\ge0$ is taken in every period, as printed in (1).
Explicit readings of the paper's phrases.
- "min" (over $\zeta\le0$ , over $v_+$ , over $(a,w)$ ) is an infimum over the constraint set. In the model every cost is nonnegative, so the infimum is genuine. The generic Lemma 2 assumes the values bounded below, and the generic milestone 5 assumes the continuation nonnegative on $V$ .
- "the $d_t$ are independent and nonnegative": one law $\mu$ with $\mu(-\infty,0)=0$ , since data are stationary.
- "unit cost", "discount rate": $c,\hat h,p\ge0$ and $0<\gamma\le1$ .
- Finite mean demand is added: without it $\hat q^0$ is infinite.
- "the optimal $a=\min\{d,v_0-v_1\}$ ": stated as the equality of the infimum of program (4) with its value at $v_+=\max(v_0-d,v_1)$ .
Ruled out. A statement that holds because a value function is the junk constant $0$ (constants are L♮-convex), plain submodularity on $V$ in place of the shift condition, quantification over all of $\mathbb R^L$ instead of $V$ , and a goal about an arbitrary function assumed to satisfy the recursion. None of these is the paper's theorem; the goal is stated for the recursion itself.
Not in scope. "L♮-convex implies convex" for a generic function, which is false without regularity (a non-measurable additive function is L♮-convex in this sense); Lemma 3 and Corollary 5, for a follow-up mission that references Theorem 4; the smooth-case Hessian discussion; the infinite-horizon remarks.
Welcome contributions. Reusable lemmas on submodularity over sublattices of $\mathbb R^n$ (partial minimization, Topkis 2.7.6), on preservation of submodularity under integration, and on measurability of the value functions.

Selected references

P. Zipkin, On the structure of lost-sales inventory models, Operations Research 56(4) (2008) 937–944. https://doi.org/10.1287/opre.1070.0482
S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
T. E. Morton, Bounds on the solution of the lagged optimal inventory equation with no demand backlogging and proportional costs, SIAM Review 11(4) (1969) 572–596. https://doi.org/10.1137/1011090
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.

8 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Negative Dynamic Programming II: With Non-Positive Rewards on Borel Spaces, the Optimal Return Satisfies the Optimality EquationResearch Paper

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

Theorem 5.2 (a)–(g): monotonicity, translation, sup-, limit- and selection properties of $U$ .
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$ .
Lemma 6.2: $U$ conserves $\sup_n I({}^n\pi)$ and $\lim_n U^n \sup_n I({}^n\pi)$ .
Theorem 6.2: one Markov policy comes within $\varepsilon$ of the supremum of the returns of countably many Markov policies.
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$ .
Theorem 7.1: $v^*$ is absolutely measurable.
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

21 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Optimal Inventory Policies for Assembly Systems Under Random Demands 2: If an Item and Its Predecessors Have Negative Discounted Echelon Holding Cost, the Minimal Cost Is Unbounded BelowResearch Paper

Motivation

Assembly systems — components purchased from outside, assembled into subassemblies, and those into an end product facing random customer demand — are the standard model of material requirements planning under uncertainty. Rosling's paper (Oper. Res. 37(4), 1989) shows that, under a cost assumption, the optimal policies of such a system are those of an equivalent series system, so that the Clark–Scarf decomposition of serial systems (Clark and Scarf, 1960) applies to assembly systems.

The cost assumption of the main results requires every echelon holding cost to be positive. In §4 Rosling replaces it by a weaker Generalized Assumption (GA), which allows some echelon holding costs to be negative, and then argues with Theorem 4 that GA "covers all cases of practical interest for a long-run analysis". Part (i) of Theorem 4 is the first step of that argument: when GA(i) fails strictly for some item, the model is degenerate, because its minimal cost is $-\infty$ . This mission formalizes that statement.

Setting

There are $N \ge 1$ items $1, \dots, N$ ; item $1$ is the end item. Every item $i \ge 2$ has exactly one immediate successor $s(i)$ with $1 \le s(i) < i$ , and $s(1) = 0$ , so the items form a tree rooted at the end item. Write $A(i)$ for the set of all successors of $i$ , $B(i)$ for the set of all its predecessors, and $P(i)$ for its immediate predecessors. Item $i$ has a lead time $l_i \in \mathbb N$ , and its total lead time is $M_0 = 0$ , $M_i = l_i + \sum_{k\in A(i)} l_k$ ; the items are indexed so that $M_{i-1} \le M_i$ .

Time runs in periods $t = 1, 2, \dots$ . The demands $\xi_1, \xi_2, \dots$ for the end item are independent, identically distributed, nonnegative, with a density and a finite mean $\lambda > 0$ . In period $t$ a policy chooses the echelon inventory positions after ordering $Y_{1t}, \dots, Y_{Nt}$ as functions of the demands already observed. The position before ordering is $X_{it} = Y_{i,t-1} - \xi_{t-1}$ , and the echelon stock on hand after arrivals is $X^l_{it} = Y_{i,t-l_i} - \sum_{r=t-l_i}^{t-1}\xi_r$ ; positions referring to periods before $1$ are read off given initial data $x^0$ . Problem P asks for a policy satisfying

X_{it} \le Y_{it} \le X^l_{kt}\qquad\text{for all } k\in P(i) \text{ and all } i,t \tag{3}

that minimizes

E\Big\{\sum_{t=1}^\infty \alpha^{t-1}\Big(\sum_{i=1}^N \alpha^{l_i} h_i Y_{it} + \alpha^{l_1}(p+H_1)\int_{Y_{1t}}^\infty(\xi - Y_{1t})\,\varphi_1^{l+1}(\xi)\,d\xi\Big)\Big\} + \text{constant}, \tag{2}

where $h_i$ is the echelon holding cost of item $i$ , $p$ the backlogging cost, $H_1$ the installation holding cost of the end item, $\alpha$ the discount factor and $\varphi_1^{l+1}$ the density of the demand over $l_1 + 1$ periods.

The quantity of interest is the discounted echelon holding cost of item $i$ and its predecessors,

h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}}.

GA(i) asks it to be positive for every item.

Formalization targets

Goal: Theorem 4(i), p. 574

If for some item $i$

h_i\,\alpha^{-M_{s(i)}} + \sum_{k\in B(i)} h_k\,\alpha^{-M_{s(k)}} < 0,

then the minimal cost of Problem P is unbounded below: for every real $C$ there is a feasible policy whose cost is a real number less than $C$ .

Milestones: the proof of Theorem 4(i), p. 578

The one-more-unit policy is feasible. Ordering extra units of every item $k$ of the subsystem $\{i\}\cup B(i)$ in period $M_m - M_k + 1$ , where $M_m$ is the greatest total lead time in the subsystem, and holding them forever, preserves (3).
The total cost increase. For a non-end item $i$ and a policy of finite cost, $\delta$ extra units change the cost by exactly

\delta\,\alpha^{M_m - M_i}\,\frac{\alpha^{l_i}\big(h_i + \sum_{k\in B(i)} h_k\,\alpha^{-(M_{s(k)} - M_{s(i)})}\big)}{1-\alpha}.

Significance

Theorem 4(i) explains why the Generalized Assumption is the natural boundary of the theory: a strict violation of GA(i) makes Problem P meaningless, since no policy is optimal and the infimum is $-\infty$ . Together with parts (ii) and (iii) of Theorem 4 it reduces every case of interest to systems satisfying GA, for which Rosling's series-system results apply. The quantity in the condition is the natural "net value of stockpiling" of a subsystem, and the same exchange — buy more of a subsystem early and hold it forever — is the basic perturbation behind many optimality arguments for multi-echelon systems.

The result is proved in the paper, in a few lines. To our knowledge neither Theorem 4 nor the assembly model of Problem P has been machine-checked. A formalization adds a precise statement of what "the minimal cost is unbounded below" means for a stochastic infinite-horizon problem with an extended-real cost, and the definitions of the assembly model — product tree, total lead times, echelon positions, history-dependent policies, constraint (3) and objective (2) — which other statements of the same paper need.

Difficulty

The algebra of the cost increase is a geometric series. The work lies elsewhere. First, the one-more-unit policy must be shown feasible for every item of the subsystem in every period, including the boundary items: the successor of $i$ , whose constraint loosens, and predecessors with zero lead time. Second, the cost of a policy is an expectation of an infinite discounted sum whose terms have no sign; the cost increase can only be added to a cost that is finite, and the argument needs a feasible policy of finite cost to start from, which the paper takes for granted. Third, for the end item $i = 1$ the extra units also change the expected backlog term of (2), which the printed display omits, so the end item needs a separate bound.

Formalization scope

Periods start at Lean index $k = 0$ with $k = t - 1$ ; the discount weight $\alpha^{t-1}$ is $\alpha^k$ , and coordinate $j$ of a demand path is $\xi_{j+1}$ . Items are natural numbers $1..N$ .
Demand is the product law (Measure.infinitePi) of a probability measure $\nu$ on $\mathbb R$ with $\nu((-\infty,0)) = 0$ , $\nu \ll$ Lebesgue, $\nu$ integrable and $\int x\,d\nu > 0$ .
Policies are history-dependent and measurable; feasibility (3) holds almost surely.
Initial data $x^0_i(s)$ , $s \ge 1$ , the echelon position of item $i$ at the start of period 1 ordered $s$ periods ago or earlier, are assumed well formed: nonincreasing in $s$ , and $x^0_i(s) \le x^0_k(s + l_k)$ for $k \in P(i)$ . The paper takes this for granted; it is what makes Problem P feasible.
Cost is (2) without its policy-independent constant, as an extended real $E[\sum(\alpha^{t-1}c_t)^+] - E[\sum(\alpha^{t-1}c_t)^-]$ .
Added restriction: $0 < \alpha < 1$ . The page allows $\alpha = 1$ , where the average cost is minimized and is defined only through a limit recipe.
No sign condition is imposed on $h_i$ , $p$ or $H_1$ ; neither the Assumption nor GA is a hypothesis.

In the extended reals, $\top - \top = \bot$ : a policy whose positive and negative cost parts are both infinite gets the value $-\infty$ . The goal therefore asks for policies of real cost below every bound; a formalization that only exhibits a policy of cost $\bot$ would be trivially true and is ruled out. Milestone 2 is stated for $i \ge 2$ , where the backlog term is unchanged.

Needed infrastructure: lower Lebesgue integrals of discounted sums under the infinite product measure, linearity of the cost under a deterministic perturbation, and the finiteness of the cost of the "never order" policy (whose decisions decrease linearly in the accumulated demand). Contributions of general lemmas on discounted costs of history-dependent policies under infinitePi are welcome and reusable.

Selected references

K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818

6 thms2 active usersReviewed

Machine Learning Markov Chain Probability+1·Captain: mikedeng1

An Analysis of Temporal-Difference Learning with Function Approximation 1: Linear TD(λ) Converges with Probability 1 to the Fixed Point of ΠT^(λ), with Error ≤ ‖ΠJ* − J*‖_D/(1 − α(1−λ)/(1−αλ))Research Paper

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:

the chain has a unique invariant distribution with $\pi(i) > 0$ , $E_0[g^2] < \infty$ , and finite $J^*$ ;
the $\phi_k$ are linearly independent with $E_0[\phi_k^2] < \infty$ ;
polynomial moment growth and summable mixing conditions, relative to coordinates $\sigma(i) \in \mathbb R^N$ of the states;
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

13 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 3: Dynamic Program DP3 Minimizes the Number of Tardy Equal-Length Jobs on a Batch Machine with Agreeable Release and Due DatesResearch Paper

Motivation

Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).

Setting

There are $n$ jobs and one batch processing machine with capacity $B\ge1$ . Job $j$ has release time $r_j$ , due date $d_j$ , and processing time $p_j$ . In the main problem every processing time equals a common value $p$ . A batch is a nonempty set of at most $B$ jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.

The completion time $C_j(S)$ of job $j$ in schedule $S$ is the completion time of its batch. A job is on time when $C_j(S)\le d_j$ and tardy when $d_j<C_j(S)$ . Write $U(S)=\#\{j:d_j<C_j(S)\}$ and let $U^*$ be the minimum of $U(S)$ over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.

For the structural lemmas, agreeable release times and due dates mean that $r_i<r_j$ implies $d_i\le d_j$ . For the dynamic program, jobs are indexed so that both $r_j$ and $d_j$ are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).

Formalization targets

Structural optimal schedules

Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which $U^*$ is defined.

Correctness of Algorithm DP3

Let $f(i,j)$ be the table defined by Algorithm DP3 for the first $j$ jobs and a selected count $i$ of on-time jobs. Its boundary values are $f(0,j)=0$ and $f(i,j)=+\infty$ for $i>j$ . For $1\le i\le j$ , it takes the minimum of $f(i,j-1)$ and the eligible transitions that append a batch of $k$ jobs, $1\le k\le\min(B,i)$ . A transition uses $\max\{f(i-k,j-k),r_j\}+p$ and is eligible when that completion time does not exceed $d_{j-k+1}$ . The main target is

U^*=n-\max\{i\in\{0,\ldots,n\}:f(i,n)<+\infty\}.

The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).

Unequal processing times

The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common $p$ by $f(i-k,j-k)+p_j$ . The corresponding correctness statement is a further milestone (p. 771).

Significance

The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.

The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.

Difficulty

The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.

Formalization scope

Jobs use Fin n, with index zero representing the paper's job 1; the table's $j$ is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; $+\infty$ in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most $B$ , pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.

The strict implication $r_i<r_j\Rightarrow d_i\le d_j$ makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that $r_j$ is the last batch's latest release and $d_{j-k+1}$ its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range $1\le k\le\min(B,i)$ , with an empty range giving $+\infty$ . Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.

This mission covers correctness only. The paper's $O(n^2B)$ running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.

Selected references

C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 1992, pp. 764–775. DOI: 10.1287/opre.40.4.764.

9 thms2 active usersReviewed

Linear Optimization Markov Chain Operations Research·Captain: mikedeng1

Linear Programming and Markov Decision Chains 2: Representatives of Average Optimal Stationary Policies Are Optimal Dual Solutions, and Every Optimal Dual Solution Gives an Average Optimal PolicyResearch Paper

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.

13 thms2 active usersReviewed

Markov Chain Operations Research Reinforcement Learning·Captain: mikedeng1

Planning and Acting in Partially Observable Stochastic Domains: The Witness Theorem, a Set of Useful Policy Trees Is Incomplete iff Replacing One Subtree Improves on It at Some Belief StateResearch Paper

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

§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$ .
§4.1: $V_t$ is convex on $B$ .
§4.2: the useful trees represent the same upper surface and are contained, up to identification, in every representing subset.
§4.3: for every belief and subtree there is a useful subtree that is at least as good.
§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)$ .
§4.4.1: $\hat Q^a_t \le Q^a_t$ on $B$ .
Appendix A: if $V_{p^*}(b) > V_p(b)$ for trees with the same root, one subtree swap already improves on $p$ at $b$ .
§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

11 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 2: The Greedy Forward Dual Solution Is Optimal and Its Value Is the Lot-Sizing CostResearch Paper

Motivation

Economic lot sizing asks when to produce goods across a finite planning horizon when demand in each period is known. Producing in a period incurs a fixed setup charge and a marginal cost per unit, while goods may be produced before the period in which they are needed. Such a decision has to balance paying another setup charge against producing more units earlier. The model is a standard setting for studying how dynamic programming and linear optimization describe the same planning decision. Wagelmans, Van Hoesel and Kolen study faster algorithms for this model and, in Section 4, connect the optimal lot-sizing cost to a greedy solution of a dual program Wagelmans et al. (1992).

The dual connection is useful in its own right. It supplies a certificate for the cost returned by the forward dynamic program: a feasible dual vector attains that cost. The paper allows demand to vanish in some periods, which makes the dual values at those periods free and forces care in defining the dynamic program. The mission targets precisely that case.

Setting

There are periods $1,\ldots,n$ . Demand $d_t$ and setup cost $f_i$ are nonnegative for the periods in the horizon. The marginal production cost $c_i$ is any real number. Write $d_{i,j}=\sum_{t=i}^j d_t$ for cumulative demand from $i$ through $j$ . Values at period zero and beyond the horizon are bookkeeping only; every optimization constraint concerns periods $1,\ldots,n$ .

The forward lot-sizing cost $F(j)$ describes the least cost of serving periods $1,\ldots,j$ under the zero-inventory property cited by the paper. Its recursion starts with $F(0)=0$ . If $d_j=0$ , no new production is needed and $F(j)=F(j-1)$ . If $d_j>0$ , the last production setup may occur at some $i\le j$ , giving

F(j)=\min_{1\le i\le j}\bigl(f_i+c_i d_{i,j}+F(i-1)\bigr).

This piecewise definition matters even when only one period has zero demand. Taking the displayed minimum at $d_j=0$ would charge a setup that need not occur.

Program D′ chooses free real values $v_1,\ldots,v_n$ to maximize $\sum_{t=1}^n d_tv_t$ , subject to

\sum_{t=i}^n d_t\max\{0,v_t-c_i\}\le f_i \qquad(1\le i\le n).

“Free” means there is no nonnegativity constraint on $v_t$ . The paper obtains D′ from the dual of the linear relaxation of its simple plant location formulation, using the variables of Formulation III Wagelmans et al., pp. S147, S152–S153. The mission takes D′ as the defined optimization problem.

The greedy forward rule visits periods in increasing order. At a period with $d_j>0$ , the chosen value is the minimum of the upper bounds left by the constraints indexed $i\le j$ :

v_j=\min_{1\le i\le j} \left(c_i+\frac{f_i-\sum_{t=i}^{j-1}d_t\max\{0,v_t-c_i\}}{d_j}\right).

When $d_j=0$ , the rule places no restriction on $v_j$ . This matches the paper's statement that it may be assigned an arbitrary value. One concrete recursive vector in the definitions sets each such value to zero, but the goal covers every assignment.

Formalization targets

The goal says that every vector satisfying the greedy rule is feasible for D′, agrees with the dynamic-programming cost at every prefix, and is optimal among all feasible D′ vectors:

\sum_{t=1}^j d_tv_t=F(j)\quad(1\le j\le n), \qquad \sum_{t=1}^n d_tu_t\le\sum_{t=1}^n d_tv_t \quad\text{for every feasible }u.

The milestone path follows the Section 4 statements: feasibility of the greedy vector; decreasing greedy values across positive-demand periods; the prefix upper bound for any feasible dual vector; and Equation (2), which expresses a greedy prefix value using a minimizing production period. Equation (2) is stated with the induction hypothesis that appears immediately before it in the paper. The goal combines these claims without treating the desired value identity as a hypothesis.

Significance

The result identifies a dual certificate whose value matches the forward lot-sizing cost. It also explains why a greedy forward assignment can solve D′ despite each constraint linking the current value with all later periods. The full-horizon identity recovers the cost $F(n)$ , and the comparison with every feasible vector makes the word “optimal” precise. The paper additionally says that this dual computation directly provides an optimal primal solution; this mission does not encode that reconstruction because it would require the primal formulation and its correspondence to $F$ Wagelmans et al., p. S153.

A formal proof would provide a reusable finite-horizon certificate theorem for this dual formulation and a careful treatment of empty and zero-demand prefixes. The paper's result is already proved mathematically. The Lean files in this proposal state the goal and its milestones; their theorem proofs remain to be supplied by solvers. Related platform goals about the convex hull of other lot-sizing formulations and the Federgruen–Tzur forward algorithm concern different objects, so they are credited as neighboring work rather than imported as this theorem.

Difficulty

A current greedy value is limited by every earlier production index, and feasibility must still hold for the entire horizon, not merely for the constraints truncated at the current period. Equality with $F(j)$ also has to survive periods with zero demand, where the dual coordinate is unrestricted but its weighted contribution vanishes. The forward recurrence has a separate branch at exactly those periods. A formulation that assumes every demand is strictly positive would avoid the delicate case and would miss a feature the authors explicitly retain.

Formalization scope

Lean represents the horizon by natural-number indices $1,\ldots,n$ and the demand, setup, marginal-cost and dual sequences by functions $\mathbb N\to\mathbb R$ . Finite sums use closed intervals; the sum before period $j$ uses $[i,j)$ , so it is empty when $i=j$ . Minima are over the nonempty finite set $\{1,\ldots,j\}$ , only when $j\ge1$ . The horizon $n=0$ has empty sums and no constraints. The cost and dual values are real, with no sign condition on $c_i$ or $v_i$ .

Several informal phrases are made explicit. “The solution is feasible” means every D′ constraint through $n$ holds. “Optimal” includes feasibility, every prefix identity, and comparison with every feasible dual vector. “Can be given an arbitrary value” is represented by no greedy-rule condition at zero demand; the theorem quantifies over all vectors that satisfy the positive-demand conditions. The paper states monotonicity for consecutive nonzero-demand periods; the milestone uses any two positive-demand periods, skipping zero-demand positions so it holds for every choice of their dual values. The weak-duality milestone spells out the paper's reference to “duality and the structure of D′” as an inequality for each feasible vector and prefix.

The identification of $F$ with the optimum of the primal lot-sizing model relies on the zero-inventory property cited by the authors and is not separately formalized. Neither the equivalence of Program D and D′ nor the recovery of a primal production plan is an item here. The paper's running-time claims, including $O(n^2)$ for the greedy forward algorithm and $O(n\log n)$ for its backward algorithm, are outside the scope: the paper does not fix a machine model or constants for them. A definition of $F$ as the optimum of D′ would make the value identity circular; the proposal defines it by the paper's forward recursion instead. The backward algorithm of pp. S153–S155 belongs to a separate development.

Selected references

A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1, 1992, S145–S156. DOI

7 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Multi-armed Bandits and the Gittins Index: With Per-Project Horizons the Maximal M-Process Reward Is K − ∫_M^K ∏ᵢ ∂φᵢ/∂m dm and the Gittins Index Rule Attains ItResearch Paper

Motivation

The multi-armed bandit problem asks how to allocate effort sequentially among $N$ independent projects, only one of which can be worked on at a time, so as to maximise expected total discounted reward. It is the model behind research planning, clinical-trial allocation and job scheduling, and it is the prototypical example of a Markov decision problem whose state space grows exponentially in $N$ yet whose optimal policy is simple. Gittins and Jones (1974) and Gittins (1979) showed that each project can be given an index computed from that project alone, and that it is optimal always to engage a project of largest index. P. Whittle's 1980 paper gave a short proof of this theorem by attaching a retirement option to the process, and extended it to projects with individual horizons.

Timeline:

1974–1979. Gittins and Jones introduce the dynamic allocation index; Gittins (1979, JRSS B) proves its optimality by an interchange argument.
1980. Whittle (JRSS B 42, 143–149) introduces the $M$ -process, proves the finite-horizon formula (Theorem 1 below), derives the infinite-horizon identity (12), and extends the result to superprocesses (Theorem 2).
1980s–2010s. Weber (1992) and Tsitsiklis (1994) give further short proofs; the index theory is collected in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (Wiley, 2011).

Setting

There are $N$ projects. Project $i$ has a state $x_i$ in a measurable space $X_i$ . Engaging project $i$ in state $x_i$ earns the expected reward $R_i(x_i)$ and moves its state by a Markov kernel $P_i$ ; the other projects' states do not change. Rewards are discounted by $\beta$ , $0 \le \beta < 1$ , and bounded:

k(1-\beta) \le R_i(x_i) \le K(1-\beta). \qquad (1)

The operator $L_i\theta(x) = R_i(x_i) + \beta\,\mathbb E[\theta(x(t+1)) \mid x(t) = x, i(t) = i]$ evaluates engaging project $i$ for one step.

In the $M$ -process one may also retire at any time for the reward $M$ . Its value $F(x, M)$ solves $F = \max(M, \max_i L_i F)$ (4), and the value $\varphi_i(x_i, M)$ of the single-project $M$ -process solves $\varphi_i = \max(M, L_i\varphi_i)$ (9).

With per-project horizons, project $i$ may be operated at most $s_i$ more times. A project with $s_i > 0$ is active, and $D_i s$ lowers $s_i$ by one. The single-project value $\varphi_i(x_i, s_i, M)$ satisfies $\varphi_i(x_i, 0, M) = M$ and

\varphi_i(x_i, s_i, M) = \max\big[M,\ R_i(x_i) + \beta\,\mathbb E\,\varphi_i(x_i(t+1), s_i - 1, M)\big]. \qquad (14)

$F(x, s, M)$ is the maximal expected reward of the $M$ -process under these limits. The index $M_i(x_i, s_i)$ is the infimal $M$ with $\varphi_i(x_i, s_i, M) = M$ , and $v_i = (1-\beta)M_i$ is the Gittins index. Finally

\hat F(x, s, M) = K - \int_M^K \prod_i \frac{\partial \varphi_i(x_i, s_i, m)}{\partial m}\, dm. \qquad (13)

Formalization targets

Goal: Theorem 1 (p. 147)

F(x, s, M) = \hat F(x, s, M),

and $F$ is attained by the policy that, at $(x, s)$ , engages a project $i$ maximising $M_i(x_i, s_i)$ when this maximum exceeds $M$ , and otherwise retires. The Lean goal has three conjuncts: $F = \hat F$ , every measurable index rule (any tie-breaking) earns $F$ , and no feasible measurable Markov policy earns more than $F$ .

Milestones (the steps of the proof)

Lemma 1 (p. 144): $F(x, M)$ is non-decreasing and convex in $M$ , equals $\Phi(x)$ for $M \le k$ and $M$ for $M \ge K$ .
(18) (p. 147): $P_i(x,s,M) = \prod_{j \ne i}\partial\varphi_j/\partial M$ is a distribution function in $M$ , equal to $1$ for $M \ge M_{(i)} = \max_{j\ne i} M_j$ .
(19) (p. 147): $\hat F = \varphi_i P_i + \int_M^\infty \varphi_i\, d_m P_i$ .
(21) (p. 148): $\hat F \ge L_i\hat F$ , with equality if $M_i = \max_j M_j \ge M$ .
Retirement case (p. 148): if $\max_j M_j \le M$ then $\hat F = M$ .
(16) (p. 147): $\hat F = \max(M, \max_i L_i\hat F)$ and $\hat F(x, 0, M) = M$ .

Further item

Infinite horizon (p. 148, formula (12) of p. 146): $F(x, M) = K - \int_M^K \prod_i \partial\varphi_i(x_i, m)/\partial m\, dm$ , with the index rule optimal.

Significance

Theorem 1 reduces an $N$ -project problem, whose state space is a product, to $N$ one-dimensional retirement problems. The formula (13) shows more than optimality of the index rule: the derivative of the multi-project value in $M$ is the product of the single-project derivatives, so the multi-project value is computable from the projects separately. The finite-horizon version gives an inductive argument that avoids the interchange arguments of earlier proofs, and the infinite-horizon identity (12) follows from it.

The result is classical and proved. What this mission adds is a machine-checked version in a generality not yet on the platform: heterogeneous projects (each with its own kernel and reward on its own measurable space), a retirement option, and per-project horizons. The platform already has a proved index theorem for identical arms sharing one kernel and reward without retirement, BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári, Theorem 35.9), single-arm retirement values in charge form (GittinsFiniteRetirementValue), and open Beta–Bernoulli special cases from Bäuerle–Rieder (MDPFinance.InfiniteHorizonApplications.proposition_7_6_7, proposition_7_6_9, theorem_7_6_10). None of these states Theorem 1, formula (13) or formula (12).

Difficulty

The obvious approach, value iteration on the product state space, gives existence of an optimal policy but says nothing about its structure. The content of Theorem 1 lies in the identity of a multi-dimensional value with an integral of a product of one-dimensional derivatives. Verifying it requires differentiating single-project values in $M$ (they are convex, but have a kink exactly at the index, where the choice of one-sided derivative matters), an integration by parts against a Stieltjes measure in $M$ , and an exchange of the expectation over the next state with the $M$ -integral. The exhausted projects ( $s_i = 0$ ) and the boundary $M = M_i$ need separate care in every step.

Formalization scope

Projects are indexed by Fin N (0-based; the paper uses $1, \dots, N$ ). State spaces are arbitrary measurable spaces; no finiteness or countability is assumed. Kernels are Markov, rewards measurable and bounded as in (1), and $0 \le \beta < 1$ (β = 0 is allowed). $k$ and $K$ are any constants satisfying (1).
Budgets are s : Fin N → ℕ; $D_i s$ is Function.update s i (s i - 1) and is only applied to active projects.
$F(x, s, M)$ , the "maximal reward", is the backward-induction value: $F(x, 0, M) = M$ and $F = \max(M, \max_{i\ \text{active}} L_iF)$ , defined by recursion on $\sum_i s_i$ . It is not defined through $\hat F$ , the index, or a policy. $\varphi_i(x_i, s_i, M)$ is defined by (14) with $\varphi_i(x_i, 0, M) = M$ .
$\partial/\partial m$ is the right derivative. Since the $\varphi_i$ are convex in $m$ , this changes (13) at no point, and it makes (18) hold at the kink $M = M_{(i)}$ .
The index of an exhausted project is the paper's $-\infty$ . In Lean index takes the junk value 0 there; every use (the index rule, $M_{(i)}$ , $\max_j M_j$ ) ranges over active projects only.
Policies are Markov in $(x, s, M)$ , valued in Option (Fin N) (none = retire), feasible (they engage only active projects) and measurable (each decision set is measurable), so that their expected rewards are well defined. The index rule allows arbitrary tie-breaking; the goal quantifies over every such rule.
Infinite-horizon values (Lemma 1, the further item) are any bounded measurable solutions of (2), (4), (9); such solutions exist and are unique by the contraction property.
(19) uses the Stieltjes measure of any monotone right-continuous function agreeing with $P_i$ , and integrates over $m > M$ .
Trivializing formalizations are excluded: $F$ is not $\hat F$ by definition, exhausted projects cannot be engaged by the index rule, and maxima over $i$ are seeded with $M$ rather than taken as a junk real supremum.

A complete development needs measurability of the recursive values, convexity of $\varphi_i$ in $M$ with one-sided derivatives, Lebesgue–Stieltjes integration by parts, and Fubini for kernels. Convexity of finite-horizon retirement values and the integration-by-parts identity are reusable beyond this mission. Contributions to any milestone, and sorry-free lemmas on these ingredients, are welcome.

Selected references

P. Whittle, Multi-armed Bandits and the Gittins Index, J. R. Statist. Soc. B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, J. R. Statist. Soc. B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

8 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Negative Dynamic Programming IV: Switching at Each Stage to the Policy with the Better Continuation Return Does at Least as Well as Both PoliciesResearch Paper

Motivation

Policy improvement is one of the two classical ways of solving a Markov decision problem: start from a policy, compute its return, and change the decision wherever another action looks better against that return. Howard (1960, Dynamic Programming and Markov Processes) introduced it for finite state and action spaces, and Blackwell (1965) proved it for discounted problems on Borel spaces. A related routine combines two given policies instead of improving one: at each state, follow whichever policy has the larger return there. Eaton and Zadeh (1962, J. Basic Eng. Ser. D 84, 23–29) proved that this combination of two stationary policies is at least as good as both in the negative case with finite state and action spaces (as credited on p. 889 of Strauch's paper).

Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966) 871–890) treats the negative case: all one-stage returns are non-positive (costs) and there is no discounting. This case covers stochastic shortest-path and optimal-stopping problems with positive costs, where expected total returns may be $-\infty$ and the contraction arguments of the discounted case are not available. Section 9 of the paper shows that both improvement routines remain valid there, for arbitrary randomized history-dependent policies on Borel spaces, and that they fail in the positive case (Examples 4.2 and 9.1 of the paper).

Timeline:

1960, Howard: policy iteration for finite state and action spaces.
1962, Eaton and Zadeh: the two-policy combination for finite negative problems.
1965, Blackwell: both routines for discounted problems with Borel state and action spaces.
1966, Strauch, §9: Howard's routine (Theorem 9.2), the history-dependent switching theorem (Theorem 9.3) and its Markov and stationary forms (Corollaries 9.1, 9.2) in the negative case on Borel spaces.

Setting

The state space $S$ and the action space $A$ are non-empty Borel sets. The law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$ , and the return $r(s,a,t)$ is a Borel function with $-\infty<r\le 0$ whose one-step expectation $\int r(s,a,t)\,q(dt\mid s,a)$ is finite at every $(s,a)$ . There is no discounting ( $\beta=1$ ).

A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the $n$ -th action $a_n$ from a probability kernel $\pi_n(\cdot\mid h)$ that may depend on the whole history $h=(s_1,a_1,\dots,a_{n-1},s_n)$ . The expected return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\pi_1q\cdots\pi_nqr\,(s)\in[-\infty,0],

the sum of the expected one-stage returns. For a terminal reward $w\le 0$ that depends on the history $(s_1,a_1,\dots,s_{n+1})$ , $I_n(\pi,w)$ is the expected return of following $\pi$ for $n$ stages and then receiving $w$ .

Given two policies $\sigma$ and $\tau$ , their continuation returns at a history $h=(s_1,\dots,s_n)$ are

u_n(h)=\sum_{j=n}^{\infty}\sigma_nq\cdots\sigma_jqr\,(h),\qquad v_n(h)=\sum_{j=n}^{\infty}\tau_nq\cdots\tau_jqr\,(h),

the expected returns from stage $n$ on if $\sigma$ , respectively $\tau$ , is used from $h$ on with its own kernels fed the full history. The switching policy $\pi$ uses $\sigma_n$ on $B_n=\{u_n>v_n\}$ and $\tau_n$ on its complement. In Lean these objects are contReturn, IsSwitch, wmax (for $w_n=\max(u_n,v_n)$ ), InH (for $I_n(\pi,w)$ ) and I, in the namespace NegativeDP.Switching.

Formalization targets

Goal: Theorem 9.3 (negative case)

For all policies $\sigma,\tau$ , the switching rule defines a policy $\pi$ , and every such $\pi$ satisfies

I(\pi)\ge\max\big(I(\sigma),I(\tau)\big)\quad\text{at every initial state.}

Milestones (proof of Theorem 9.3, p. 888)

With $w_n=\max(u_n,v_n)$ and $\pi$ the switching policy:

I_0(\pi,w_1)=w_1=\max(I(\sigma),I(\tau)),

w_n=\pi_n(r+u_{n+1})\text{ on }B_n,\qquad w_n=\pi_n(r+v_{n+1})\text{ on }B_n^c,

w_n\le\pi_n(r+w_{n+1}),\qquad I_{n-1}(\pi,w_n)\le I_n(\pi,w_{n+1}),\qquad I_{n-1}(\pi,w_n)\ge\max(I(\sigma),I(\tau)).

Further results (not milestones)

Theorem 9.2 (Howard): if $I(f,\pi)\ge I(\pi)$ then $I(f^{(\infty)})\ge I(\pi)$ . Corollary 9.1: the switching theorem for Markov policies, comparing $I(^{n-1}\sigma)$ and $I(^{n-1}\tau)$ at the current state. Corollary 9.2 (Eaton–Zadeh): for stationary $f^{(\infty)},g^{(\infty)}$ , the rule $h=f$ where $I(f^{(\infty)})\ge I(g^{(\infty)})$ and $h=g$ elsewhere satisfies $I(h^{(\infty)})\ge\max(I(f^{(\infty)}),I(g^{(\infty)}))$ .

Significance

Theorem 9.3 yields an improvement step that needs only the returns of two policies, not an optimality equation or a value function. Its Markov and stationary forms give policy-combination results usable for stochastic shortest-path and positive-cost problems, and together with Theorem 9.2 they justify policy-iteration schemes in the negative case on general state spaces. Example 9.1 of the paper shows that no comparable routine exists in the positive case, so the sign assumption is essential.

The results are proved in the paper. No machine-checked version of any of them exists, for the negative case or on Borel spaces; the related items on Prove2Me treat finite or discounted models. This mission produces the statements in Lean over Blackwell's published model of history-dependent plans, a construction of continuation returns from an arbitrary history, and terminal rewards that depend on the whole history.

Difficulty

The argument of the discounted case, which passes to the limit through the vanishing tail $\beta^n w_n$ , is not available: with $\beta=1$ the terminal term does not vanish, and returns may be $-\infty$ . Comparing $u_n$ and $v_n$ at the current state only is not enough either: for history-dependent policies the continuation returns depend on the whole history, and the switching set $B_n$ must be shown to be Borel in the history before the switching rule is even a policy. The induction also requires integrating extended-real terminal rewards against the history law and identifying the integral of the one-step operator with the next-stage expected return.

Formalization scope

Borel sets are non-empty standard Borel types; Baire functions are measurable functions. Policies are Blackwell's DiscountedDP.Stationary.Plan (one Markov kernel per decision, on Hist S A n). Decisions are numbered from $0$ in Lean, so Lean's index $n$ is the paper's stage $n+1$ .
Only the negative case is formalized ( $r\le0$ real-valued, $q$ -integrable at every $(s,a)$ , $\beta=1$ ). The paper states Theorem 9.3 for the discounted and negative cases; the discounted case is not part of this mission.
Returns lie in $[-\infty,0]$ and are EReal values computed as minus the lintegral of the loss $-r$ ; Bochner integrals and toReal are never used, so a return of $-\infty$ is not silently turned into $0$ . $I(\pi)$ is the sum of stage expectations, equal to $e_\pi\rho$ by monotone convergence.
Terminal rewards are read through their negative parts; they are applied only to $w_n\le 0$ .
The switching policy is characterized by the predicate IsSwitch, not constructed. A statement "every switching policy satisfies the bound" would hold vacuously if no plan satisfied the rule; the goal therefore also asserts that a switching plan exists, which is the content of the paper's "define $\pi$ by". The same pattern is used in Corollaries 9.1 and 9.2 (the rule defines a measurable decision rule).
Ties $u_n=v_n$ go to $\tau$ in Theorem 9.3, and $I(^{n-1}\sigma)=I(^{n-1}\tau)$ to $g_n$ in Corollary 9.1 (strict $>$ as printed); in Corollary 9.2 ties go to $f$ (non-strict $\ge$ as printed).
Lemma 3.1 ( $I_n(\pi,0)\downarrow I(\pi)$ ), used in the last step of the proof, is posed in mission I of this series and not repeated here.

Contributions welcome: measurability of continuation returns in the history (needed for the existence part), the identification of the history law with the continuation law from the initial state, and a Chapman–Kolmogorov identity for the continuation kernels. These are reusable in any development on history-dependent policies over Borel spaces.

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
J. H. Eaton and L. A. Zadeh, Optimal pursuit strategies in discrete-state probabilistic systems, J. Basic Eng. Ser. D 84 (1962) 23–29 (reference [7] of Strauch's paper).
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.

9 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Negative Dynamic Programming I: With Non-Positive Rewards, If an Optimal Policy Exists Then an Optimal Stationary Policy ExistsResearch Paper

Motivation

Many sequential decision problems accumulate costs that are never recovered: inventory holding and shortage costs, waiting times, the expected number of steps until a target is reached. Written as rewards, these are non-positive rewards summed over an infinite horizon without discounting. Ralph Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966), doi:10.1214/aoms/1177699369) is the foundational treatment of this negative case on general Borel state and action spaces. It complements Blackwell's treatment of the discounted case (Blackwell 1965) and of the positive bounded case (Blackwell 1964, mimeographed), and it sets out which conclusions of the discounted theory survive when rewards are non-positive and undiscounted.

A central question in that theory is how simple an optimal policy can be taken to be. A policy may in principle randomize and consult the entire past history. Strauch showed that in the negative case, whenever an optimal policy exists, an optimal stationary one exists, using one measurable decision rule at every stage. This mission formalizes that result together with the reduction from general policies to semi-Markov ones on which its proof rests.

Timeline. Blackwell (1965) proved that in the discounted case a stationary optimal policy exists whenever an optimal policy does, and gave an example showing that Markov policies need not suffice on Borel spaces. Strauch (1966) proved the corresponding statement for the negative case and proved that semi-Markov policies, which remember the initial state as well as the current one, are enough.

Setting

A negative dynamic programming problem consists of non-empty Borel sets $S$ (states) and $A$ (actions), a law of motion $q(\cdot\mid s,a)$ , which is a probability kernel from $S\times A$ to $S$ , and a Borel return function $r(s,a,t)$ with

r\le 0,\qquad r>-\infty,\qquad \int r(s,a,t)\,dq(t\mid s,a)>-\infty\ \ \text{for all }(s,a).

There is no discounting. A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the action $a_n$ at stage $n$ from a probability kernel $\pi_n(\cdot\mid h_n)$ , where $h_n=(s_1,a_1,\dots,a_{n-1},s_n)$ is the history. A policy is Markov if $a_n=f_n(s_n)$ for Borel maps $f_n:S\to A$ , semi-Markov if $a_n=g_n(s_1,s_n)$ for Borel $g_n$ , and stationary, written $f^{(\infty)}$ , if $a_n=f(s_n)$ for one Borel rule $f$ . Random Markov and random semi-Markov policies draw $a_n$ from kernels in $s_n$ , respectively $(s_1,s_n)$ .

The expected total return from the initial state $s$ is

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

the optimal return is $v^*(s)=\sup_\pi I(\pi)(s)$ over all policies, and $\pi^*$ is optimal if $I(\pi^*)(s)\ge v^*(s)$ for every $s$ . For a Borel rule $f$ , the operator $T$ acts on non-positive Borel functions $u$ by

Tu(s)=\int r(s,f(s),t)+u(t)\,dq(t\mid s,f(s)).

The namespace is NegativeDP.Stationary. The objects above are Problem, Plan, I, In, vstar, IsOptimal and T.

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

\big(\exists\,\pi^*\ \ I(\pi^*)\ge v^*\big)\ \Longrightarrow\ \exists\,f\ \text{Borel},\ \ I(f^{(\infty)})\ge v^* .

Milestones

Lemma 2.1: for a kernel $q(\cdot\mid x)$ and a Borel $u\le 0$ on $X\times Y$ there is a Borel $f$ with $u(x,f(x))\ge\int u(x,y)\,dq(y\mid x)$ .
Lemma 3.1 (N): $I_n(\pi)\downarrow I(\pi)$ .
Lemma 4.1 (a), (b): policies built from the conditional laws of $a_n$ given $(s_1,s_n)$ , respectively given $s_n$ under an initial law $p$ , reproduce the laws of $(s_1,s_n,a_n,s_{n+1})$ , respectively the $p$ -averaged laws of $(s_n,a_n,s_{n+1})$ .
Theorem 4.1: for every policy $\pi$ and initial law $p$ there are a random semi-Markov $\pi^*$ and a random Markov $\pi^{**}$ with $I(\pi)=I(\pi^*)$ and $pI(\pi)=pI(\pi^{**})$ for every return function.
Theorem 4.2 (N): if $I(\pi^n\sigma)\ge I(\sigma)$ for all large $n$ , then $I(\pi)\ge I(\sigma)$ .
Theorem 4.3 (N): a semi-Markov $\tau$ with $I(\tau)\ge I(\pi)$ and a Markov $\sigma$ with $pI(\sigma)\ge pI(\pi)$ .
Theorem 5.1 (N), parts (a)–(g): the properties of $T$ , including $TI(\pi)=I(f,\pi)$ , $TI(f^{(\infty)})=I(f^{(\infty)})=\lim_n T^n0$ and $I_n(\pi,v)=T_1\cdots T_nv$ for Markov $\pi$ .

Significance

Theorem 8.3 reduces a search over all randomized, history-dependent policies to a search over single measurable decision rules, whenever an optimal policy exists at all. It underlies policy iteration and the stationary-policy conclusions of the later negative-programming literature, and it shows that the negative case behaves like the discounted case on this point. In the positive case only a weaker statement holds. The reduction of §4 (Theorems 4.1–4.3) is reused throughout the paper: Theorem 8.1 on $(p,\varepsilon)$ -optimal Markov policies starts from Theorem 4.3, and the value-iteration results of §9 use Lemma 3.1 and Theorem 5.1.

All results in this mission are proved in the paper. None of them has a machine-checked proof that we know of. The closest formal result is part 2 of Bertsekas's Proposition 7, formalized in an abstract monotone-mapping model (MonotoneDP.Increase.prop7_optimal_stationary_criterion). There, policies are sequences of selectors, so it contains neither the measure-theoretic reduction from randomized history-dependent policies nor Borel state spaces. The formal work here is to build the law of the controlled process on Borel spaces, carry out the conditional-distribution argument of Theorem 4.1, and combine it with the operator calculus of §5.

Difficulty

The obvious argument starts from an optimal $\pi^*$ , takes its first decision rule $f$ , and shows that $f^{(\infty)}$ is optimal. That fails for a general $\pi^*$ , because its first action may be randomized and its later actions may depend on the entire history. One first needs Theorem 4.3, which says a non-random semi-Markov policy is at least as good. That theorem needs two things. One is Theorem 4.1, which replaces a history-dependent policy by one built from conditional distributions of actions, and this requires disintegration of measures on Borel spaces. The other is the measurable selection of Lemma 2.1, which the paper takes from Theorem 2 of Blackwell and Ryll-Nardzewski 1963, applied stage by stage, with Theorem 4.2 to pass to the limit. On Borel spaces Markov policies are not enough (Blackwell's example, Example 4.1 of the paper), so the semi-Markov step cannot be skipped. Returns can equal $-\infty$ , and every limit exchange has to respect that.

Formalization scope

Borel sets are non-empty standard Borel types and Baire functions are measurable functions. The return $r$ is real-valued, non-positive and integrable under $q(\cdot\mid s,a)$ for every $(s,a)$ . Returns live in the extended reals. $I(\pi)$ , $I_n(\pi,v)$ , $T$ and all integrals of non-positive functions are computed as minus lower Lebesgue integrals of the corresponding losses in $[0,\infty]$ , so a return of $-\infty$ is never collapsed to $0$ . $I(\pi)$ is the sum of stage expectations, which equals the paper's expectation of the total return by monotone convergence. $v^*$ is the supremum over every randomized history-dependent plan. Restricting it to Markov or stationary policies would make the goal weaker, and that encoding is ruled out. Only the negative case ( $r\le 0$ , $\beta=1$ ) is formalized. Results the paper labels "D, P, N" or "D, N" appear here in their N form.

Explicit choices:

Lean numbers decisions from $0$ . Hist S A n is the paper's $H_{n+1}$ and the plan's kernel κ n is $\pi_{n+1}$ .
The objects $\pi^*$ and $\pi^{**}$ of Lemma 4.1 are defined in the paper's proof as conditional distributions. Here their defining property is a hypothesis: for every initial state, or after averaging over $p$ , the joint law of $(s_n,a_n)$ is the law of $s_n$ followed by the kernel.
In Theorem 4.1, "for any return function $r$ " is a quantifier over every negative problem with the same law of motion, placed after the choice of $\pi^*$ and $\pi^{**}$ .
In Theorem 5.1 (b), $u+c$ is required to lie in $M(S)$ . In (d), the increasing part holds only on $\{\sup_jTu_j>-\infty\}$ .
In Theorem 5.1 (f), $T$ is applied to $I(\pi)$ for a general plan with no measurability hypothesis. The lower integral is defined for every function.

Infrastructure needed: the law of the controlled process (built here by iterated kernel composition, as in the published DiscountedDP.Stationary model), disintegration of kernels on standard Borel spaces, a measurable selection theorem of Blackwell–Ryll-Nardzewski type, and monotone convergence for lower integrals. The disintegration and selection results are reusable well beyond this paper. Contributions to Theorems 4.1 and 4.3 are especially welcome, since missions II–IV of this series build on them.

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 and C. Ryll-Nardzewski, Non-existence of everywhere proper conditional distributions, Ann. Math. Statist. 34(1) (1963) 223–225. https://doi.org/10.1214/aoms/1177704259

16 thms2 active usersReviewed

Machine Learning Probability Reinforcement Learning·Captain: mikedeng1

Technical Note: Q-Learning: With Bounded Rewards and Learning Rates with Σα = ∞, Σα² < ∞ at Every State–Action Pair, Tabular Q-Learning Converges to Q* with Probability 1Research Paper

Motivation

Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.

Timeline.

1989: Watkins' thesis introduces Q-learning and sketches a convergence argument.
1992: Watkins and Dayan publish the proof via the action-replay process, for bounded rewards, discount $0<\gamma<1$ and learning rates satisfying condition (3) at every state–action pair.
1994: Jaakkola, Jordan and Singh (Neural Computation 6) and Tsitsiklis (Machine Learning 16) give proofs through stochastic approximation for asynchronous iterations, with predictable random choices of state, action and step.
Later work (Szepesvári 1997; Even-Dar and Mansour 2003) quantifies the convergence rate.

Setting

A finite controlled Markov process has a finite state set $X$ , a finite nonempty action set $\mathfrak A$ (the same in every state), mean rewards $\mathcal R_x(a)$ and transition probabilities $P_{xy}[a]$ . Rewards received $s$ steps later are discounted by $\gamma^s$ with $0<\gamma<1$ . The optimal action-value function $Q^*$ is the unique solution of the Bellman optimality equation

Q^*(x,a)=\mathcal R_x(a)+\gamma\sum_y P_{xy}[a]\max_b Q^*(y,b).

In the $n$ -th episode the agent observes a state $x_n$ , performs an action $a_n$ , observes the next state $y_n$ and a reward $r_n$ of mean $\mathcal R_{x_n}(a_n)$ , and updates its table with a learning rate $\alpha_n$ :

Q_n(x,a)=\begin{cases}(1-\alpha_n)Q_{n-1}(x,a)+\alpha_n\bigl[r_n+\gamma\max_b Q_{n-1}(y_n,b)\bigr]&(x,a)=(x_n,a_n),\\ Q_{n-1}(x,a)&\text{otherwise,}\end{cases}

from given initial values $Q_0$ . Episodes need not form a single trajectory. Writing $n^i(x,a)$ for the episode of the $i$ -th visit to $(x,a)$ , the learning-rate condition is

\sum_{i=1}^\infty\alpha_{n^i(x,a)}=\infty,\qquad\sum_{i=1}^\infty\bigl[\alpha_{n^i(x,a)}\bigr]^2<\infty\qquad\forall x,a.\tag{3}

The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states $\langle x,n\rangle$ (a real state and a level $n$ ), in which taking $a$ at $\langle x,n\rangle$ replays a randomly chosen earlier episode that tried $a$ in $x$ , emitting its reward and dropping to the level below that episode. Its expected one-step reward is $\mathcal R^{(n)}_x(a)$ and its aggregated transition probabilities are $P^{(n)}_{xy}[a]$ .

Formalization targets

Goal: the Theorem (p. 282)

Given bounded rewards $|r_n|\le\mathcal R$ , learning rates $0\le\alpha_n<1$ and (3),

Q_n(x,a)\to Q^*(x,a)\quad\text{as }n\to\infty,\ \forall x,a,\ \text{with probability }1.

Milestones (the paper's appendix, in attack order)

Lemma A (p. 288): $Q_n(x,a)=Q^*_{\mathrm{ARP}}(\langle x,n\rangle,a)$ for all $a,x$ and $n\ge0$ .
Lemma B.1 (p. 289): the values of $s$ actions with and without a continuation policy differ by at most $\gamma^s\mathcal R/(1-\gamma)$ .
Lemma B.2 (p. 289): started high enough, the ARP strays below any level $l$ within $s$ actions with arbitrarily small probability.
The stochastic-convergence theorem quoted in the proof of B.3 (p. 290): $X_{n+1}=X_n+\beta_n(\xi_n-X_n)$ with $\sum\beta_n=\infty$ , $\sum\beta_n^2<\infty$ and bounded $\xi_n$ of mean $\Xi$ converges to $\Xi$ almost surely.
Lemma B.3 (p. 290): almost surely $P^{(n)}_{xy}[a]\to P_{xy}[a]$ and $\mathcal R^{(n)}_x(a)\to\mathcal R_x(a)$ .
Lemma B.4 (p. 291): rewards within $\eta$ and transition rows within $\eta/\mathcal R$ give values of $s$ actions within $\eta s(s+1)/2$ .

A further item states that the optimality equation has exactly one solution for $0\le\gamma<1$ .

Significance

The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD( $\lambda$ ), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.

Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.

Difficulty

The update touches one table entry at a time, at random times chosen by the agent, and its target $r_n+\gamma\max_b Q_{n-1}(y_n,b)$ depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize $Q_n$ as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.

Formalization scope

Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:

$X$ and $\mathfrak A$ are Fintypes with decidable equality, $\mathfrak A$ is nonempty, and $\max_b$ is Finset.sup'. The process is a structure with R x a $=\mathcal R_x(a)$ and P x a y $=P_{xy}[a]$ , rows nonnegative and summing to $1$ .
$Q^*$ enters the goal through the predicate IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.
Lean index $n$ is the paper's episode $n\ge1$ ; index $0$ of the episode data is unused and qIter … 0 $=Q_0$ .
Condition (3) is written over episodes: the learning rate charged to $(x,a)$ at episode $n$ is $\alpha_n$ if $(x_n,a_n)=(x,a)$ and $0$ otherwise; its partial sums tend to $+\infty$ and its squares are summable. This equals (3) and forces infinitely many visits.
Probability model (pinned). The paper describes it in words only. On a filtered probability space, $x_n,a_n,\alpha_n$ are $\mathcal F_{n-1}$ -measurable, $y_n,r_n$ are $\mathcal F_n$ -measurable, $\Pr[y_n=y\mid\mathcal F_{n-1}]=P_{x_ny}[a_n]$ , $\mathbb E[r_n\mid\mathcal F_{n-1}]=\mathcal R_{x_n}(a_n)$ , $|r_n|\le\mathcal R$ , $0\le\alpha_n<1$ , and (3) holds almost surely. Fixed episode schedules with independent outcomes are a special case.
The ARP deck at level $n$ includes card $n$ (as in the card game and Lemma A's proof); $P^{(n)}$ keeps the printed range of levels $1,\dots,n-1$ ; ARP optimality is over deterministic Markov policies of the ARP. Finite action sequences are lists of actions with $0$ terminal reward.
Corrections disclosed in the items. B.1 is stated with $\le$ (the page's strict inequalities fail for a constant reward). B.4 assumes closeness of transition rows in $\ell^1$ and $s\ge1$ : with the page's entrywise closeness the printed constant is false once $|X|\ge4$ . The stochastic-convergence theorem is read with conditional mean $\Xi$ and adapted steps.

Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.

The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.

Selected references

C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292. https://doi.org/10.1023/A:1022676722315
C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989.
T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994), 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. https://doi.org/10.1007/BF00993306
H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8

8 thms2 active usersReviewed

Completed

Markov Chain Operations Research·Captain: mikedeng1

Discrete Dynamic Programming with Sensitive Discount Optimality Criteria 1: If Every Stationary Policy Is Transient, Some Stationary Policy Maximizes the Expected Total Reward over All PoliciesResearch Paper

Motivation

A finite dynamic program with total reward is the basic model of sequential decision making without discounting: a system moves among finitely many states, a decision maker picks an action in each state, collects a reward, and the system moves on or stops. The quantity of interest is the expected total reward of a policy, summed over the whole (possibly infinite) horizon, and the question is whether a simple policy — one that uses the same decision rule at every step — is as good as any other.

For discounted or strictly substochastic models the answer has long been known. Shapley (1953) showed by successive approximations that, when every transition matrix has row sums strictly below one, some stationary policy maximizes the total reward among stationary policies; Howard (1960) gave the policy-improvement method for finding one; Blackwell (1962) showed that the maximum over all policies is attained among stationary ones. All of these rest on a contraction hypothesis $\|P(f)\|<1$ .

Veinott's 1969 paper (DOI 10.1214/aoms/1177697379), best known for its sensitive discount optimality criteria, opens in §2 by proving these classical results under the much weaker hypothesis that each stationary policy is transient, and without requiring the transition weights to be substochastic at all. Partial results in this direction were due to Eaton and Zadeh, Derman, and Denardo. The total-reward model without a contraction assumption covers stopping problems, shortest-path type problems and models in which "transition weights" are not probabilities (growth factors, populations), which is why the generalized model is of independent interest.

Setting

There are $S\ge 1$ states $1,\dots,S$ . In state $s$ a finite nonempty set $A_s$ of actions is available; taking action $a$ earns the real reward $r(s,a)$ and assigns the transition weight $p(t\mid s,a)\ge 0$ to each state $t$ . No bound on $\sum_t p(t\mid s,a)$ is assumed. The set of decision rules is $F=\times_{s=1}^S A_s$ ; for $f\in F$ , $r(f)$ is the vector $(r(s,f(s)))_s$ and $P(f)$ the matrix $(p(t\mid s,f(s)))_{s,t}$ .

A policy is a sequence $\pi=(f_1,f_2,\dots)$ of decision rules. The policy $f^\infty=(f,f,\dots)$ is stationary; $(g,\pi)=(g,f_1,f_2,\dots)$ uses $g$ first and then follows $\pi$ ; ${}^N\pi$ repeats the first $N$ rules of $\pi$ forever and is called periodic. Let $P^0(\pi)=I$ and $P^N(\pi)=P(f_1)\cdots P(f_N)$ . The policy $\pi$ is transient if $\sum_{N\ge0}P^N(\pi)$ converges, and then its vector of total returns is

V(\pi)=\sum_{N=0}^\infty P^N(\pi)\,r(f_{N+1}).

The one-step comparison $v(g,\pi^*)=V(g,\pi^*)-V(\pi^*)$ measures the gain from deviating to $g$ for one step. Vectors are compared coordinatewise, and $x>y$ means $x\ge y$ , $x\ne y$ . For a matrix $B$ , $\|B\|=\max_i\sum_j|b_{ij}|$ and $|\sigma(B)|$ is its spectral radius. Finally $V^*=\max_f V(f^\infty)$ and $\Re V=\max_g[r(g)+P(g)V]$ , both coordinatewise.

Formalization targets

Goal: Corollary 6

If every stationary policy is transient, there is $f\in F$ with

V(\pi)\le V(f^\infty)\qquad\text{for every policy }\pi.

The hypothesis concerns only the finitely many stationary policies; the conclusion compares against every policy, stationary or not.

Milestones

Lemma 1. For transient $\pi=(g_i)$ and $\pi^*$ : $V(\pi)-V(\pi^*)=\sum_N P^N(\pi)\,v(g_{N+1},\pi^*)$ , and $V(g^\infty)-V(\pi^*)=[I-P(g)]^{-1}v(g,\pi^*)$ .
Lemma 2. If every stationary policy is transient and $f\in F$ : either $v(g,f^\infty)>0$ for some $g$ , and then $V(g^\infty)>V(f^\infty)$ , or $v(g,f^\infty)\le0$ for all $g$ , which holds iff $f^\infty$ is best among stationary policies.
Corollary 1. If every stationary policy is transient, some stationary policy maximizes $V$ over the stationary policies.
Corollary 2. Under the same hypothesis, $V^*$ is the unique fixed point of $\Re$ .
Lemma 3 (Hoffman). For every $\varepsilon>0$ and every program there is a positively similar program with $\max_g\|\tilde P(g)\|<\max_g|\sigma(P(g))|+\varepsilon$ .
Corollary 4, read with "every" and with "some": stationary, periodic and arbitrary policies are transient together, and this is equivalent to $\|P^N(\pi)\|<1$ for some $N\ge1$ ; with $\|P(g)\|\le1$ also to $\|P^S(\pi)\|<1$ .
Theorem 1. If every stationary policy is transient and $\pi^*$ is any policy: $v(g,\pi^*)>0$ implies $V(g^\infty)>V(\pi^*)$ , and $v(\cdot,\pi^*)\le0$ iff $V(\pi)\le V(\pi^*)$ for all $\pi$ .

Significance

Corollary 6 is the existence half of the theory of total-reward Markov decision processes: it says that the search for an optimal policy can be restricted to the finite set of stationary policies, and, together with Corollary 2 and Theorem 1, that such a policy is characterized by the optimality equation $\Re V=V$ and by the absence of one-step improvements. Corollary 4, which the paper's introduction singles out as the section's main new result, shows that transience of the finitely many stationary policies already forces transience of every policy, uniformly; this is what makes $V(\pi)$ well defined for all policies. Hoffman's Lemma 3 converts transience into a contraction in a rescaled norm, the device behind geometric convergence of value iteration (Corollary 3 of the paper).

On the formal side, Mathlib has matrices, summability and spectral radii but no total-reward decision model. These results are proved in the 1969 paper and are standard in the textbook literature on Markov decision processes; none of them has a machine-checked proof that we know of. Related platform items concern other models: the stochastic shortest path results of Bertsekas and Tsitsiklis (a cost model with a termination state, stochastic rows and an infinite-cost assumption on improper policies) and Blackwell's discounted model; neither covers nonnegative, non-substochastic weights.

Difficulty

Without a contraction, the standard argument — $\Re$ is a contraction, so it has a unique fixed point attained by a stationary policy — has nothing to start from: $\|P(g)\|$ may exceed one for every $g$ , and the transition weights need not be probabilities, so no probabilistic coupling or stopping-time argument applies directly. Transience of each stationary policy is a statement about finitely many matrix powers $P(g)^N$ , whereas the goal concerns infinite products of different matrices $P(f_1)P(f_2)\cdots$ , whose behaviour is not controlled by the spectral radii of the factors in general. Passing from the stationary policies to all policies is the step where the obvious argument fails.

Formalization scope

The Lean development fixes these conventions.

States are a nonempty finite type St; actions are a family of nonempty finite types A : St → Type, so $F$ is the dependent function type (s : St) → A s, not a common action set.
A program is a structure Program St A with real rewards and nonnegative weights; no row-sum bound is part of the structure. Only 5° of Corollary 4 assumes $\|P(g)\|\le1$ .
Policies are deterministic Markov sequences ℕ → F, indexed from $0$ : π 0 is $f_1$ . "All policies" means all such sequences.
Transience is Summable of $N\mapsto P^N(\pi)$ in the entrywise topology. $V$ is a tsum; it is the genuine series exactly for transient policies.
$>$ on vectors is written out as $\ge$ and $\ne$ ; $\|\cdot\|$ is the maximum absolute row sum, defined explicitly; $|\sigma(\cdot)|$ is Mathlib's spectralRadius ℂ of the complexified matrix, valued in $[0,\infty]$ .
$V^*$ and $\Re$ are coordinatewise Finset.sup' over the finite set $F$ .

A trivializing formalization is ruled out: the goal and Theorem 1 do not assume the competing policies transient (that would hide Corollary 4 inside the hypothesis), and since a non-summable tsum is $0$ , no statement compares $V$ of a policy whose transience is not either assumed or implied by the hypotheses. The hypothesis "every stationary policy is transient" is satisfiable (for instance when all weights are zero) and is not implied by any row-sum bound.

A complete development needs Neumann series for nonnegative matrices, the Perron–Frobenius-type fact that a nonnegative matrix with spectral radius below one has a nonnegative $(I-B)^{-1}=\sum B^N$ , and finite-dimensional spectral theory relating $|\sigma(B)|<1$ to $B^N\to0$ . These are reusable well beyond this mission; contributions of such lemmas, and of proofs of the milestones in any order, are welcome.

Selected references

A. F. Veinott, Jr., Discrete dynamic programming with sensitive discount optimality criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
D. Blackwell, Discrete dynamic programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
L. S. Shapley, Stochastic games, Proc. Nat. Acad. Sci. 39(10):1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2):165–177, 1967. https://doi.org/10.1137/1009030
C. Derman, On sequential decisions and Markov chains, Management Sci. 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16

12 thms2 active usersReviewed

Dynamic Programming

Missions

Optimality of (s, S) Policies in Inventory Models with Markovian Demand II: In the Nonstationary Discounted Infinite-Horizon Problem, a State-Dependent (s, S) Policy Is OptimalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robust Dynamic Programming 2: The Discounted Robust Value Function Is the Unique Fixed Point of the Robust Bellman OperatorResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 2(b)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robust Dynamic Programming 1: The Robust Bellman Recursion and Optimality of Deterministic Markov Policies in Finite HorizonResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (Markov optimality)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning VI: In a Deterministic MDP an Algorithm Acts T-Step Optimally at All but NAT TimestepsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 8.3.5 (deterministic sample complexity)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning III: Non-Stationary Approximate Policy Iteration Is Within 2T Times the Regression Error Averaged over Any Competitor's State-Time DistributionTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 5.3.2 (p. 64)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning II: The Gradient of the Normalized Discounted Value Is the Sum over Actions of ∇π·Q under the Discounted Future State DistributionTextbook

Why the gradient of the value matters

Setting

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning I: Approximate Policy Iteration with Max-Norm Evaluation Error ε Is Eventually Within 2ε/(1−γ)² of OptimalTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

Milestones

Significance

Difficulty