# How Janus (Reversible Programming Language) if, while, and Update Work

In Reversible Computing, all program statements are reversible. I understand for example that the following:

\begin{align} x\ {+}&{=}\ 4\\ y\ {*}&{=}\ x\\ x\ {-}&{=}\ 10 \end{align}

Has the inverse:

\begin{align} x\ {+}&{=}\ 10\\ y\ {/}&{=}\ x\\ x\ {-}&{=}\ 4 \end{align}

However, I am not following the following if statement, while loop, and reversible update:

$$\texttt{if}\;e_1\;\texttt{then}\;s_1\;\texttt{else}\;s_2\;\texttt{fi}\;e_2$$

$$\texttt{from}\;e_1\;\texttt{do}\;s_1\;\texttt{loop}\;s_2\;\texttt{until}\;e_2$$

$$x \odot f(y)$$

I understand that for a statement to be reversible, the function has to be injective. So you can't have $f(x, y) \mapsto x$ because information is lost.

I don't understand how those if/loop/update functions can be reversible without storing some sort of information/state in the program's evaluation. For example:

x += 4


While that does have the inverse x -= 4, that is not inherent in the statement x += 4. For it to be reversible, it is almost like it would have to store state about it's previous value:

statement1 x = 1
statement2 x.values.push(x)
statement3 x.value = x.value + 4


Then you can do undo x and it would do something like:

x.value = x.values.pop()
x // 1


which is equivalent to:

x -= 4


So basically I'm wondering, how these "reversible" statements work. If they are saving state in some hidden way, or if it is reversible in some sort of tricky way. Maybe an example of stepping forward and backward through the program as it evaluates any of these expressions.

• Please ask a specific question and put it in the title. I think want you want to know is how ifand while constructs can be reversible in Janus or any other reversible programming language. In which case the answer seems to be, from glancing at the slides, that thesr constructs explicitly contain the case distinguishing postcondition, i.e. the condition needed on the reverse. Jul 2 '18 at 12:44