Policy iteration

DefinitionPolicy improvement step#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards \(r(s, a)\) and stochastic transition probabilities \(P(s' \mid s, a)\), and let \(0 \le \gamma < 1\). The improvement of a deterministic policy \(\pi : S \to A\) is a fixed choice of policy greedy for the value \(V^\pi\) of \(\pi\): in each state \(s\) it takes a chosen action \(a\) maximizing \(r(s, a) + \gamma \sum_{s'} P(s' \mid s, a) V^\pi(s')\) over \(A\) (ties broken arbitrarily).

noncomputable def improve (π : S → A) : S → A :=
  greedy M γ (policyValue M γ hM hγ0 hγ1 π)

Uses 4 · Used by 6

Statement usesMarkov decision process · Stochastic Markov decision process · Greedy policy · Value of a policy

Used byPolicy iteration · Improvement stalls exactly at optimal policies · Away from optimality, improvement changes the value · Policy improvement theorem · Policy iteration terminates · Policy iteration never decreases the value

DefinitionPolicy iteration#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Policy iteration run for \(n\) steps from a deterministic policy \(\pi : S \to A\) is the policy obtained from \(\pi\) by applying the policy improvement step \(n\) times.

noncomputable def policyIteration (n : ℕ) (π : S → A) : S → A :=
  (improve hM hγ0 hγ1)^[n] π

Uses 3 · Used by 3

Statement usesMarkov decision process · Stochastic Markov decision process · Policy improvement step

Used byPolicy iteration terminates · Policy iteration never decreases the value · Once optimal, policy iteration stays optimal

TheoremValues below their Bellman image lie below the policy value#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Let \(\pi\) be a deterministic policy, with Bellman operator \(T^\pi\) and value \(V^\pi\). If \(V : S \to \mathbb{R}\) satisfies \(V(s) \le (T^\pi V)(s)\) for every state \(s\), then \(V(s) \le V^\pi(s)\) for every state \(s\).

theorem le_policyValue_of_le_policyBellman (π : S → A) {V : S → ℝ}
    (h : V ≤ policyBellman M γ π V) : V ≤ policyValue M γ hM hγ0 hγ1 π

Uses 5 · Used by 1

Statement usesMarkov decision process · Stochastic Markov decision process · Bellman operator of a policy · Value of a policy

Proof usesQ-value of an action

Used byPolicy improvement theorem

TheoremPolicy improvement theorem#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Write \(V^\pi\) for the value of a deterministic policy \(\pi : S \to A\). For every deterministic policy \(\pi\), the improved policy \(\pi'\), which is greedy for \(V^\pi\), satisfies \(V^\pi(s) \le V^{\pi'}(s)\) for every state \(s\).

theorem policyValue_le_policyValue_improve (π : S → A) :
    policyValue M γ hM hγ0 hγ1 π ≤ policyValue M γ hM hγ0 hγ1 (improve hM hγ0 hγ1 π)

Uses 11 · Used by 2

Statement usesMarkov decision process · Stochastic Markov decision process · Policy improvement step · Value of a policy

Proof usesBellman optimality operator · Greedy policy · Values below their Bellman image lie below the policy value · Bellman operator of a policy · A policy's Bellman update is at most the optimal one · A policy's value satisfies its Bellman equation · The greedy action attains the Bellman maximum

Used byImprovement stalls exactly at optimal policies · Policy iteration never decreases the value

TheoremImprovement stalls exactly at optimal policies#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Write \(V^\pi\) for the value of a deterministic policy \(\pi : S \to A\) and \(V^*\) for the optimal value. For every deterministic policy \(\pi\), with improved policy \(\pi'\), we have \(V^{\pi'} = V^\pi\) if and only if \(V^\pi = V^*\) (as functions on \(S\)).

theorem policyValue_improve_eq_iff (π : S → A) :
    policyValue M γ hM hγ0 hγ1 (improve hM hγ0 hγ1 π) = policyValue M γ hM hγ0 hγ1 π ↔
      policyValue M γ hM hγ0 hγ1 π = optimalValue M γ hM hγ0 hγ1

Uses 13 · Used by 1

Statement usesMarkov decision process · Stochastic Markov decision process · Policy improvement step · Optimal value of a discounted Markov decision process · Value of a policy

Proof usesBellman optimality operator · Uniqueness of the solution of the Bellman optimality equation · Greedy policy · Bellman operator of a policy · A policy's value satisfies its Bellman equation · No policy beats the optimal value · Policy improvement theorem · The greedy action attains the Bellman maximum

Used byAway from optimality, improvement changes the value

TheoremAway from optimality, improvement changes the value#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Write \(V^\pi\) for the value of a deterministic policy \(\pi : S \to A\) and \(V^*\) for the optimal value. If \(V^\pi \ne V^*\), then the improved policy \(\pi'\) satisfies \(V^{\pi'} \ne V^\pi\) (as functions on \(S\)).

theorem policyValue_improve_ne (π : S → A)
    (h : policyValue M γ hM hγ0 hγ1 π ≠ optimalValue M γ hM hγ0 hγ1) :
    policyValue M γ hM hγ0 hγ1 (improve hM hγ0 hγ1 π) ≠ policyValue M γ hM hγ0 hγ1 π

Uses 6 · Used by 1

Statement usesMarkov decision process · Stochastic Markov decision process · Policy improvement step · Optimal value of a discounted Markov decision process · Value of a policy

Proof usesImprovement stalls exactly at optimal policies

Used byPolicy iteration terminates

TheoremPolicy iteration never decreases the value#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Write \(V^\pi\) for the value of a deterministic policy \(\pi : S \to A\), and \(\pi_k\) for the policy after \(k\) steps of policy iteration from \(\pi\). If \(i \le j\), then \(V^{\pi_i}(s) \le V^{\pi_j}(s)\) for every state \(s\).

theorem policyValue_policyIteration_mono (π : S → A) {i j : ℕ} (hij : i ≤ j) :
    policyValue M γ hM hγ0 hγ1 (policyIteration hM hγ0 hγ1 i π) ≤
      policyValue M γ hM hγ0 hγ1 (policyIteration hM hγ0 hγ1 j π)

Uses 6 · Used by 2

Statement usesMarkov decision process · Stochastic Markov decision process · Policy iteration · Value of a policy

Proof usesPolicy improvement step · Policy improvement theorem

Used byPolicy iteration terminates · Once optimal, policy iteration stays optimal

TheoremOnce optimal, policy iteration stays optimal#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Write \(V^\pi\) for the value of a deterministic policy \(\pi : S \to A\), \(V^*\) for the optimal value, and \(\pi_k\) for the policy after \(k\) steps of policy iteration from \(\pi\). If \(i \le j\) and \(V^{\pi_i} = V^*\), then \(V^{\pi_j} = V^*\).

theorem policyValue_policyIteration_of_eq (π : S → A) {i j : ℕ} (hij : i ≤ j)
    (h : policyValue M γ hM hγ0 hγ1 (policyIteration hM hγ0 hγ1 i π) =
      optimalValue M γ hM hγ0 hγ1) :
    policyValue M γ hM hγ0 hγ1 (policyIteration hM hγ0 hγ1 j π) =
      optimalValue M γ hM hγ0 hγ1

Uses 7 · Used by 1

Statement usesMarkov decision process · Stochastic Markov decision process · Optimal value of a discounted Markov decision process · Policy iteration · Value of a policy

Proof usesNo policy beats the optimal value · Policy iteration never decreases the value

Used byPolicy iteration terminates

TheoremPolicy iteration terminates#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Write \(V^\pi\) for the value of a deterministic policy \(\pi : S \to A\), \(V^*\) for the optimal value, and \(N = |A|^{|S|}\) for the number of deterministic policies. For every deterministic policy \(\pi\), the policy \(\pi_N\) obtained after \(N\) steps of policy iteration from \(\pi\) is optimal: \(V^{\pi_N} = V^*\).

theorem policyValue_policyIteration [DecidableEq S] (π : S → A) :
    policyValue M γ hM hγ0 hγ1 (policyIteration hM hγ0 hγ1 (Fintype.card (S → A)) π) =
      optimalValue M γ hM hγ0 hγ1

Uses 9

Statement usesMarkov decision process · Stochastic Markov decision process · Optimal value of a discounted Markov decision process · Policy iteration · Value of a policy

Proof usesPolicy improvement step · Away from optimality, improvement changes the value · Policy iteration never decreases the value · Once optimal, policy iteration stays optimal

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.