可变状态语义

纯 λ 演算中，变量可由值替换；一旦引入可变引用，同一个位置的内容会随时间改变，程序含义便依赖“现在的存储是什么”。最有效的图像是两层映射：变量名找到一个抽屉编号，存储记录每个抽屉此刻装什么。别名使两个不同表达式指向同一抽屉，因此局部赋值可能被远处代码观察到。闭包公理库程序语言闭包Programming-language closure · Function closure · Lexical closure将函数代码与其定义位置的词法环境配对而成的运行时函数值。捕获可变变量时也通常保存这个位置，而非复制某一时刻的内容。

程序 let r = ref 0 in r := 1; !r 先分配新位置 $\ell$ 并存入 $0$，赋值把存储更新为 $\sigma [\ell \mapsto 1]$，最后读取结果 $1$。若再令 s = r，则 s := 2 后 !r 也为 $2$，因为 r 与 s 是同一位置的别名。

边界是把赋值误作普通代换。表达式 f(r); !r 的结果取决于 f 是否能写入该位置，不能把 r 在源码中简单替换为初始值。垃圾回收通常不改变可观察语义，但若语言暴露地址、终结器或弱引用，就需要更细致的等价条件。

可变状态语义为命令式语言、对象、数组和函数共享可变位置提供基础。分离逻辑公理库分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。以堆的可分资源结构支持局部推理，所有权与借用公理库所有权与借用Ownership and borrowing · Ownership type system · Borrow checking以所有者、移动、共享或独占借用及生命周期约束静态组织资源责任与别名访问。则用静态 owner、loan 和生命周期限制别名访问；两者都建立在位置与存储之上，却不是运行配置本身。

在并发环境中，多个线程共享 $\sigma$ 会产生数据竞争公理库数据竞争Data race · 数据竞态不同线程对同一内存位置的冲突访问既未按模型同步排序、也未通过原子操作协调的情形。和原子性问题；事务、内存模型与并发对象语义都可看作对这套基本配置的扩展。证明有状态程序等价或表示独立时，有状态逻辑关系公理库逻辑关系Logical relation · Logical predicate · Reducibility relation按类型结构定义值与计算之间的关系，用于把局部类型规则提升为终止、等价或参数性结论。还需用 possible worlds 或 step index 记录两边堆单元的持续对应，而不能只比较当前返回值。