systemic-game-design-course/course/07-rule-resolution/lesson.md

Module 7: Resolving rules: NOT, identity, meta-nouns

Module 6 built a parser that reports everything the board says. This module decides what the board means when its sentences disagree. BABA IS YOU and BABA IS NOT YOU can lie on the same board, and so can BABA IS BABA and BABA IS ROCK. The parser reads them all. A second stage, the resolution pass, reads the whole rule list at once and decides which rules are in force. Then every question an object asks ("am I YOU?") goes through one function that looks only at the rules in force.

Part I had a step like this too. In Module 4, Baron Rivendare changed what a Deathrattle does without the Deathrattle's code knowing he exists: an interceptor, consulted at the moment the trigger runs. BABA IS NOT YOU changes whether BABA IS YOU applies, and nothing in BABA IS YOU knows about it either. Keep both in mind while you build. The course's closing question asks you to compare them.

You need your Module 6 workspace with all Module 1–6 tests passing, under git.

Observe

All quotes come from sources recorded in the course's research notes. The Baba Is You Wiki is an unofficial community wiki; the course treats it as the best available description of the game, not as Hempuli's own word.

What NOT does, from the wiki's NOT page:

When added after a verb it makes the corresponding rule not apply, overriding other instances of the rule it disables. ROCK IS NOT PUSH makes ROCK NOT PUSHable, even if ROCK IS PUSH exists elsewhere.

It works on conversions as well as properties: "ROCK IS NOT GRASS disables ROCK IS GRASS." The IS page says the same about properties: "BABA IS NOT YOU prevents BABA from having the property YOU, overriding any BABA IS YOU rule."

A noun can be its own complement. The IS page:

BABA IS BABA prevents BABA from transforming into any object, including those not in ALL. It does not affect transforming objects into BABA.

And the negation of that, X IS NOT X, from the NOT page:

X IS NOT X makes an object disappear, similarly to X IS EMPTY but with particles. ... As it negates X IS X, it enables other X IS Y rules, which can result in transformation in addition to the disappearance.

The IS page puts it more briefly: "BABA IS NOT BABA causes BABA to vanish in a puff of logic."

Base rules are not exempt. The Rule page says the base rules, TEXT IS PUSH among them, "can still be detected by FEELING and MIMIC and negated by NOT and BROKEN", and the Advanced rulebook relies on it: "Text can be stacked if TEXT IS NOT PUSH can be formed with another way to move text".

Finally, where the game does this. Teikari, in the Game Developer article (Designing Baba Is You's delightfully innovative rule-writing system), describes the last step of building the rules: "Finally, once everything is (hopefully) set, the game goes through the final set of rules and adjusts them if needed." And Teikari's example: "(For example, if the rule "Baba Is Not You" exists, "Baba Is You" is marked as being not valid.)"

Notice what the article says and what it doesn't. The adjustment happens in a pass over "the final set of rules", after the rules are built, and BABA IS YOU is "marked as being not valid" there. The article doesn't describe the data structures beyond that. The course takes the quote to mean that the parser reads BABA IS YOU like any other rule, and a later pass over the whole set decides that it doesn't apply. That is the course's reading, and it is the design you'll build.

Predict

Write your answers down before you open the discussion, for example in notes/07.md in your workspace.

1. BABA IS YOU on the top row and BABA IS NOT YOU two rows below. Is Baba YOU? Would the answer change if the rows swapped places?
2. Three sentences: BABA IS BABA, BABA IS ROCK, ROCK IS BABA. Which of them are in force?
3. Three sentences: BABA IS NOT BABA, BABA IS BABA, BABA IS ROCK. Which are in force, and what happens to Baba?
4. TEXT IS NOT PUSH is on the board. Is the text spelling it pushable? Is a rock?
5. One row: NOT BABA IS YOU. Your Module 6 parser reads something from it. What, and is that right?
6. Back to Part I: Baron makes a Deathrattle activate twice; BABA IS NOT YOU makes BABA IS YOU not apply. In your engines, where is each of those decisions made, and when?

Discussion

1. No, and no. NOT overrides "other instances of the rule it disables", wherever they are. If your engine let the later sentence win, the answer would depend on which row the parser reads first, and moving a sentence up a row would change the game. Negation is a fact about the whole rule set, not about reading order.

2. BABA IS BABA and ROCK IS BABA. BABA IS BABA blocks Baba converting into anything, so BABA IS ROCK is out. It doesn't stop rocks becoming Baba.

3. BABA IS NOT BABA and BABA IS ROCK. BABA IS NOT BABA is the negation of BABA IS BABA, so it cancels it exactly as BABA IS NOT YOU cancels BABA IS YOU; with the lock gone, the conversion applies again. And every Baba vanishes. Which happens to a given Baba first, conversion or vanishing, is a question about the turn (Module 9); this module only has to know that both are in force.

4. No, and no. The base rule is a rule like any other; NOT cancels it, and no text on the board is pushable. A rock was never pushable: TEXT names text objects, not the things they name.

5. BABA IS YOU. The subject run walks back from IS, finds BABA, finds no AND before it, and stops: the NOT is ignored. That reads a sentence that isn't on the board. Module 7's parser has to do something with it. See Build for the course's choice and "How the real game differs" for the game's.

6. Baron is consulted while a trigger runs: the step asks the modifiers in play how many times to activate. NOT is consulted when the rules are compiled, before anyone asks a question: by the time an object asks "am I YOU?", the cancelled rule is already gone. Hold on to that difference; you'll come back to it at the end of the course.

Spec

From the course repository, copy the module's tests into your workspace:

node tools/start-module.mjs 07 ~/my-engine

The harness

Two new functions on Baba, and one change:

TypeScript	Rust
activeRules(): string[]	active_rules(&self) -> Vec<String>
hasProperty(id, prop): boolean	has_property(&self, id: Id, prop: &str) -> bool

• rules() still lists everything the text spells, before resolution. It now includes negated rules, written "BABA IS NOT YOU".
• activeRules() lists the rules in force after resolution, in the same format: sorted, each distinct rule once, "TEXT IS PUSH" included unless TEXT IS NOT PUSH cancels it. Negated rules stay in it: a negated rule is in force, because it keeps overriding (the tests check this, for example ["BABA IS NOT YOU", "TEXT IS PUSH"]).
• hasProperty(id, prop) answers for one object. A thing is named by its noun (a baba object by BABA); a text object is named by TEXT.

The tests

The full statements are in course/07-rule-resolution/scenarios.md.

• test_07_not_overrides: Predict question 1. Baba is YOU until BABA IS NOT YOU is written below BABA IS YOU. rules() shows both sentences; activeRules() shows only the negation and the base rule.
• test_07_x_is_x_blocks_conversion: Predict question 2, exactly.
• test_07_x_is_not_x_deletes_and_unlocks: Predict question 3. activeRules() contains BABA IS ROCK and not BABA IS BABA.
• test_07_text_is_not_push: Predict question 4, checked with hasProperty on a piece of text and on a rock, before and after.
• test_07_leading_not_breaks_sentence: Predict question 5. NOT BABA IS YOU spells nothing in the course's grammar.

The third test, which carries the module's subtlest point:

#[test]
fn test_07_x_is_not_x_deletes_and_unlocks() {
    let mut b = new_baba(empty_level(4, 5));
    write(
        &mut b,
        &[
            ("BABA", 0, 0),
            ("IS", 1, 0),
            ("NOT", 2, 0),
            ("BABA", 3, 0),
            ("BABA", 0, 2),
            ("IS", 1, 2),
            ("BABA", 2, 2),
            ("BABA", 0, 4),
            ("IS", 1, 4),
            ("ROCK", 2, 4),
        ],
    );

    assert_eq!(
        b.rules(),
        vec![
            "BABA IS BABA",
            "BABA IS NOT BABA",
            "BABA IS ROCK",
            "TEXT IS PUSH"
        ]
    );
    let active = b.active_rules();
    assert!(active.contains(&"BABA IS ROCK".to_string()));
    assert!(!active.contains(&"BABA IS BABA".to_string()));
}

test("test_07_x_is_not_x_deletes_and_unlocks", () => {
  const b = newBaba(emptyLevel(4, 5));
  write(b, [
    ["BABA", 0, 0],
    ["IS", 1, 0],
    ["NOT", 2, 0],
    ["BABA", 3, 0],
    ["BABA", 0, 2],
    ["IS", 1, 2],
    ["BABA", 2, 2],
    ["BABA", 0, 4],
    ["IS", 1, 4],
    ["ROCK", 2, 4],
  ]);

  expect(b.rules()).toEqual(["BABA IS BABA", "BABA IS NOT BABA", "BABA IS ROCK", "TEXT IS PUSH"]);
  expect(b.activeRules()).toContain("BABA IS ROCK");
  expect(b.activeRules()).not.toContain("BABA IS BABA");
});

The test doesn't check that Baba vanishes. Nothing moves or vanishes until the turn exists (Module 9). This module decides that Baba is to vanish; Module 9 does it.

Run cargo test or npm test. The Module 7 tests fail to compile (Rust) or fail (TypeScript). Modules 1–6 still pass. That is RED.

Build

Make the five tests pass, and keep Modules 1–6 green. Where code goes:

• The parser learns NOT, and only reads. After IS, a NOT negates the complement right after it: BABA IS NOT YOU AND WIN is BABA IS NOT YOU and BABA IS WIN. A rule now carries a flag, negated or not. The parser never cancels anything; it reports what is written.
• A NOT before a subject breaks the sentence. The course's grammar has no negated subjects. When the subject run meets a NOT in front of a noun, it stops and drops that noun. Reading NOT BABA IS YOU as BABA IS YOU is the one thing it must not do.
• A separate resolution pass. A function from the parsed rules to the rules in force, run after every parse. It sees the whole list at once, so where a sentence sits on the board can't matter.
• One question, one place. hasProperty(id, prop) looks only at the rules in force, and asks one more function: does this noun name this object? BABA names objects of kind baba; TEXT names every text object. TEXT is the first noun you meet that names a group rather than its own kind. Decide whether that is a special case in your engine or a fact about the word.
• Keep the record. X IS NOT X means "every X vanishes". Nothing vanishes yet, but the decision is made here, and the turn in Module 9 will need to find it.

Hint 1 — nudge

You will be tempted to do it in the parser: when you read BABA IS NOT YOU, delete BABA IS YOU from the list. Try Predict question 1 with the rows swapped. Then try question 3: BABA IS NOT BABA cancels BABA IS BABA, which would have cancelled BABA IS ROCK. How many orders of reading do you have to get right?

Hint 2 — concept

• Two steps, in a fixed order, over the whole list. First negation: drop every positive rule X IS Y for which a negated X IS NOT Y exists. Keep the negated rules: they are still in force. Then identity: for each positive X IS X that survived, drop every X IS Y where Y is a noun other than X.
• The order does the work for X IS NOT X. It negates X IS X in the first step, so in the second step there is no lock. There's no special case for it.
• Telling conversions from properties. The identity step needs to know whether a complement is a noun. The parser knows (the lexer gave every word a role): store it on the rule.
• hasProperty is about objects, not rules. Collect the rules in force whose complement is the property and whose subject names the object. The object has the property if one of them is positive and none is negated. Doing the negation per object, not only per rule, is what lets a negation about BABA beat a positive rule written about a larger group.
• Base rules are rules. If TEXT IS PUSH is in the parsed list like any other rule, TEXT IS NOT PUSH needs no code of its own.

Hint 3 — pseudo-code

complements(tiles, at, step):            // after IS
    found = []
    branches = [(not negated, at)] + [(negated, at + step) for each NOT in tiles[at]]
    for (sign, p) in branches:
        words = [w in tiles[p] where w is noun or property]
        if words is empty: continue
        found += words, each with this sign
        if tiles[p + step] has an AND:
            found += complements(tiles, p + 2 * step, step)
    return found

subjects(tiles, at, step):               // before IS, walking backwards
    if tiles[at + step] has NOT: return []
    ... as in Module 6

resolve(rules):
    kept = [r in rules where not exists n: n.negated and not r.negated
                                         and n.subject == r.subject and n.complement == r.complement]
    locked(x) = exists r in kept: not r.negated and r.subject == x and r.complement == x
    return [r in kept where r.negated or r.complement is not a noun
                           or r.subject == r.complement or not locked(r.subject)]

hasProperty(id, prop):
    about = [r in active where r.complement == prop and names(r.subject, object id)]
    return any(r positive in about) and not any(r negated in about)

When your tests pass, compare with the reference engine in course/07-rule-resolution/reference/rust/src/engine/puzzle/ or course/07-rule-resolution/reference/ts/src/engine/puzzle/: parse (now with NOT), the new resolve, level (has_property / hasProperty) and word (Lexicon::names).

Decisions in the reference that the tests don't force:

• BABA IS NOT BABA in activeRules() is the deletion record. The tests do force negated rules to stay in activeRules() (see the harness above: a negated rule is in force and keeps overriding). They don't check that BABA IS NOT BABA is listed, even though the reference lists it as its record that every Baba is to vanish. The sources say Baba vanishes; they don't say how an engine should record it.
• X IS NOT Y with Y a noun is just a negation. In the resolution pass it cancels X IS Y and nothing else, as the NOT page says of ROCK IS NOT GRASS. Like a negated property, it also has to be settled per object once two nouns can name the same thing: Module 9's conversion does that.
• Negation is settled twice. Once per rule in the resolution pass (activeRules() drops BABA IS YOU), and once per object in hasProperty. Only the second matters when the subjects differ, which the Expansion Drop shows.
• Which objects a noun names is a fact about the word. The reference's word list has an optional field, "selects": "named" (the default: the noun's own things), "text" (every text object) or "things" (every object that isn't text). The engine registers TEXT with "text". Lexicon::names / Lexicon.names reads the field.
• One NOT only. IS NOT NOT PUSH spells nothing (see the box below).
• Duplicates as before. The engine keeps a rule once per set of text objects, now including the NOT; the harness deduplicates.

How the real game differs

• NOT before a noun is real grammar in the game. The TEXT page says "TEXT is not included in ALL, but is included in NOT ALL", so NOT ALL names a group. The course's parser doesn't read negated subjects: it refuses the sentence rather than misread it. baba-is-auto makes the same cut: "Negated subjects, predicates, condition targets, repeated NOT, and nested forms are unsupported" (rule-language.md).
• NOT can stack: "NOT negates itself before negating anything else, so ROCK IS NOT NOT PUSH makes ROCK IS PUSH" (NOT). The course reads one NOT.
• X IS NOT X makes X disappear "similarly to X IS EMPTY but with particles" (same page). The course has no EMPTY, and the disappearance waits for Module 9's turn.
• Base rules can also be negated by BROKEN (Rule). The course has no BROKEN.
• BABA IS BABA blocks every conversion of Baba, "including those not in ALL" (IS). The course has no conversion into ALL, and the wiki's Order of Operations gives X IS ALL its own place in the turn ("X IS ALL takes the lowest priority").
• Course simplification: recording the deletion. The course keeps X IS NOT X in activeRules() as the record that every X is to vanish. The sources say X disappears (NOT); none read for the course says how the game records that, so this record is the course's choice, not the game's.
• Course simplification: what ALL names (Expansion Drop). The course's ALL names every object on the board that isn't text. The TEXT page says only that "TEXT is not included in ALL, but is included in NOT ALL"; the sources the course recorded don't define the rest of what ALL covers in the real game, so "every non-text object" is the course's rule, not a description of the game.

Name it

The pattern is a resolution pass (a post-pass): parse everything into candidate rules, then resolve the conflicts in one deterministic pass over the whole set, and let every query read only the result. The parser stays simple because it never decides anything. The resolver stays simple because it never reads the board. And every system that asks "is Baba YOU?" gets the same answer, because there is exactly one place that answers.

The reference's whole resolver:

pub fn resolve(rules: &[Rule]) -> Vec<Rule> {
    let survives_negation: Vec<&Rule> = rules
        .iter()
        .filter(|r| !rules.iter().any(|n| n.negates(r)))
        .collect();
    let locked = |subject: &str| {
        survives_negation
            .iter()
            .any(|r| !r.negated && r.is_identity() && r.subject == subject)
    };
    survives_negation
        .iter()
        .filter(|r| r.negated || !r.is_conversion() || r.is_identity() || !locked(&r.subject))
        .map(|&r| r.clone())
        .collect()
}

export function resolve(rules: readonly Rule[]): Rule[] {
  const survivesNegation = rules.filter((r) => !rules.some((n) => negates(n, r)));
  const locked = (subject: string) =>
    survivesNegation.some((r) => !r.negated && isIdentity(r) && r.subject === subject);
  return survivesNegation.filter((r) => r.negated || !isConversion(r) || isIdentity(r) || !locked(r.subject));
}

The order of the two steps is part of the meaning. Swap them and BABA IS NOT BABA no longer unlocks BABA IS ROCK, because the lock would already have removed it.

Magic: The Gathering has the large version of this. When many continuous effects change the same object, rule 613.1 of the Comprehensive Rules says: "Then all applicable continuous effects are applied in a series of layers in the following order", and inside a layer, "determining which order effects are applied in is usually done using a timestamp system" (613.7) and "is sometimes done using a dependency system" (613.8) (Comprehensive Rules). The shape is the same as yours: collect every effect first, then apply them in an order fixed by the rules, not by where the cards sit. Your resolver has two layers, negation and identity, and needs no timestamps, because a rule's position on the board never matters.

Compare it with Module 4. Baron's interceptor is consulted at the moment a Deathrattle runs, and it changes how many times something happens. NOT is applied when the rules are compiled, and it changes whether a rule exists at all. Both keep the thing they modify ignorant of them. Which one would you rather debug? The course's closing question returns to Baron and BABA IS NOT YOU; keep your notes.

Run the coupling audit again: node tools/coupling-audit.mjs ~/my-engine should print coupling-audit: ok. The resolver names no noun: it compares subjects and complements, whatever they spell.

Expansion Drop

A new word arrives: ALL, a meta-noun. As a subject it names every object on the board that is not text: the TEXT page is explicit that "TEXT is not included in ALL".

The constraint, as always: do not edit anything under src/engine/. The harness doesn't change either. Only your word list should.

1. Commit your workspace and note the commit: git add -A && git commit -m "module 7 done".
2. Copy the expansion test for your track from course/07-rule-resolution/expansion/tests/rust/test_07x.rs or course/07-rule-resolution/expansion/tests/ts/test_07x.test.ts into your workspace's tests/. Run it and watch it fail.
3. Add ALL to your word list.
4. When the tests pass, run the check from the course repository:

node tools/expansion-check.mjs ~/my-engine HEAD

The test, test_07x_all_meta_noun, writes ALL IS YOU with a baba, a rock and a piece of text on the board. Baba and the rock are YOU; the text is not. Then it writes BABA IS NOT YOU: Baba stops being YOU, the rock doesn't. The full scenario is in course/07-rule-resolution/expansion/README.md.

Discussion: what this drop measures

If "which objects does this noun name" is a fact about the word, ALL is one line:

{ "name": "ALL", "role": "noun", "selects": "things" }

That is the reference answer, in course/07-rule-resolution/expansion/solution/words.json (the Module 7 word list with that line added), the same file for both tracks.

Shapes that fail this drop:

• TEXT as a branch in the engine. If hasProperty says if subject == TEXT { object is text } else { object's noun == subject }, then ALL is a third branch, under src/engine/. The test can't pass without an engine change. The fix is to move the question "which objects does this noun name" into the word list, and let TEXT be the first entry that uses it. Make it a normal commit, then redo the drop.
• Negation only per rule. If your resolver cancels X IS Y only when a rule X IS NOT Y has the very same subject, and hasProperty then trusts any positive rule, ALL IS YOU survives and Baba stays YOU after BABA IS NOT YOU. The second half of the test fails. The negation has to be checked for the object, against every noun that names it.
• Expanding ALL in the parser. Turning ALL IS YOU into BABA IS YOU, ROCK IS YOU, ... for every noun in the word list works for this test, but the parser now needs to know the board's objects, and activeRules() shows rules nobody wrote. Keep the parser about text.

If the check fails, fix your engine (a normal commit, outside the drop), then redo the drop from step 1.

Stress it

Optional. Each question pushes the design past what this module's tests check. Predict first, then open the discussion.

1. Start from an empty board and place three sentences, one at a time: BABA IS ROCK, then BABA IS BABA, then BABA IS NOT BABA. After each, is BABA IS ROCK in activeRules()? What does that tell you about the function from "text on the board" to "rules in force"?

Discussion

Yes, no, yes. Adding text removed a rule, and adding more text brought it back.

In logic, a system where more premises can only give more conclusions is called monotonic. This one isn't: NOT and the identity lock are both ways for a sentence to take something away. That has a practical consequence for an engine. In a monotonic system you could update the rule set incrementally, adding what each new sentence implies. Here a new sentence can invalidate any earlier conclusion, so the safe design is the one the module builds: throw the conclusions away and derive them again from all the premises.

It also has a consequence for players, and it is the reason the game is a puzzle game at all. Every "aha" in Baba Is You is a non-monotonic step: you make something stop being true by adding a word.

2. The resolver runs negation first and identity second, once each. Why is one pass of each enough? Could a rule removed in the second step have been needed in the first? Invent a kind of rule that would make two passes not enough.

Discussion

Negation only reads what the parser wrote: a negated rule is never removed by anything, so the set of negations is known before the pass starts, and the first step can't be affected by the second. Identity reads the survivors of the first step. Information flows one way, parse → negation → identity, so each step runs once.

Database people call this stratification. Datalog, the classic rule language, allows negation only in this layered form: "Stratified negation can be added to Datalog while retaining its model-theoretic and fixed-point semantics." (Datalog, Wikipedia). A stratum may negate facts from lower strata, never from its own or a higher one.

To break it you need a rule whose applicability depends on the resolved rule set, so that resolving can change what needs resolving. The real game has several: conditions such as ON and NEAR depend on the board, and words that make an object count as text feed the parser from the rules. With those, "is this rule in force?" can depend on itself, and a design has to choose between iterating to a fixed point, detecting the loop, or forbidding the construction. Jonathan Geller's Baba is You is Undecidable (2022) shows how far the full rule set goes: "We establish the undecidability of 2019 puzzle game Baba is You through a reduction from the Post correspondence problem." The course's grammar is deliberately small enough to stratify.

3. Two facts every correct resolve satisfies, whatever the rules: running it on its own output changes nothing, and shuffling its input only shuffles its output. Test both on a few hundred random rule lists. Then find the mistake in this plausible resolver: "walk the list once; when you meet X IS NOT Y, delete any X IS Y you have already seen".

Discussion

The first property is idempotence: resolve(resolve(R)) = resolve(R). It holds because the negations and the surviving locks are all still present in the output, so a second run finds nothing new to remove. The second is order-independence, and it is Predict question 1 stated for every input at once.

The one-walk resolver fails order-independence: a negation deletes what came before it and misses what comes after. On the list [BABA IS NOT YOU, BABA IS YOU] it keeps BABA IS YOU. A hand-written test finds this only if its author thought to put the negation first; a shuffle finds it in a handful of tries. The generator needs no board: make rules from three nouns and three properties, with a random sign.

Idempotence is worth the extra line because of where resolvers go wrong as they grow. The day a third step is added that can remove a lock, a rule that the lock had removed should come back, and a single pass in the old order won't bring it. The property fails that day.

4. Do the Expansion Drop first. Then: ALL IS YOU, BABA IS BABA, and ALL IS ROCK are on the board, with one Baba and one key. Which rules does activeRules() list? Is Baba going to become a rock? Is the key?

Discussion

All three rules are listed. BABA IS BABA locks the subject BABA, and ALL IS ROCK has a different subject, so the resolution pass leaves it alone. And yet Baba must not become a rock, because BABA IS BABA "prevents BABA from transforming into any object". The key, named by ALL and by no lock, does convert.

So activeRules() can't be the whole answer to "what happens to this object". It is a list of sentences; the truth about an object needs every sentence whose subject names that object. This is the per-rule and per-object split the drop's discussion describes for properties, and it applies to locks and to negated conversions (ALL IS ROCK with BABA IS NOT ROCK) in the same way. hasProperty already asks the question per object. Module 9's conversion has to as well, and its test_09_negated_conversion_beats_group is there because the first version of the course's reference forgot.

The general point: once two names can refer to one thing, every rule about a name has to be re-read as a rule about the things it names at the moment of use. Group nouns are the cheapest feature in this module to add and the one with the longest reach.

5. TEXT IS NOT PUSH is written on the board. Can the player ever undo it?

Discussion

Not by pushing: the three words that spell it are text, and no text is pushable while it stands. The rule protects itself. Another rule could still move text some other way, which is what the wiki's rulebook alludes to ("Text can be stacked if TEXT IS NOT PUSH can be formed with another way to move text"), but the course has no other way.

A level that lets the player form this sentence with nothing else in reach is unwinnable from that point, and nothing tells the player so. That is a property of the level, not the engine, and you can check it mechanically: Module 13 builds a search that finds every position a level can reach, including the dead ones.

Further reading

• The Baba Is You Wiki's NOT and IS pages: every case in this module, and the ones the course leaves out (stacked NOT, NOT before nouns). Then TEXT for TEXT IS PUSH and ALL.
• John Harris, Designing Baba Is You's delightfully innovative rule-writing system, Game Developer, 8 May 2019: Teikari on the final pass over the rule set, the pass you just built.
• Wizards of the Coast, Magic: The Gathering Comprehensive Rules, rule 613 (613.1, 613.7, 613.8): interaction of continuous effects, in layers, by timestamp and by dependency. A resolution pass for a game with thousands of cards.
• Argentum, docs/architecture-principles.md, §2.3 "Rule 613: Base State vs. Projected State": "the engine doesn't need to 'undo' +3/+3. It simply removes the floating effect." The same idea as recompiling the rules from the board.
• Datalog, Wikipedia, the sections on negation and on evaluation: the same problem as this module (derive everything that follows from a set of facts and rules, with negation), studied for decades. Read it for the words stratified and fixed point.
• baba-is-auto, Game::ParseRules in Sources/baba-is-auto/Games/Game.cpp (around line 611) and RuleManager::HasProperty in Sources/baba-is-auto/Rules/RuleManager.cpp: one place that answers "does this object have this property?". It is an example of rules as data, not an authority on the game: it has no IS NOT for properties or nouns and hard-codes text as pushable (rule-language.md), so it can't run this module's tests.