Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Braid is undecidable (2014) [pdf]

arxiv.org

Post reply on HN
Print view View original

11–20 of 31 posts

Re: Braid is undecidable (2014) [pdf]

#11

Post by CJefferson »

secant wrote: post #10
wolfgke wrote: post #2

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

Re: Braid is undecidable (2014) [pdf]

#12

Post by wolfgke »

CJefferson wrote: post #11
secant wrote: post #10

Earlier quoted context omitted.

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…

> The classic decidable problem is "the halting problem".

The classic undecidable problem ...

Re: Braid is undecidable (2014) [pdf]

#13

Post by seanwilson »

CJefferson wrote: post #11
secant wrote: post #10

Earlier quoted context omitted.

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…

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.

Re: Braid is undecidable (2014) [pdf]

#14

Post by tshadwell »

xacaxulu wrote: post #4

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.

Make sure you collected all the secret stars and got the second ending. It's pretty hard to do, though.

Re: Braid is undecidable (2014) [pdf]

#15

Post by gremble »

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.

Re: Braid is undecidable (2014) [pdf]

#16

Post by prezjordan »

mushishi wrote: post #9
xacaxulu wrote: post #4

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.

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)

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/

Re: Braid is undecidable (2014) [pdf]

#17

Post by xacaxulu »

mushishi wrote: post #9
xacaxulu wrote: post #4

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.

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)

Thanks Mushishi! These are great recommendations!!

Re: Braid is undecidable (2014) [pdf]

#18

Post by breadbox »

gremble wrote: post #15

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.…

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.

Re: Braid is undecidable (2014) [pdf]

#19

Post by gremble »

breadbox wrote: post #18
gremble wrote: post #15

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.…

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…

> 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.

Re: Braid is undecidable (2014) [pdf]

#20

Post by nemo1618 »

mushishi wrote: post #9
xacaxulu wrote: post #4

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.

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)

Also, watch Mushishi.
Post reply on HN