Table of Contents
Fetching ...

Baba is You is Undecidable

Jonathan Geller

TL;DR

This paper proves the undecidability of Baba is You by introducing a modest generalization, baba+2, which appends an arbitrarily long hallway to the level boundary to enable information storage. The authors formalize a restricted Post correspondence problem, $pcp5-2$, and construct a polynomial-time reduction from it to baba+2, using three main gadgets: writing strings, comparing strings, and a level-construction scheme that encodes and verifies the PCP instance. The key result is a biconditional: $pcp5-2$ is solvable if and only if the corresponding baba+2 level is solvable, establishing undecidability for the generalized game. This work provides the first formal undecidability proof for a tile-based puzzle game and clarifies that small structural changes to game boundaries can fundamentally alter computational properties, while leaving open the question of Turing-completeness for even slightly modified rules.

Abstract

We establish the undecidability of 2019 puzzle game Baba is You through a reduction from the Post correspondence problem. In particular, we consider a restricted form of the Post correspondence problem introduced by Neary (arXiv:1312.6700) that is limited to five pairs of words. Baba is You is an award winning tile-based game in which the player can reprogram the game's mechanisms by pushing blocks that spell out the rules. We achieve undecidability through a generalization of the size of the playfield in the horizontal direction, adding a "hallway" to one side of the level. The undecidability of Baba is You has been claimed several times online using different source problems, including the simulation of Turing machines and Conway's Game of Life, however, this contribution appears to be the first formal proof of the result.

Baba is You is Undecidable

TL;DR

This paper proves the undecidability of Baba is You by introducing a modest generalization, baba+2, which appends an arbitrarily long hallway to the level boundary to enable information storage. The authors formalize a restricted Post correspondence problem, , and construct a polynomial-time reduction from it to baba+2, using three main gadgets: writing strings, comparing strings, and a level-construction scheme that encodes and verifies the PCP instance. The key result is a biconditional: is solvable if and only if the corresponding baba+2 level is solvable, establishing undecidability for the generalized game. This work provides the first formal undecidability proof for a tile-based puzzle game and clarifies that small structural changes to game boundaries can fundamentally alter computational properties, while leaving open the question of Turing-completeness for even slightly modified rules.

Abstract

We establish the undecidability of 2019 puzzle game Baba is You through a reduction from the Post correspondence problem. In particular, we consider a restricted form of the Post correspondence problem introduced by Neary (arXiv:1312.6700) that is limited to five pairs of words. Baba is You is an award winning tile-based game in which the player can reprogram the game's mechanisms by pushing blocks that spell out the rules. We achieve undecidability through a generalization of the size of the playfield in the horizontal direction, adding a "hallway" to one side of the level. The undecidability of Baba is You has been claimed several times online using different source problems, including the simulation of Turing machines and Conway's Game of Life, however, this contribution appears to be the first formal proof of the result.
Paper Structure (10 sections, 1 equation, 8 figures, 2 tables)

This paper contains 10 sections, 1 equation, 8 figures, 2 tables.

Figures (8)

  • Figure 1: An example section of a Baba is You level. In the first image, the rule baba is you means that if the player moves to the right, the baba object will move to the right, pushing the text banana and baba to the right, as seen in the second image. Now, the rule formed is banana is you, so if the player moves right again, the banana object will move rather than the baba object.
  • Figure 2: Example instance of baba+2 constructed from the earlier instance of pcp5-2. Road objects are present on top of each lava and ice object, but are hidden to allow the other objects on those tiles to be visible. All lava and ice objects are right-facing. Note the positioning of the "hallway" at the bottom right of the level.
  • Figure 3: Three components of the level: from left to right, a button gadget, the timer gadget, and a duplication gadget. The duplication gadget corresponds to the tile with $\alpha =1$, $\beta=10$ from the earlier instance of pcp5-2. Important rules found elsewhere in the level are wall is stop, baba is you, lava and ice on tile is move, bird is push, car is push, baba is push, lava and ice is push, and dog is move.
  • Figure 4: If the player pushes up on the is text shown in the first image of Figure \ref{['fig:gadgets']}, each of the gadgets takes the state shown in (a). After this, the player's moves do not matter, and the state in (b) will be reached no matter what.
  • Figure 5: The gadget with which the player can interact when they have created two matching strings. Pushing down on wall enables the player to win the game if and only if they have produced strings of lava and ice in the top and bottom row of the hallway that correspond to matching binary strings. Additional relevant rules are lava is open, circle is push, tree is stop, and level without lava and without ice is you and win.
  • ...and 3 more figures

Theorems & Definitions (2)

  • Definition 1
  • Definition 2