BABA IS TURING COMPLETE: A sketch of a proof


As with most proofs of this form, the first step is to generalize Baba is You to an infinite grid.

The basic idea is to use Baba Is You to implement Cellular Automaton 110, proven to be Turing-Complete by Matthew Cook. A rock represents 1; an empty square represents 0.

The cellular automaton is driven by an engine which executes a sequence of rules for one turn each, in order, on loop, forever. I would build the engine in Baba Is You if it were possible, but the game has no level editor.

A gadget that executes a rule for one turn each is not difficult to build. Suppose you want to build a gadget for the rule ROCK MAKE STAR. Place the rule horizontally, with a wall below it. Place the global rule WALL IS STOP somewhere. Place a conveyor belt, facing upwards, under the verb of the sentence; in this case, MAKE. Define the global rule TEXT ON BELT IS MOVE, and another global rule TEXT IS UP. Place a wall n+1 squares above the verb. Place Keke, facing either up or down, somewhere in the column above the verb. Define KEKE IS MOVE. Thus, Keke will move up and down, and once every 2n turns, will push the verb into place, activating the rule. The very next turn, Keke will turn around and begin moving back upwards, and the verb will be made to move up one square by the rule TEXT ON BELT IS MOVE. Thus, the rule will be activated for one turn, and will not be activated again until Keke makes a full trip up to the wall, turns around, and comes back (2n turns).

Build enough of these gadgets, and choose a large enough value for n, and place Keke at a different position and/or facing in each gadget, and you can execute any sequence of rules you like in order on loop.

These rules are used to drive the cellular automaton algorithm. Each loop, the rock produces three distinct objects; a love, a star, and a moon. Each of these objects then moves down one square. Then, love moves one square right, and moon moves one square left. At this point, the square will have a love in it if the square to its upper left had a rock, it will have a star if the square above had a rock, and it will have a moon if the square to its upper right had a rock.

a sequence of rules is executed in order to implement Cellular Automaton Rule 110, transforming the love, moon, and/or star into either a rock or nothing. Then, the whole sequence repeats.

We only care about the bottom row, so after the love, star, and moons are generated, we turn the rocks into pillars, so that they do not generate any more objects and become inert, simply displaying the history of the cellular automaton.

The set of global (always on) rules are as follows:

WALL IS STOP
KEKE IS MOVE
TEXT ON BELT IS MOVE
TEXT IS UP

The sequence of rules is as follows:

1. ROCK MAKE LOVE AND STAR AND MOON
2. ROCK IS PILLAR
3. LOVE AND STAR AND MOON IS DOWN
4. LOVE AND STAR AND MOON IS MOVE
5. LOVE IS RIGHT
6. MOON IS LEFT
7. LOVE AND MOON IS MOVE
8. LOVE ON STAR IS ROCK (110 -> 1)
9. ROCK ON MOON IS EMPTY (111 -> 0)
10. LOVE ON MOON IS ROCK (101 -> 1)
11. STAR ON MOON IS ROCK (011 -> 1)
12. LOVE IS EMPTY (100 -> 0)
13. STAR IS ROCK (010 -> 1)
14. MOON IS ROCK (001 -> 1)
(and 000 -> 0 happens by default, needing no special rules to handle it.)

Since this algorithm takes 14 steps, choose n = 7 when building the rule gadgets. Some of these rules may occur in parallel; 13 and 14 in particular definitely can. The purpose of the proof is correctness, not the building of a maximally efficient cellular automata engine. An actual build would likely be more optimized to save time and space.

The input row may be of any arbitrary length, but there must be no other rocks in the initial setup anywhere in the entire level but the input row. The input row may be put in by the level editor, or the machinery and rules necessary for a player to create rocks and move them into place may be provided, along with the added global rule BABA IS YOU and one Baba for the player to control. All global rules, gadgets, and other machinery must be placed above the input row. The gadgets are paused until the player is done laying inputs; this can be done by disconnecting the rule KEKE IS YOU initially, and then having the player engage it when they are ready to begin computation. Once computation begins, the player must not interfere with the computation; this may be enforced with a construction that completes the rule BABA IS DEFEAT when KEKE IS YOU is engaged.

Reply · Report Post