Reversible Programming

The single most common statement in all of programming is also the most destructive. x = 42 looks harmless — but whatever x held a moment ago is now gone, unrecoverable, erased. Every ordinary program is a long chain of these little acts of forgetting. We have spent this course building hardware that never forgets — all the way up to a reversible processor. Now comes the natural question: what does it feel like to program such a machine? What does a language look like when destructive assignment is simply not on the menu?

The answer is a small, beautiful discipline: build every program out of steps that are individually invertible, and the whole program inherits an inverse automatically. This lesson lays out the two pillars of that discipline — invertible updates and assertions at joins — and the rest of the module builds real languages on top of them.

Updates that can be undone

Recall from variables and assignment that x = e replaces the value of x. That replacement is a many-to-one funnel: every possible old value of x leads to the same new state, so the old value cannot be deduced afterwards. Irreversible.

But not every assignment forgets. An update that combines the old value with something else, using an operation that can be unpicked, keeps the past recoverable:

Update	Meaning	Inverse
`x += e`	add `e` to `x`	`x -= e`
`x -= e`	subtract `e` from `x`	`x += e`
`x ^= e`	XOR `e` into `x`	`x ^= e` (its own inverse)
swap `x`, `y`	exchange two variables	swap again (its own inverse)

with one crucial side condition: the updated variable must not occur in the expression e. As long as that holds, the new value of x together with the (unchanged) value of e pins down the old value of x exactly — the update is a bijection on the program state. In the language of maths, x \mapsto x + e for fixed e is invertible, with inverse x \mapsto x - e; plain assignment x \mapsto e is a constant map, the least invertible function there is.

The side condition — the updated variable may not appear in its own update expression — is not bureaucratic fussiness. Consider x += x. It doubles x, and doubling integers is one-to-one… but its inverse is halving, which only lands on an integer when x is even. The update sneaks you out of the tidy world where += is undone by -=: mechanically applying the rule "invert x += e as x -= e" would give x -= x, which zeroes x — a genuinely destructive step! And x ^= x is even worse: it sets x to 0 no matter what, erasing x outright. So reversible languages enforce the rule syntactically: the variable being updated must not be free in the right-hand side. Then, and only then, every update is invertible by the simple symbol-for-symbol swap in the table above.

Run it forwards, run it backwards

Here is a three-step program written as explicit forward/backward pairs. Watch the state go out and come back — the backward pass runs the inverse updates in reverse order:

type State = { x: number; y: number }; type Step = { name: string; fwd: (s: State) => void; bwd: (s: State) => void }; const program: Step[] = [ { name: "x += 7", fwd: (s) => { s.x += 7; }, bwd: (s) => { s.x -= 7; } }, { name: "y += x", fwd: (s) => { s.y += s.x; }, bwd: (s) => { s.y -= s.x; } }, { name: "x ^= y", fwd: (s) => { s.x ^= s.y; }, bwd: (s) => { s.x ^= s.y; } }, ]; const s: State = { x: 3, y: 10 }; console.log("start ", JSON.stringify(s)); for (const step of program) { step.fwd(s); console.log("after " + step.name + " ", JSON.stringify(s)); } console.log("--- inverse: reverse order, inverse ops ---"); for (const step of [...program].reverse()) { step.bwd(s); console.log("undid " + step.name + " ", JSON.stringify(s)); }

The final line is the starting state, bit for bit. Nothing was journalled, nothing was backed up — the current state alone was enough to walk home.

Socks and shoes: the whole program gets an inverse

That reverse-order rule is worth staring at. You put on socks, then shoes; to undo it you remove shoes, then socks. Formally, if a program is the composition P = S_n \circ \cdots \circ S_2 \circ S_1 of invertible steps, then

P^{-1} = S_1^{-1} \circ S_2^{-1} \circ \cdots \circ S_n^{-1}

— and each S_i^{-1} is obtained by a purely mechanical symbol swap (+= ↔ -=, ^= ↔ ^=). This is the payoff of the discipline: every reversible program comes with a derivable inverse, for free. You never write the "undo" code; the compiler can spell it out from the forward text. The next lessons exploit this relentlessly — a whole language (Janus) where calling a procedure backwards is one keyword, and a syntactic algorithm (program inversion) that flips any program in one pass.

A fun corollary: because swap and ^= are legal, the classic XOR-swap trick is a perfectly good reversible program — three invertible updates that exchange two variables with no temporary at all:

let a = 5, b = 9; console.log("before:", a, b); a ^= b; // a now holds a XOR b b ^= a; // b becomes the original a a ^= b; // a becomes the original b console.log("after: ", a, b); // run the same three steps again — each is its own inverse, // and in this symmetric case the sequence undoes itself: a ^= b; b ^= a; a ^= b; console.log("again: ", a, b);

The assertion idea: pay for your control flow

Updates are only half the story. Programs also branch and loop — and control flow forgets too, in a sneakier way. Think about a plain if: two different execution paths run through it and then join into one continuation. Standing just after the if, a conventional program has no idea which branch it took. That knowledge — one whole bit of it, per join — has been discarded. The same happens every time a condition-controlled loop exits: was the body run zero times or fifty? The join doesn't remember.

Running backwards, that lost bit is exactly what you need: arriving at a join from below, the inverse program must decide which branch to un-run. So reversible languages impose a matching discipline on control flow:

Wherever control paths merge (after an if, at a loop's entry), the program must supply an assertion — a condition that is true on one incoming path and false on the other.
Forwards, the assertion is checked; backwards, it is read — it tells the inverse execution which path to take.
An assertion at a join replaces the bit that a conventional program throws away: the program doesn't forget which way it came, it proves which way it came.

This is the deep symmetry of reversible programming: conditions (tested on the way in) and assertions (established on the way out) are mirror images, and backwards execution swaps their roles. In the next lesson we meet Janus, the canonical language built exactly on this idea — its if has an exit assertion, its loop has an entry assertion, and every procedure can be called in either direction.

Absolutely — that is what an undo stack, a database journal, and a time-travel debugger all do: before each destructive write, squirrel away the value being destroyed. It works, and later in this module we will see industrial tools built on precisely that trick. But notice the cost: the log grows with the length of the run, without bound, and the destructive steps still physically happened (with their Landauer cost, if you care about the physics). The reversible-programming discipline is the zero-log alternative: restructure the computation so there is nothing to squirrel away, because nothing is ever destroyed. The two approaches — journal the forgetting versus never forget — are the two poles this whole module moves between.