| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
SMCDEL.Other.MCTRIANGLE
Description
This module implements an alternative representation of the Muddy Children, as proposed in:
- Nina Gierasimczuk, Jakub Szymanik (2011): A note on a generalization of the Muddy Children puzzle. https://doi.org/10.1145/2000378.2000409
The main idea is to not distinguish individual children who are in the same state which also means that their observations are the same. Sections of Pascal's triangle can then be used to solve the Muddy Children puzzle in a Kripke model with less worlds than needed in the classical analysis, namely \(2n+1\) instead of \(2^n\) for \(n\) children.
Synopsis
- data Kind
- type State = (Int, Int)
- data McModel = McM [State] [State] State
- mcModel :: State -> McModel
- posFrom :: McModel -> State -> [State]
- obsFor :: McModel -> Kind -> State
- posFor :: McModel -> Kind -> [State]
- type Quantifier = State -> Bool
- some :: Quantifier
- data McFormula
- = Neg McFormula
- | Conj [McFormula]
- | Qf Quantifier
- | KnowSelf Kind
- | NotKnowSelf Kind
- nobodyknows :: McFormula
- everyoneKnows :: McFormula
- eval :: McModel -> McFormula -> Bool
- mcUpdate :: McModel -> McFormula -> McModel
- step :: State -> Int -> McModel
- showme :: State -> IO ()
Documentation
type State = (Int, Int) Source #
States are pairs of integers indicating how many children are (clean,muddy).
A muddy children model consists of three things: A list of observational states, a list of factual states and a current state.
type Quantifier = State -> Bool Source #
Note that instead of naming or enumerating agents we only distinguish two Kind`s, the muddy and non-muddy ones, represented by Haskells constants Muddy` and Clean` which allow pattern matching.
Quantifiers on the number triangle, e.g. some.
some :: Quantifier Source #
The "some" quantifier.
The paper does not give a formal language definition, so here is our suggestion:
\[ \phi ::= \lnot \phi \mid \bigwedge \Phi \mid Q \mid K_b \mid \overline{K}_b \]
where $Phi$ ranges over finite sets of formulas, $b$ over ${0,1}$ and $Q$
over generalized quantifiers.
Note that when there are no agents of kind `b, the formulas
`KnowSelf b` and `NotKnowSelf b` are both true.
Hence `Neg (KnowSelf b)` and `NotKnowSelf b` are not the same!
Constructors
| Neg McFormula | |
| Conj [McFormula] | |
| Qf Quantifier | |
| KnowSelf Kind | |
| NotKnowSelf Kind |
nobodyknows :: McFormula Source #
Formula for ``Nobody knows their own state.''
everyoneKnows :: McFormula Source #
Formula for ``Everybody knows their own state.''
eval :: McModel -> McFormula -> Bool Source #
Note that in contrast to the standard DEL language the formulas are independent of how many children there are. This is due to our identification of agents with the same state and observations.
The semantics for the minimal language. The four nullary knowledge operators can be thought of as ``All agents who are (not) muddy do (not) know their own state.'' Hence they are vacuously true whenever there are no such agents. If there are, the agents do know their state iff they consider only one possibility (i.e. their observational state has only one successor).