CHAPTER 4

Semantics for Arithmetic Expressions via Finite Maps

为了解释章节 2 中数学表达式的含义。我们需要一个表示每个变量值的方法。使用finite maps（有限映射），顾名思义，有限域，可通过\(m[k \mapsto v]\)进行拓展，注意得到还是一个 map。符合下面的基本公理

\[\dfrac{}{m[k \mapsto v](k) = v} \quad \dfrac{k_1 \ne k_2}{m[ k_1 \mapsto v](k_2) = m(k_2)}\]

有了上述工具在手，我们就可以写出算术表达式的语义了。

递归函数描述maps variable valuations to numbers。

\[ \begin{aligned} [n] v & = n \\ [x] v & = v(x) \\ [e_1 + e_2] v & = [e_1] v + [e_2] v \\ [e_1] \times [e_2] v & = [e_1] v \times [e_2] v \\ \end{aligned} \]

！！注意理解，括号内的 operation 是语法上的！括号外才是数学上的含义。

为了测试语义的正确性，定义一个 variable sustitution function 替换函数。