Adrian Prantl
TU Vienna

A reversible interpreter

A reversible interpreter for a reversible programming language

Janus is a programming language that was designed to support both forward and backward execution. So I decided that it would be an interesting project to design an interpreter for such a language that is itself reversible. By choosing Prolog as implementation language this was easily doable, although I have to acknowledge that only a subset of the language was implemented. The feature set includes recursion, arithmetic and un-calling of functions.

Implementation notes

Throughout the interpreter reversability is implemented using unification and (sometimes) backtracking. There are two implementations for basic blocks, depending on the direction of control flow. All other language elements are implemented with only one bidirectional predicate.

The syntax is recognized with a funny combination of infix operators. Check out the if-then-else-fi construct!

Arithmetic was implemented with constraints, as the is predicate does not support logical variables on the right-hand side..

The test-predicate starts from an initial state and executes the program yielding a new state. From the new state, the program is the un-computed yielding the final state. The sorted initial and final states are then compared,a s they should be identical.

Source code

The program was tested with SWI-Prolog. Download the file instead.


% A reversible interpreter for the JANUS reversible programming language
% (C) 2009 Adrian Prantl

:- use_module(library(clpfd)).
:- op(600, xfx, [ +=, -=, <=> ]).
:- op(804, fx, [call, uncall, if]).
:- op(803, yfx, [then]).
:- op(802, yfx, [else]).
:- op(801, yfx, [fi]).

ptrace(S0, P, S1, Dir) :- format('~w ~w ~w ~w ~w~n', [S0, Dir, P, Dir, S1]).

reval(S, _, [], S). % Speedup hack, reverse blocks
reval(S0, P, [Z|Zs], Sn) :-
  length(Sn, N), length(Sn_min1, N), % Skip useless backtracking
  eval(Sn_min1, P, Z, Sn),
  ptrace(Sn_min1, Z, Sn, '<--'),
  reval(S0, P, Zs, Sn_min1).
eval(S0, P, L, Sn) :- % This is the only special case for reverse execution
  is_list(L), \+ ground(S0), reverse(L, Lr), reval(S0, P, Lr, Sn).

eval(S0, _, [], Sn) :- permute(S0, Sn).
eval(S0, P, [Z|Zs], Sn) :-
  eval(S0, P, Z, S1), ptrace(S0, Z, S1, '-->'), eval(S1, P, Zs, Sn).

eval(S, _, procedure(_, _), S).

eval(S0, P, uncall F, Sn) :- eval(Sn, P, call F, S0).
eval(S0, P, call F, Sn) :- member(procedure(F, Body), P), eval(S0, P, Body, Sn).
eval(S0, P, if Cond then A else B fi Assert, Sn) :-
  freeze(Sn, eval1(Assert, Sn, Yes)), % Reduce useless backtracking
  eval1(Cond, S0, Yes),
  ( Yes = true -> eval(S0, P, A, Sn) ; eval(S0, P, B, Sn) ).
eval(S0, _, X <=> Y, Sn) :- % Swap
  select(X=Vx, S0, S1),
  select(Y=Vy, S1, S2),
  select(X=Vy, S3, S2),
  select(Y=Vx, Sn, S3).

eval(S0, _, Stmt, Sn) :-  % Expression Statements
  Stmt =.. [Op, X, Y],
  eval1(Y, S0, Vy),
  select(X=Vx,  S0, S1),
  select(X=Vx1, Sn, S1),
  eval1(Op, Vx1, Vx, Vy).

% Subexpressions
eval1(I, _, I) :- integer(I).
eval1(A, S, Va) :- atom(A), member(A=Va, S).
eval1(X=Y, S, true)  :- eval1(X, S, V),  eval1(Y, S, V).
eval1(X=Y, S, false) :- eval1(X, S, Vx), eval1(Y, S, Vy), Vx #\= Vy.
eval1((+=), R, X, Y) :- R #= X + Y.
eval1((-=), R, X, Y) :- R #= X - Y.

finalize(_=X) :- indomain(X).

test(S, P) :-
  sort(S, S0),
  eval(S0, P, P, S1),
  eval(S2, P, P, S1),
  maplist(finalize, S2),
  sort(S2, S0),
  format('~w ---> ~w ---> ~w ~n~n', [S0, P, S1]), !.

  test([x1=2,x2=0], [x1 += 3, x2 -= x1]),
  test([x1=2,x2=0], x1 <=> x2),
  test([x1=2], if x1=0 then x1+=42 else x1-=1 fi x1=42),
                  [if n=0 then [x1 += 1,
                                x2 += 1]
                  else [n -= 1,
                        call fib,
                        x1 += x2,
                        x1 <=> x2]
                  fi x1=x2]
        x1 += 5,
        x2 += 8,
        n -= 4,
        uncall fib

Complang Group
Adrian Prantl
   Reversible Computing
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2014-06-07 (Adrian)