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.
