BABA IS TURING COMPLETE: A sketch of a proof (v2)
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. The rules that drive the cellular automaton all use exactly one verb: IS. This allows us to build the engine by having a single free IS verb traveling downwards. Two clouds are used, with the rule CLOUD IS TELE, to return IS to the top at the end of each loop iteration.
Each loop, the rock produces four distinct objects; a love, a star, a moon, and a pillar. The pillar stays where it is, and remains inert forever; its sole purpose is to record the history of the cellular automaton for the viewer's convenience. Each of the other three objects then moves down one square. Next, 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.
Finally, 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:
CLOUD IS TELE
WALL IS STOP
TEXT IS MOVE
The sequence of rules is as follows:
1. ROCK IS LOVE AND STAR AND MOON AND PILLAR
2. LOVE AND STAR AND MOON IS DOWN AND MOVE
3. MOON IS LEFT AND MOVE
4. LOVE IS RIGHT AND MOVE
6. LONELY STAR IS ROCK (010 -> 1)
7. LONELY MOON IS ROCK (001 -> 1)
8. STAR ON MOON IS GHOST
9. MOON ON GHOST IS EMPTY
10. GHOST ON LOVE IS EMPTY (111 -> 0)
11. LONELY LOVE IS EMPTY (100 -> 0)
12. GHOST AND LOVE IS ROCK (011 -> 1, 101 -> 1, 110 -> 1)
13. STAR AND MOON IS EMPTY
Rule 1 spawns all of the needed objects. Rules 2-4 move them to the correct place in the next row down. Rule 5 is empty because of the way the rule LOVE IS MOVE works. It does not move the same turn the rule is completed, but rather, the next turn. Rule 5 is inserted to create a buffer between rules 4 and 6 so that all love objects have time to move to their proper square.
Rules 6 and 7 pretty straightforwardly implement the patterns 010->1 and 001->1. Stars and moons will turn into rocks only if they are lonely--the only objects in their squares. (Putting LONELY LOVE IS EMPTY to implement 100->0 is possible here, but is left for later for reasons that will be explained at that point.)
From this point, we must consider squares with more than one object on them; to this end, we use the ON preposition. We first combine stars and moons in the same square into ghosts. Rule 8 produces the ghost; rule 9 removes the redundant moon left over after rule 8.
Next, we implement pattern 111->0 with rule 9: GHOST ON LOVE IS EMPTY. Then, we invoke rule 11, LONELY LOVE IS EMPTY for two reasons; first, to implement pattern 100->0, and second, to clean up the leftover love left by rule 10. If we had used LONELY LOVE IS EMPTY earlier, we would still need to invoke it again here, so this saves us a step.
Rule 12 implements all remaining patterns. It transforms ghosts into rocks, implementing pattern 011->1. Next, any love objects that remain at this point are either pattern 110->1, or 101->1, so all remaining loves are turned into rocks. Then, rule 13 removes any remaining stars or moons, cleaning up objects left over by rule 12. Now we have implemented all rules except 000->0, which happens on its own by default anyway.
It may be possible to condense this algorithm further, so that the engine takes less room or takes fewer steps per loop; the purpose of this design is to prove Baba Is You is Turing-Complete, not to be maximally efficient.
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 TEXT IS MOVE 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 TEXT IS MOVE is engaged.