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.

While that does have the inverse x -= 4, that is not inherent in the statement x += 4.

Invertibility means that every program A has an inverse B such that, if A terminates, A ; B terminates and does nothing. A = (x += 4) and B = (x -= 4) satisfy this criterion.

In pseudocode, if p then A else B fi q is equivalent to

if p
then
    A
    assert q
else
    B
    assert not q

(If an assertion fails, the whole program halts with an error.) Thus q is true after the loop if and only if p is true before the loop. This fact allows us to recover which branch was taken originally, when we enter the conditional backwards:

inverse (if p then A else B fi q) = if q then (inverse A) else (inverse B) fi p

The assertion becomes the test, and the test becomes the assertion.

Similarly, from p do A loop B until q is equivalent to

assert p
loop
    A
    if q
    then
        break
    B
    assert not p

When entering the loop backwards (through the break statement, which is the only place we could have exited the loop), we first invert A. Now p holds if and only if we entered the loop at this point (due to the assert before the loop and the assert at the end of the loop body). Thus if p holds, we exit. Otherwise, we invert B and repeat the process. Therefore, the inverse is

inverse (from p do A loop B until q) = from q do (inverse A) loop (inverse B) until p

References:

-
Janus: a reversible programming language (1986)

-
A reversible programming language and its invertible self-interpreter (2007)

-
Reversible flowchart languages and the structured reversible program theorem (2008)

-
Partial evaluation of the reversible language janus (2011)

StackExchange Computer Science Q#93736, answer score: 2