Janus: A Reversible Language

In 1982, two students at Caltech — Christopher Lutz and Howard Derby — designed a little programming language as a class project, wrote an interpreter for it, and moved on with their lives. The language could do something no mainstream language could: every program in it ran backwards as easily as forwards. Then it was essentially forgotten for twenty-five years, surviving as a letter Lutz wrote to the physicist Rolf Landauer. In 2007, researchers in Copenhagen (Tetsuo Yokoyama and Robert Glück) rediscovered it, gave it a formal semantics, and it became the fruit-fly of reversible programming — the canonical language every paper studies. Its name: Janus.

Janus takes the discipline from the previous lesson and makes it a complete language: reversible updates only, assertions at every join, and one killer feature — uncall, which runs any procedure backwards, for free.

The syntax tour

Janus has a very small surface. The statements you can write:

Updates: x += e, x -= e, x ^= e — with the rule you already know: x must not occur in e. There is no plain = in the language at all. Swap is written x <=> y.
Conditional: if c then A else B fi e. The c is the ordinary entry condition — but look at the end: fi e carries an exit assertion. The rule is exact: e must be true after the statement precisely when the then-branch ran (and false precisely when the else-branch ran). That one condition is what lets backwards execution pick the correct branch to un-run.
Loop: from a do A loop B until c. Mirror-image rules: the entry assertion a must be true when the loop is first entered and false on every re-entry; the exit condition c stops the loop. Run backwards, c plays the role of entry assertion and a the exit condition.
Procedures: call p runs procedure p forwards; uncall p runs its inverse. No inverse code is ever written by the programmer — the interpreter derives it from the forward text.

That's it. No garbage, no history tape, no hidden log: the state you can see is the whole state, and every statement is a bijection on it. A whole Janus program is therefore a bijection too — an injective function from initial stores to final stores.

Janus is the Roman god of doorways, transitions and time — always depicted with two faces, one looking forward and one looking back. He gave his name to January, the month that looks back at the old year and forward to the new. It is hard to imagine a more perfect patron for a language in which every program has two faces: run it forward and it computes f; run it backward and it computes f^{-1} — the same source text, read in two directions. (The 1982 authors chose the name themselves; some jokes are simply too good to pass up.)

Worked example: Fibonacci, both ways

The most famous Janus program computes a pair of consecutive Fibonacci numbers. Read it slowly — especially the last line of the procedure:

procedure fib(int x1, int x2, int n) if n = 0 then x1 += 1 x2 += 1 else n -= 1 call fib(x1, x2, n) x1 += x2 x1 <=> x2 fi x1 = x2 procedure main() int x1 int x2 int n n += 6 call fib(x1, x2, n)

Forwards, starting from x1 = x2 = 0: the base case (n = 0) bumps both to 1; the recursive case computes the previous pair, adds, and swaps, so (x1, x2) ends as consecutive Fibonacci numbers with n counted down to 0. Now the exit assertion fi x1 = x2: after the then-branch the pair is (1, 1) — equal; after the else-branch the pair is two consecutive Fibonacci numbers beyond (1,1) — never equal. True exactly when the then-branch ran: the assertion is correct.

And that assertion is what uncall fib reads. Running backwards from a pair (x_1, x_2), the inverse asks "is x_1 = x_2?" — if yes, un-run the then-branch (subtract the two += 1s); if no, un-run the else-branch (un-swap, un-add, recurse, restore n). The effect: uncall turns the Fibonacci pair back into n — it computes "which Fibonacci numbers are these?" without anyone writing that program.

Here is a faithful TypeScript emulation, with the assertions checked explicitly:

The round trip recovers n = 6 exactly. Notice what unfib is: line for line, it is fib read bottom-to-top with every statement inverted and the condition/assertion roles swapped. The next lesson turns that observation into an algorithm.

The loop, emulated

The from a do A loop B until c construct deserves its own trace. Here is a Janus-style loop summing 1 + 2 + \cdots + n, emulated with its assertion checks, then run backwards — the backward run recovers n from the sum:

Newcomers read fi x1 = x2 as documentation and write whatever feels plausible. It is not decoration — it is the one bit of information a conventional program throws away at the join, promoted to part of the program text. Get it wrong and the program is broken in both directions: forwards, a strict Janus interpreter checks the assertion after the branch and halts with a runtime error if it doesn't correctly separate the two paths; backwards, the inverse execution would take the wrong branch and un-run code that never ran, producing garbage (which the entry condition check then catches). A Janus if is only well-formed when c splits the states going in and e splits the states coming out — condition and assertion are a matched pair of one-bit records, one at each face of the statement.

What uncall buys you

uncall is more than a party trick — it halves your codebase. Encryption and decryption: one procedure. Compression and decompression: one procedure. Serialise and deserialise: one procedure. In each case, writing the forward direction is writing the backward one, and the two can never drift out of sync — there is no second implementation to harbour its own bugs. And because call p; uncall p is exactly the identity, Janus programs can use a powerful pattern: compute an intermediate result, use it, then uncompute it to leave the store clean — the language-level echo of the compute–copy–uncompute idea you met with Bennett's trick.