Quelle  MuddyChildren.thy   Sprache: Isabelle

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory MuddyChildren
imports ClockView SPRViewDet
begin
(*>*)

subsection‹The Muddy Children›

text‹

 label{sec:kbps-theory-mc}

  first example of a multi-agent broadcast scenario is the classic
  children puzzle, one of a class of such puzzles that exemplify
 -obvious reasoning about mutual states of knowledge. It goes as
  🚫‹‹\S1.1, Example~7.2.5› in "FHMV:1995"›:
 begin{quotation}

 $N$ children are playing together, $k$ of whom get mud on their
 foreheads. Each can see the mud on the others' foreheads but not
 their own.

 A parental figure appears and says ``At least one of you has mud on your
 forehead.'', expressing something already known to each of them if $k >
 1$.

 The parental figure then asks ``Does any of you know whether you have mud
 on your own forehead?'' over and over.

 Assuming the children are perceptive, intelligent, truthful and they
 answer simultaneously, what will happen?
 end{quotation}
  puzzle relies essentially on \emph{synchronous public broadcasts}
  particular facts \emph{common knowledge}, and that agents are
  of the requisite logical inference.

  the mother has complete knowledge of the situation, we integrate
  behaviour into the environment. Each agent $\mbox{child}_i$
  with the following KBP:
 begin{center}
 \begin{tabular}{lll}
 $\mathbf{do}$\\
 & $\gcalt\ \hat{\mathbf{K}}_{\mbox{child}_i} \mbox{muddy}_i$ & $‹→›$ Say ``I know if my forehead is muddy''\\
 & $\gcalt\ ‹¬›\hat{\mathbf{K}}_{\mbox{child}_i} \mbox{muddy}_i$ & $‹→›$ Say nothing\\
 $\mathbf{od}$\\
 \end{tabular}
 end{center}
  $\hat{\mathbf{K}}_a ‹φ›$ abbreviates $\mathbf{K}_a
 ‹φ›\ ‹∨›\ \mathbf{K}_a ‹¬φ›$.

  this protocol is deterministic, we use the SPR algorithm of
 S\ref{sec:kbps-theory-spr-deterministic-protocols}.

 begin{wrapfigure}{r}{0.5\textwidth}
 \vspace{-20pt}
 \includegraphics[width=0.48\textwidth]{MC}
 \vspace{-10pt}
 \caption{The protocol of $\mbox{child}_0$.}
 \label{fig:mc}
 end{wrapfigure}

  model records a child's initial observation of the mother's
  and the muddiness of the other children in her initial
  state, and these states are not changed by @{term
 envTrans"}. The recurring common observation is all of the children's
  responses to the mother's questions. Being able to distinguish
  observations is crucial to making this a broadcast scenario.

  the algorithm for three children and minimising using
 's algorithm yields the automaton in Figure~\ref{fig:mc} for
 \mbox{child}_0$. The initial transitions are labelled with the
  observation, i.e., the cleanliness ``C'' or muddiness ``M'' of
  other two children. The dashed initial transition covers the case
  everyone is clean; in the others the mother has announced that
  is dirty. Later transitions simply record the actions
  by each of the agents, where ``K'' is the first action in
  above KBP, and ``N'' the second. Double-circled states are those
  which $\mbox{child}_0$ knows whether she is muddy, and
 -circled where she does not.

  essence the child counts the number of muddy foreheads she sees and
  that many rounds before announcing that she knows.

  that a solution to this puzzle is beyond the reach of the clock
  as it requires (in general) remembering the sequence of
  broadcasts of length proportional to the number of
 . We discuss this further in \S\ref{sec:kbps-muddychildren}.

 ›
(*<*)

datatype Agent = Child0 | Child1 | Child2
datatype Proposition = Dirty Agent

datatype ChildAct = SayIKnow | SayNothing

lemma Agent_univ: "(UNIV :: Agent set) = {Child0, Child1, Child2}"
  unfolding UNIV_def
  apply auto
  apply (case_tac x)
  apply auto
  done

instance Agent :: finite
  apply intro_classes
  apply (auto iff: Agent_univ)
  done

instantiation Agent :: linorder
begin

fun
  less_Agent
where
  "less_Agent Child0 Child0 = False"
| "less_Agent Child0 _ = True"
| "less_Agent Child1 Child2 = True"
| "less_Agent Child1 _ = False"
| "less_Agent Child2 _ = False"

definition
  less_eq_Agent :: "Agent → Agent → bool"
where
  "less_eq_Agent x y ≡ x = y ∨ x < y"

instance
  apply intro_classes
  unfolding less_eq_Agent_def
  apply (case_tac x, case_tac y, simp_all)
  apply (case_tac y, simp_all)
  apply (case_tac y, simp_all)
  apply (case_tac x, case_tac y, case_tac z, simp_all)
  apply (case_tac x, case_tac z, simp_all)
  apply (case_tac x, case_tac y, simp_all)
  apply (case_tac y, simp_all)
  apply (case_tac x, case_tac y, simp_all)
  apply (case_tac y, simp_all)
  apply (case_tac y, simp_all)
  done
end

instantiation Agent :: enum
begin

definition
  "enum_class.enum = [Child0, Child1, Child2]"

definition
  "enum_class.enum_all P = (P Child0 ∧ P Child1 ∧ P Child2)"

definition
  "enum_class.enum_ex P = (P Child0 ∨ P Child1 ∨ P Child2)"

instance
  apply standard
  unfolding enum_Agent_def enum_all_Agent_def enum_ex_Agent_def
  by auto (case_tac x, auto)+

end

lemma Act_univ: "(UNIV :: ChildAct set) = {SayIKnow, SayNothing}"
  unfolding UNIV_def
  apply auto
  apply (case_tac x)
  apply auto
  done

instance ChildAct :: finite
  by standard (auto iff: Act_univ)

instantiation ChildAct :: enum
begin

definition
  "enum_class.enum = [SayIKnow, SayNothing]"

definition
  "enum_class.enum_all P = (P SayIKnow ∧ P SayNothing)"

definition
  "enum_class.enum_ex P = (P SayIKnow ∨ P SayNothing)"

instance
  apply standard
  unfolding enum_ChildAct_def enum_all_ChildAct_def enum_ex_ChildAct_def
  by auto (case_tac x, auto)+

end

instantiation ChildAct :: linorder
begin

fun
  less_ChildAct
where
  "less_ChildAct SayIKnow SayNothing = True"
| "less_ChildAct _ _ = False"

definition
  less_eq_ChildAct :: "ChildAct → ChildAct → bool"
where
  "less_eq_ChildAct x y ≡ x = y ∨ x < y"

instance
  apply intro_classes
  unfolding less_eq_ChildAct_def
  apply (case_tac x, case_tac y, simp_all)
  apply (case_tac y, simp_all)
  apply (case_tac y, simp_all)
  apply (case_tac x, case_tac y, simp_all)
  apply (case_tac y, simp_all)
  done
end

type_synonym EnvAct = "unit"
type_synonym EnvState = "(bool × bool × bool) × (ChildAct × ChildAct × ChildAct)"
type_synonym AgentState = "bool × bool × bool"
type_synonym GlobalState = "(Agent, EnvState, AgentState) BEState"

definition "agents ≡ fromList [Child0, Child1, Child2]"

fun
  aChildIsDirty :: "bool → bool → bool → bool"
where
  "aChildIsDirty False False False = False"
| "aChildIsDirty _ _ _ = True"

definition
  initPS :: "bool → bool → bool → (Agent × (bool × bool × bool)) odlist"
where
  "initPS c0 c1 c2 ≡
     let acid = aChildIsDirty c0 c1 c2
      in fromList [ (Child0, (acid, c1, c2)), (Child1, (acid, c0, c2)), (Child2, (acid, c0, c1))]"

definition
  envInit :: "GlobalState list"
where
  "envInit ≡
    let bu = [False, True]
     in [ ( es = ((c0, c1, c2), (SayNothing, SayNothing, SayNothing)), ps = initPS c0 c1 c2 ) .
             c0 ← bu, c1 ← bu, c2 ← bu ]"

(* The environment is passive, but it still needs to do something in
   each round for the system as a whole to evolve. *)

definition
  envAction :: "GlobalState → EnvAct list"
where
  "envAction ≡ λ_. [()]"

(* Transitions involve broadcasting the children's private actions,
leaving their private states unchanged. *)

definition
  envTransES :: "EnvAct → (Agent → ChildAct) → EnvState → EnvState"
where
  "envTransES ≡ λeAct aAct s. (fst s, aAct Child0, aAct Child1, aAct Child2)"

definition
  envTrans :: "EnvAct → (Agent → ChildAct) → GlobalState → GlobalState"
where
  "envTrans eact aact s ≡ s ( es := envTransES eact aact (es s) )"

(* Common observation: the actions of the agents. *)

definition "envObsC ≡ snd"

definition
  envVal :: "GlobalState → Proposition → bool"
where
  "envVal ≡ λs p.
     case p of Dirty a →
       (case es s of ((c0, c1, c2), _) →
         (case a of
            Child0 → c0
          | Child1 → c1
          | Child2 → c2))"

(* FIXME This is a bit grot, this definition is already made for us in the locale. *)

definition "envObs ≡ λa s. (envObsC (es s), ODList.lookup (ps s) a)"

(* The KBP. Clearly subjective and deterministic. *)

abbreviation
  "Kor φ ψ ≡ Knot (Kand (Knot φ) (Knot ψ))"

definition
  jkbp :: "Agent → (Agent, Proposition, ChildAct) KBP"
where
  "jkbp a = [ ( guard = Kor (K (Kprop (Dirty a)))
                            (K (Knot (Kprop (Dirty a)))), action = SayIKnow ),
              ( guard = Kand (Knot (K (Kprop (Dirty a))))
                             (Knot (K (Knot (Kprop (Dirty a))))), action = SayNothing ) ]"

subsubsection‹Locale instantiations›

interpretation MC: Environment jkbp envInit envAction envTrans envVal envObs
  apply unfold_locales
  apply (auto simp: jkbp_def)
  done

subsubsection‹The Clock view implementation›

interpretation MC_Clock:
  FiniteLinorderEnvironment jkbp envInit envAction envTrans envVal envObs agents
  apply unfold_locales
  apply (simp add: Agent_univ agents_def)
  done

definition
  mc_ClockDFS
where
  "mc_ClockDFS ≡ ClockAutoDFS agents jkbp envInit envAction envTrans envVal envObs"

definition
  mc_ClockAlg
where
  "mc_ClockAlg ≡ mkClockAuto agents jkbp envInit envAction envTrans envVal envObs"

lemma (in FiniteLinorderEnvironment)
  "MC.Clock.implements mc_ClockAlg"
  unfolding mc_ClockAlg_def by (rule MC_Clock.mkClockAuto_implements)

subsubsection‹The SPR view implementation›

interpretation MC_SPR:
  FiniteDetBroadcastEnvironment jkbp envInit envAction envTrans envVal envObs agents envObsC
  apply unfold_locales
  prefer 3
  apply (fold envObs_def envAction_def envTrans_def)
  apply clarify
  apply (erule MC.SPR.jkbpDetI)
   apply (simp add: jkbp_def)
   apply (auto simp: jkbp_def)[1]

  unfolding envAction_def envTrans_def envObs_def agents_def
  apply (simp_all add: Agent_univ jkbp_def)

  done

definition
  mc_SPRDFS
where
  "mc_SPRDFS ≡ SPRDetAutoDFS agents jkbp envInit envAction envTrans envVal envObsC envObs"

definition
  mc_SPRAlg
where
  "mc_SPRAlg ≡ mkSPRDetAuto agents jkbp envInit envAction envTrans envVal envObsC envObs"

lemma (in FiniteDetBroadcastEnvironment)
  "MC.SPR.implements mc_SPRAlg"
  unfolding mc_SPRAlg_def by (rule MC_SPR.mkSPRDetAuto_implements)

end
(*>*)