Theory MergeAnomaly
chapter‹ Annex: A Note on a Classical Example: The ``Merge Anomaly''›
theory MergeAnomaly
imports "HOL-CSP"
begin
text‹Manfred Broy proposed in his 'Habilitationsschrift' (⁋‹Published in
``A Theory for Nondeterminism, Parallelism, Communication, and Concurrency. TCS (1986)''›)
a stream processing language ‹AMPL›, which is in many respect similar to \<^theory>‹HOL-CSP›.
Unfortunately, the underlying Powerset-construction contained a error that made it possible
that in an interleaving between a stream ‹1⇧∞› and a stream ‹1.0⇧∞› a ‹0› can get ahead of the
leading ‹1› which contradicts the intuition that interleaving should preserve causality in
both inputs.
Since we believe in the importance of a ∗‹formally verified› semantics of a language for
concurrency, we take this anecdotical reference to the Merge-Anomaly as an example to
study in the process algebra \<^theory>‹HOL-CSP›, so in a setting with trace, failure and
failure/divergence semantics.
First, we define the three processes corresponding to the notation ‹1⇧∞›, ‹0⇧∞› and ‹1.0⇧∞›:
›
definition ones :: "nat process" where ‹ones = (μ X. 1 → X)›
definition zeros :: "nat process" where ‹zeros = (μ X. 0 → X)›
definition oneszeros :: "nat process" where ‹oneszeros = (μ X. □x∈{0,1} → X)›
text‹... and derive the more handy recursive stream-equations:›
lemma ones_rec: "ones = 1 → ones" by (subst cont_process_rec[OF ones_def]) simp_all
lemma zeros_rec: "zeros = 0 → zeros" by (subst cont_process_rec[OF zeros_def]) simp_all
lemma oneszeros_rec: "oneszeros = □x∈{0,1} → oneszeros"
by (subst cont_process_rec[OF oneszeros_def]) simp_all
text‹Now, we can establish that ‹ones ||| zeros› and ‹oneszeros› are indeed equal
in the failure/divergence semantics in \<^theory>‹HOL-CSP›. This is formally proven as follows: ›
lemma ones_Inter_zeros_eq_oneszeros : ‹ones ||| zeros = oneszeros›
proof (rule FD_antisym)
show ‹oneszeros ⊑⇩F⇩D ones ||| zeros›
proof (unfold oneszeros_def, induct rule: cont_fix_ind)
fix X assume ‹X ⊑⇩F⇩D ones ||| zeros›
have ‹ones ||| zeros = (1 → (ones ||| 0 → zeros)) □ (0 → (1 → ones ||| zeros))›
by (subst ones_rec, subst zeros_rec) (simp add: write0_Inter_write0)
also have ‹… = (1 → (ones ||| zeros)) □ (0 → (ones ||| zeros))›
by (simp del: One_nat_def flip: ones_rec zeros_rec)
also have ‹… = □a∈{0, 1} → (ones ||| zeros)›
by (metis Mprefix_Un_distrib Mprefix_singl Un_insert_right sup_bot.right_neutral)
also have ‹□a∈{0, 1} → X ⊑⇩F⇩D …›
by (simp add: ‹X ⊑⇩F⇩D ones ||| zeros› mono_Mprefix_FD)
finally show ‹□a∈{0, 1} → X ⊑⇩F⇩D ones ||| zeros› .
qed simp_all
next
show ‹ones ||| zeros ⊑⇩F⇩D oneszeros›
proof (unfold ones_def zeros_def, induct rule: parallel_fix_ind_inc)
fix X Y
assume hyps : ‹(Λ X. 1 → X)⋅X ||| Y ⊑⇩F⇩D oneszeros›
‹X ||| (Λ Y. 0 → Y)⋅Y ⊑⇩F⇩D oneszeros›
have ‹(Λ X. 1 → X)⋅X ||| (Λ Y. 0 → Y)⋅Y = (1 → X) ||| (0 → Y)› by simp
also have ‹… = (1 → (X ||| 0 → Y)) □ (0 → (1 → X ||| Y))›
by (simp add: write0_Inter_write0)
also have ‹… = □a ∈ {0, 1} → (if a = 0 then 1 → X ||| Y else X ||| 0 → Y)›
by (auto simp add: write0_def Mprefix_Det_Mprefix intro: mono_Mprefix_eq)
also have ‹… ⊑⇩F⇩D oneszeros›
by (subst oneszeros_rec)
(use hyps in ‹auto intro: mono_Mprefix_FD›)
finally show ‹(Λ X. 1 → X)⋅X ||| (Λ Y. 0 → Y)⋅Y ⊑⇩F⇩D oneszeros› .
qed simp_all
qed
text‹As a consequence, in the trace model, we can establish that there will be no ``Anomaly''
in \<^theory>‹HOL-CSP›, so ‹ones ||| (1 → zeros)› will be equal to ‹1 → oneszeros› in the
originally intended trace-projection. The proof proceeds indirectly over induction over the traces;
This is the recommended proof strategy if arguments over trace sets have to be established. In
contrast, an argument over the \<^term>‹lfp›-operator, which seems natural at first sight, is amazingly
complicated. We have:›
lemma ‹𝒯 (ones ||| (1 → zeros)) = 𝒯 (1 → oneszeros)› (is ‹?lhs = ?rhs›)
proof (rule set_eqI)
show ‹t ∈ ?lhs ⟷ t ∈ ?rhs› for t
proof (induct t)
case Nil show ?case by simp
next
case (Cons e t)
show ?case
proof (rule iffI)
assume ‹e # t ∈ 𝒯 (1 → oneszeros)›
hence ‹e = ev 1› ‹t ∈ 𝒯 oneszeros›
by (simp_all add: T_write0)
thus ‹e # t ∈ 𝒯 (ones ||| 1 → zeros)›
apply (subst ones_rec)
apply (simp del: One_nat_def add: write0_Inter_write0 T_Det T_write0)
apply (fold ones_rec ones_Inter_zeros_eq_oneszeros)
..
next
show ‹e # t ∈ 𝒯 (ones ||| 1 → zeros) ⟹ e # t ∈ 𝒯 (1 → oneszeros)›
apply (subst (asm) ones_rec)
apply (simp del: One_nat_def add: write0_Inter_write0 T_Det T_write0)
apply (fold ones_rec)
apply (unfold Cons.hyps)
apply (unfold ones_Inter_zeros_eq_oneszeros)
apply (subst (asm) (2) oneszeros_rec, subst oneszeros_rec)
by (auto simp add: T_Mprefix T_write0)
qed
qed
qed
text‹However, ‹ones ||| (1 → zeros)› will be ∗‹not› equal to ‹1 → oneszeros› in the failure
model and therefore not in the failure/divergence model. The deeper reason is the interleave
operator ∗‹can neither refuse› ‹0› or ‹1›; it is designed to be sensitive to the process
context and let pass any possible interleaving admitted by the context which is reflected
in the rule @{thm Read_Write_CSP_Laws.write0_Inter_write0}.›
lemma ‹ones ||| (1 → zeros) ≠ 1 → oneszeros› (is ‹?P1 ≠ ?P2›)
proof -
have ‹([ev 1], {ev 0}) ∉ ℱ ?P2›
by (subst oneszeros_rec)
(simp add: Process_eq_spec F_write0 F_Mprefix)
moreover have ‹([ev 1], {ev 0}) ∈ ℱ ?P1›
by (subst ones_rec, subst ones_rec)
(simp add: write0_Inter_write0 Process_eq_spec F_Det F_write0)
ultimately show ‹?P1 ≠ ?P2› by metis
qed
text‹One might ask what happens if we would have defined the process \<^const>‹oneszeros› via the
non-deterministic choice, so using the following definition:›
definition oneszeros' :: "nat process" where ‹oneszeros' = (μ X. ⊓x∈{0,1} → X)›
lemma oneszeros'_rec : ‹oneszeros' = ⊓x ∈ {0, 1} → oneszeros'›
by (subst cont_process_rec[OF oneszeros'_def]) simp_all
text‹But this means that already the first step in the above argument breaks down:
Since interleaving ∗‹can neither refuse› ‹0› or ‹1›, while the deterministic choice of
\<^const>‹oneszeros'› does, we can easily show:›
lemma ‹ones ||| zeros ≠ oneszeros'›
proof (rule notI)
assume ‹ones ||| zeros = oneszeros'›
with ones_Inter_zeros_eq_oneszeros have ‹oneszeros' = oneszeros› by metis
moreover have ‹([], {ev 0}) ∈ ℱ oneszeros'›
by (subst oneszeros'_rec)
(simp add: F_Mndetprefix')
moreover have ‹([], {ev 0}) ∉ ℱ oneszeros›
by (subst oneszeros_rec) (simp add: F_Mprefix)
ultimately show False by simp
qed
end