Small-step 操作语义

Small-step Operational Semantics

1. 简介

程序所要表达的"意思"是什么? 当我们写程序的时候, 用不同种类的字符按照特定的顺序编成代码. 但是以某种特定语法(syntax)形式所构成的仅仅是程序自身而已, 并不能说明程序所包含的意义.

或许在程序执行的时候, 我们可以用解释器去定义一段程序的意思. 但是解释器或者编译器中不可避免地会有bug, 也就是说解释器或者编译器并不能准确地反映出程序的意义. 所以, 必须要找到能够表达程序意思的方法.

这个方法就是, 要给出语言语义的形式化的数学定义. 形式化的定义主要有如下几个好处:

• 较少歧义. 语言的行为的明晰的, 这对那些需要用该语言编程的人员是有用的, 为该语言实现一个编译器或者解释器, 或者为语言添加新的特性等等.
• 更加精确. 数学形式的概念和符号能够精确且准确地描述一种语言, 并且说明合法程序中的一些限制.
• 形式化论证. 形式化的语义允许我们说明和证明需求的程序性质.

但是, 形式化的语义可能导致复杂的数学模型, 尤其当尝试对一个具有复杂特性的编程语言的所有细节进行描述时. 现实世界中的编程语言很少有形式化的语义描述, 因为编程语言很复杂, 有很多的特性, 难度很大. 为了能够描述这些语言特性, 用于建模的数学公式或者符号必定非常复杂且难以理解. 那么, 就需要重新设计一套基于数学符号的能够精确对语言特性进行建模的形式化规范. 那么, 在学术和应用研究中通常使用三种方法对编程语言的语义进行形式化的描述:

• 操作语义(operational semantics): 描述程序在一个抽象机器上是如何执行的.

• 指称语义(denotational semantics): 讲程序建模为数学上的函数形式.

• 公理语义(axiomatic semantics): 以逻辑表达式的形式对满足程序执行前后的行为进行定义.

以上三种方法在不同的应用场景都有各自的优缺点. 感兴趣的读者可以阅读综述文章形式化方法概貌.

2. 简易语言的算术表达式

为了介绍操作语义, 先设计一个简单的语言, 基于该语言能够实现基本的算术运算. 使用下列域(domain)来描述该语言的结构:

\[ \begin{aligned} x,y,z &\in \mathbf{Var}\\ n,m &\in \mathbf{Int}\\ e &\in \mathbf{Exp} \end{aligned} \]

其中, \(\mathbf{Var}\) 是变量名的集合(例如, foo, bar). \(\mathbf{Int}\) 是整型常量的集合(例如, 42). \(\mathbf{Exp}\) 是表达式所在域, 这里我们使用 BNF 范式对表达式进行语法的定义:

\[ e::=x\ |\ n\ |\ e_1+e_2\ |\ e_1\times e_2\ |\ x:=e_1;e_2 \]

表达式 \(x:=e_1;e_2\) 说明变量 \(x\) 先赋值为 \(e_1\), 后被赋值为 \(e_2\), 范式中其他各项的含义不再做详细说明.

上述的语法为语言指定了格式. 但是存在歧义. 比如表达式 \(1+2\times 3\), 根据语法可以构造出两个不同的抽象语法树(abstract syntax tree).

有很多中方法解决存在的歧义问题. 其一, 重写语法规则, 这样会使得语法变得复杂, 且难以理解. 其二, 加括号.

\[ x\ |\ n\ |\ (e_1+e_2)\ |\ (e_1\times e_2)\ |\ x:=e_1;e_2 \]

然而, 这也导致了不必要的混乱和复杂. 相反, 我们把语言的"具体语法"(它规定了如何无歧义地将字符串解析为程序片段)与语言的"抽象语法"(它描述了程序片段的结构, 可能是有歧义的)分开. 后续阐述中, 将使用抽象语法, 并假定抽象语法树是已知的. 在编写表达式时, 我们偶尔会使用括号来表示抽象语法树的结构, 但小括号不是语言本身的一部分.

3. 小步操作语义

操作语义 operational semantics描述了程序是如何在抽象机器上执行的. 小步 small-step 操作语义细化了这种执行, 将其转变为表达式的连续规约(reduction), 直到得到一个数值(对应上文中的语言), 该数值表示计算的结果.

抽象机器(abstract machine)的状态通常称为配置 configuration(在程序逻辑的理论研究中, 经常会遇到这个单词), 那么对于本文所述的语言就肯定包含两条信息:

• store 也叫环境 environment 或者状态 state, store 所做的是将整型的数值赋给变量. 在程序的执行过程中, 通常使用 store 去决定与变量的数值大小, 同时也可以对 store 进行更新来反映有一个新的数值赋给了变量.
• 表达式左式的赋值.

这里的 store 与计算机系统中的 store 概念类似, 都有"存储"之意, 保存或者说明当前程序的状态. 文中涉及较多术语, 作者认为不作硬性翻译为好.

由此, stores 的域就是从 \(\mathbf{Var}\) 到 \(\mathbf{Int}\) 的函数形式(映射 map, \(\mathbf{Var}\to \mathbf{Int}\)), configuration 的域是 表达式和 stores 的二元组.

\[ \begin{aligned} \mathbf{Config}&=\mathbf{Exp}\times\mathbf{Store}\\ \mathbf{Store}&=\mathbf{Var}\to\mathbf{Int} \end{aligned} \]

在形式上, 使用一组方括号来表示 configurations. 例如, \(\langle(foo+2)\times(bar+1),\sigma\rangle\), 这里的 \(\sigma\) 就是一个 store, 前者是一个包含了两个变量的表达式.

本文语言的小步操作语义就是一种关系 \(\rightarrow \subset \mathbf{Config}\times\mathbf{Config}\), 该关系描述了一种配置是如何迁移(transition)到另一种配置的. 即, 关系 \(\rightarrow\) 说明了是如何一步一步地对程序的状态进行判定的. 我们用中缀的形式表示这种关系. 给定任意两个configurations \(\langle e_1,\sigma_1\rangle\) 与 \(\langle e_2,\sigma_2\rangle\), 如何二者存在关系 \(\rightarrow\), 则 \(\langle e_1,\sigma_1\rangle\rightarrow \langle e_2,\sigma_2\rangle\).

现在, 语言语义的定义就转变为对关系 \(\rightarrow\) 的定义, 该关系说明了抽象机配置之间的迁移.

这里存在一个问题, 整型域是无限的, 表达式的域也是无限的. 因此, 可能的抽象机配置也是一个未知数, 可能的每一步的迁移状态也是一个未知数. 所以, 我们要用有限的描述去表达迁移状态的无限集合.

我们可以使用推理规则来描述迁移函数:

\[ \begin{aligned} &{\rm VAR} \frac{}{\langle x,\sigma\rangle\rightarrow\langle n,\sigma\rangle}{\rm where}\ n=\sigma(x)\\ \\ &{\rm LADD} \frac{\langle e_1,\sigma\rangle\rightarrow\langle e_1^\prime,\sigma^\prime\rangle} {\langle e_1+e_2,\sigma\rangle\rightarrow\langle e_1^\prime+e_2,\sigma^\prime\rangle} \hspace{6mm} {\rm RADD} \frac{\langle e_2,\sigma\rangle\rightarrow\langle e_2^\prime,\sigma^\prime\rangle} {\langle n+e_2,\sigma\rangle\rightarrow\langle n+e_2^\prime,\sigma^\prime\rangle}\\ \\ &{\rm ADD} \frac{}{\langle n+m,\sigma\rangle\rightarrow\langle p,\sigma\rangle}{\rm where}\ p {\rm is\ the\ sum\ of\ }n\ {\rm and\ }m\\ \\ &{\rm LMUL} \frac{\langle e_1,\sigma\rangle\rightarrow\langle e_1^\prime,\sigma^\prime\rangle} {\langle e_1\times e_2,\sigma\rangle\rightarrow\langle e_1^\prime\times e_2,\sigma^\prime\rangle} \hspace{6mm} {\rm RMUL} \frac{\langle e_2,\sigma\rangle\rightarrow\langle e_2^\prime,\sigma^\prime\rangle} {\langle n\times e_2,\sigma\rangle\rightarrow\langle n\times e_2^\prime,\sigma^\prime\rangle}\\ \\ &{\rm MUL} \frac{}{\langle n\times m,\sigma\rangle\rightarrow\langle p,\sigma\rangle}{\rm where}\ p {\rm is\ the\ product\ of\ }n\ {\rm and\ }m\\ \\ &{\rm ASG1} \frac{\langle e_1,\sigma\rangle\rightarrow\langle e_1^\prime,\sigma^\prime\rangle} {\langle x:=e_1;e_2,\sigma\rangle\rightarrow\langle x:=e_1^\prime;e_2,\sigma^\prime\rangle} \hspace{6mm} {\rm ASG} \frac{} {\langle x:=n;e_2,\sigma\rangle\rightarrow\langle e_2,\sigma[x\mapsto n]\rangle} \end{aligned} \]

所谓推理规则, 直线上方公式和附加条件都成立的话, 直线下方的事实也是成立的. 线上称为前提, 线下称为结论. 没有前提的推理规则为公理, 有前提的即为推导规则.

同时, 我们使用标记 \(\sigma[x\mapsto n]\) 表示一个 store 将变量 \(x\) 映射(map)到 一个整型 \(n\). 更形式化和准确的表达是, 如果 \(f\) 是函数 \(\sigma[x\mapsto n]\), 那么有:

\[ \begin{equation} f(y)= \left\{ \begin{aligned} &n & {\rm if}\ y=x\\ &\sigma(y) & {\rm otherwise} \end{aligned} \right. \end{equation} \]

4. 应用语义规则

基于第3节的语义推理规则, 我们尝试判定表达式 \((foo+2)\times(bar+1)\) 的值, 其中 \(\sigma(foo)=4,\ \sigma(bar)=3\). 也就是说, 我们要为配置: \(\langle (foo+2)\times(bar+1),\sigma\rangle\) 找到状态迁移的推导树(derivation tree). 可以逐步的运用第3节的语义规则进行推理.

根据表达式的形式, 我们应用语义规则 LMUL 来进行推理, 其中 \(e_1=foo+2\), \(e_2=bar+1\), \(e_1^\prime\) 暂且未知.

\[ {\rm LMUL}\frac{\langle foo+2,\sigma\rangle\rightarrow\langle e_1^\prime,\sigma\rangle} {\langle (foo+2)\times(bar+1),\sigma\rangle\rightarrow\langle e_1^\prime\times(bar+1),\sigma\rangle} \]

接下来, 我们需要确定 \(e_1^\prime\) 的值. 从推理规则中找到符合 \(\langle foo+2,\sigma\rangle\rightarrow \langle e_1^\prime,\sigma\rangle\) 结论的形式. 那么, 接下就应用 LADD 规则.

\[ {\rm LADD} \frac{\langle foo,\sigma\rangle\rightarrow\langle e_1^{\prime\prime},\sigma\rangle} {\langle foo+2,\sigma\rangle\rightarrow\langle e_1^{\prime\prime}+2,\sigma\rangle} \]

其中, \(e_1^\prime = e_1^{\prime\prime} + 2\). 然后, 重复这个过程, 对 \(\langle foo,\sigma\rangle\rightarrow\langle e_1^{\prime\prime},\sigma\rangle\) 进行推理, 应用公理 VAR.

\[ {\rm VAR} \frac{}{\langle foo,\sigma\rangle\rightarrow\langle 4,\sigma\rangle} \]

因为有 \(\sigma(foo)=4\), 所以应用公理, 证明结束. \(e^{\prime\prime}=4\) 并且 \(e_1^\prime=4+2\). 由此, 可以构建推导树.

\[ \begin{aligned} &{\rm VAR} \frac{} {\langle foo,\sigma\rangle\rightarrow\langle 4,\sigma\rangle}\\ &{\rm LADD} \frac{} {\langle foo+2,\sigma\rangle\rightarrow\langle 4+2,\sigma\rangle}\\ &{\rm LMUL} \frac{} {\langle (foo+2)\times(bar+1),\sigma\rangle\rightarrow\langle (4+2)\times(bar+1),\sigma\rangle} \end{aligned} \]

基于语义规则, 上述推理证明了一步迁移: \(\langle (foo+2)\times(bar+1),\sigma\rangle\rightarrow\langle (4+2)\times(bar+1),\sigma\rangle\) 在抽象机上是可行的. 需要注意的是, 证明或者推导树必须是有穷的, 也就是在有限步的计算之后是有结果的, 而且结论是有效的. 接下去的推理步骤在此就省略了.

如果我们继续这个推理过程, 就能得到一个具体的计算结果.

\[ \begin{aligned} \langle (foo+2)\times(bar+1),\sigma\rangle&\longrightarrow\langle (4+2)\times(bar+1),\sigma\rangle\\ &\longrightarrow\langle 6\times(bar+1),\sigma\rangle\\ &\longrightarrow\langle 6\times(3+1),\sigma\rangle\\ &\longrightarrow\langle 6\times 4,\sigma\rangle\\ &\longrightarrow\langle 24,\sigma\rangle \end{aligned} \]

\(\langle 24,\sigma\rangle\) 就成为最终配置. 对于简易语言的表达式来说, 最终配置的形式就是 \(\langle n,\sigma\rangle\), \(n\) 是一个整数, \(\sigma\) 是 store.

那么, 关系 \(\rightarrow^*\) 是关系 \(\rightarrow\) 的自反传递闭包(reflexive transitive closure). 即, 如果 \(\langle e,\sigma\rangle\rightarrow^*\langle e^\prime,\sigma^\prime\rangle\), 那么经过 0 或者多次的推导(有限次), 最终能够得到从配置 \(\langle e,\sigma\rangle\) 到 \(\langle e^\prime,\sigma^\prime\rangle\) 的迁移. 这时候, 我们可以记

\[ \langle (foo+2)\times(bar+1),\sigma\rangle\longrightarrow^*\langle 24,\sigma\rangle. \]