| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Puzzles.Birthday
Contents
Description
This is a formalization of the Cheryl's birthday problem, which went viral in April 2015.
Here's the puzzle:
Albert and Bernard just met Cheryl. "When’s your birthday?" Albert asked Cheryl. Cheryl thought a second and said, "I’m not going to tell you, but I’ll give you some clues." She wrote down a list of 10 dates: May 15, May 16, May 19 June 17, June 18 July 14, July 16 August 14, August 15, August 17 "My birthday is one of these," she said. Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday. To Bernard, she whispered the day, and only the day. “Can you figure it out now?” she asked Albert. Albert: I don’t know when your birthday is, but I know Bernard doesn’t know, either. Bernard: I didn’t know originally, but now I do. Albert: Well, now I know, too! When is Cheryl’s birthday?
NB. Thanks to Amit Goel for suggesting the formalization strategy used in here.
Synopsis
- data Month
- data Day
- cv2Month :: String -> [CV] -> Month
- _undefiner_Month :: a
- type SMonth = SBV Month
- sMay :: SBV Month
- sJun :: SBV Month
- sJul :: SBV Month
- sAug :: SBV Month
- isMay :: SBV Month -> SBool
- isJun :: SBV Month -> SBool
- isJul :: SBV Month -> SBool
- isAug :: SBV Month -> SBool
- sCaseMonth :: Mergeable result => SBV Month -> result -> result -> result -> result -> result
- cv2Day :: String -> [CV] -> Day
- _undefiner_Day :: a
- type SDay = SBV Day
- sD14 :: SBV Day
- sD15 :: SBV Day
- sD16 :: SBV Day
- sD17 :: SBV Day
- sD18 :: SBV Day
- sD19 :: SBV Day
- isD14 :: SBV Day -> SBool
- isD15 :: SBV Day -> SBool
- isD16 :: SBV Day -> SBool
- isD17 :: SBV Day -> SBool
- isD18 :: SBV Day -> SBool
- isD19 :: SBV Day -> SBool
- sCaseDay :: Mergeable result => SBV Day -> result -> result -> result -> result -> result -> result -> result
- data Birthday = BD SMonth SDay
- mkBirthday :: Symbolic Birthday
- valid :: Birthday -> SBool
- puzzle :: ConstraintSet
- cheryl :: IO ()
Types and values
Months. We only put in the months involved in the puzzle for simplicity
Instances
Days. Again, only the ones mentioned in the puzzle.
Instances
_undefiner_Month :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
sCaseMonth :: Mergeable result => SBV Month -> result -> result -> result -> result -> result Source #
Case analyzer for the type Month.
_undefiner_Day :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
sCaseDay :: Mergeable result => SBV Day -> result -> result -> result -> result -> result -> result -> result Source #
Case analyzer for the type Day.
mkBirthday :: Symbolic Birthday Source #
Make a valid symbolic birthday
valid :: Birthday -> SBool Source #
Is this a valid birthday? i.e., one that was declared by Cheryl to be a possibility.
The puzzle
puzzle :: ConstraintSet Source #
Encode the conversation as given in the puzzle.
NB. Lee Pike pointed out that not all the constraints are actually necessary! (Private
communication.) The puzzle still has a unique solution if the statements a1 and b1
(i.e., Albert and Bernard saying they themselves do not know the answer) are removed.
To experiment you can simply comment out those statements and observe that there still
is a unique solution. Thanks to Lee for pointing this out! In fact, it is instructive to
assert the conversation line-by-line, and see how the search-space gets reduced in each
step.