Now we want to add the treatment of variables and the assignment statement to our interpreter. Adding variables poses a challenge because we need to be able to remember their values from one expression to the next. We can no longer evaluate expressions without concern for the evaluation environment, or context. In our case, the environment is simply a set of variables and their values. To correctly account for the assignment expression, a proposition must be proved in a context. And, the proof of the proposition may alter the context. Each context must also be propagated to premises of rules used to prove the proposition.
With this in mind, we introduce additional semantic specifications to handle variables and the assignment statement:
To evaluate the variable operator:
To evaluate the assign operator: