如果操作语义讲的是程序一步一步怎样运行，那么指称语义更关心另一个问题：能否给每个程序找到一个数学对象，使程序的意义不再依赖某一次具体执行？这个想法听起来抽象，却让程序等价、递归和状态都进入了可以计算与证明的模型。
这五篇文章是一条进阶路线。它从类型化 Lambda 演算的模型条件出发，补充偏序、完备偏序与连续函数，再利用不动点解释递归。理解这些基础以后，后两篇分别建立 PCF 与命令式程序的模型，把前面的数学结构重新带回程序。
这组文章默认读者已经接触过 Lambda 演算、类型和基本程序语义。如果这些概念还不熟悉，可以先阅读“程序语言基础”导航中的前四篇。
五篇文章
01
Henkin 模型：程序项怎样获得数学意义？
从应用结构、外延性与框架出发，理解环境模型条件和可靠性。
02
偏序、完备偏序与连续函数
为递归定义准备数学结构，并理解函数空间本身如何构成 CPO。
03
不动点与全连续层级
把连续函数组织成类型层级，并说明不动点如何为递归提供指称。
04
为 PCF 建立 CPO 模型
借助阶乘等例子理解 PCF 的模型、多个不动点以及不动点归纳。
05
把存储带入模型：命令式程序的指称语义
从带存储的类型化 Lambda 演算出发，定义状态与命令的语义函数。
怎样选择阅读路线？
完整学习模型
按 01 → 05 阅读；第 02、03 篇是理解后续两个模型的关键桥梁。
重点理解递归
先补充第 02 篇的 CPO 与连续函数，再读第 03、04 篇的不动点内容。
关注命令式语义
在掌握第 02、03 篇后进入第 05 篇，观察存储如何改变语义函数的形态。
指称语义的抽象并不是为了离程序更远，而是为了找到一种足够稳定的语言，让不同实现、不同执行步骤背后的共同意义能够被讨论和证明。