3.4 Revisiting the Forget operation

The forget operation is applicable for assignment statements whenever the substitution operation cannot be performed. This means that the following statement should use the ``forget'' operation:

This is because the RHS of the assignment does not refer to the LHS. There is no inverse function to reverse the new value of $x$ back to its previous value before the assignment statement.

As a result, you can use the substitution rule if and only if the following conditions are all true for an assignment statement $x \leftarrow e$ ($e$ is an expression):

• The RHS ($e$) refers to the LHS. If so, let us define $f(x)=e$
• There is an inverse function $f'(x)$ such that $f'(f(x))=x$

For all other assignment statements, the forget rule should be used. This include the following statement:

This is because even though the RHS refers to the LHS in this case, it is not reversible. Once variable $x$ becomes zero after this statement, there is no way to ``recover'' its previous value before the assignment statement.