When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.
Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (BertsekasDPModel), its policy cost recursion, and the open-loop cost of a fixed control sequence (BertsekasDPOpenLoopCost). For rollout (§6.4.1): a graph search problem — a finite digraph with destination set and terminal costs on destinations (BertsekasGraphSearch); a base heuristic producing from every node a path to a destination (BertsekasBaseHeuristic), with projection and heuristic cost ; the rollout algorithm repeatedly moves to a neighbor minimizing (BertsekasIsRolloutRun). is sequentially consistent if its paths have the tail property (Def. 6.4.1), sequentially improving if (Def. 6.4.2).
For sequentially improving and any terminating rollout run :
— BertsekasDP.rollout_sequential_improvement (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects ), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).
Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.
The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the IsLeast membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.
Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets per Eq. (6.19); all statements at the level of the Mission I model.
namespace BertsekasDP
theorem rollout_sequential_improvement {V : Type} [Fintype V] [DecidableEq V]
(G : BertsekasGraphSearch V) (H : BertsekasBaseHeuristic G)
(himp : BertsekasSeqImproving G H)
(l : List V) (hrun : BertsekasIsRolloutRun G H l)
(i₁ : V) (hhead : l.head? = some i₁) (hstart : i₁ ∉ G.dest)
(d : V) (hlast : l.getLast? = some d) :
G.cost d ≤ BertsekasHeurCost G H i₁ ∧
IsLeast {c : ℝ | c = BertsekasHeurCost G H i₁ ∨
∃ v ∈ l.dropLast, ∃ j ∈ BertsekasNbrs G v, c = BertsekasHeurCost G H j}
(G.cost d) := by sorry
end BertsekasDPProposition 6.4.2 (rollout improves on a sequentially improving heuristic). Let the base heuristic be sequentially improving, i.e. at every non-destination node , and let be a path generated by a terminating run of the rollout algorithm from a non-destination node to a destination . Then the rollout cost improves on the heuristic,
and is in fact the least of the heuristic cost at the start and at every neighbor visited along the way (Eq. (6.37)):
This is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, and the ancestor of the improvement step in Monte-Carlo tree search and modern reinforcement learning. The second identity is stronger than the first: it says the rollout has an automatic cost sorting property, always ending at the best destination among all those its base heuristic proposed along the run, so it can exhibit good behavior that the base heuristic alone never would.
Formalization Note The equality is phrased as a least element (IsLeast) of the displayed set, which asserts both that is a lower bound and that it is attained by one of the listed values. Ties in the neighbor selection are permitted; the run is any complete node sequence satisfying the rollout selection rule.
No open leaves. Every sub-goal is proved or awaiting decomposition.