7 ms·

Braid is undecidable (2014) [pdf]

136 points by cjg 11y ago

wolfgke 11y ago
It is rather easy to build behaviors in systems that are Turing-complete (thus undecidable). What is more complicated is building nontrivial models (i.e. showing complex behavior) that are still decidable or even decidable in polynomial time.
- secant 11y ago
  I'm a bit of a math novice, but is the term "decidable" analogous with satisfiability (SAT), or is this a completely different set of modelling?
  - CJefferson 11y ago
    Nope, decidable is a much higher level. A problem is decidable if it can ever be solved by any computer, given as much time as it wants. The classic undecidable problem is "the halting problem". In short, given a computer program (and some input for it), decide if that program will ever stop, or continue forever. It turns out there is NO WAY to write a program which will, for any input program, check if it will halt in finite time. This stuff is a little mind-blowing at first -- the wikipedia article isn't bad. EDIT: Fixed typo from wolfgke
    - wolfgke 11y ago
      > The classic decidable problem is "the halting problem". The classic undecidable problem ...
    - seanwilson 11y ago
      A simple summary is: a problem domain is decidable if there exists an algorithm that will always be able to tell you true or false if any problem in that domain is solvable. Some examples of this are propositional logic and linear logic are decidable, whereas the halting problem and nonlinear logic are not. For instance, the halting problem isn't decidable because although you can answer true or false for some specific programs, there exists programs where you do not know if they halt or not. Arbitrary mathematical problems in general are undecidable (see Gödel's incompleteness theorems) but we can still carve out domains within this that are decidable.
      - eru 11y ago
        To be pedantic: the Halting Problem for Turing Machines is undecidable. There are simpler computing models for which we can decide halting.
spranesh 11y ago
What an excellently well written paper! It does all the basics right - describes it's objective, the domain of the problem, a quick example (Rush hour) to nudge some intuition toward the reader, before going on to prove undecidability. It even tackles the decidability of another "should-obviously-work" (Bounded braid) idea that the author had (turns out to be decidable). Also, I wonder if most programmers have unknowingly built a ton of Braid intuition because of the way the time reversal tree matches the way we model the undo tree in $EDITOR.
xacaxulu 11y ago
I felt sad when I finally completed Braid. It's still one of the best games I've ever played and I knew I was never going to find something like that again. This paper brought me back to that sense of wonder that I had the first time I played Braid.
- pdpi 11y ago
  That very last stage stands in my memory as one of the best uses of game mechanics as part of the story telling I've ever seen. It's the rare sort of thing that truly makes games an art of its own, rather than some sort of "interactive movie".
  - chiaro 11y ago
    Ludonarrative resonance. It's fun to see the critical/theory sphere develop alongside the medium. We sometimes forget just how young videos games are. Compared to film, they're completely in their infancy, and narrative film isn't even 100 years old yet. I can't think of many other games where the mechanics themselves reinforce the story. Papers, Please does it pretty well.
    - marcelluspye 11y ago
      Brothers - A Tale of Two Sons is another example.
      - wtallis 11y ago
        Yeah. The phantom limb sort of sensation was surprisingly powerful.
- mushishi 11y ago
  Yes it is. Hopefully Blow's the Witness will as awesome. Also consider playing the following if you have thirst for puzzle games - The Swapper - Snakebird - Spacechem - Starseed Pilgrim (this one I haven't played but Blow recommended it, iirc)
ericye16 11y ago
Jonathan Blow, creator of Braid, is coming out with a new game called "The Witness" pretty Soon™. http://the-witness.net/news/ http://the-witness.net/news/
- AndyKelley 11y ago
  Yes, it's set to be released in mid-2014.
  - JohnTHaller 11y ago
    It was delayed, as games often are. The latest progress report was on May 5, 2015.
- sj4nz 11y ago
  Jonathan Blow is also working on Jai, a programming language for game developers. https://inductive.no/jai/ https://inductive.no/jai/
  - M8 11y ago
    Oh, it has a website and a name now, cool! PS: the usual recommendation is to build a game not an engine, I guess nobody have foreseen an experienced developer going even lower in abstraction :). One of these days: "I am not satisfied with the hardware we have, where is my soldering iron..."
Sniffnoy 11y ago
A note -- if you're linking to arXiv, it's better to link to the abstract (http://arxiv.org/abs/1412.0784 http://arxiv.org/abs/1412.0784) rather than directly to the PDF. From the abstract, one can easily click through to the PDF; not so the reverse. And the abstract allows one to do things like see different versions of the paper, search for other things by the same authors, etc. Thank you!
gremble 11y ago
I could use some guidance, as I seem to have gotten lost. The implementation of the counter is IO (the levers that Tim pulls), ADD, SUB (branch if 0), M1 (the counter).. and then M2. M2 is the counter that holds the monsters as they are subtracted from M1. It is also used as IO for the branch part of SUB (if I understood the article correctly). Therefore, if I call SUB with M2 = 0, then the counter will malfunction. I think that the consequence of this is that the given function has a decided halting point.(Branching was taken out). I have no idea how to say this in a better way, sadly my computer science education is tragically lacking.
- breadbox 11y ago
  Not sure exactly what you're referring to (didn't find "m1" or "m2" anywhere in the paper), but ... When a monstar leaves the counter (due to a SUB lever emitting a bunny), the monstar has to proceed to the area under the ladder, where Tim has to kill it in order to proceed. If Tim pulls a SUB lever when the counter equals zero (no monstars), then the bunny will die on the ceiling spikes and be removed. Tim will not be able to reach the ladder and will have to exit the branch point and proceed to the next spot.
  - gremble 11y ago
    > To perform the “Branch if 0” part of the operation, we would like to guide this monstar into the appropriate Branch gadget. To do this, build a room that catches all monstars leaving the counter. This room should consist of a flat floor for the monstar to walk back and forth across, along with many platforms forming trap doors in the floor. Next, force Tim through a second Lever Pull Gadget, whose lever opens one of these trap doors. Build a path below this trap door, leading the monstar to the appropriate Branch gadget. Alright, M1 the first memory "thing", the counter where the result of ADD is stored. M2 is the second memory "thing", the room mentioned in the part quoted. However, you have made me feel rather silly for not realising the very obvious solution to the problem. Thanks.

136 points by cjg 11y ago

It is rather easy to build behaviors in systems that are Turing-complete (thus undecidable). What is more complicated is building nontrivial models (i.e. showing complex behavior) that are still decidable or even decidable in polynomial time.

secant 11y ago
I'm a bit of a math novice, but is the term "decidable" analogous with satisfiability (SAT), or is this a completely different set of modelling?
- CJefferson 11y ago
  Nope, decidable is a much higher level. A problem is decidable if it can ever be solved by any computer, given as much time as it wants. The classic undecidable problem is "the halting problem". In short, given a computer program (and some input for it), decide if that program will ever stop, or continue forever. It turns out there is NO WAY to write a program which will, for any input program, check if it will halt in finite time. This stuff is a little mind-blowing at first -- the wikipedia article isn't bad. EDIT: Fixed typo from wolfgke
  - wolfgke 11y ago
    > The classic decidable problem is "the halting problem". The classic undecidable problem ...
  - seanwilson 11y ago
    A simple summary is: a problem domain is decidable if there exists an algorithm that will always be able to tell you true or false if any problem in that domain is solvable. Some examples of this are propositional logic and linear logic are decidable, whereas the halting problem and nonlinear logic are not. For instance, the halting problem isn't decidable because although you can answer true or false for some specific programs, there exists programs where you do not know if they halt or not. Arbitrary mathematical problems in general are undecidable (see Gödel's incompleteness theorems) but we can still carve out domains within this that are decidable.
    - eru 11y ago
      To be pedantic: the Halting Problem for Turing Machines is undecidable. There are simpler computing models for which we can decide halting.

spranesh 11y ago

What an excellently well written paper! It does all the basics right - describes it's objective, the domain of the problem, a quick example (Rush hour) to nudge some intuition toward the reader, before going on to prove undecidability. It even tackles the decidability of another "should-obviously-work" (Bounded braid) idea that the author had (turns out to be decidable). Also, I wonder if most programmers have unknowingly built a ton of Braid intuition because of the way the time reversal tree matches the way we model the undo tree in $EDITOR.

xacaxulu 11y ago

I felt sad when I finally completed Braid. It's still one of the best games I've ever played and I knew I was never going to find something like that again. This paper brought me back to that sense of wonder that I had the first time I played Braid.

pdpi 11y ago
That very last stage stands in my memory as one of the best uses of game mechanics as part of the story telling I've ever seen. It's the rare sort of thing that truly makes games an art of its own, rather than some sort of "interactive movie".
- chiaro 11y ago
  Ludonarrative resonance. It's fun to see the critical/theory sphere develop alongside the medium. We sometimes forget just how young videos games are. Compared to film, they're completely in their infancy, and narrative film isn't even 100 years old yet. I can't think of many other games where the mechanics themselves reinforce the story. Papers, Please does it pretty well.
  - marcelluspye 11y ago
    Brothers - A Tale of Two Sons is another example.
    - wtallis 11y ago
      Yeah. The phantom limb sort of sensation was surprisingly powerful.
mushishi 11y ago
Yes it is. Hopefully Blow's the Witness will as awesome. Also consider playing the following if you have thirst for puzzle games - The Swapper - Snakebird - Spacechem - Starseed Pilgrim (this one I haven't played but Blow recommended it, iirc)

ericye16 11y ago

Jonathan Blow, creator of Braid, is coming out with a new game called "The Witness" pretty Soon™. http://the-witness.net/news/ http://the-witness.net/news/

AndyKelley 11y ago
Yes, it's set to be released in mid-2014.
- JohnTHaller 11y ago
  It was delayed, as games often are. The latest progress report was on May 5, 2015.
sj4nz 11y ago
Jonathan Blow is also working on Jai, a programming language for game developers. https://inductive.no/jai/ https://inductive.no/jai/
- M8 11y ago
  Oh, it has a website and a name now, cool! PS: the usual recommendation is to build a game not an engine, I guess nobody have foreseen an experienced developer going even lower in abstraction :). One of these days: "I am not satisfied with the hardware we have, where is my soldering iron..."

Sniffnoy 11y ago

A note -- if you're linking to arXiv, it's better to link to the abstract (http://arxiv.org/abs/1412.0784 http://arxiv.org/abs/1412.0784) rather than directly to the PDF. From the abstract, one can easily click through to the PDF; not so the reverse. And the abstract allows one to do things like see different versions of the paper, search for other things by the same authors, etc. Thank you!

gremble 11y ago

I could use some guidance, as I seem to have gotten lost. The implementation of the counter is IO (the levers that Tim pulls), ADD, SUB (branch if 0), M1 (the counter).. and then M2. M2 is the counter that holds the monsters as they are subtracted from M1. It is also used as IO for the branch part of SUB (if I understood the article correctly). Therefore, if I call SUB with M2 = 0, then the counter will malfunction. I think that the consequence of this is that the given function has a decided halting point.(Branching was taken out). I have no idea how to say this in a better way, sadly my computer science education is tragically lacking.

breadbox 11y ago
Not sure exactly what you're referring to (didn't find "m1" or "m2" anywhere in the paper), but ... When a monstar leaves the counter (due to a SUB lever emitting a bunny), the monstar has to proceed to the area under the ladder, where Tim has to kill it in order to proceed. If Tim pulls a SUB lever when the counter equals zero (no monstars), then the bunny will die on the ceiling spikes and be removed. Tim will not be able to reach the ladder and will have to exit the branch point and proceed to the next spot.
- gremble 11y ago
  > To perform the “Branch if 0” part of the operation, we would like to guide this monstar into the appropriate Branch gadget. To do this, build a room that catches all monstars leaving the counter. This room should consist of a flat floor for the monstar to walk back and forth across, along with many platforms forming trap doors in the floor. Next, force Tim through a second Lever Pull Gadget, whose lever opens one of these trap doors. Build a path below this trap door, leading the monstar to the appropriate Branch gadget. Alright, M1 the first memory "thing", the counter where the result of ADD is stored. M2 is the second memory "thing", the room mentioned in the part quoted. However, you have made me feel rather silly for not realising the very obvious solution to the problem. Thanks.