指称语义(denotational semantics):一种形式语义学方法,用数学对象(如函数、集合、域等)来刻画程序或表达式的意义,强调“一个表达式的意义是什么”(它所指称的数学值/函数),并通常遵循组合性原则(整体意义由部分意义组合而成)。常用于编程语言语义与逻辑/语言学中的形式化研究。
/dɪˌnoʊˈteɪʃənəl sɪˈmæntɪks/
Denotational semantics maps each expression to a mathematical meaning.
指称语义把每个表达式映射到一个数学意义。
In denotational semantics, the meaning of a program is often defined as a function from inputs to outputs, making equivalence proofs more systematic.
在指称语义中,程序的意义常被定义为从输入到输出的函数,从而让程序等价性的证明更系统化。
denotational 来自 denote(“指称、表示”),词根 note 与“标记、记号”相关;semantics 来自希腊语 sēmantikos(“与意义有关的”)。合起来表示“用指称(所对应的对象)来研究意义的语义学方法”。该术语在20世纪编程语言研究中尤其常见,用于与 operational semantics(操作语义)、axiomatic semantics(公理语义) 等方法相对照。