变量赋值 | Codeboy's Blog

形式陈述

对$L$-结构 $\mathcal M$ ，变量赋值是函数 $s:\mathrm{Var}\to M$ 。项的值递归定义：

\llbracket x\rrbracket_{\mathcal M,s}=s(x),\qquad \llbracket f(t_1,\ldots,t_n)\rrbracket_{\mathcal M,s} =f^{\mathcal M}(\llbracket t_1\rrbracket_{\mathcal M,s},\ldots,\llbracket t_n\rrbracket_{\mathcal M,s}).

$s[x\mapsto a]$ 表示只把变量 $x$ 改赋为 $a$ 的赋值。项值只依赖其中实际出现的变量；闭项不依赖 $s$ 。

直觉

结构与赋值像两份用途不同的说明表。结构说明符号 $+$ 究竟是哪一个运算、常元 $0$ 指向哪个元素；赋值说明这次计算让变量 $x,y$ 分别取什么值。改动 $s(x)$ 不会顺便改变常元的解释，也不会改变加法规则。

赋值在形式上给所有变量取值，量词求值时再临时覆盖其中一个位置。对整个公式而言，只有自由出现可能受到初始赋值影响；这不等于“赋值函数只对自由变量有定义”。即使计算句子，递归过程仍会使用量词更新后的赋值。

例子与边界

在通常的整数结构中令 $s(x)=2,s(y)=3$ 。计算 $t=(x+y)\cdot x$ 时，先得到 $x+y=5$ ，再得到 $t=10$ 。若改为 $s[x\mapsto4]$ ，同一个项的值为 $(4+3)\cdot4=28$ ；改变一个未出现的变量 $z$ 则不会影响结果。

闭项如 $1+1$ 不需要读取变量表，但仍依赖结构。例如整数中的结果是 $2$ ，模 $2$ 的环中结果是 $0$ 。因此“不依赖赋值”不能误读为“不依赖解释”。

令 $s(x)=2,s(y)=5$ ，考虑

(x<y)\land\exists x\,(x=y+1).

左侧用原赋值得到 $2<5$ 。右侧寻找某个更新值 $a$ ，使 $s[x\mapsto a]$ 满足 $x=y+1$ ，可选 $a=6$ 。两个合取项因此都真；右侧的量词不会把左侧的 $x$ 也永久改成 $6$ 。

若把初始 $s(x)$ 改为 $7$ ，左侧变假，右侧仍真，整个合取变假。这个比较具体说明：同一个变量名可以在同一公式中既有自由出现，也有约束出现；量词按作用域覆盖取值。

赋值更新只是数学函数，不是原地修改共享程序状态。实现语义解释器时可以复制环境或临时保存并恢复旧值，但必须保证离开量词作用域后，其他子公式仍使用它们应有的环境。

推论与应用

满足关系通过赋值让开放公式获得精确语义，替换引理把赋值更新与语法代入对应；参数定义集和量词递归也依赖它。证明中常用 coincidence lemma：若两个赋值在公式的自由变量上相同，公式真值也相同。程序语义中的环境、λ 演算中的变量解释与约束求解同样复用这一概念。

参考资料

Open Logic Project contributors, The Open Logic Text, 2026-07-12 修订版，Satisfaction of a Formula in a Structure；Variable Assignments。
David Marker, Model Theory: An Introduction, Springer, 2002，§1.1，结构、项值与语义。