Reversible programming language

Design philosophy

Janus embodies the principle of local invertibility. It operates on a global store of variables (no heap allocation or local procedure scope in early versions) and ensures that every statement has a unique inverse.

Syntax and semantics

• Program Structure: A Janus program consists of global variable declarations followed by procedure declarations. The execution starts at a procedure named main, or the last procedure defined if main is absent.
• Data Types: Janus primarily uses 32-bit integers (interpreters may differ on signed vs. unsigned) and one-dimensional integer arrays of fixed size. Some versions include stacks. All variables and array elements are initialized to zero.
• Statements:
  • Assignment: Reversible updates x op= e or x[e] op= e, where op is +, -, or ^ (bitwise XOR). The variable x must not appear in the expression e.
  • Swap: x <=> y exchanges the values of x and y.
  • Conditional: if e1 then s1 else s2 fi e2. The expression e1 is the test evaluated upon forward entry. The expression e2 is an assertion evaluated upon forward exit; it must be true if s1 was executed and false if s2 was executed. For backward execution (e.g., via uncall), e2 acts as the test to determine which inverse branch (s1⁻¹ or s2⁻¹) to take, and e1 becomes the assertion checked upon exiting backward.
  • Loop: from e1 do s1 loop s2 until e2. Upon forward entry, assertion e1 must be true. s1 is executed. Then, test e2 is evaluated. If true, the loop terminates. If false, s2 is executed, after which assertion e1 must now be false for the loop to continue back to s1. In reverse, e2 is the entry assertion, s2⁻¹ is executed, e1 is the test (loop continues if false, terminates if true), and s1⁻¹ is executed if the loop continues.
  • Stack Operations: push(x, stack) and pop(x, stack). Reversibility often relies on assumptions about the state of x (for example, x must be set to 0 after a call to push in order to be the perfect inverse of pop, which must restore x from 0 to the top value on the stack).
  • Local Variables: local t x = e1 in s delocal t x = e2 This block introduces a local variable x of type t, initializes it reversibly using e1 and executes s. After executing s the value of x must be equal to the value of e2. The delocal-part of the statement stores the final value of x directly in the code. By storing the final value of x, it can be restored on a backwards run of the code. This in effect allows for the deletion of x after it leaves the scope.
  • Procedure Call: call id executes procedure id forwards; uncall id executes procedure id backwards. Procedures operate via side effects on the global store.
  • Skip: skip does nothing and is its own inverse.
  • Sequence: s1; s2. The inverse is s2−1; s1−1.

Implementations and code examples

Several online interpreters for Janus exist. Janus has been used to implement various algorithms reversibly, including computing Fibonacci pairs and simulating RTMs, Fast Fourier Transform (FFT) and graph algorithms, and simulating the Schrödinger wave equation.

The following fibpair procedure in Janus calculates a pair of consecutive Fibonacci numbers. Given an input n, it sets x1 to F(n) and x2 to F(n+1), assuming x1 and x2 are initially 0:

int n x1 x2 // variable declarations

procedure fibpair
    if n=0 then
        x1 += 1
        x2 += 1
    else
        n -= 1
        call fibpair
        x1 += x2
        x1 <=> x2
    fi x1=x2

For calling and uncalling the Fibonacci-pair procedure we use

procedure main_fwd 
    n += 4
    call fibpair

prodecure main_bwd
    x1 += 5
    x2 += 8 
    uncall fibpair 

Syntax and semantics

• Program Structure: Programs are defined using (defmain ...) for the main routine and (defsub ...) for subroutines. Global variables and arrays are declared with (defword ...) and (defarray ...).
• Data Types: R primarily supports integers and integer arrays.
• Statements:
  • Assignment/Update: Includes increment (loc ++), negation (- loc), swap (loc <-> loc), and reversible updates (loc op= e) using operators like +=, -=, ^=, and specialized comparison-updates (<=<, >=>). Similar restrictions to Janus apply regarding variable dependencies.
  • Conditional: (if e then s*). To ensure reversibility, the language requires that the value of the conditional expression e must be the same before and after the execution of the then block (s*). This acts as an implicit invariant assertion, similar in function to Janus's explicit exit assertion.
  • Loop: (for name = e_start to e_end s*). Reversibility requires that the loop iteration variable (name) must have the same value before entering and after exiting the loop.
  • Local Binding: (let ((name <- e)) s*). Introduces a local variable name initialized with e. Reversibility is ensured by requiring the variable to be returned to a known state (e.g., zero-cleared) before the scope is exited, analogous to Janus's local/delocal.
  • Procedure Call: Explicit forward (call subname e*) and reverse (rcall subname e*) calls are provided.
  • Output: (printword e) and (println) are included for output. These are inherently irreversible operations.

Pendulum/PISA target architecture

The R language was designed with a specific hardware target: the Pendulum processor.

• Architecture: Pendulum is a 12-bit, RISC-inspired, fully reversible microprocessor implemented in 0.5 μm CMOS. It features general-purpose registers and fixed-length instructions.
• PISA Features: The instruction set includes several features tailored for reversibility:
  • A Direction Bit (DIR) register tracks forward/backward execution mode.
  • A Branch Bit (BR) register assists with reversible control flow.
  • Branch instructions (e.g., BEZ, BLTZ) are conditional and require careful pairing. Reverse branches (RBEZ, RBLTZ) also toggle the DIR bit.
  • Memory access uses a reversible EXCH (exchange) instruction that swaps register and memory contents.
  • Arithmetic and logic instructions (e.g., ADD, ANDX, XOR, SLLX, RL) are designed to be reversible, with some operations' behavior (like addition/subtraction or rotation direction) dependent on the DIR bit.

Code examples

The following PISA assembly code simulates a free-falling object. It includes a main section to call and "uncall" (reverse) a subroutine named Fall, which contains the core simulation logic.

Call Fall:
10: ADDI h 1000
11: ADDI tend 5
12: BRA 16       ; call

Uncall Fall:
18: ADDI v 40
19: ADDI t 4
20: ADDI tend 4
21: RBRA 7       ; uncall

Subroutine Fall:
27: BRA 9
28: SWAPBR rtn   ; br <=> rtn
29: NEG rtn      ; rtn=-rtn
30: BGTZ t 5     ; t > 0?
31: ADDI v 10    ; v += 10
32: ADDI h 5     ; h += 5
33: SUB h v      ; h -= v
34: ADDI t 1     ; t += 1
35: BNE t tend -5 ; t != tend?
36: BRA -9

The R program defines global variables for height (h), end time (tend), velocity (v), and current time (t). The core logic is encapsulated in the Fall subroutine, which simulates the object's motion. The main routine initializes parameters, calls Fall to simulate forward motion, then modifies parameters and calls Fall in reverse (rcall Fall), mirroring the structure of the PISA example's "Call Fall" and "Uncall Fall" sections.

A key feature of R's if statement is that the conditional expression must evaluate to the same truth value before and after the execution of its then block. The Fall subroutine in PISA (lines 30-36) effectively has a loop that runs as long as t is not equal to tend, but this loop is only entered if an initial condition (implied by BGTZ t 5 meaning skip if t > 0, so run if t <= 0) is met. To translate this faithfully and handle R's if semantics, the R code for Fall uses a let binding to capture the state of the initial condition (t <= 0) before the loop. The if then operates on this captured, unchanging boolean value. The loop itself is represented by R's for construct, iterating tend times, which corresponds to the PISA loop structure (BNE t tend -5).

;; Global variable declarations
(defword h)
(defword tend)
(defword v)
(defword t)

;; Subroutine to simulate falling
;; Corresponds to PISA "Subroutine Fall" (lines 27-36)
(defsub Fall ()
  ;; The PISA code at line 30 (BGTZ t 5) skips the main simulation
  ;; if t > 0. This means the simulation loop runs if t <= 0.
  ;; We use 'let' to capture this condition, and 'if' operates on the captured value.
  (let ((do_run <- (<= t 0))) ;; Capture condition: t must be <= 0 to run.
                             ;; 'do_run' is a local temporary.
    (if do_run ;; If the condition was true (t was <= 0 initially)
        then
          (progn ;; Execute the simulation loop
            ;; The PISA loop (lines 31-35) effectively iterates 'tend' times,
            ;; incrementing 't' each time, starting from its initial value (which is 0
            ;; when 'do_run' is true). The BNE t tend -5 continues as long as t != tend.
            ;; R's 'for' loop is a suitable high-level representation.
            ;; We assume 'tend' represents the number of iterations *from t=0*.
            (for i = 1 to tend ;; Loop 'tend' times
              (progn
                (+= v 10)      ;; PISA: ADDI v 10
                (+= h 5)       ;; PISA: ADDI h 5
                (-= h v)       ;; PISA: SUB h v
                (++ t)         ;; PISA: ADDI t 1
              )
            )
          )
        ;; else (if 'do_run' is false, meaning t was > 0 initially), do nothing,
        ;; mimicking the PISA BGTZ t 5 branch.
    )
    ;; Upon exiting 'let', 'do_run' is restored/cleared, satisfying R's rules
    ;; for 'let' and ensuring the 'if do_run' invariant holds for 'do_run'.
  )
)

;; Main program routine
(defmain ()
  ;; Initialize global variables to 0.
  ;; While PISA doesn't show explicit zeroing, R programs often start clean.
  ;; These are reversible assignments.
  (-= h h)         ;; h = 0
  (-= tend tend)   ;; tend = 0
  (-= v v)         ;; v = 0
  (-= t t)         ;; t = 0

  ;; --- "Call Fall" section from PISA ---
  ;; Set initial parameters for forward simulation
  (+= h 1000)     ; PISA: ADDI h 1000
  (+= tend 5)     ; PISA: ADDI tend 5
                  ; t and v are 0 from initialization.

  ;; Call the Fall subroutine to simulate forward motion
  ;; PISA: BRA 16 (relative branch to call setup, actual call is implicit)
  (call Fall)

  ;; State after (call Fall) with h_initial=1000, tend_initial=5, t_initial=0, v_initial=0:
  ;; Inside Fall: do_run = (<= 0 0) = true. Loop runs 5 times.
  ;; t becomes 0 + 5 = 5.
  ;; v becomes 0 + 5*10 = 50.
  ;; h becomes 1000 + 5*5 - (10+20+30+40+50) = 1000 + 25 - 150 = 875.
  ;; tend remains 5 (Fall does not modify the 'tend' global it uses for loop count).

  ;; (printword h) (printword v) (printword t) (printword tend) (println)
  ;; Expected: h=875, v=50, t=5, tend=5

  ;; --- "Uncall Fall" section from PISA ---
  ;; The PISA code modifies v, t, and tend before the reverse call.
  ;; Current state from R perspective: h=875, v=50, t=5, tend=5.
  (+= v 40)    ; PISA: ADDI v 40. v = 50 + 40 = 90
  (+= t 4)     ; PISA: ADDI t 4.  t = 5 + 4 = 9
  (+= tend 4)  ; PISA: ADDI tend 4. global 'tend' becomes 5 + 4 = 9
  ;; h remains 875.

  ;; Perform the reverse call to Fall
  ;; PISA: RBRA 7 (relative branch to uncall setup)
  (rcall Fall)

  ;; Behavior of (rcall Fall):
  ;; 'rcall Fall' executes the inverse of 'Fall'.
  ;; Inside 'Fall' (conceptually, during rcall):
  ;;   The (let ((do_run <- (<= t 0))) ...) block is reversed.
  ;;   The (<= t 0) condition is evaluated with current t=9. (<= 9 0) is false.
  ;;   So, 'do_run' (if we consider its "uncomputed" state) would correspond to 'false'.
  ;;   The 'if do_run' block's 'then' part (the loop) was not executed in the forward
  ;;   direction corresponding to this 'false' condition. Thus, its reverse also does nothing.
  ;; The net effect, matching PISA's BGTZ t 5, is that if t > 0, the main body of Fall
  ;; (and its reverse) is skipped.
  ;; Final state after (rcall Fall): h=875, v=90, t=9, tend=9.
  ;; This is because 'Fall' was effectively a no-op due to t=9 > 0.
  ;; The 'rcall' correctly reverses this no-op.

  ;; (printword h) (printword v) (printword t) (printword tend) (println)
  ;; Expected: h=875, v=90, t=9, tend=9
)