Following and giving precise instructions

In a classroom in Nairobi, Mr Otieno has a loaf of bread, a jar of jam and a spoon. "I am a robot," he says. "I will make a jam sandwich, but I will do exactly what you tell me — nothing more."

"Put the jam on the bread!" calls Wanjiru.

Mr Otieno picks up the whole jar and puts it on top of the loaf. Everybody laughs. That is not what Wanjiru meant! But it is what she said.

"Open the jar," tries Baraka. "Take a slice of bread out of the bag. Put a spoonful of jam on the slice. Spread it with the spoon…" Step by step, the sandwich gets made.

Here is a map drawn on a grid of squares. You start on the gold star. Each arrow card tells you to move one square in the direction of the arrow. Follow the cards in order, from left to right.

A list of instructions like this is called a program, or an algorithm. The person (or robot) following it does not need to guess anything: each card says exactly what to do.

This map shows the streets of a small town. H is Home, L is the Library, S is the School, P is the Park and M is the Market; the numbers are other street corners. Plan a route from H to L by clicking the streets one after another, starting at H. Your route is a program: "go along this street, then this one, then this one…".

What to try:

• Find a route that uses only 4 streets. Then find a different route with 4 streets. How many can you find? (Margaret's computer says there are 6.)
• Try clicking a street that does not touch the corner where you are. The map will not let you jump — every step must follow on from the last one.
• Can you find a route that goes past the Park (P) and the Market (M)?

A robot or a computer does not know what you mean. It only does what you say. That is why the jam went on the loaf.

• Each step must be clear. "Turn" is not enough: turn left or right? "Go forward" — how many squares?
• The steps must be in the right order. Spreading the jam before opening the jar does not work.
• The same program always does the same thing. If you follow a program twice from the same start, you end up in the same place twice. That is what makes programs so useful — and it is why, when a program has a bug, it does the wrong thing every time until you fix it.

Gideon reads a statement. Is it true or false?

1. "The program → → ↑ takes you to the square 2 across and 1 up." — True.
2. "There is only one correct program to reach a square." — False! ↑ → → and → → ↑ both reach the same square.
3. "For the robot, forward then turn right does the same as turn right then forward." — False. The robot ends on different squares.
4. "Turn left, then turn right leaves the robot exactly as it was." — True. The second turn undoes the first.
5. "You can reach the square 3 across and 2 up with only 4 arrow cards." — False. Each card moves you only one square, and you need 3 across and 2 up: at least 5 cards.

/-- The four arrow cards. -/
inductive Arrow where
  | up | down | left | right
  deriving DecidableEq, Repr

/-- What one arrow card does: move one square in its direction. -/
def step : Arrow → Pos → Pos
  | .up, p => ⟨p.x, p.y + 1⟩
  | .down, p => ⟨p.x, p.y - 1⟩
  | .left, p => ⟨p.x - 1, p.y⟩
  | .right, p => ⟨p.x + 1, p.y⟩

/-- Follow a program of arrow cards from the square `p`: do the first card, then follow the
rest of the program from where you are. -/
def run : List Arrow → Pos → Pos
  | [], p => p
  | a :: prog, p => run prog (step a p)

/-- The program `→ → ↑` takes you from the start to the square 2 across and 1 up. -/
theorem to_the_tree : run [.right, .right, .up] start = ⟨2, 1⟩ := rfl

/-- There is more than one correct program: `↑ → →` and `→ ↑ →` are different programs that
end on the same square as `→ → ↑`. -/
theorem two_programs :
    run [.up, .right, .right] start = ⟨2, 1⟩ ∧ run [.right, .up, .right] start = ⟨2, 1⟩ ∧
    [Arrow.up, .right, .right] ≠ [.right, .up, .right] := by
  decide

/-- Following program `p` and then program `q` is the same as following the joined program
`p ++ q`. Proof by induction on `p`. -/
theorem run_append (p q : List Arrow) (s : Pos) : run (p ++ q) s = run q (run p s) := by
  induction p generalizing s with
  | nil => rfl
  | cons a p ih => exact ih (step a s)

/-- The "across plus up" distance between two squares: how many squares across, plus how many
squares up or down. (Grown-ups call it the taxicab distance.) -/
def taxi (p q : Pos) : Nat := (q.x - p.x).natAbs + (q.y - p.y).natAbs

/-- **No program is shorter than the distance.** Every arrow program that goes from `s` to a
square uses at least as many cards as the "across plus up" distance to that square: each card
moves you at most one square closer. Proof by induction on the program. -/
theorem taxi_le_length (prog : List Arrow) (s : Pos) : taxi s (run prog s) ≤ prog.length := by
  -- Strengthen: start the program at any square `p`, measuring from `s`.
  suffices h : ∀ p : Pos, taxi s (run prog p) ≤ taxi s p + prog.length by
    have := h s
    simpa [taxi] using this
  induction prog with
  | nil => intro p; simp [run]
  | cons a prog ih =>
    intro p
    have h1 := ih (step a p)
    have h2 := taxi_step s p a
    simp only [run, List.length_cons]
    omega

/-- **A shortest program always exists**: to reach the square `a` across and `b` up, use `a`
right arrows and then `b` up arrows — exactly `a + b` cards, the distance. -/
theorem straight_route (a b : Nat) :
    run (List.replicate a .right ++ List.replicate b .up) start = ⟨a, b⟩ := by
  rw [run_append]
  -- Each block of identical arrows moves you that many squares.
  have hr : ∀ (n : Nat) (p : Pos), run (List.replicate n .right) p = ⟨p.x + n, p.y⟩ := by
    intro n
    induction n with
    | zero => intro p; simp [run]
    | succ n ih =>
      intro p
      simp only [List.replicate, run, step, ih]
      congr 1
      omega
  have hu : ∀ (n : Nat) (p : Pos), run (List.replicate n .up) p = ⟨p.x, p.y + n⟩ := by
    intro n
    induction n with
    | zero => intro p; simp [run]
    | succ n ih =>
      intro p
      simp only [List.replicate, run, step, ih]
      congr 1
      omega
  rw [hr, hu]
  simp [start]

/-- What one button does to the robot. -/
def exec : Cmd → Robot → Robot
  | .forward, ⟨p, .north⟩ => ⟨⟨p.x, p.y + 1⟩, .north⟩
  | .forward, ⟨p, .east⟩ => ⟨⟨p.x + 1, p.y⟩, .east⟩
  | .forward, ⟨p, .south⟩ => ⟨⟨p.x, p.y - 1⟩, .south⟩
  | .forward, ⟨p, .west⟩ => ⟨⟨p.x - 1, p.y⟩, .west⟩
  | .turnLeft, ⟨p, .north⟩ => ⟨p, .west⟩
  | .turnLeft, ⟨p, .west⟩ => ⟨p, .south⟩
  | .turnLeft, ⟨p, .south⟩ => ⟨p, .east⟩
  | .turnLeft, ⟨p, .east⟩ => ⟨p, .north⟩
  | .turnRight, ⟨p, .north⟩ => ⟨p, .east⟩
  | .turnRight, ⟨p, .east⟩ => ⟨p, .south⟩
  | .turnRight, ⟨p, .south⟩ => ⟨p, .west⟩
  | .turnRight, ⟨p, .west⟩ => ⟨p, .north⟩

/-- **The order of the steps matters.** "Forward, then turn right" leaves the robot one square
up, facing east; "turn right, then forward" leaves it one square to the right. -/
theorem order_matters :
    runRobot [.forward, .turnRight] home = ⟨⟨0, 1⟩, .east⟩ ∧
    runRobot [.turnRight, .forward] home = ⟨⟨1, 0⟩, .east⟩ := by
  decide

/-- "Turn left, then turn right" does nothing at all, wherever the robot is and whichever way
it faces. (Check all four headings.) -/
theorem left_then_right (r : Robot) : exec .turnRight (exec .turnLeft r) = r := by
  obtain ⟨p, h⟩ := r
  cases h <;> rfl

/-- **Finding and fixing a bug.** The target is 2 squares up and 1 square to the right. The
program "forward, forward, turn left, forward" goes the wrong way (left instead of right);
changing the one wrong instruction to "turn right" fixes it. -/
theorem debug :
    (runRobot [.forward, .forward, .turnLeft, .forward] home).pos = ⟨-1, 2⟩ ∧
    (runRobot [.forward, .forward, .turnRight, .forward] home).pos = ⟨1, 2⟩ := by
  decide

Margaret's computer found that the shortest program to a square always has exactly "squares across plus squares up" cards, and that there are usually many shortest programs. To reach the square 2 across and 2 up there are 6 different shortest programs; to reach 3 across and 3 up there are 20!

"""Shortest programs, many correct answers, and fixing a bug.

Part 1 runs every arrow-card program of up to 6 cards (up, down, left,
right) from the start square of a grid. For each square it finds the
shortest programs that end there, and checks two patterns: the shortest
length is "squares across plus squares up", and the number of shortest
programs is a binomial coefficient. Part 2 is a floor robot with the buttons
forward (F), turn left (L) and turn right (R): it tries every one-instruction
change of a buggy program to find the fixes, counts the correct programs, and
checks which pairs of instructions can be swapped without changing the result.

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

from itertools import product
from math import comb
import textwrap

MOVES = {"U": (0, 1), "D": (0, -1), "L": (-1, 0), "R": (1, 0)}
HEADINGS = [(0, 1), (1, 0), (0, -1), (-1, 0)]  # north, east, south, west

def run_arrows(program, start=(0, 0)):
    """Follow arrow cards (a string of U, D, L, R); return the end square."""
    x, y = start
    for card in program:
        dx, dy = MOVES[card]
        x, y = x + dx, y + dy
    return (x, y)

def shortest_programs(max_cards):
    """Map each square to (shortest length, number of shortest programs)."""
    best = {(0, 0): (0, 1)}
    for n in range(1, max_cards + 1):
        for program in product("UDLR", repeat=n):
            end = run_arrows(program)
            if end not in best:
                best[end] = (n, 1)
            elif best[end][0] == n:
                best[end] = (n, best[end][1] + 1)
    return best

def distance(square):
    """Squares across plus squares up or down from the start."""
    return abs(square[0]) + abs(square[1])

def run_robot(program, pos=(0, 0), facing=0):
    """Press robot buttons (a string of F, L, R); return (square, facing).

    The robot starts facing north (index 0 of HEADINGS); turns happen on
    the spot.
    """
    x, y = pos
    for button in program:
        if button == "F":
            dx, dy = HEADINGS[facing]
            x, y = x + dx, y + dy
        elif button == "L":
            facing = (facing - 1) % 4
        elif button == "R":
            facing = (facing + 1) % 4
        else:
            raise ValueError(f"unknown button {button!r}")
    return (x, y), facing

def one_change_fixes(program, target):
    """Every program that differs in one instruction and ends on target."""
    fixes = []
    for i, old in enumerate(program):
        for new in "FLR":
            if new != old:
                changed = program[:i] + new + program[i + 1:]
                if run_robot(changed)[0] == target:
                    fixes.append(changed)
    return fixes

def correct_robot_programs(target, max_len):
    """All robot programs of length 1..max_len that end on the target."""
    return ["".join(p) for n in range(1, max_len + 1)
            for p in product("FLR", repeat=n) if run_robot(p)[0] == target]

def main():
    best = shortest_programs(6)
    print("1. Arrow programs: every program of 1 to 6 cards was run.")
    print("   square    shortest  how many shortest  (a+b choose a)")
    for sq in [(1, 0), (2, 1), (-2, 1), (2, 2), (3, 1), (3, 3)]:
        n, count = best[sq]
        a, b = abs(sq[0]), abs(sq[1])
        print(f"   {str(sq):<9} {n:6d} {count:13d} {comb(a + b, a):16d}")
    near = [sq for sq in best if distance(sq) <= 6]
    ok_len = all(best[sq][0] == distance(sq) for sq in near)
    ok_count = all(best[sq][1] == comb(distance(sq), abs(sq[0])) for sq in near)
    print(f"   {len(near)} squares reached. Shortest = across + up: {ok_len}")
    print(f"   Number of shortest programs = (a+b choose a): {ok_count}")
    print()
    target, buggy = (1, 2), "FFLF"
    print("2. Floor robot: F = forward, L = turn left, R = turn right.")
    print(f"   Target: 1 right and 2 up. Buggy program {buggy} ends at "
          f"{run_robot(buggy)[0]}.")
    print(f"   One-instruction fixes: {', '.join(one_change_fixes(buggy, target))}")
    good = correct_robot_programs(target, 6)
    shortest = min(len(p) for p in good)
    print(f"   Correct programs of up to 6 buttons: {len(good)}; "
          f"the shortest has {shortest}.")
    for a, b in [("F", "L"), ("F", "R"), ("L", "R")]:
        same = run_robot(a + b) == run_robot(b + a)
        print(f"   {a}{b} and {b}{a} end the same way: {same}")
    print()
    print(textwrap.fill(
        "Epistemic status: exact and exhaustive for the programs tried (all "
        "arrow programs of up to 6 cards, all robot programs of up to 6 "
        "buttons), so these results are certain for them. The patterns are "
        "evidence, not a proof, for longer programs; the lesson's Lean file "
        "proves that no arrow program is shorter than the distance and that "
        "a program of exactly that length always exists.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Draw a grid on paper, or use the floor tiles, and act the programs out. You can ask for a hint whenever you like.

A program is a chain of actions, done one after another. In Doing and undoing you saw single actions and how to undo them; One thing after another chains them together. (How would you undo a whole robot program? Hint: think about the order!)

• The word "algorithm". Around 820 CE, in Baghdad, Muḥammad ibn Mūsā al-Khwārizmī wrote a book explaining how to calculate with the Hindu–Arabic numerals 0 to 9. When it was translated into Latin, his name was written Algoritmi — and that gave us the word algorithm.
• A loom that follows instructions. In 1804, Joseph-Marie Jacquard in France built a weaving loom controlled by a chain of punched cards. The holes in the cards told the loom which threads to lift, so the same pattern could be woven again and again.
• The first published computer program. In 1843, Ada Lovelace published notes on Charles Babbage's planned Analytical Engine, including a step-by-step method for the machine to calculate a sequence of numbers called the Bernoulli numbers.
• The first "actual bug". In 1947, the team working on the Harvard Mark II computer found a moth stuck in one of its switches, and taped it into their logbook as the "first actual case of bug being found". (Engineers had already called mistakes "bugs" for decades.) Grace Hopper, a member of the team, loved to tell the story.
• Turtles for children. In the late 1960s, Seymour Papert, Cynthia Solomon and Wally Feurzeig created the Logo language, in which children give instructions like "forward" and "right" to a "turtle" — sometimes a little floor robot — to draw shapes.

• Tim Bell, Ian H. Witten and Mike Fellows, Computer Science Unplugged (1998; later editions) — classroom activities for computing ideas without computers.
• Seymour Papert, Mindstorms: Children, Computers, and Powerful Ideas (1980) — the classic book on children programming turtles.
• Linda Liukas, Hello Ruby: Adventures in Coding (2015) — a picture book about thinking like a programmer, with activities.