Braid is undecidable (2014) [pdf](arxiv.org)
arxiv.org
Braid is undecidable (2014) [pdf]
http://arxiv.org/pdf/1412.0784.pdf
6 comments
A note -- if you're linking to arXiv, it's better to link to the abstract (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!
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.
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".
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.
I can't think of many other games where the mechanics themselves reinforce the story. Papers, Please does it pretty well.
Brothers - A Tale of Two Sons is another example.
Yeah. The phantom limb sort of sensation was surprisingly powerful.
Yes it is. Hopefully Blow's the Witness will as awesome.
Also consider playing the following if you have thirst for puzzle games
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)Currently playing Snakebird and it is driving me _nuts_.
Also check out The Talos Principle [0], it resembles The Witness (based on little clips I've seen of it), and feels like Portal with a dash of Isaac Asimov and a sprinkle of Religion.
Beautiful audio, beautiful scenery, clever puzzles. One of the best games I've ever played.
[0]: http://store.steampowered.com/app/257510/
Also check out The Talos Principle [0], it resembles The Witness (based on little clips I've seen of it), and feels like Portal with a dash of Isaac Asimov and a sprinkle of Religion.
Beautiful audio, beautiful scenery, clever puzzles. One of the best games I've ever played.
[0]: http://store.steampowered.com/app/257510/
Also, watch Mushishi.
Thanks Mushishi! These are great recommendations!!
Braid was fun, but it didn't tie together very well. The mechanics are disjointed. From an artistic point of view, Limbo outshines Braid.
I've replayed Limbo, but never Braid.
I've replayed Limbo, but never Braid.
Gotta disagree with you there. IMO Limbo was mostly polish with little substance (and don't get me wrong, I think it does a great job at that, it has amazing aesthetics).
FWIW I've revisited Braid multiple times, but don't think I'd get anything new out of Limbo if I played through it again.
FWIW I've revisited Braid multiple times, but don't think I'd get anything new out of Limbo if I played through it again.
To make a broader statement: I can count on one hand the times I've played Limbo and Braid. I don't have enough appendages for Spelunky.
Ha! Very true. I've sunk well over a thousand hours into Dungeon Crawl Stone soup, and hundreds into Spelunky, Binding of Isaac, and other roguelike/lites.
I don't think I'd consider them better games than Braid, however, they just have (much!) more replayability/content.
(I would consider them better than Limbo, but that's neither here nor there).
I don't think I'd consider them better games than Braid, however, they just have (much!) more replayability/content.
(I would consider them better than Limbo, but that's neither here nor there).
Make sure you collected all the secret stars and got the second ending. It's pretty hard to do, though.
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.
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.
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.
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?
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
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
> The classic decidable problem is "the halting problem".
The classic undecidable problem ...
The classic undecidable problem ...
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.
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.
To be pedantic: the Halting Problem for Turing Machines is undecidable. There are simpler computing models for which we can decide halting.
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/
Yes, it's set to be released in mid-2014.
It was delayed, as games often are. The latest progress report was on May 5, 2015.
Jonathan Blow is also working on Jai, a programming language for game developers.
https://inductive.no/jai/
https://inductive.no/jai/
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..."
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..."
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.
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.
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.
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.
> 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.
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.