Doing and undoing

Rosa and her little brother Mateo, in Oaxaca in Mexico, are playing a game. Rosa does something. Then Mateo has to undo it — to put everything back exactly as it was.

• Rosa opens the window. Mateo closes it. Back as it was!
• Rosa puts on Grandpa's hat. Mateo takes it off her head.
• Rosa takes 3 big steps forward. Mateo says, "Now take 3 big steps back!"
• Rosa turns over a card, so the picture is hidden. Mateo turns it over again.

Then Grandma cracks an egg into the pan for breakfast. "Undo that!" laughs Rosa. Mateo looks at the egg. He thinks hard. Can anybody put a cracked egg back together?

An action is something you do that changes something: open a door, add a block to a tower, turn an arrow, walk forward. Every action has an effect: the door was closed, and now it is open.

Some actions can be undone. To undo an action, you do a second action that puts everything back the way it was before.

Blocks. Here are 5 dots. Tap Add one three times. Now undo what you did. How many times do you need to tap Take one away?

Time. The clock shows 8 o'clock. Press + to move it on half an hour. Which button undoes that?

Turning. Pick the triangle, switch on Rotational symmetry and press Turn. The gold dot shows where one corner went. Now, without a "turn back" button, how can you get the gold dot back where it started? Keep turning! How many more turns does it take? Try the square and the hexagon too.

Doing nothing is a funny action, but a very useful one. Doing nothing and then flipping a card is just the same as flipping the card. And doing an action and then undoing it has the same effect as doing nothing at all!

Some actions cannot be undone, however hard we try: cracking an egg, mixing two paints, cutting paper into pieces, squashing a sandcastle. Why not?

Here is a big clue. Kenji's class has a little whiteboard. One day it has a picture of a cat on it. Another day it has a picture of a dog. Each day, after school, the teacher wipes it clean.

Could some action undo the wiping? It would have to look at the blank board and bring back the picture. But which picture — the cat or the dog? Both boards turned into the very same blank board. Nothing about the blank board tells you which one it was.

So here is the rule: if an action turns two different things into the same thing, it can never be undone. The egg is like that, too: a whole egg and an egg that is already cracked both end up cracked. Orange paint could have come from red and yellow, or straight from a tin of orange.

Gideon reads a statement. Is it true or false?

1. "Flipping a card is undone by flipping it again." — True.
2. "Every action is undone by doing it again." — False! Walking 3 steps forward twice takes you 6 steps away. One counterexample is enough.
3. "A quarter turn can be undone by three more quarter turns." — True. Four quarter turns make a full turn.
4. "Every action can be undone." — False. Wiping the board cannot be undone.
5. "Doing nothing, and then flipping the card, is the same as just flipping the card." — True.

/-- An action on a world of things of type `α`: for each thing, what it becomes. -/
abbrev Action (α : Type) : Type := α → α

/-- The action of **doing nothing**: every thing stays exactly as it was. -/
def doNothing {α : Type} : Action α := fun x => x

/-- Do `a`, and then do `b`. -/
def andThen {α : Type} (a b : Action α) : Action α := fun x => b (a x)

/-- `u` **undoes** `a` when doing `a` and then `u` puts every thing back as it was. -/
def Undoes {α : Type} (u a : Action α) : Prop := ∀ x, u (a x) = x

/-- Doing nothing and then doing `a` has the same effect as just doing `a`. -/
theorem doNothing_andThen {α : Type} (a : Action α) : andThen doNothing a = a := rfl

/-- Flip the card over. -/
def flip : Action Card
  | .faceUp => .faceDown
  | .faceDown => .faceUp

/-- Flipping a card is undone by flipping it again. Check both cases. -/
theorem flip_undoes_flip : Undoes flip flip := by
  intro c
  cases c <;> rfl

/-- Turn the arrow a quarter turn clockwise (the way clock hands go). -/
def quarterTurn : Action Arrow
  | .up => .right
  | .right => .down
  | .down => .left
  | .left => .up

/-- A quarter turn is undone by a quarter turn back. -/
theorem quarterBack_undoes_quarterTurn : Undoes quarterBack quarterTurn := by
  intro a
  cases a <;> rfl

/-- A quarter turn is *also* undone by three more quarter turns the same way. -/
theorem three_more_turns_undo :
    Undoes (fun a => quarterTurn (quarterTurn (quarterTurn a))) quarterTurn := by
  intro a
  cases a <;> rfl

/-- A quarter turn is **not** undone by doing it again: an arrow pointing up ends up pointing
down. One counterexample is enough. -/
theorem quarterTurn_not_undone_by_itself : ¬ Undoes quarterTurn quarterTurn := by
  intro h
  have hup : quarterTurn (quarterTurn Arrow.up) = Arrow.up := h Arrow.up
  -- But two quarter turns take `up` to `down`, and `down ≠ up`.
  exact absurd hup (by decide)

/-- "Take 3 steps forward" is undone by "take 3 steps back" — for any number of steps.
This applies core Lean's `Int.add_sub_cancel`. -/
theorem back_undoes_forward (n : Int) : Undoes (back n) (forward n) :=
  fun x => Int.add_sub_cancel x n

/-- Walking forward again does **not** undo walking forward (unless the number of steps is
`0`): starting from `0`, two walks of `n` steps end at `n + n`, not at `0`. -/
theorem forward_not_undone_by_itself (n : Int) (hn : n ≠ 0) :
    ¬ Undoes (forward n) (forward n) := by
  intro h
  have h0 : 0 + n + n = 0 := h 0
  omega

/-- **Why some actions cannot be undone.** If an action sends two *different* things `x`
and `y` to the *same* result, then no action can undo it: an undo would have to take that one
result back to `x` and also back to `y`.
`x = u (a x) = u (a y) = y`, which contradicts `x ≠ y`. -/
theorem cannot_undo_of_same_result {α : Type} (a : Action α) {x y : α} (hxy : x ≠ y)
    (h : a x = a y) : ¬ ∃ u, Undoes u a := by
  intro ⟨u, hu⟩
  apply hxy
  calc x = u (a x) := (hu x).symm
    _ = u (a y) := by rw [h]
    _ = y := hu y

/-- Wiping the board cannot be undone: the cat board and the dog board both become blank,
so no action can know which picture to bring back. -/
theorem wipe_cannot_be_undone : ¬ ∃ u, Undoes u wipe :=
  cannot_undo_of_same_result wipe (x := .cat) (y := .dog) (by decide) rfl

/-- Cracking an egg cannot be undone, even in our tiny model: a whole egg and a cracked egg
both end up cracked. -/
theorem crack_cannot_be_undone : ¬ ∃ u, Undoes u crack :=
  cannot_undo_of_same_result crack (x := .whole) (y := .cracked) (by decide) rfl

/-- But "take a block away" cannot be undone in general: a tower of 1 block and an empty
spot both end up with 0 blocks, so nothing can tell whether to put a block back. -/
theorem takeBlock_cannot_be_undone : ¬ ∃ u, Undoes u takeBlock :=
  cannot_undo_of_same_result takeBlock (x := 1) (y := 0) (by decide) rfl

Margaret found that only 6 of the 27 actions can be undone: the ones that just shuffle the counters around, never turning two counters into the same one. And only 4 of those 6 are undone by doing them again. The other 2 move every counter one place round in a circle, and they are undone by going round the other way.

"""Every action in a tiny world: which ones can be undone?

A tiny world has a few things in it, say a red, a blue and a green counter in
three boxes. An action says, for each thing, what it becomes. With n things
there are n^n actions. For worlds of 1 to 4 things this program lists every
action, searches all n^n candidates for an action that undoes it, and checks
the lesson's rule: an action can be undone exactly when it never sends two
different things to the same result. It also counts the actions that are
undone by simply doing them again, like flipping a card, and finds how many
quarter turns undo one quarter turn of an arrow.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from itertools import product
from math import factorial
import textwrap

def all_actions(n):
    """Every action on the things 0..n-1, as a tuple: thing i becomes a[i]."""
    return list(product(range(n), repeat=n))

def then(a, b):
    """Do action a, then action b."""
    return tuple(b[a[i]] for i in range(len(a)))

def do_nothing(n):
    """The action that leaves every thing as it was."""
    return tuple(range(n))

def undoes(u, a):
    """Does u undo a, i.e. does doing a then u put everything back?"""
    return then(a, u) == do_nothing(len(a))

def find_undo(a):
    """Search every action for one that undoes a; return it, or None."""
    for u in all_actions(len(a)):
        if undoes(u, a):
            return u
    return None

def no_two_the_same(a):
    """True when the action never sends two different things to one result."""
    return len(set(a)) == len(a)

def turns_to_undo(turn, start):
    """How many more times must `turn` be done to undo one `turn`?"""
    count, state = 0, turn(start)
    while state != start:
        state = turn(state)
        count += 1
    return count

def describe(a):
    """Write an action as 'thing -> result' pairs, e.g. '0->1, 1->2, 2->0'."""
    return ", ".join(f"{i}->{j}" for i, j in enumerate(a))

ARROWS = ["up", "right", "down", "left"]

def quarter_turn(arrow):
    """Turn an arrow a quarter turn clockwise."""
    return ARROWS[(ARROWS.index(arrow) + 1) % 4]

def main():
    print("Tiny worlds: every action, and every possible undo, checked.")
    print("  things  actions  can be undone  undone by doing it again")
    rule_holds, counts = True, []
    for n in range(1, 5):
        acts = all_actions(n)
        undoable = [a for a in acts if find_undo(a) is not None]
        rule_holds &= all((a in undoable) == no_two_the_same(a) for a in acts)
        self_undo = sum(1 for a in acts if undoes(a, a))
        counts.append(len(undoable))
        print(f"  {n:6d} {len(acts):8d} {len(undoable):14d} {self_undo:25d}")
    print()
    print("Can be undone exactly when no two things end up the same:",
          rule_holds)
    shuffles = [factorial(n) for n in range(1, 5)]
    print("Undoable counts are the numbers of shuffles 1, 1x2, 1x2x3, 1x2x3x4:",
          counts == shuffles)
    print()
    print("Three things, an action that goes round: 0->1, 1->2, 2->0.")
    go_round = (1, 2, 0)
    print(f"  undone by doing it again? {undoes(go_round, go_round)}")
    print(f"  undone by:                {describe(find_undo(go_round))}"
          "  (round the other way)")
    extra = turns_to_undo(quarter_turn, "up")
    print(f"A quarter turn of an arrow is undone by {extra} more quarter turns.")
    print()
    print(textwrap.fill(
        "Epistemic status: exact and exhaustive for worlds of 1 to 4 things "
        "(every action and every candidate undo was tried), so these counts "
        "are certain. It is not a proof for bigger worlds. The lesson proves, "
        "for every world, that an action sending two things to the same "
        "result can never be undone.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Act them out if you can: walk, turn, flip cards, build towers. You can ask for a hint whenever you like.

Doing one action after another is the next step: One thing after another asks how to undo a whole chain of actions (think about socks and shoes!).

• "Algebra" means "restoring". Around 820 CE, in Baghdad, Muḥammad ibn Mūsā al-Khwārizmī wrote a book about solving problems by two kinds of steps. One was called al-jabr, "restoring": when something has been taken away on one side of a problem, add it back, on both sides, so that nothing is missing. Our word algebra comes from it.
• Groups. In the 1830s the young French mathematician Évariste Galois studied collections of shuffles that can all be undone, to understand when equations can be solved. Today such collections are called groups.
• A famous puzzle. In 1974, Ernő Rubik, a teacher of design in Budapest, invented his cube puzzle. Every twist can be undone by twisting back — but undoing a long muddle of twists takes careful thinking about the order.

• F. William Lawvere and Stephen H. Schanuel, Conceptual Mathematics: A First Introduction to Categories (1997; 2nd ed. 2009) — maps, identity maps and inverses ("retractions" and "sections") with everyday examples.
• Eugenia Cheng, How to Bake Pi: An Edible Exploration of the Mathematics of Mathematics (2015) — a popular introduction to the ideas behind category theory.
• Nathan Carter, Visual Group Theory (2009) — groups as collections of actions, with many pictures.