8 ms·

Formally modeled Dreidel for no good reason

243 points by JNRowe 3y ago

mjb 3y ago
I love this, and have similar feelings about PRISM. I hope recent work to add probabilistic properties to TLA+ and P provide a route towards doing this kind of work with languages that are easier to use. While this example is a bit silly, the ability to check properties like availability, latency, etc alongside the traditional liveness and safety properties is super useful for distributed systems work.
kennethrc 3y ago
"Was this worth it? Ugh no I hate PRISM" :) ... that being said, as someone who only has a passing knowledge of the Dreidel the article held my interest
e28eta 3y ago
My first thought for “can’t generalize over number of players” was that he could write code that emits a PRISM program…
- tgv 3y ago
  Passing the state from n to n-1 players is harder.
  - hwayne 3y ago
    I think I can do that with having an action for each player that passes if they don't have any money. The tricky bit is implementing the ante logic to only add n-1 coins to the pot, but I have an idea on how to hardcode that. After that it's "just" a matter of generating it all with another program.
- ColonelPhantom 3y ago
  This is also what I did when I used PRISM for my thesis. Honestly also not the greatest experience, but I think it does show that the limitations of the PRISM language are not inherent to the problem domain.
meepmorp 3y ago
Finally, someone calls out the lie that is Big Dreidel.
- FergusArgyll 3y ago
  A Wikipedia gem: "Robert Feinerman has shown that the game of dreidel is unfair, in that the first player to spin has a better expected outcome than the second player, and the second better than the third, and so on"
  - gbacon 3y ago
    That’d be interesting to see modeled out in PRISM.
smachiz 3y ago
When I play dreidel you ante every turn… it does not take 860 spins.
- tunesmith 3y ago
  To really teach people about gambling, try a variation where everyone someone antes, they ante a second coin to the "house".
  - willcipriano 3y ago
    Dad's job is to sit at the table and eat a handful of coins per round.
    - names_are_hard 3y ago
      When I was little and we'd get ice cream, my mother would get each of the kids a cone but not for herself. Then she'd do rounds and eat a little from each of ours. We were annoyed, but she explained that this process is called "taxes".
kromem 3y ago
Conversely, in an age before TV or Internet, the longer the game could keep kids occupied the better, no? We might even imagine that anthropologically given the role of keeping kids occupied there were other games that were more fun but of a shorter duration which died out because parents instead pushed for teaching their kids the cultural equivalent of Monopoly.
- dj_gitmo 3y ago
  My head-cannon for Dreidel was that it invented by very bored people waiting out a siege during the Maccabean Revolt. That would explain the length of the game. Apparently it’s not nearly that old.
  - riffic 3y ago
    in case anyone is curious the game is derivative of teetotum. https://en.wikipedia.org/wiki/Teetotum https://en.wikipedia.org/wiki/Teetotum
- deleted 3y ago
  [deleted]
- zamadatix 3y ago
  I dunno if I'd agree. If you asked a group of kids to play "see who can find the first prime greater than 2^201" then, per your criteria, that sounds great on paper but the kids will promptly discover the game sucks worse than massaging grandma's feet, quit playing, and never believe your game recommendations again. On the other hand, if a game is short but fun then it's likely it'll be played more than a single time per sitting on top of still be played in future sittings. The only key additional filter I can think of that is the game needs to not be so repetitive it is only fun the first time you play it. After that it doesn't much matter if it takes 5 minutes and you play 10 times of 50 minutes and you play once - it just matters you had enough fun to entice you to keep playing instead of trying to find something else to do. How much fun that requires likely varies greatly by era though.
  - 3y ago
aftbit 3y ago
>So why bother with all this when the Python would be like ten lines? Why not just write the Python to write this? Seems like you could add things like functions and generalizations to your meta-programming language and generate simple PRISM.
bee_rider 3y ago
Simulating a game you hate in a language you also hate, does that cancel out or double up?
- atticora 3y ago
  If double negatives cancelled regress we'd drown in mediocrity. (Failure is a feature.) If a double positive cancelled progress we would stand next to the giants rather than on their shoulders.
  - Tao3300 3y ago
    And standing next to giants quickly turns into standing under giants.
FergusArgyll 3y ago
This is why in our family there is an ante which increases every couple rounds...
khazhoux 3y ago
While writing a formal dreidel model might make you a better theorist, it won't make you a better dreidel spinner. In fact, it might make you worse at spinning dreidels, because it embodies the disastrous "formalism above all" doctrine. Spinners like to obsess about gimmels and shins and other high-theory stuff, yet the following skills, essential for spinning dreidels, are almost never discussed and even more rarely practiced: - Deciding how to grip the dreidel - Proper vertical positioning so it doesn't immediately tumble - Waiting until the clay is dry and ready, before you play In that spirit, I offer the following alternative challenge: Create your own dreidel out of clay. Don't bother with formal theory, others have already done that for you. "Just" make a dreidel that can actually spin, even if it only supports a subset of the game at the beginning.
- jkingsman 3y ago
  [flagged]
  - jdelman 3y ago
    The OP doesn’t read like a ChatGPT comment to me, though maybe I’m easily fooled. It has a bit more personality (“High-theory”, putting “just” in quotes as an ironic wink). It’s tongue-in-cheek, not nonsensical.
    - kevinventullo 3y ago
      “High-theory stuff” in fact. I think it’d take a fairly specific prompt to elicit the word “stuff”.
    - GuB-42 3y ago
      Also, unless cleverly prompted, ChatGPT normally has a positive attitude. This post looks too negative and dismissive for a typical ChatGPT answer: "worse", "disastrous", "stuff", "don't bother", etc... It follows the general construction of a ChatGPT answer though.
      - 3y ago
jmclnx 3y ago
Nice Read! Looks like a fun game especially when using chocolate coins. But I can see how that can get boring after a while and if finished there will be a lot of upset children. I think the winner will have to run for his life :)
ur-whale 3y ago
Not entirely sure why such a simple game requires pulling out as big a gun as PRISM seems to be. Looks to me like a very basic monte carlo simulation of Dreidel should take less than a 100 lines of C and would pretty much produce the exact same outcome. Am I missing something? Does PRISM do formal, complicated things a brute force MC attack can't touch?
- carlob 3y ago
  While I was reading the post I had the opposite thought: isn't this some kind of Ehrenfest model? It shouldn't be too hard to formalize with pen and paper.
- hnbad 3y ago
  The article is literally called "Formally modeled Dreidel for no good reason" so that should answer your question.
- jonahx 3y ago
  From the beginning of the article: > In 2015 Ben Blatt simulated the game and found that for P=4 and N=10, the average game will take 860 spins to finish. > But this was based on a mere 50,000 simulated games! We can do better than a mere simulation. We can mathematically model the game and get exact numbers. So we're busting out PRISM.
SkipperCat 3y ago
Was the eating of chocolate coins factored in? I think you can consider the reduction of chocolate coins due to consumption as theta . My initial assumption would be that there would be increased theta dependent on proximity to dinner. Plus you could factor in gamma as the rate of change of the value of those coins as gummy bears are within proximity. Just sayin' if you wanted to be real technical....
- irrational 3y ago
  What quality of chocolate coins are we talking about? Are these Palmer quality or Lindt quality?
  - bargle0 3y ago
    If they’re legally called “chocolate”, that’s a step up from Palmer.
zachwdc 3y ago
>Traditionally this game is played by kids, as it's an excellent way to convince them that gambling is boring as all hell. I’m amazed it has endured this long.
- Supermancho 3y ago
  New children are born every day. I'm not jewish, but I had jewish friends who taught me.
purpleflame1257 3y ago
PROTIP: make everyone antes every single time, instead of just when the pot is empty. Quicker eliminations and more exciting pots.
ScoobleDoodle 3y ago
Home rules adjustment to make a game of Dreidel conclude in a reasonable amount of time: The ante increases by one each time the spin returns to the starting player. Getting a Shin and adding to the pot matches the current ante. Adopted this from poker tournament's increasing blinds.
babyshake 3y ago
Is there a way to make Dreidel more fun? Presumably some aspect of strategy, and perhaps a bit like lier's dice (or poker) in that there could be bluffing.
- riwsky 3y ago
  https://en.m.wikipedia.org/wiki/Beyblade https://en.m.wikipedia.org/wiki/Beyblade
- mikewarot 3y ago
  According to the author, game is designed to convince you that gambling isn't fun. Let's not corrupt that social good with technical fixes. >Traditionally this game is played by kids, as it's an excellent way to convince them that gambling is boring as all hell.
  - evan_ 3y ago
    I think that’s a joke.
- resolutebat 3y ago
  No Limit Texas Dreidel sounds like an improvement: http://www.texasdreidel.com/ http://www.texasdreidel.com/
  - einpoklum 3y ago
    That video is awesome! Was worth reading about the useless boring Dreidel game :-P
einpoklum 3y ago
More interesting IMNSHO than this post itself is the teaser for a future post: "Next week will be the last newsletter of the year. Quick updates on this year's projects: ... Why programming languages doesn't have graph types: Done with interviews, writing an outline!"
einpoklum 3y ago
I live in Israel/Palestine, and strangely enough - the game is not played here AFAICT. I mean, we have dreidels (they're called "svivonim" in Hebrew, from the root S, B/V, B/V , relating to rotation: "histovev" means "rotate" or "turn around", and "sivuv" is a rotation or a round) ; and we also have those chocolate coins - but they're not really related to each other. Frankly I have no idea how the chocolate coins relate to Hannukah at all, but whatever. Anyway, the play with the dreidel is trying to get it to last as much time as you can without falling over, and that's basically it. There are fancy dreidels with colored lighting and a structure which increases the rotation time, that was a kind of a thing when I was younger at least. But the gambling is weird.
lou1306 3y ago
I'll likely start diving into probabilistic formal methods in a few months and this seems like a good place to ask: How does Storm [1] compare to PRISM? It looks like a promising alternative and the academic pedigree seems top-notch, but I would like to know more from anyone with hands-on experience with it. [1] https://www.stormchecker.org https://www.stormchecker.org
- lheck 3y ago
  Hi lou, I'm a contributor to Storm and will continue to work on it in my upcoming PhD position. The bottom line is that there are some things you can only do in PRISM and there are more things you can only do in Storm, but if you can do it in both, Storm is usually much faster (see QComp: https://qcomp.org/ https://qcomp.org/). PRISM has better documentation. Storm has recently recieved a grant that will help improve its user interface and applicabilty. I would like to hear from you what ideas and applications you have for using PMC! :)
  - lou1306 3y ago
    Thank you for the reply and congratulations on the PhD position! I am still not 100% sure about the specifics but my new team focuses on cyber-physical systems and whatnot, so probabilistic modelling and analysis techniques will likely play a big part. I will definitely try pinging you and the other Storm devs when things become clearer :) Also, I'm really glad to hear there's an interest in UX, I feel it's a weak spot of many otherwise excellent formal tools out there.
  - NooneAtAll3 3y ago
    since you're a Storm contributor, can you explain what exactly makes it OS-dependent?
    - lheck 3y ago
      The dependencies. It does work on Linux and Mac. On Windows, you can use the WSL.
aferr 3y ago
[flagged]
aerodog 3y ago
[flagged]
NooneAtAll3 3y ago
I'd probably prefer to Markov chain the problem manually over that PRISM ugliness...
throw4847285 3y ago
I've always assumed that Dreidel is more like Poker than it is like War. In other words, it's a game designed around betting that is no fun when you take the betting out, rather than a game that is just a miserable time waster that only children enjoy.
xwowsersx 3y ago
Well written. I thoroughly enjoyed this. Is PRISM more or less the state of the art as far as software to analyze/model probabilistic systems?

243 points by JNRowe 3y ago

mjb 3y ago

I love this, and have similar feelings about PRISM. I hope recent work to add probabilistic properties to TLA+ and P provide a route towards doing this kind of work with languages that are easier to use. While this example is a bit silly, the ability to check properties like availability, latency, etc alongside the traditional liveness and safety properties is super useful for distributed systems work.

kennethrc 3y ago

"Was this worth it? Ugh no I hate PRISM" :) ... that being said, as someone who only has a passing knowledge of the Dreidel the article held my interest

e28eta 3y ago

My first thought for “can’t generalize over number of players” was that he could write code that emits a PRISM program…

tgv 3y ago
Passing the state from n to n-1 players is harder.
- hwayne 3y ago
  I think I can do that with having an action for each player that passes if they don't have any money. The tricky bit is implementing the ante logic to only add n-1 coins to the pot, but I have an idea on how to hardcode that. After that it's "just" a matter of generating it all with another program.
ColonelPhantom 3y ago
This is also what I did when I used PRISM for my thesis. Honestly also not the greatest experience, but I think it does show that the limitations of the PRISM language are not inherent to the problem domain.

meepmorp 3y ago

Finally, someone calls out the lie that is Big Dreidel.

FergusArgyll 3y ago
A Wikipedia gem: "Robert Feinerman has shown that the game of dreidel is unfair, in that the first player to spin has a better expected outcome than the second player, and the second better than the third, and so on"
- gbacon 3y ago
  That’d be interesting to see modeled out in PRISM.

smachiz 3y ago

When I play dreidel you ante every turn… it does not take 860 spins.

tunesmith 3y ago
To really teach people about gambling, try a variation where everyone someone antes, they ante a second coin to the "house".
- willcipriano 3y ago
  Dad's job is to sit at the table and eat a handful of coins per round.
  - names_are_hard 3y ago
    When I was little and we'd get ice cream, my mother would get each of the kids a cone but not for herself. Then she'd do rounds and eat a little from each of ours. We were annoyed, but she explained that this process is called "taxes".

kromem 3y ago

Conversely, in an age before TV or Internet, the longer the game could keep kids occupied the better, no? We might even imagine that anthropologically given the role of keeping kids occupied there were other games that were more fun but of a shorter duration which died out because parents instead pushed for teaching their kids the cultural equivalent of Monopoly.

dj_gitmo 3y ago
My head-cannon for Dreidel was that it invented by very bored people waiting out a siege during the Maccabean Revolt. That would explain the length of the game. Apparently it’s not nearly that old.
- riffic 3y ago
  in case anyone is curious the game is derivative of teetotum. https://en.wikipedia.org/wiki/Teetotum https://en.wikipedia.org/wiki/Teetotum
deleted 3y ago
[deleted]
zamadatix 3y ago
I dunno if I'd agree. If you asked a group of kids to play "see who can find the first prime greater than 2^201" then, per your criteria, that sounds great on paper but the kids will promptly discover the game sucks worse than massaging grandma's feet, quit playing, and never believe your game recommendations again. On the other hand, if a game is short but fun then it's likely it'll be played more than a single time per sitting on top of still be played in future sittings. The only key additional filter I can think of that is the game needs to not be so repetitive it is only fun the first time you play it. After that it doesn't much matter if it takes 5 minutes and you play 10 times of 50 minutes and you play once - it just matters you had enough fun to entice you to keep playing instead of trying to find something else to do. How much fun that requires likely varies greatly by era though.
- 3y ago

aftbit 3y ago

>So why bother with all this when the Python would be like ten lines? Why not just write the Python to write this? Seems like you could add things like functions and generalizations to your meta-programming language and generate simple PRISM.

bee_rider 3y ago

Simulating a game you hate in a language you also hate, does that cancel out or double up?

atticora 3y ago
If double negatives cancelled regress we'd drown in mediocrity. (Failure is a feature.) If a double positive cancelled progress we would stand next to the giants rather than on their shoulders.
- Tao3300 3y ago
  And standing next to giants quickly turns into standing under giants.

FergusArgyll 3y ago

This is why in our family there is an ante which increases every couple rounds...

khazhoux 3y ago

While writing a formal dreidel model might make you a better theorist, it won't make you a better dreidel spinner. In fact, it might make you worse at spinning dreidels, because it embodies the disastrous "formalism above all" doctrine. Spinners like to obsess about gimmels and shins and other high-theory stuff, yet the following skills, essential for spinning dreidels, are almost never discussed and even more rarely practiced: - Deciding how to grip the dreidel - Proper vertical positioning so it doesn't immediately tumble - Waiting until the clay is dry and ready, before you play In that spirit, I offer the following alternative challenge: Create your own dreidel out of clay. Don't bother with formal theory, others have already done that for you. "Just" make a dreidel that can actually spin, even if it only supports a subset of the game at the beginning.

jkingsman 3y ago
[flagged]
- jdelman 3y ago
  The OP doesn’t read like a ChatGPT comment to me, though maybe I’m easily fooled. It has a bit more personality (“High-theory”, putting “just” in quotes as an ironic wink). It’s tongue-in-cheek, not nonsensical.
  - kevinventullo 3y ago
    “High-theory stuff” in fact. I think it’d take a fairly specific prompt to elicit the word “stuff”.
  - GuB-42 3y ago
    Also, unless cleverly prompted, ChatGPT normally has a positive attitude. This post looks too negative and dismissive for a typical ChatGPT answer: "worse", "disastrous", "stuff", "don't bother", etc... It follows the general construction of a ChatGPT answer though.
    - 3y ago

jmclnx 3y ago

Nice Read! Looks like a fun game especially when using chocolate coins. But I can see how that can get boring after a while and if finished there will be a lot of upset children. I think the winner will have to run for his life :)

ur-whale 3y ago

Not entirely sure why such a simple game requires pulling out as big a gun as PRISM seems to be. Looks to me like a very basic monte carlo simulation of Dreidel should take less than a 100 lines of C and would pretty much produce the exact same outcome. Am I missing something? Does PRISM do formal, complicated things a brute force MC attack can't touch?

carlob 3y ago
While I was reading the post I had the opposite thought: isn't this some kind of Ehrenfest model? It shouldn't be too hard to formalize with pen and paper.
hnbad 3y ago
The article is literally called "Formally modeled Dreidel for no good reason" so that should answer your question.
jonahx 3y ago
From the beginning of the article: > In 2015 Ben Blatt simulated the game and found that for P=4 and N=10, the average game will take 860 spins to finish. > But this was based on a mere 50,000 simulated games! We can do better than a mere simulation. We can mathematically model the game and get exact numbers. So we're busting out PRISM.

SkipperCat 3y ago

Was the eating of chocolate coins factored in? I think you can consider the reduction of chocolate coins due to consumption as theta . My initial assumption would be that there would be increased theta dependent on proximity to dinner. Plus you could factor in gamma as the rate of change of the value of those coins as gummy bears are within proximity. Just sayin' if you wanted to be real technical....

irrational 3y ago
What quality of chocolate coins are we talking about? Are these Palmer quality or Lindt quality?
- bargle0 3y ago
  If they’re legally called “chocolate”, that’s a step up from Palmer.

zachwdc 3y ago

>Traditionally this game is played by kids, as it's an excellent way to convince them that gambling is boring as all hell. I’m amazed it has endured this long.

Supermancho 3y ago
New children are born every day. I'm not jewish, but I had jewish friends who taught me.

purpleflame1257 3y ago

PROTIP: make everyone antes every single time, instead of just when the pot is empty. Quicker eliminations and more exciting pots.

ScoobleDoodle 3y ago

Home rules adjustment to make a game of Dreidel conclude in a reasonable amount of time: The ante increases by one each time the spin returns to the starting player. Getting a Shin and adding to the pot matches the current ante. Adopted this from poker tournament's increasing blinds.

babyshake 3y ago

Is there a way to make Dreidel more fun? Presumably some aspect of strategy, and perhaps a bit like lier's dice (or poker) in that there could be bluffing.

riwsky 3y ago
https://en.m.wikipedia.org/wiki/Beyblade https://en.m.wikipedia.org/wiki/Beyblade
mikewarot 3y ago
According to the author, game is designed to convince you that gambling isn't fun. Let's not corrupt that social good with technical fixes. >Traditionally this game is played by kids, as it's an excellent way to convince them that gambling is boring as all hell.
- evan_ 3y ago
  I think that’s a joke.
resolutebat 3y ago
No Limit Texas Dreidel sounds like an improvement: http://www.texasdreidel.com/ http://www.texasdreidel.com/
- einpoklum 3y ago
  That video is awesome! Was worth reading about the useless boring Dreidel game :-P

einpoklum 3y ago

More interesting IMNSHO than this post itself is the teaser for a future post: "Next week will be the last newsletter of the year. Quick updates on this year's projects: ... Why programming languages doesn't have graph types: Done with interviews, writing an outline!"

einpoklum 3y ago

I live in Israel/Palestine, and strangely enough - the game is not played here AFAICT. I mean, we have dreidels (they're called "svivonim" in Hebrew, from the root S, B/V, B/V , relating to rotation: "histovev" means "rotate" or "turn around", and "sivuv" is a rotation or a round) ; and we also have those chocolate coins - but they're not really related to each other. Frankly I have no idea how the chocolate coins relate to Hannukah at all, but whatever. Anyway, the play with the dreidel is trying to get it to last as much time as you can without falling over, and that's basically it. There are fancy dreidels with colored lighting and a structure which increases the rotation time, that was a kind of a thing when I was younger at least. But the gambling is weird.

lou1306 3y ago

I'll likely start diving into probabilistic formal methods in a few months and this seems like a good place to ask: How does Storm [1] compare to PRISM? It looks like a promising alternative and the academic pedigree seems top-notch, but I would like to know more from anyone with hands-on experience with it. [1] https://www.stormchecker.org https://www.stormchecker.org

lheck 3y ago
Hi lou, I'm a contributor to Storm and will continue to work on it in my upcoming PhD position. The bottom line is that there are some things you can only do in PRISM and there are more things you can only do in Storm, but if you can do it in both, Storm is usually much faster (see QComp: https://qcomp.org/ https://qcomp.org/). PRISM has better documentation. Storm has recently recieved a grant that will help improve its user interface and applicabilty. I would like to hear from you what ideas and applications you have for using PMC! :)
- lou1306 3y ago
  Thank you for the reply and congratulations on the PhD position! I am still not 100% sure about the specifics but my new team focuses on cyber-physical systems and whatnot, so probabilistic modelling and analysis techniques will likely play a big part. I will definitely try pinging you and the other Storm devs when things become clearer :) Also, I'm really glad to hear there's an interest in UX, I feel it's a weak spot of many otherwise excellent formal tools out there.
- NooneAtAll3 3y ago
  since you're a Storm contributor, can you explain what exactly makes it OS-dependent?
  - lheck 3y ago
    The dependencies. It does work on Linux and Mac. On Windows, you can use the WSL.

aferr 3y ago

[flagged]

aerodog 3y ago

[flagged]

NooneAtAll3 3y ago

I'd probably prefer to Markov chain the problem manually over that PRISM ugliness...

throw4847285 3y ago

I've always assumed that Dreidel is more like Poker than it is like War. In other words, it's a game designed around betting that is no fun when you take the betting out, rather than a game that is just a miserable time waster that only children enjoy.

xwowsersx 3y ago

Well written. I thoroughly enjoyed this. Is PRISM more or less the state of the art as far as software to analyze/model probabilistic systems?