Theory Conclusion
chapter‹ Conclusion ›
theory Conclusion
imports CSPM "HOL-Library.LaTeXsugar"
begin
text ‹In this session, we defined three architectural operators: \<^const>‹GlobalDet›,
\<^const>‹MultiSync›, and \<^const>‹MultiSeq› as respective generalizations
of \<^term>‹P □ Q›, \<^term>‹P ⟦S⟧ Q›, and \<^term>‹P ❙; Q›.
The generalization of \<^term>‹P ⊓ Q›, \<^term>‹GlobalNdet›, is already in
\<^session>‹HOL-CSP› since it is required for some algebraic laws.›
text ‹We did this in a fully-abstract way, that is:
▪ \<^const>‹Det› is commutative, idempotent and admits \<^const>‹STOP› as a neutral element so
we defined \<^const>‹GlobalDet› on a \<^typ>‹'a set› \<^term>‹A› by making it equal
to \<^const>‹STOP› when \<^term>‹A = {}›. Continuity only holds for finite cases,
while the operator is always defined.
▪ \<^const>‹Ndet› is also commutative and idempotent so in \<^session>‹HOL-CSP›
\<^const>‹GlobalNdet› has been defined
on a \<^typ>‹'a set› \<^term>‹A› by making it equal to \<^const>‹STOP› when \<^term>‹A = {}›.
Beware of the fact that \<^const>‹STOP› is not the
neutral element for \<^const>‹Ndet› (this operator does not admit a neutral element) so
we ❙‹do not have› the equality
@{term [display, eta_contract = false] ‹(⊓p ∈ {a}. P p) = P a ⊓ (⊓p ∈ {}. P p)›}
while this holds for \<^const>‹Det› and \<^const>‹GlobalDet›).
Again, continuity only holds for finite cases.
▪ \<^const>‹Sync› is commutative but is not idempotent so we defined \<^const>‹MultiSync›
on a \<^typ>‹'a multiset› \<^term>‹M› to keep the multiplicity of the processes.
We made it equal to \<^const>‹STOP› when \<^term>‹M = {#}› but like \<^const>‹Ndet›,
\<^const>‹Sync› does not admit a neutral element so beware of the fact that in general
@{term [display, eta_contract = false] ‹(❙⟦S❙⟧p ∈# {#a#}. P p) ≠ P a ⟦S⟧ (❙⟦S❙⟧p ∈# {#}. P p)›}.
By construction, multiset are finite and therefore continuity holds.
▪ \<^const>‹Seq› is neither commutative nor idempotent, and \<^term>‹SKIP r› is neutral only on
the left hand side (note if the second type \<^typ>‹'r› of \<^typ>‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› is actually
\<^typ>‹unit›, that is to say we go back to the old version without parameterized termination,
it is neutral element on both sides, see @{thm Seq_SKIP SKIP_Seq}).
Therefore we defined \<^const>‹MultiSeq› on a \<^typ>‹'a list› \<^term>‹L› to keep the multiplicity
and the order of the processes, and the folding is done on the reversed list in order to
enjoy the neutrality of \<^term>‹SKIP r› on the left hand side.
For example, proving
@{term [eta_contract = false] ‹SEQ p ∈@ L1. P p ❙; SEQ p ∈@ L2. P p = SEQ p ∈@ (L1 @ L2). P p›}
in general requires \<^term>‹L2 ≠ []›.›
text ‹We presented two examples: Dining philosophers, and POTS.
In both, we underlined the usefulness of the architectural operators
for modeling complex systems.›
text ‹Finally we provided powerful results on \<^const>‹events_of› and \<^const>‹deadlock_free›
among which the most important is undoubtedly:
@{thm [display, eta_contract = false] MultiInter_deadlock_free[no_vars]}
This theorem allows, for example, to establish:
@{term [display, eta_contract = false]
‹0 < n ⟹ deadlock_free (❙|❙|❙| m ∈# mset [0..<n]. P m)›}
under the assumption that a family of processes parameterized by
\<^term>‹m› @{text "::"} \<^typ>‹nat› verifies \<^term>‹∀m < n::nat. deadlock_free (P m)›.
›
text ‹More recently, two operators \<^const>‹Throw› and \<^const>‹Interrupt› have been added.
The corresponding continuities and algebraic laws can also be found
in this session.›
end