Reversible programming language

A reversible programming language is designed to bridge the gap between the theoretical models of reversible computing and practical software development. They provide constructs that allow programmers to write code that is guaranteed, by the language's syntax and semantics, to be executable both forwards and backwards deterministically.

A reversible programming language is designed to bridge the gap between the theoretical models of reversible computing and practical software development. They provide constructs that allow programmers to write code that is guaranteed, by the language's syntax and semantics, to be executable both forwards and backwards deterministically. Reversible Updates: Standard assignment statements ( x = expression ) are inherently irreversible because they overwrite and erase the previous value of x. Reversible languages replace these with reversible updates, often denoted using operators like += , -= , ^= (bitwise XOR). An important restriction is that the variable being updated (e.g., x in x += e ) must not appear in the expression on the right-hand side (e) to ensure the operation is bijective. The swap operation ( x y ), which exchanges the values of two variables, is another fundamental reversible update. Reversible Control Flow: Conventional control flow structures like If-then-else and While loops merge computational paths, making them irreversible. Reversible languages introduce specialized constructs. Conditionals often require both a test condition (evaluated on entry) and an assertion (a predicate that must hold true on exit from one branch and false on exit from the other). Similarly, loops might require entry assertions and exit tests. These additional predicates store the necessary information to determine the execution path uniquely during backward execution, where the roles of tests and assertions are typically swapped. This explicit management of control flow information is a significant difference from conventional programming. Procedure Calls: Languages need mechanisms to invoke procedures both forwards and backwards. This is often achieved through paired commands like call (forward execution) and uncall or rcall (backward execution). Data Structures: Early reversible languages often restricted data types to simple ones like integers and fixed-size arrays. Handling dynamic data structures like stacks requires careful semantic design to maintain reversibility, such as assuming variables are zero-cleared before being pushed onto a stack, ensuring pop can perfectly reverse push . More recent research has explored reversible object-oriented features, including user-defined types, inheritance, and polymorphism. Computational Power: A common benchmark for the computational power of a reversible language is r-Turing completeness, which means the language can simulate any Reversible Turing Machine cleanly (without garbage accumulation). ===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 −1 or s2 −1 ) 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 −1 is executed, e1 is the test (loop continues if false, terminates if true), and s1 −1 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 . 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 ) 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 ) 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 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, 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 )

Text derived from https://en.wikipedia.org/w/index.php?oldid=1347938682 under CC BY-SA 4.0; modifications have been made.