密尔纳-赖特语义（指称语义，Denotational Semantics）

指称语义是一种为编程语言赋予精确数学含义的形式化方法，其核心思想是把每一段程序（表达式、语句、整个程序）映射为一个抽象数学对象，通常是定义在特定数学结构上的函数，这个对象被称为该程序的指称。

概述

指称语义由克里斯托弗·斯特雷奇（Christopher Strachey）与达纳·斯科特（Dana Scott）在二十世纪六七十年代于牛津大学奠基。它区别于操作语义关注程序如何一步步执行，而是直接回答程序意味着什么。一个程序的含义由其组成部分的含义按固定规则组合得到，这一原则称为组合性。

核心原理

• 语义函数：用一族映射把语法结构送到语义域，常写作双方括号包裹的记号，表示取某语法对象的含义。
• 组合性：整体含义只依赖于各部分含义及组合方式，与部分内部的语法细节无关。
• 语义域：用来承载含义的数学空间，往往需要处理不终止与递归，因而引入了完全偏序集与连续函数。
• 不动点：递归定义的程序含义通过求解方程的最小不动点得到，这是斯科特的核心贡献。

应用场景

指称语义为编译器正确性证明、程序等价性判定、类型系统的模型构造提供了坚实基础。它在验证优化变换是否保持含义、设计领域专用语言的严格规范、以及抽象解释等静态分析理论中都有直接应用。函数式语言的理论研究尤其倚重这一框架。

常见问题

问：指称语义和操作语义有什么区别？答：操作语义描述程序如何执行，像一台抽象机器逐步推进；指称语义则忽略执行过程，直接给出程序对应的数学对象。两者可以互相验证，若一致则称语义是充分且完备的。

问：为什么需要完全偏序集这类结构？答：因为程序可能不终止，其含义要用一个表示未定义的底元素来表达，而递归需要求不动点，完全偏序集上的连续函数恰好保证最小不动点存在。