Program Inversion

When you learned that Janus runs procedures backwards with a single keyword, you may have wondered what uncall actually does. Does it interpret the program in some exotic reversed mode? No — it does something far more satisfying: it rewrites the source code. There is a purely syntactic transformation, a handful of rewrite rules you can apply with a pencil, that turns any reversible program text P into the text of its inverse \mathcal{I}[P]. No execution, no search, no semantics needed — just pattern matching on syntax. This transformation is called program inversion, and it is this lesson's whole subject.

The inversion rules

Write \mathcal{I}[\,\cdot\,] for "the inverse of". The rules are applied recursively, from the outside in:

Program	Its inverse	Why
`x += e`	`x -= e`	subtraction undoes addition
`x -= e`	`x += e`	and vice versa
`x ^= e`	`x ^= e`	XOR is its own inverse
`x <=> y`	`x <=> y`	swapping twice is the identity
`A; B`	`ℐ[B]; ℐ[A]`	socks and shoes: undo the last thing first
`if c then A else B fi e`	`if e then ℐ[A] else ℐ[B] fi c`	condition and assertion swap roles
`from a do A loop B until c`	`from c do ℐ[A] loop ℐ[B] until a`	entry assertion and exit condition swap
`call p`	`uncall p`	by definition
`uncall p`	`call p`	inverting twice returns the original
`skip`	`skip`	doing nothing undoes itself

Two of these rows carry all the intellectual weight. The sequence rule reverses the order (you must undo the most recent step first). And the conditional rule is the assertion idea made mechanical: forwards, c chooses the branch and e records the choice; backwards, e chooses which branch to un-run and c becomes the thing to verify. The information flows through the join in one direction, and inversion turns it around.

Because every rule maps a legal statement to a legal statement, \mathcal{I}[P] is itself a well-formed reversible program — and applying the rules twice gives back exactly what you started with: \mathcal{I}[\mathcal{I}[P]] = P. Inversion is an involution on program texts.

Worked example, pencil first

Take this four-line program:

x += 5 y += x x <=> y x -= 2

Apply the sequence rule (reverse the lines), then the statement rules (flip each operator):

x += 2 <- inverse of x -= 2 x <=> y <- swap is self-inverse y -= x <- inverse of y += x x -= 5 <- inverse of x += 5

To verify an inversion, compose the two: running the original and then the candidate inverse must be the identity on every starting state. Let's make the machine do both the inverting and the checking. Below, a mini-language is represented as a data structure, invert() implements the rule table, and an interpreter traces the round trip:

type Stmt = | { op: "add"; x: string; e: string | number } | { op: "sub"; x: string; e: string | number } | { op: "xor"; x: string; e: string | number } | { op: "swap"; x: string; y: string }; type Env = { [name: string]: number }; function val(env: Env, e: string | number): number { return typeof e === "number" ? e : env[e]; } function show(st: Stmt): string { if (st.op === "swap") return st.x + " <=> " + st.y; const sym = { add: "+=", sub: "-=", xor: "^=" }[st.op]; return st.x + " " + sym + " " + st.e; } function run(prog: Stmt[], env: Env): void { for (const st of prog) { if (st.op === "add") env[st.x] += val(env, st.e); else if (st.op === "sub") env[st.x] -= val(env, st.e); else if (st.op === "xor") env[st.x] ^= val(env, st.e); else { const t = env[st.x]; env[st.x] = env[st.y]; env[st.y] = t; } console.log(" " + show(st) + " -> " + JSON.stringify(env)); } } // The rule table, as code: reverse the order, flip each statement. function invertStmt(st: Stmt): Stmt { if (st.op === "add") return { op: "sub", x: st.x, e: st.e }; if (st.op === "sub") return { op: "add", x: st.x, e: st.e }; return st; // xor and swap are self-inverse } function invert(prog: Stmt[]): Stmt[] { return [...prog].reverse().map(invertStmt); } const P: Stmt[] = [ { op: "add", x: "x", e: 5 }, { op: "add", x: "y", e: "x" }, { op: "swap", x: "x", y: "y" }, { op: "sub", x: "x", e: 2 }, ]; const env: Env = { x: 3, y: 4 }; console.log("start: " + JSON.stringify(env)); console.log("forward P:"); run(P, env); console.log("inverse I[P]:"); run(invert(P), env); console.log("round trip complete — compare with the start.");

The inverter is four lines long. That is the punchline of this whole module: in a reversible language, inversion is not a research problem, it is a compiler pass.

The classic slip is to invert each statement but forget to reverse the order: \mathcal{I}[A;B] \ne \mathcal{I}[A];\mathcal{I}[B]. Try it on x += 5; y += x: keeping the order gives x -= 5; y -= x, which subtracts the wrong x from y (the already-restored one). The correct inverse, y -= x; x -= 5, undoes the most recent effect first, while the state it depends on is still in place. Exactly the same as undressing: shoes off before socks. If your hand-derived inverse fails the round-trip test, an un-reversed sequence is the first thing to check.

Inverting the irreversible: why the general problem is hard

Everything above leaned on the program being reversible in the first place. What about inverting an arbitrary program — given code for f, produce code for something that maps each output back to an input? This is a famous, genuinely hard problem. The oldest answer is John McCarthy's 1956 observation, the generate-and-test inverter: to invert f, enumerate all possible inputs x and return the first with f(x) = y — a one-line universal solution that is correct, general, and catastrophically slow. Worse, when f is not injective the answer isn't even well-defined:

Contrast the two worlds. For a reversible program: inversion is syntactic, runs in time proportional to the length of the text, and yields a program exactly as fast as the original. For an irreversible program: inversion needs search over the input space, may find many answers or none, and in general is not computable at all. The whole discipline of reversible-language design is the price paid to stay in the first world.

Yes — it's a lively research area, precisely because it is hard. Grammar-based inverters can turn a printer into a parser; the logic-programming world gets partial inversion "for free" by running relations sideways (a Prolog append can split a list as happily as it joins one); and program-synthesis tools search for inverses with clever pruning rather than brute force. But every such technique hits the same wall sooner or later: where the forward program destroyed information, no amount of cleverness can conjure it back — the inverter must either search, guess, or give up. Reversible languages don't dodge that wall; they simply never build it, by refusing to destroy the information in the first place.