I am having difficulty understanding the meaning of these arithmetic rules in operational semantics. Hoping for a brief explanation of their meaning. The expressions are from here:
Arithmetic reductions:
$$\frac{}{\langle n_1 \oplus n_2, \sigma \rangle \longrightarrow_a n_3}\ (where\ n_3 = n_1 \oplus n_2)$$
Arithmetic subexpressions:
$$\frac{\langle a_1, \sigma \rangle \longrightarrow_a a_1'}{\langle a_1 \oplus a_2, \sigma \rangle \longrightarrow_a a_1' \oplus a_2} \quad \frac{\langle a_2, \sigma \rangle \longrightarrow_a a_2'}{\langle n_1 \oplus a_2, \sigma \rangle \longrightarrow_a n_1' \oplus a_2'}$$
One subtle point: in the rule for arithmetic operations $\oplus$, the $\oplus$ appearing in the expression a1 $\oplus$ a2 represents the operation symbol in the IMP language, which is a syntactic object; whereas the $\oplus$ appearing in the expression $n_1 \oplus n_2$ represents the actual operation in Z, which is a semantic object. In this case, at the risk of confusion, we have used the same metanotation $\oplus$ for both of them.
(1) Just to make sure I'm following, the first one defines addition as an axiom. Though it is interesting that the $where$ clause exists which says already what the rule says. I don't understand why that is necessary (e.g. duplication).
(2) I'm not sure why the second ones are called "subexpressions". It seems because they use the addition axiom in their conclusion, not sure if that's why.
(3) Not sure what the conclusions mean in the last two, or why they are necessary to be specified.
$$\frac{...}{\langle a_1 \oplus a_2, \sigma \rangle \longrightarrow_a a_1' \oplus a_2} \quad \frac{...}{\langle n_1 \oplus a_2, \sigma \rangle \longrightarrow_a n_1' \oplus a_2'}$$
The first one seems to say (in the premise) that "if $a_1$ evaluates to $a_1'$", then (conclusion), doing addition in state $\sigma$ will be rewritten do doing addition with $a_1'$. That pretty much makes sense, but I'm not sure why that needs to be stated.
(4) In the last one, they say $\langle n_1 \oplus a_2, \sigma \rangle$, using $n$, a literal number instead of an expression $a$. I'm not sure why this is being done.
Hoping to better understand these 4 points. Thank you so much for your help.
(1) Without the where clause, there would be no relation between $n_1$, $n_2$ and $n_3$. The where clause appeals to the meta level operation of $\oplus$ instead of the syntax level one, which is mentioned in the cited text.
To explain in more detail, say we were going to interpret the operation $\oplus$ as denoting the usual arithmetic $+$. In this case, we would write the rule as $$\frac{}{\langle n_1 \oplus n_2, \sigma \rangle \longrightarrow_a n_3}\ (where\ n_3 = n_1 + n_2)$$
(2) I can't speak to the naming conventions of the authors, but I would hazard a guess that it is due to the fact the rules are about the evaluation of the left and right subexpressions.
(3) These rules need to be stated, because the system is a small step operational semantics. To explain this in more detail, small step operational semantics concerns itself with the smallest increment of computation you could make. Each rule represents one such step.
What is happening here is that $a_1$ and $a_2$ are expressions that can be evaluated, whereas $n_1$ and $n_2$ are literal numbers. So, what the rules say is that
If you have two literal numbers combined with an $\oplus$ you can take a computation step by actually doing the operation.
If you have an expression on the left of $\oplus$, and a way to compute a little bit on it ($\langle a_1, \sigma \rangle \to a'_1$), then you can compute a little bit on $a_1 \oplus a_2$.
If you have literal number on the left of the $\oplus$, but an expression on the right, and a way to compute a little bit on that expression, you can compute a little on $n_1 \oplus a_2$.
(4) Hopefully I addressed this in the last response.