Expectimax (source code)

= Expectimax

A <game tree> evaluation rule using maxima at the controlled player’s decision nodes and <expected values> at chance nodes:
$$
V(s)=\max_a V(T(s,a)),\qquad V(s)=\sum_{s'}P(s'\mid s)V(s'),
$$
respectively. Terminal <utilities> fix the boundary values. These rules exactly optimize a finite-horizon <expected utility> objective by <backward induction>. For cyclic infinite-horizon reachability problems, a finite <Markov decision process> formulation and <value iteration> replace naive expansion of an infinite <game tree>. Start with one at successful terminal states and zero elsewhere, keep terminal values fixed, and apply the maximizing/expectation backups repeatedly. The $t$th iterate is the greatest success <probability> achievable within $t$ transitions, by <backward induction>. These values are nondecreasing and bounded by one. For every policy, eventual success is the increasing <set union> of success within finite horizons, so its <probability> is the <limit> of those finite-horizon <probabilities>. Taking the supremum over policies and horizons in either order proves that the iterates converge to the optimal eventual-success <probability>. The limiting fixed-point equations can also admit larger solutions, so the initialization from terminal-success indicators matters.