Theory Termination
section "Loop Termination"
theory Termination imports Embedding StructuredReasoning Loops begin
text_raw ‹\label{s:termination}›
text ‹Termination for loops can be shown by classical means (using a variant, or a measure
function), or by probabilistic means: We only need that the loop terminates \emph{with probability
one}.›
subsection ‹Trivial Termination›
text ‹A maximal transformer (program) doesn't affect termination. This is
essentially saying that such a program doesn't abort (or diverge).›
lemma maximal_Seq_term:
fixes r::"'s prog" and s::"'s prog"
assumes mr: "maximal (wp r)"
and ws: "well_def s"
and ts: "(λs. 1) ⊩ wp s (λs. 1)"
shows "(λs. 1) ⊩ wp (r ;; s) (λs. 1)"
proof -
note hs = well_def_wp_healthy[OF ws]
have "wp s (λs. 1) = (λs. 1)"
proof(rule antisym)
show "(λs. 1) ⊩ wp s (λs. 1)" by(rule ts)
have "bounded_by 1 (wp s (λs. 1))"
by(auto intro!:healthy_bounded_byD[OF hs])
thus "wp s (λs. 1) ⊩ (λs. 1)" by(auto intro!:le_funI)
qed
with mr show ?thesis
by(simp add:wp_eval embed_bool_def maximalD)
qed
text ‹From any state where the guard does not hold, a loop terminates
in a single step.›
lemma term_onestep:
assumes wb: "well_def body"
shows "«𝒩 G» ⊩ wp do G ⟶ body od (λs. 1)"
proof(rule le_funI)
note hb = well_def_wp_healthy[OF wb]
fix s
show "«𝒩 G» s ≤ wp do G ⟶ body od (λs. 1) s"
proof(cases "G s", simp_all add:wp_loop_nguard hb)
from hb have "sound (wp do G ⟶ body od (λs. 1))"
by(auto intro:healthy_sound[OF healthy_wp_loop])
thus "0 ≤ wp do G ⟶ body od (λs. 1) s" by(auto)
qed
qed
subsection ‹Classical Termination›
text ‹The first non-trivial termination result is quite standard: If we can provide a
natural-number-valued measure, that decreases on every iteration, and implies termination on
reaching zero, the loop terminates.›
lemma loop_term_nat_measure_noinv:
fixes m :: "'s ⇒ nat" and body :: "'s prog"
assumes wb: "well_def body"
and guard: "⋀s. m s = 0 ⟶ ¬ G s"
and variant: "⋀n. «λs. m s = Suc n» ⊩ wp body «λs. m s = n»"
shows "λs. 1 ⊩ wp do G ⟶ body od (λs. 1)"
proof -
note hb = well_def_wp_healthy[OF wb]
have "⋀n. (∀s. m s = n ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s)"
proof(induct_tac n)
fix n
show "∀s. m s = 0 ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s"
proof(clarify)
fix s
assume "m s = 0"
with guard have "¬ G s" by(blast)
with hb show "1 ≤ wp do G ⟶ body od (λs. 1) s"
by(simp add:wp_loop_nguard)
qed
assume IH: "∀s. m s = n ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s"
hence IH': "∀s. m s = n ⟶ 1 ≤ wp do G ⟶ body od «λs. True» s"
by(simp add:embed_bool_def)
have "∀s. m s = Suc n ⟶ 1 ≤ wp do G ⟶ body od «λs. True» s"
proof(intro fold_premise healthy_intros hb, rule le_funI)
fix s
show "«λs. m s = Suc n» s ≤ wp do G ⟶ body od «λs. True» s"
proof(cases "G s")
case False
hence "1 = «𝒩 G» s" by(auto)
also from wb have "... ≤ wp do G ⟶ body od (λs. 1) s"
by(rule le_funD[OF term_onestep])
finally show ?thesis by(simp add:embed_bool_def)
next
case True note G = this
from IH' have "«λs. m s = n» ⊩ wp do G ⟶ body od «λs. True»"
by(blast intro:use_premise healthy_intros hb)
with variant wb
have "«λs. m s = Suc n» ⊩ wp (body ;; do G ⟶ body od) «λs. True»"
by(blast intro:wp_Seq wd_intros)
hence "«λs. m s = Suc n» s ≤ wp (body ;; do G ⟶ body od) «λs. True» s"
by(auto)
also from hb G have "... = wp do G ⟶ body od «λs. True» s"
by(simp add:wp_loop_guard)
finally show ?thesis .
qed
qed
thus "∀s. m s = Suc n ⟶ 1 ≤ wp do G ⟶ body od (λs. 1) s"
by(simp add:embed_bool_def)
qed
thus ?thesis by(auto)
qed
text ‹This version allows progress to depend on an invariant. Termination is then determined by
the invariant's value in the initial state.›
lemma loop_term_nat_measure:
fixes m :: "'s ⇒ nat" and body :: "'s prog"
assumes wb: "well_def body"
and guard: "⋀s. m s = 0 ⟶ ¬ G s"
and variant: "⋀n. «λs. m s = Suc n» && «I» ⊩ wp body «λs. m s = n»"
and inv: "wp_inv G body «I»"
shows "«I» ⊩ wp do G ⟶ body od (λs. 1)"
proof -
note hb = well_def_wp_healthy[OF wb]
note scb = sublinear_sub_conj[OF well_def_wp_sublinear, OF wb]
have "«I» ⊩ wp do G ⟶ body od «λs. True»"
proof(rule use_premise, intro healthy_intros hb)
fix s
have "⋀n. (∀s. m s = n ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True» s)"
proof(induct_tac n)
fix n
show "∀s. m s = 0 ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True» s"
proof(clarify)
fix s
assume "m s = 0"
with guard have "¬ G s" by(blast)
with hb show "1 ≤ wp do G ⟶ body od «λs. True» s"
by(simp add:wp_loop_nguard)
qed
assume IH: "∀s. m s = n ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True» s"
show "∀s. m s = Suc n ∧ I s ⟶ 1 ≤ wp do G ⟶ body od «λs. True» s"
proof(intro fold_premise healthy_intros hb le_funI)
fix s
show "«λs. m s = Suc n ∧ I s» s ≤ wp do G ⟶ body od «λs. True» s"
proof(cases "G s")
case False with hb show ?thesis
by(simp add:wp_loop_nguard)
next
case True note G = this
have "«λs. m s = Suc n» && «I» && «G» =
«λs. m s = Suc n» && («I» && «I») && «G»"
by(simp)
also have "... = («λs. m s = Suc n» && «I») && («I» && «G»)"
by(simp add:exp_conj_assoc exp_conj_unitary del:exp_conj_idem)
also have "... = («λs. m s = Suc n» && «I») && («G» && «I»)"
by(simp only:exp_conj_comm)
also {
from inv hb have "«G» && «I» ⊩ wp body «I»"
by(rule wp_inv_stdD)
with variant
have "(«λs. m s = Suc n» && «I») && («G» && «I») ⊩
wp body «λs. m s = n» && wp body «I»"
by(rule entails_frame)
}
also from scb
have "wp body «λs. m s = n» && wp body «I» ⊩
wp body («λs. m s = n» && «I»)"
by(blast)
finally have "«λs. m s = Suc n » && « I » && « G » ⊩
wp body (« λs. m s = n » && « I »)" .
moreover {
from IH have "«λs. m s = n ∧ I s» ⊩ wp do G ⟶ body od «λs. True»"
by(blast intro:use_premise healthy_intros hb)
hence "«λs. m s = n» && «I» ⊩ wp do G ⟶ body od «λs. True»"
by(simp add:exp_conj_std_split)
}
ultimately
have "«λs. m s = Suc n » && « I » && « G » ⊩
wp (body ;; do G ⟶ body od) «λs. True»"
using wb by(blast intro:wp_Seq wd_intros)
hence "(«λs. m s = Suc n ∧ I s» && « G ») s ≤
wp (body ;; do G ⟶ body od) «λs. True» s"
by(auto simp:exp_conj_std_split)
with G have "«λs. m s = Suc n ∧ I s» s ≤
wp (body ;; do G ⟶ body od) «λs. True» s"
by(simp add:exp_conj_def)
also from hb G have "... = wp do G ⟶ body od «λs. True» s"
by(simp add:wp_loop_guard)
finally show ?thesis .
qed
qed
qed
moreover assume "I s"
ultimately show "1 ≤ wp do G ⟶ body od «λs. True» s"
by(auto)
qed
thus ?thesis by(simp add:embed_bool_def)
qed
subsection ‹Probabilistic Termination›
text ‹Any loop that has a non-zero chance of terminating after each step terminates with
probability 1.›
lemma termination_0_1:
fixes body :: "'s prog"
assumes wb: "well_def body"
and onestep: "(λs. p) ⊩ wp body «𝒩 G»"
and nzp: "0 < p"
and mb: "maximal (wp body)"
shows "λs. 1 ⊩ wp do G ⟶ body od (λs. 1)"
proof -
note hb = well_def_wp_healthy[OF wb]
note sb = healthy_scalingD[OF hb]
note sab = sublinear_subadd[OF well_def_wp_sublinear, OF wb, OF healthy_feasibleD, OF hb]
from hb have hloop: "healthy (wp do G ⟶ body od)"
by(rule healthy_intros)
hence swp: "sound (wp do G ⟶ body od (λs. 1))" by(blast)
txt ‹@{term p} is no greater than $1$, by feasibility.›
from onestep have onestep': "⋀s. p ≤ wp body «𝒩 G» s" by(auto)
also {
from hb have "unitary (wp body «𝒩 G»)" by(auto)
hence "⋀s. wp body «𝒩 G» s ≤ 1" by(auto)
}
finally have p1: "p ≤ 1" .
txt ‹This is the crux of the proof: that given a lower bound below $1$, we can find another,
higher one.›
have new_bound: "⋀k. 0 ≤ k ⟹ k ≤ 1 ⟹ (λs. k) ⊩ wp do G ⟶ body od (λs. 1) ⟹
(λs. p * (1-k) + k) ⊩ wp do G ⟶ body od (λs. 1)"
proof(rule le_funI)
fix k s
assume X: "λs. k ⊩ wp do G ⟶ body od (λs. 1)"
and k0: "0 ≤ k" and k1: "k ≤ 1"
from k1 have nz1k: "0 ≤ 1 - k" by(auto)
with p1 have "p * (1-k) + k ≤ 1 * (1-k) + k"
by(blast intro:mult_right_mono add_mono)
hence "p * (1 - k) + k ≤ 1"
by(simp)
txt ‹The new bound is @{term "p * (1-k) + k"}.›
hence "p * (1-k) + k ≤ «𝒩 G» s + «G» s * (p * (1-k) + k)"
by(cases "G s", simp_all)
txt ‹By the one-step termination assumption:›
also from onestep' nz1k
have "... ≤ «𝒩 G» s + «G» s * (wp body «𝒩 G» s * (1-k) + k)"
by (simp add: mult_right_mono ordered_comm_semiring_class.comm_mult_left_mono)
txt ‹By scaling:›
also from nz1k
have "... = «𝒩 G» s + «G» s * (wp body (λs. «𝒩 G» s * (1-k)) s + k)"
by(simp add:right_scalingD[OF sb])
txt ‹By the maximality (termination) of the loop body:›
also from mb k0
have "... = «𝒩 G» s + «G» s * (wp body (λs. «𝒩 G» s * (1-k)) s + wp body (λs. k) s)"
by(simp add:maximalD)
txt ‹By sub-additivity of the loop body:›
also from k0 nz1k
have "... ≤ «𝒩 G» s + «G» s * (wp body (λs. «𝒩 G» s * (1-k) + k) s)"
by(auto intro!:add_left_mono mult_left_mono sub_addD[OF sab] sound_intros)
also
have "... = «𝒩 G» s + «G» s * (wp body (λs. «𝒩 G» s + «G» s * k) s)"
by(simp add:negate_embed algebra_simps)
txt ‹By monotonicity of the loop body, and that @{term k} is a lower bound:›
also from k0 hloop le_funD[OF X]
have "... ≤ «𝒩 G» s +
«G» s * (wp body (λs. «𝒩 G» s + «G» s * wp do G ⟶ body od (λs. 1) s) s)"
by(iprover intro:add_left_mono mult_left_mono le_funI embed_ge_0
le_funD[OF mono_transD, OF healthy_monoD, OF hb]
sound_sum standard_sound sound_intros swp)
txt ‹Unrolling the loop once and simplifying:›
also {
have "⋀s. «𝒩 G» s + «G» s * wp body (wp do G ⟶ body od (λs. 1)) s =
«𝒩 G» s + «G» s * («𝒩 G» s + «G» s * wp body (wp do G ⟶ body od (λs. 1)) s)"
by(simp only:distrib_left mult.assoc[symmetric] embed_bool_idem embed_bool_cancel)
also have "⋀s. ... s = «𝒩 G» s + «G» s * wp do G ⟶ body od (λs. 1) s"
by(simp add:fun_cong[OF wp_loop_unfold[symmetric, where P="λs. 1", simplified, OF hb]])
finally have X: "⋀s. «𝒩 G» s + «G» s * wp body (wp do G ⟶ body od (λs. 1)) s =
«𝒩 G» s + «G» s * wp do G ⟶ body od (λs. 1) s" .
have "«𝒩 G» s + «G» s * (wp body (λs. «𝒩 G» s + «G» s *
wp do G ⟶ body od (λs. 1) s) s) =
«𝒩 G» s + «G» s * (wp body (λs. «𝒩 G» s + «G» s *
wp body (wp do G ⟶ body od (λs. 1)) s) s)"
by(simp only:X)
}
txt ‹Lastly, by folding two loop iterations:›
also
have "«𝒩 G» s + «G» s * (wp body (λs. «𝒩 G» s + «G» s *
wp body (wp do G ⟶ body od (λs. 1)) s) s) =
wp do G ⟶ body od (λs. 1) s"
by(simp add:wp_loop_unfold[OF _ hb, where P="λs. 1", simplified, symmetric]
fun_cong[OF wp_loop_unfold[OF _ hb, where P="λs. 1", simplified, symmetric]])
finally show "p * (1-k) + k ≤ wp do G ⟶ body od (λs. 1) s" .
qed
txt ‹If the previous bound lay in $[0,1)$, the new bound is strictly greater. This is where
we appeal to the fact that @{term p} is nonzero.›
from nzp have inc: "⋀k. 0 ≤ k ⟹ k < 1 ⟹ k < p * (1 - k) + k"
by(auto intro:mult_pos_pos)
txt ‹The result follows by contradiction.›
show ?thesis
proof(rule ccontr)
txt ‹If the loop does not terminate everywhere, then there must exist some state
from which the probability of termination is strictly less than one.›
assume "¬ ?thesis"
hence "¬ (∀s. 1 ≤ wp do G ⟶ body od (λs. 1) s)" by(auto)
then obtain s where point: "¬ 1 ≤ wp do G ⟶ body od (λs. 1) s" by(auto)
let ?k = "Inf (range (wp do G ⟶ body od (λs. 1)))"
from hloop
have Inflb: "⋀s. ?k ≤ wp do G ⟶ body od (λs. 1) s"
by(intro cInf_lower bdd_belowI, auto)
also from point have "wp do G ⟶ body od (λs. 1) s < 1" by(auto)
txt ‹Thus the least (infimum) probabilty of termination is strictly less than one.›
finally have k1: "?k < 1" .
hence "?k ≤ 1" by(auto)
moreover from hloop have k0: "0 ≤ ?k"
by(intro cInf_greatest, auto)
txt ‹The infimum is, naturally, a lower bound.›
moreover from Inflb have "(λs. ?k) ⊩ wp do G ⟶ body od (λs. 1)" by(auto)
ultimately
txt ‹We can therefore use the previous result to find a new bound, \ldots›
have "⋀s. p * (1 - ?k) + ?k ≤ wp do G ⟶ body od (λs. 1) s"
by(blast intro:le_funD[OF new_bound])
txt ‹\ldots which is lower than the infimum, by minimality, \ldots›
hence "p * (1 - ?k) + ?k ≤ ?k"
by(blast intro:cInf_greatest)
txt ‹\ldots yet also strictly greater than it.›
moreover from k0 k1 have "?k < p * (1 - ?k) + ?k" by(rule inc)
txt ‹We thus have a contradiction.›
ultimately show False by(simp)
qed
qed
end