Theory FunSeriesInHOL-CSP
chapter‹Annex: A Note on State-based Processes in HOL-CSP›
theory "FunSeriesInHOL-CSP"
imports "HOL-CSP" "HOL.Transcendental" "GenFixrec-HOLCF"
begin
text‹This section is intended to give an intuition to the power of HOL-CSP processes by a set
of examples. In our view, it can be stated that HOL-CSP are a more powerful modeling instrument
for indefinite behavior than, for example, co-inductive definitions, since they posses a theory
of synchronisation and monadic sequential composition that co-inductively defined streams lack.
On the other hand, there is no denying that the entire machinery is more complex.
›
section‹The 'Random' Key-Generator›
subsection‹Example for the basic Construction with ‹μ››
abbreviation key_generator_fun :: ‹('α set ⇒ 'α process) ⇒ ('α set ⇒ 'α process)›
where ‹key_generator_fun X A ≡ ⊓a ∈ A → X (A - {a})›
definition key_generator :: ‹'α set ⇒ 'α process› (‹KEY›)
where ‹key_generator ≡ μ X. (λ A. ⊓a ∈ A → X (A - {a}))›
lemma key_generator_fun_cont[simp]: ‹cont key_generator_fun›
by (simp add: cont_fun)
lemma key_generator_unfold: ‹KEY A = ⊓a ∈ A → KEY (A - {a})›
by (subst cont_process_rec[OF key_generator_def[THEN meta_eq_to_obj_eq]]) simp_all
text‹Now, the process \<^term>‹KEY ℕ› denotes the set of all traces that enumerate the natural
numbers without repetition... ›
subsection‹Example in High-level Notation›
text‹The ‹Fixrec ... where ...› notation provided by the generic fixpoint-support package
has the same effect as the construction above:›
Fixrec keygen ::"'α set ⇒ 'α process" where kg_rec : "keygen A = (⊓a ∈ A → keygen (A - {a}))"
section‹Cauchy-Series as Processes›
subsection‹The Construction in basic Steps (Again)›
text‹It is kind of fun - but also instructive wrt. the power and generality of the process type -
to see Cauchy-sequences of numerical approximations in the number system with base 10 as processes.
This shows that processes in HOL-CSP are not finite, not rational, but transcendent objects with
a non-enumerable cardinality.
›
definition digits :: ‹real ⇒ int process›
where ‹digits ≡ μ X. (λx. ⌊x⌋ → X ((frac x) * 10)) ›
lemma digits_unfold: ‹digits x = ⌊x⌋ → digits (frac x * 10)›
apply (subst cont_process_rec[OF digits_def[THEN meta_eq_to_obj_eq]])
by (simp add: cont_fun)(simp)
text‹ Note that the floor function ‹⌊x⌋› yields the largest integer smaller or equal ‹x›, while
‹frac x› returns the rest between ‹⌊x⌋› and ‹x›.
Now, the process \<^term>‹digits pi› enumerates the representation at base 10 of the
transcendental number ‹π›, so: ‹3 → 1 → 4 → 1 → 5 → 9 → ...›, while
while \<^term>‹digits (exp (1::real))› does the same for the transcendental number ‹e›.
While these two perfectly well-defined mathematical objects imported from the
\<^theory>‹HOL.Transcendental› theory have as such no computational content, their approximation
by a HOL-CSP process has. Although we do not yet have a code-generator that shows this... ;-)›
subsection‹The Example again in High-level Notation›
text‹The ‹Fixrec›-package supports this construction directly: ›
Fixrec digits' ::"real ⇒ int process"
where digits'_rec : "digits' x = ⌊x⌋ → digits' (frac x * 10)"
section‹The Collatz-Function as Process›
text‹Note that the Collatz function is unknown to be terminating; a standard definition in HOL
via the recursive function definitions such as @{command primrec} or @{command fun} is therefore
out of reach. This example shows, however, that it is perfectly possible to represent the Collatz
process as a recursive HOL-CSP process, since HOL-CSP is built for modeling potentially
non-terminating computations. ›
abbreviation Even where "Even ≡ Collect even"
abbreviation Odd where "Odd ≡ Collect odd"
abbreviation Div3 where "Div3 ≡ {x. x mod 3 = 0}"
text‹We use the deterministic choice to express a case-distinction:›
Fixrec Collatz ::"nat ⇒ nat process"
where Collatz_rec : "Collatz n = (□x ∈ ({0, 1} ∩ {n}) → Skip)
□ (□x ∈ ((Even - {0}) ∩ {n}) → Collatz (x div 2 ))
□ (□x ∈ ((Odd - {1}) ∩ {n}) → Collatz (3 * x + 1))"
section‹True Concurrent Evolution of States.›
text‹It is a common misconception of CSP that it can not handle "true-concurrent' computations
given that its fundamental concept of ∗‹events›: They are "indivisible obervations on a specific
time-point". However, the contrary is the case: Since HOL-CSP allows for modeling non-determinism
and potentially infinite states,
true-concurrent calculations over non-overlapping parts of a state are possible
between synchronisation points. If portions of a state are overlapping and computations do not
agree --- so: races will occur --- then these situations are represented in HOL-CSP as deadlock. ›
Fixrec Twos⇩L :: ‹nat ⇒ (nat × nat) process›
where Twos⇩L_unfold: ‹Twos⇩L n⇩1 = (□σ ∈ ({n⇩1<..} ∩ Even) × UNIV → Twos⇩L (fst σ))›
Fixrec Threes⇩R :: ‹nat ⇒ (nat × nat) process›
where Threes⇩R_unfold: ‹Threes⇩R n⇩2 = (□σ ∈ UNIV × ({n⇩2<..} ∩ Div3) → Threes⇩R (snd σ))›
text‹These two processes work on a state ‹σ›, consisting of a pair of two counters ‹n⇩1› and ‹n⇩2›.
While \<^const>‹Twos⇩L› choses an even number larger than its current local state ‹n⇩1›, \<^const>‹Threes⇩R›
chooses a number devisable by three larger than its current local state ‹n⇩2›. Putting these two
together via:
@{term [indent=10, margin=60]‹Twos⇩L 0 ⟦Id⟧ Threes⇩R 0›}
... where \<^term>‹Id› is the identity relation, this synchronization over these two processes
calculate independently two values but have to agree on a joint state. A trace of this combined
processes is, for example:
@{cartouche [indent=10, margin=60]‹(2,6) → (24,24) → (16,33) → ... ›}
Of course, this example is a bit simplistic since the the global state ‹σ=(n⇩1,n⇩2)› has a simple
structure, the access to the global variables is distinct and the underlying choices are deter-
ministic, so to speak, ∗‹angelic›. An obvious generalization of this handling of the common state
are algebraic lenses as provided by the theory ▩‹Optics› in the AFP. Wrt. to the choice, one might
model a more aggressive, i.e. ∗‹demonic› behaviour as follows: ›
Fixrec Twos⇩L' :: ‹nat ⇒ (nat × nat) process›
where Twos⇩L'_unfold: ‹Twos⇩L' n⇩1 = (⊓σ ∈ ({n⇩1<..} ∩ Even) × UNIV → Twos⇩L' (fst σ))›
Fixrec Threes⇩R' :: ‹nat ⇒ (nat × nat) process›
where Threes⇩R'_unfold: ‹Threes⇩R' n⇩2 = (⊓σ ∈ UNIV × ({n⇩2<..} ∩ Div3) → Threes⇩R' (snd σ))›
text‹The intersection may again be defined via:
@{term [indent=10, margin=60]‹Twos⇩L' 0 ⟦Id⟧ Threes⇩R' 0›}
but the traces of this combined process will contain explicit deadlocks on all places
where an agreement could not be reached due to "ruthless behaviour" demonic processes that
chose deviant values from each other... Which means that races occurred. ›
text‹One might want to prove these facts, i.e. that the synchronized processes produce only
streams enjoying the conjunction of the devisability properties and the agreement is angelic
or demonic. This is not too hard to do in HOL-CSP. The handy recursive equations needed for this,
e.g. @{thm [source] Twos⇩L_unfold} and @{thm [source] Threes⇩R'_unfold}, are provided by the
‹Fixrec›-package, as well as the fixpoint definitions @{thm [source] Twos⇩L_rec_def} etc.
that allow for fixpoint induction.›
text‹And there we go: We state that \<^const>‹Twos⇩L› and \<^const>‹Threes⇩R› in parallel composition
are the same to a process that does these computations in one step. The proof proceeds by breaking
the stated equality into two \<^term>‹(⊑⇩F⇩D)›-refinements that were each proven by fixpoint-induction.›
lemma parallel_exec :‹(Twos⇩L (fst σ) || Threes⇩R (snd σ))
= ((μ X. (λ(n⇩1, n⇩2). (□σ ∈((({n⇩1<..} ∩ Even )×({n⇩2<..} ∩ Div3))) → X σ)))σ)›
(is "?lhs σ = (fix ⋅ ?rhs) σ")
proof (rule FD_antisym)
show ‹ ?lhs σ ⊑⇩F⇩D (fix ⋅ ?rhs)(σ)› for σ
unfolding Twos⇩L_def Twos⇩L_rec_def Threes⇩R_def Threes⇩R_rec_def
proof -
have * : ‹adm (λx. ∀xa. fst x (fst xa) || snd x (snd xa)
⊑⇩F⇩D (μ x. (λ(n⇩1, n⇩2). Mprefix (({n⇩1<..} ∩ Even)
× ({n⇩2<..} ∩ Div3)) x)) xa)›
apply(rule adm_all,rule le_FD_adm_cont)
by (simp_all add: cont2cont_fun)
have ** : ‹ ({a<..} ∩ Even) × UNIV ∩ UNIV × ({b<..} ∩ Div3)
= ({a<..} ∩ Even) × ({b<..} ∩ Div3)› for a b::nat
by (simp add: Times_Int_Times)
show ‹ (μ x. (λn⇩1. □σ∈({n⇩1<..} ∩ Even) × UNIV → x (fst σ))) (fst σ)
|| (μ x. (λn⇩2. □σ∈UNIV × ({n⇩2<..} ∩ Div3) → x (snd σ))) (snd σ) ⊑⇩F⇩D (fix ⋅ ?rhs)(σ) ›
(is "(fix ⋅ ?lhs1)(fst σ) || (fix ⋅ ?lhs2)(snd σ) ⊑⇩F⇩D _ ")
apply(induct arbitrary:"σ" rule: parallel_fix_ind [where F = ‹?lhs1› and G = ‹?lhs2›])
using * apply auto
apply(subst Mprefix_Par_Mprefix)
using ** apply(auto)
apply(subst cont_process_rec [where P = ‹fix ⋅ ?rhs› ]) apply(rule refl) apply(auto)
by(rule mono_Mprefix_FD) force
qed
next
show ‹(fix ⋅ ?rhs) σ ⊑⇩F⇩D ?lhs σ› for σ
apply(induct arbitrary:"σ" rule: fix_ind [where F = ‹?rhs›], auto)
apply(subst Twos⇩L_unfold, subst Threes⇩R_unfold)
apply(subst Mprefix_Sync_Mprefix_subset, simp_all)
by (metis (no_types, lifting) Sigma_cong Times_Int_Times inf_top.right_neutral
inf_top_left mono_Mprefix_FD surjective_pairing)
qed
text‹Of course, we could use this modeling technique --- which is roughly similar to the conjunction
of two preconditions --- by adding a process that ensures that first and second component of
the joint agree in their value, that is:
@{cartouche [indent=10, margin=60]‹(6,6) → (24,24) → (36,36) → ... ›}
We bind the combined process to the constant ‹Join›:
›
Fixrec Join :: ‹nat × nat ⇒ (nat × nat) process›
where Join_unfold: ‹Join (n⇩1, n⇩2) = (□σ ∈ ({n⇩1<..} ∩ Even) × ({n⇩2<..} ∩ Div3) → Join σ)›
text‹With \<^const>‹Join›, the statement of @{thm [source] parallel_exec} reads:›
corollary parallel_exec_Join: ‹(Twos⇩L (fst σ) || Threes⇩R (snd σ)) = Join σ›
unfolding Join_def Join_rec_def by (fact parallel_exec)
text‹... which is set under the constraint as follows:
\<^term>‹ Join σ || (μ X . (λσ. □σ∈Id → X σ)) σ ›
We refrain from a formal proof which will follow the lines of @{thm "parallel_exec"}.›
end