Theory Topology_C2KA
section ‹Notions of Topology for \CCKAabbrv \label{sec:topology}›
text ‹
Orbits, stabilisers, and fixed points are notions that allow us to perceive a kind of topology of a system
with respect to the stimulus-response relationships among system agents. In this context, the term ``topology''
is used to capture the relationships (influence) and connectedness via stimuli of the agents in a distributed
system. It intends to capture a kind of reachability in terms of the possible behaviours for a given agent.
A \CCKAabbrv consists of two semimodules~$\ActSemimodule$ and~$\OutSemimodule$ for which we have a
\leftAct{\stim}~$\lSact$ and a \rightAct{\cka}~$\rKact$. Therefore, there are two complementary notions of orbits,
stabilisers, and fixed points within the context of agent behaviours and stimuli, respectively. In this way, one
can use these notions to think about distributed systems from two different perspectives, namely the behavioural
perspective provided by the action of stimuli on agent behaviours described by~$\ActSemimodule$ and the external
event (stimulus) perspective provided by the action of agent behaviours on stimuli described by~$\OutSemimodule$.
In this section, only the treatment of these notions with respect to the \leftSemimodule{\stim}~$\ActSemimodule$
and agent behaviours is provided. The same notions for the \rightSemimodule{\cka}~$\OutSemimodule$ and stimuli
can be provided in a very similar way.
When discussing the interplay between \CCKAabbrv and the notions of orbits, stabilisers, and fixed points, the
partial order of sub-behaviours~$\CKAle$ is extended to sets in order to express sets of agent behaviours
encompassing one another. For two subsets of agent behaviours~$A,B \STleq \CKAset$, we say that~$A$
\emph{is encompassed by}~$B$ (or~$B$ \emph{encompasses}~$A$), written~$\CKAencompass{A}{B}$, if and only
if~$\biglnotation{\forall}{a}{a \in A}{\lnotation{\exists}{b}{b \in B}{a \CKAle b}}$. In essence,~$A \CKAenc B$
indicates that every behaviour contained within the set~$A$ is a sub-behaviour of at least one behaviour in the
set~$B$. The encompassing relation~$\STIMenc$ for stimuli can be defined similarly.
Throughout this section, let~$\ActSemimodule$ be the unitary and zero-preserving \leftSemimodule{\stim} of a
\CCKAabbrv and let~$a \in \CKAset$.
›
theory Topology_C2KA
imports C2KA
begin
no_notation
comp (infixl "∘" 55)
and rtrancl ("(_⇧*)" [1000] 999)
text ‹
The locale \emph{topology-c2ka} extends the axiomatisation of \emph{c2ka} to support the notions of topology.
›
locale topology_c2ka = c2ka +
fixes orbit :: "'a::cka ⇒ 'a::cka set" ("Orb")
and strong_orbit :: "'a::cka ⇒ 'a::cka set" ("Orb⇩S")
and stabiliser :: "'a::cka ⇒ 'b::stimuli set" ("Stab")
and fixed :: "'a::cka ⇒ bool"
and encompassing_relation_behaviours :: "'a set ⇒ 'a set ⇒ bool" (infix "≪⇩𝒦" 50)
and encompassing_relation_stimuli :: "'b set ⇒ 'b set ⇒ bool" (infix "≪⇩𝒮" 50)
and induced :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "⊲" 50)
and orbit_equivalent :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "∼⇩𝒦" 50)
assumes orb_def: "x ∈ Orb(a) ⟷ (∃s. (s ∘ a = x))"
and orbs_def: "b ∈ Orb⇩S(a) ⟷ Orb(b) = Orb(a)"
and stab_def: "s ∈ Stab(a) ⟷ s ∘ a = a"
and fixed_def: "fixed(a) ⟷ (∀s::'b. s≠𝔡 ⟶ s ∘ a = a)"
and erb_def: "A ≪⇩𝒦 B ⟷ (∀a::'a. a ∈ A ⟶ (∃b. b ∈ B ∧ a ≤⇩𝒦 b))"
and ers_def: "E ≪⇩𝒮 F ⟷ (∀a::'b. a ∈ E ⟶ (∃b. b ∈ F ∧ a ≤⇩𝒮 b))"
and induced_def: "a ⊲ b ⟷ b ∈ Orb(a)"
and orbit_equivalent_def: "a ∼⇩𝒦 b ⟷ Orb(a) = Orb(b)"
begin
subsection ‹Orbits \label{sub:orbits}›
text ‹
The \emph{orbit} of~$a$ in~$\stim$ is the set given by~$\orb{a} = \sets{\lAct{a}{s}}{s \in \STIMset}$. The orbit of
an agent~$a \in \CKAset$ represents the set of all possible behavioural responses from an agent behaving as~$a$ to
any stimulus from~$\stim$. In this way, the orbit of a given agent can be perceived as the set of all possible
future behaviours for that agent.
›
text ‹
Lemma \emph{inf-K-enc-orb} provides an isotonicity law with respect to the orbits and the encompassing relation for agent behaviours.
›
lemma inf_K_enc_orb: "a ≤⇩𝒦 b ⟹ Orb(a) ≪⇩𝒦 Orb(b)"
unfolding erb_def orb_def
using inf_K_next_behaviour by blast
text ‹
The following lemmas provide a selection of properties regarding orbits and the encompassing relation for agent behaviours.
›
lemma enc_orb_add: "Orb(a) ≪⇩𝒦 Orb(a + b)"
using inf_K_enc_orb inf_add_K_right by auto
lemma enc_orb_exchange: "Orb((a*b) ; (c*d)) ≪⇩𝒦 Orb((a;c) * (b;d))"
using inf_K_enc_orb exchange_2 by blast
lemma enc_orb_seq_par: "Orb(a;b) ≪⇩𝒦 Orb(a*b)"
using inf_K_enc_orb seq_inf_par by auto
lemma enc_orb_add_seq_par: "Orb(a;b + b;a) ≪⇩𝒦 Orb(a*b)"
using inf_K_enc_orb add_seq_inf_par by auto
lemma enc_orb_parseq: "Orb((a*b);c) ≪⇩𝒦 Orb(a*(b;c))"
using inf_K_enc_orb exchange_3 by blast
lemma enc_orb_seqpar: "Orb(a;(b*c)) ≪⇩𝒦 Orb((a;b)*c)"
using inf_K_enc_orb exchange_4 by blast
lemma enc_orb_seqstar_parstar: "Orb(a⇧;) ≪⇩𝒦 Orb(a⇧*)"
using inf_K_enc_orb seqstar_inf_parstar by auto
lemma enc_orb_union: "Orb(a) ≪⇩𝒦 Orb(c) ∧ Orb(b) ≪⇩𝒦 Orb(c)
⟷ Orb(a) ∪ Orb(b) ≪⇩𝒦 Orb(c)"
unfolding erb_def
by auto
subsection ‹Stabilisers \label{sub:stabilisers}›
text ‹
The \emph{stabiliser} of~$a$ in~$\stim$ is the set given by~$\stab{a} = \sets{s \in \STIMset}{\lAct{a}{s} = a}$.
The stabiliser of an agent~$a \in \CKAset$ represents the set of stimuli which have no observable influence
(or act as neutral stimuli) on an agent behaving as~$a$.
›
text ‹
Lemma \emph{enc-stab-inter-add} provides a property regarding stabilisers and the encompassing relation for stimuli.
›
lemma enc_stab_inter_add: "Stab(a) ∩ Stab(b) ≪⇩𝒮 Stab(a + b)"
unfolding ers_def
by (auto simp add: stab_def, rename_tac s, rule_tac x="s" in exI, simp)
subsection ‹Fixed Points \label{sub:fixed_points}›
text ‹
An element~$a \in \CKAset$ is called a \emph{fixed point} if~$\lnotation{\forall}{s}{s \in \STIMset \STdiff \set{\Dstim}}{\lAct{a}{s} = a}$.\linebreak
When an agent behaviour is a fixed point, it is not influenced by any stimulus other than the deactivation stimulus~$\Dstim$.
It is important to note that since~$\ActSemimodule$ is zero-preserving, every agent behaviour becomes inactive when subjected to the
deactivation stimulus~$\Dstim$. Because of this, we exclude this special case when discussing fixed point agent behaviours.
›
lemma zerofix [simp]: "s ∘ 0 = 0"
proof -
have "0 = 𝔡 ∘ a" by simp
hence "s ∘ 0 = s ∘ (𝔡 ∘ a)" by simp
hence "s ∘ 0 = (s ⊙ 𝔡) ∘ a" by (simp only: lsemimodule3 [symmetric])
thus "s ∘ 0 = 0" by simp
qed
text ‹
The following lemmas provide a selection of properties regarding fixed agent behaviours.
›
lemma fixed_zero: "fixed(0)"
unfolding fixed_def
by simp
lemma fixed_a_b_add: "fixed(a) ∧ fixed(b) ⟶ fixed(a + b)"
unfolding fixed_def
by simp
lemma fix_not_deactivation: "s ∘ a = a ∧ λ(s,a) = 𝔡 ⟹ a = 0"
proof -
assume E: "s ∘ a = a ∧ λ(s,a) = 𝔡"
hence "s ∘ (a;1) = a" by simp
hence "(s∘a) ; (λ(s,a)∘1) = a" by (simp only: cascadingaxiom)
hence "0 = a" by (simp add: E)
thus ?thesis by auto
qed
lemma fixed_a_b_seq: "fixed(a) ∧ fixed(b) ⟶ fixed(a ; b)"
unfolding fixed_def
proof (rule impI)
assume hyp: "(∀s. s ≠ 𝔡 ⟶ s ∘ a = a) ∧ (∀s. s ≠ 𝔡 ⟶ s ∘ b = b)"
have C1: "(∀s. λ(s,a) = 𝔡 ⟶ s ≠ 𝔡 ⟶ s ∘ (a ; b) = a ; b)"
proof -
have E: "(∀s. s ≠ 𝔡 ∧ λ(s,a) = 𝔡 ⟶ s ∘ (a ; b) = 0)" by simp
hence "(∀s. s ≠ 𝔡 ∧ λ(s,a) = 𝔡 ⟶ s ∘ a = a ∧ λ(s,a) = 𝔡)"
by (simp add: hyp)
moreover have "(∀s. s ∘ a = a ∧ λ(s,a) = 𝔡 ⟶ a = 0)"
by (simp add: fix_not_deactivation)
ultimately have "(∀s. s ≠ 𝔡 ∧ λ(s,a) = 𝔡 ⟶ a = 0)" by auto
thus ?thesis by (auto simp add: E)
qed
moreover have C2: "(∀s. λ(s,a) ≠ 𝔡 ⟶ s ≠ 𝔡 ⟶ s ∘ (a ; b) = a ; b)"
by (simp add: hyp)
ultimately show "(∀s. s ≠ 𝔡 ⟶ s ∘ (a ; b) = a ; b)" by blast
qed
subsection ‹Strong Orbits and Induced Behaviours \label{sub:strong_orbits_and_induced_behaviours}›
text ‹
The \emph{strong orbit} of~$a$ in~$\stim$ is the set given by~$\orbS{a} = \sets{b \in \CKAset}{\orb{b} = \orb{a}}$.
Two agents are in the same strong orbit, denoted~$a \CKAsim b$ for~$a,b \in \CKAset$, if and only if their orbits are
identical. This is to say when~$a \CKAsim b$, if an agent behaving as~$a$ is influenced by a stimulus to behave as~$b$,
then there exists a stimulus which influences the agent, now behaving as~$b$, to revert back to its original behaviour~$a$.
The influence of stimuli on agent behaviours is called the \emph{induced behaviours} via stimuli. Let~$a,b \in \CKAset$
be agent behaviours with~$a \neq b$. We say that~$b$ is \emph{induced by~$a$ via stimuli} (denoted by~$\induced{b}{a}$)
if and only if~$\lnotation{\exists}{s}{s \in \STIMset}{\lAct{a}{s} = b}$. The notion of induced behaviours allows us to make
some predictions about the evolution of agent behaviours in a given system by providing some insight into how different agents
can respond to any stimuli.
›
text ‹
Lemma \emph{fixed-not-induce} states that if an agent has a fixed point behaviour, then it does not induce any agent behaviours via stimuli besides the inactive behaviour~$0$.
›
lemma fixed_not_induce: "fixed(a) ⟶ (∀b. b ≠ 0 ∧ b ≠ a ⟶ ¬(a ⊲ b))"
proof -
have "⋀s. s = 𝔡 ∨ s ≠ 𝔡 ⟹ (∀t. t ≠ 𝔡 ⟶ t ∘ a = a) ⟹ s ∘ a ≠ 0
⟹ s ∘ a ≠ a ⟹ False"
by (erule disjE, simp_all)
hence "⋀s. (∀t. t ≠ 𝔡 ⟶ t ∘ a = a) ⟹ s ∘ a ≠ 0 ⟹ s ∘ a ≠ a ⟹ False"
by simp
thus ?thesis
unfolding fixed_def induced_def orb_def
by auto
qed
text ‹
Lemma \emph{strong-orbit-both-induced} states that all agent behaviours which belong to the same strong orbit are mutually induced via some (possibly different) stimuli.
This is to say that if two agent behaviours are in the same strong orbit, then there exists inverse stimuli for each agent behaviour in a
strong orbit allowing an agent to revert back to its previous behaviour.
›
lemma in_own_orbit: "a ∈ Orb(a)"
unfolding orb_def
by (rule_tac x="𝔫" in exI, simp)
lemma strong_orbit_both_induced: "a ∼⇩𝒦 b ⟶ a ⊲ b ∧ b ⊲ a"
unfolding orbit_equivalent_def induced_def
by (blast intro: in_own_orbit)
text ‹
Lemma \emph{strong-orbit-induce-same} states that if two agent behaviours are in the same strong orbit, then a third behaviour can be induced via stimuli by either of
the behaviours within the strong orbit. This is to say that each behaviour in a strong orbit can induce the same set of behaviours
(perhaps via different stimuli).
›
lemma strong_orbit_induce_same: "a ∼⇩𝒦 b ⟶ (a ⊲ c ⟷ b ⊲ c)"
unfolding induced_def orbit_equivalent_def
by simp
end
end