| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
SMCDEL.Language
Description
This module defines the language of Dynamic Epistemic Logic (DEL). Keeping the syntax definition separate from the semantics allows us to use the same language throughout the whole report, for both the explicit and the symbolic model checkers.
Synopsis
- newtype Prp = P Int
- defaultVocabulary :: [Prp]
- freshp :: [Prp] -> Prp
- class HasVocab a where
- type Agent = String
- alice :: Agent
- bob :: Agent
- carol :: Agent
- defaultAgents :: [Agent]
- newtype AgAgent = Ag Agent
- newtype Group = Group [Agent]
- data Form
- = Top
- | Bot
- | PrpF Prp
- | Neg Form
- | Conj [Form]
- | Disj [Form]
- | Xor [Form]
- | Impl Form Form
- | Equi Form Form
- | Forall [Prp] Form
- | Exists [Prp] Form
- | K Agent Form
- | Ck [Agent] Form
- | Dk [Agent] Form
- | Kw Agent Form
- | Ckw [Agent] Form
- | Dkw [Agent] Form
- | PubAnnounce Form Form
- | PubAnnounceW Form Form
- | Announce [Agent] Form Form
- | AnnounceW [Agent] Form Form
- | Dia DynamicOp Form
- ite :: Form -> Form -> Form -> Form
- pubAnnounceStack :: [Form] -> Form -> Form
- pubAnnounceWhetherStack :: [Form] -> Form -> Form
- booloutofForm :: [Prp] -> [Prp] -> Form
- oneOf :: [Form] -> Form
- data DynamicOp = Dyn !String !Dynamic
- box :: DynamicOp -> Form -> Form
- class HasAgents a where
- class Pointed a b
- class HasVocab a => Semantics a where
- (|=) :: Semantics a => a -> Form -> Bool
- class Optimizable a where
- class HasPrecondition a where
- class (Show a, Show b, HasAgents a, Semantics a, HasPrecondition b) => Update a b where
- updates :: Update a b => a -> [b] -> a
- updateSequence :: Update a b => a -> [b] -> [a]
- haveSameAgents :: (HasAgents a, HasAgents b) => a -> b -> Bool
- showSet :: Show a => [a] -> String
- ppForm :: Form -> String
- ppFormWith :: (Prp -> String) -> Form -> String
- texForm :: Form -> String
- subformulas :: Form -> [Form]
- shrinkform :: Form -> [Form]
- substit :: Prp -> Form -> Form -> Form
- substitSet :: [(Prp, Form)] -> Form -> Form
- substitOutOf :: [Prp] -> [Prp] -> Form -> Form
- replPsInP :: [(Prp, Prp)] -> Prp -> Prp
- replPsInF :: [(Prp, Prp)] -> Form -> Form
- propsInForm :: Form -> [Prp]
- propsInForms :: [Form] -> [Prp]
- agentsInForm :: Form -> [Agent]
- simplify :: Form -> Form
- simStep :: Form -> Form
- newtype BF = BF Form
- randomboolformWith :: [Prp] -> Int -> Gen BF
- newtype SimplifiedForm = SF Form
Propositions and Agents
Propositions are represented as integers in Haskell. Agents are strings.
Instances
defaultVocabulary :: [Prp] Source #
class HasVocab a where Source #
Instances
| HasVocab KripkeModel Source # | |
Defined in SMCDEL.Explicit.K Methods vocabOf :: KripkeModel -> [Prp] Source # | |
| HasVocab KripkeModelS5 Source # | |
Defined in SMCDEL.Explicit.S5 Methods vocabOf :: KripkeModelS5 -> [Prp] Source # | |
| HasVocab BelStruct Source # | |
| HasVocab BelStruct Source # | |
| HasVocab KnowStruct Source # | |
Defined in SMCDEL.Symbolic.S5 Methods vocabOf :: KnowStruct -> [Prp] Source # | |
| HasVocab KnowStruct Source # | |
Defined in SMCDEL.Symbolic.S5_DD Methods vocabOf :: KnowStruct -> [Prp] Source # | |
| (HasVocab a, Pointed a b) => HasVocab (a, b) Source # | |
Defined in SMCDEL.Language | |
defaultAgents :: [Agent] Source #
Five default agents given by `"1"` to `"5"`.
Formulas
The language \( \mathcal{L}(V) \) for a set of propositions \(V\) and a finite set of agents \(I\) is given by \[ \phi ::= \top \mid \bot \mid p \mid \lnot \phi \mid \bigwedge \Phi \mid \bigvee \Phi \mid \bigoplus \Phi \mid \phi \rightarrow \phi \mid \phi \leftrightarrow \phi \mid \forall P \phi \mid \exists P \phi \mid K_i \phi \mid C_\Delta \phi \mid D_\Delta \phi \mid [!\phi] \phi \mid [\Delta ! \phi] \phi \] where \(p \in V\), \(P \subseteq V\), \(|P|<\omega\), \(\Phi\subseteq\mathcal{L}(V)\), \(|\Phi|<\omega\), \(i \in I\) and \(\Delta \subset I\). We also write \(\phi \land \psi\) for \(\bigwedge \{ \phi,\psi \}\) and \(\phi \lor \psi\) for \(\bigvee \{ \phi,\psi \}\). The emph{boolean} formulas are those without \(K_i\), \(C_\Delta\), \(D_\Delta\), \([!\phi]\) and \([\Delta!\phi]\).
Hence, a formula can be (in this order): The constant top or bottom, an atomic proposition, a negation, a conjunction, a disjunction, an exclusive or, an implication, a bi-implication, a universal or existential quantification over a set of propositions, or a statement about knowledge, common-knowledge, distributed knowledge, a public announcement or an announcement to a group.
Some of these connectives are inter-definable, for example \(\phi\leftrightarrow\psi\) and \(\bigwedge \{ \psi\rightarrow\phi,\phi\rightarrow\psi \}\) are equivalent according to all semantics which we will use here. Hence we could shorten Definition~ref{def-dellang} and treat some connectives as abbreviations. This would lead to brevity and clarity in the formal definitions, but also to a decrease in performance of our model checking implementations. To continue with the first example: If we have Binary Decision Diagrams (BDDs) for \(\phi\) and \(\psi\), computing the BDD for \(\phi\leftrightarrow\psi\) in one operation by calling the appropriate method of a BDD package will be faster than rewriting it to a conjunction of two implications and then making three calls to these corresponding functions of the BDD package.
We extend our language with abbreviations for "knowing whether" and "announcing whether".
\[ K^?_i \phi := \bigvee \{ K_i \phi , K_i (\lnot \phi) \} \]
\[ D^?_i \phi := \bigvee \{ D_i \phi , D_i (\lnot \phi) \} \]
\[ [?! \phi] \psi := \bigwedge \{ \phi \rightarrow [!\phi]\psi , \lnot \phi \rightarrow [!\lnot\phi]\psi \} \]
\[ [I ?! \phi] \psi := \bigwedge \{ \phi \rightarrow [I ! \phi]\psi , \lnot \phi \rightarrow [I !\lnot\phi]\psi \} \]
Note that - also for performance reasons - the three "whether" operators occur as primitives and not as abbreviations.
Formulas
Constructors
| Top | True Constant |
| Bot | False Constant |
| PrpF Prp | Atomic Proposition |
| Neg Form | Negation |
| Conj [Form] | Conjunction |
| Disj [Form] | Disjunction |
| Xor [Form] | n-ary X-OR |
| Impl Form Form | Implication |
| Equi Form Form | Bi-Implication |
| Forall [Prp] Form | Boolean Universal Quantification |
| Exists [Prp] Form | Boolean Existential Quantification |
| K Agent Form | Knowing that |
| Ck [Agent] Form | Common knowing that |
| Dk [Agent] Form | Distributed knowing that |
| Kw Agent Form | Knowing whether |
| Ckw [Agent] Form | Common knowing whether |
| Dkw [Agent] Form | Distributed knowing whether |
| PubAnnounce Form Form | Public announcement that |
| PubAnnounceW Form Form | Public announcement whether |
| Announce [Agent] Form Form | (Semi-)Private announcement that |
| AnnounceW [Agent] Form Form | (Semi-)Private announcement whether |
| Dia DynamicOp Form | Dynamic Diamond |
Instances
Abbreviations
pubAnnounceStack :: [Form] -> Form -> Form Source #
Abbreviation for a sequence of announcements using.
booloutofForm :: [Prp] -> [Prp] -> Form Source #
Abbreviation to say that exactly a given subset of a set of propositions is true.
Dynamic Operators
Instances
| Show DynamicOp Source # | |
| Eq DynamicOp Source # | |
| Ord DynamicOp Source # | |
Typeclasses for Semantics
class HasAgents a where Source #
Instances
Instances
class HasVocab a => Semantics a where Source #
Instances
| Semantics KripkeModel Source # | |
Defined in SMCDEL.Explicit.K | |
| Semantics MultipointedModel Source # | |
Defined in SMCDEL.Explicit.K | |
| Semantics PointedModel Source # | |
Defined in SMCDEL.Explicit.K | |
| Semantics KripkeModelS5 Source # | |
Defined in SMCDEL.Explicit.S5 | |
| Semantics MultipointedModelS5 Source # | |
Defined in SMCDEL.Explicit.S5 | |
| Semantics PointedModelS5 Source # | |
Defined in SMCDEL.Explicit.S5 | |
| Semantics BelScene Source # | |
| Semantics BelStruct Source # | |
| Semantics MultipointedBelScene Source # | |
Defined in SMCDEL.Symbolic.K | |
| Semantics BelScene Source # | |
| Semantics BelStruct Source # | |
| Semantics MultipointedBelScene Source # | |
Defined in SMCDEL.Symbolic.Ki | |
| Semantics KnowScene Source # | |
| Semantics KnowStruct Source # | |
Defined in SMCDEL.Symbolic.S5 | |
| Semantics MultipointedKnowScene Source # | |
Defined in SMCDEL.Symbolic.S5 | |
| Semantics KnowScene Source # | |
| Semantics KnowStruct Source # | |
Defined in SMCDEL.Symbolic.S5_DD | |
| Semantics MultipointedKnowScene Source # | |
Defined in SMCDEL.Symbolic.S5_DD | |
class Optimizable a where Source #
Instances
| Optimizable PointedModelS5 Source # | |
Defined in SMCDEL.Explicit.S5 Methods optimize :: [Prp] -> PointedModelS5 -> PointedModelS5 Source # | |
| Optimizable BelStruct Source # | |
| Optimizable MultipointedBelScene Source # | |
Defined in SMCDEL.Symbolic.K Methods optimize :: [Prp] -> MultipointedBelScene -> MultipointedBelScene Source # | |
| Optimizable KnowScene Source # | |
| Optimizable KnowStruct Source # | |
Defined in SMCDEL.Symbolic.S5 Methods optimize :: [Prp] -> KnowStruct -> KnowStruct Source # | |
| Optimizable MultipointedKnowScene Source # | |
Defined in SMCDEL.Symbolic.S5 Methods optimize :: [Prp] -> MultipointedKnowScene -> MultipointedKnowScene Source # | |
| Optimizable KnowScene Source # | |
| Optimizable KnowStruct Source # | |
Defined in SMCDEL.Symbolic.S5_DD Methods optimize :: [Prp] -> KnowStruct -> KnowStruct Source # | |
| Optimizable MultipointedKnowScene Source # | |
Defined in SMCDEL.Symbolic.S5_DD Methods optimize :: [Prp] -> MultipointedKnowScene -> MultipointedKnowScene Source # | |
Type classes for Updates
class HasPrecondition a where Source #
Instances
class (Show a, Show b, HasAgents a, Semantics a, HasPrecondition b) => Update a b where Source #
Minimal complete definition
Methods
unsafeUpdate :: a -> b -> a Source #
checks :: [a -> b -> Bool] Source #
Instances
updates :: Update a b => a -> [b] -> a Source #
Execute a list of updates, return the final resulting state.
updateSequence :: Update a b => a -> [b] -> [a] Source #
Execute a list of updates, return the list of starting, intermediate and final result states.
haveSameAgents :: (HasAgents a, HasAgents b) => a -> b -> Bool Source #
Check that two modelsactionsetc. have the same agents.
Pretty-printing
ppFormWith :: (Prp -> String) -> Form -> String Source #
Pretty-print a formula with a translation for atomic propositions.
Subformulas and Shrinking
subformulas :: Form -> [Form] Source #
List of subformulas, including the given formula itself.
In particular this is used in the shrink function for QuickCheck.
shrinkform :: Form -> [Form] Source #
Substitution
substit :: Prp -> Form -> Form -> Form Source #
Substitute a formula for a proposition in a formula. As a safety measure this method will fail whenever the proposition to be replaced occurs in a quantifier. All other cases are done by recursion.
substitSet :: [(Prp, Form)] -> Form -> Form Source #
Apply multiple substitutions after each other. Note: in general this is *not* the same as simultaneous substitution. It is equivalent to simultaneous substitution if none of the replaced propositions occurs in the replacement formulas.
substitOutOf :: [Prp] -> [Prp] -> Form -> Form Source #
The "out of" substitution \([A \sqsubseteq B]\phi\).
replPsInF :: [(Prp, Prp)] -> Form -> Form Source #
Replace propositions in a formula. In contrast to the previous substitution function this *is* simultaneous.
Vocabulary of a formula
propsInForm :: Form -> [Prp] Source #
List of all propositions occurring in a formula.
propsInForms :: [Form] -> [Prp] Source #
agentsInForm :: Form -> [Agent] Source #
List of all agents occurring in a formula.
Simplification
simplify :: Form -> Form Source #
Simplify a formula using boolean equivalences. For example, remove double negations and ``bubble up'' \(\bot\) and \(\top\) in conjunctions and disjunctions, respectively.
Example for simplify
Consider this rather unnatural formula:
>>>let testForm = Forall [P 3] $ Equi (Disj [ Bot, PrpF $ P 3, Bot ]) (Conj [ Top , Xor [Top,Kw alice (PrpF (P 4))] , AnnounceW [alice,bob] (PrpF (P 5)) (Kw bob $ PrpF (P 5)) ])>>>testFormForall [P 3] (Equi (Disj [Bot,PrpF (P 3),Bot]) (Conj [Top,Xor [Top,Kw "Alice" (PrpF (P 4))],AnnounceW ["Alice","Bob"] (PrpF (P 5)) (Kw "Bob" (PrpF (P 5)))]))>>>simplify testFormForall [P 3] (Equi (PrpF (P 3)) (Conj [Xor [Top,Kw "Alice" (PrpF (P 4))],AnnounceW ["Alice","Bob"] (PrpF (P 5)) (Kw "Bob" (PrpF (P 5)))]))
Generating random formulas
newtype SimplifiedForm Source #
Instances
| Arbitrary SimplifiedForm Source # | Simplified Formulas |
Defined in SMCDEL.Language | |
| Show SimplifiedForm Source # | |
Defined in SMCDEL.Language Methods showsPrec :: Int -> SimplifiedForm -> ShowS # show :: SimplifiedForm -> String # showList :: [SimplifiedForm] -> ShowS # | |
| Eq SimplifiedForm Source # | |
Defined in SMCDEL.Language Methods (==) :: SimplifiedForm -> SimplifiedForm -> Bool # (/=) :: SimplifiedForm -> SimplifiedForm -> Bool # | |
| Ord SimplifiedForm Source # | |
Defined in SMCDEL.Language Methods compare :: SimplifiedForm -> SimplifiedForm -> Ordering # (<) :: SimplifiedForm -> SimplifiedForm -> Bool # (<=) :: SimplifiedForm -> SimplifiedForm -> Bool # (>) :: SimplifiedForm -> SimplifiedForm -> Bool # (>=) :: SimplifiedForm -> SimplifiedForm -> Bool # max :: SimplifiedForm -> SimplifiedForm -> SimplifiedForm # min :: SimplifiedForm -> SimplifiedForm -> SimplifiedForm # | |