Types and Programming Language

这篇博客是Pierce, Benjamin C.在2002年出版的《Types and Programming Languages》的阅读笔记。

无类型系统

无类型数学表达式

书中首先给出一个语言的语法说明。语法说明的目标是给出“terms”集合$\mathcal{T}$的描述。文中采用了如下3种等价的描述:

  1. 归纳地描述:给出一系列类似“如果$t_1,\dots\in\mathcal{T}$,那么$\dots\in\mathcal{T}$”的规则,并且强调$\mathcal{T}$是满足这些规则中最小的。$t$之类的变量被称为元变量
  2. 推理规则:类似归纳,只是每个规则采用“一条横线,上方是若干前提,下方是结论”来描述,“最小的”这个要求通常隐含。没有前提的规则称为公理推理规则则是公理真规则(有至少一个前提)。公理有时候不需要横线。有些推理规则实际上是规则模式,因为它可能包含元变量,对应了一系列甚至无穷个具体规则
  3. 具体地描述:定义集合序列,并指出这一无穷集合的并就是$\mathcal{T}$

由上面的规则可以看出,对于一个term,它也肯定是推理规则中的某个给出。因而:

  1. 我们可以定义term上的函数,并按情况讨论递归地给出函数定义
  2. 我们可以按情况讨论term,进而归纳地给出其性质的证明

可以通过下面的3种方式定义语义:

  1. 操作语义:定义一个抽象的机器,并给出一个状态转移函数。机器从初始状态(可以是一个term),不断地进行状态转移(化简term),直至停机。有时可以给出一个语言的多个操作语义,从而便于理解或实现
  2. 指称语义:定义一个解释函数,从term映射到语义域(数学中的对象,如数或函数)
  3. 公理化语义:首先定义term的含义(而非先给出程序的行为)。相较更容易挖掘不变性

早期研究(70年代及之前)认为操作语义劣于其他。之后操作语义由于其简洁更受欢迎。本书主要使用操作语义。于是本书依照推理规则的形式给出了求值规则。注意:对于嵌套的term,必须从最外层开始求值(不应对内层嵌套term求值)。求值规则可以分为两类:

  • 计算规则:进行实际的计算
  • 一致性规则:决定那一子部分先计算

一个规则的实例是指将规则中的每个元变量一致地替换为某term的结果(包括结论和前提)。一个关系满足一个(求值)规则是指对于每个规则的实例,要么结论在关系中,要么存在一个前提不在关系中(这里的关系是指化简前后的两个term)。书最后定义了单步求值关系为满足所有求值规则的最小关系,记作$*\rightarrow *$。多步求值关系是单步求值关系的自反、传递闭包,记作$*\xrightarrow{*}*$。

将多个规则实例彼此组合在一起,形成树状结构,其中上方的叶子节点由公理实例组成,内部节点由真规则实例组成,这种结构被称为推导树

通过按推导归纳可以证明求值的诸多性质,如:

  • 确定性:如果$t\rightarrow t’,t\rightarrow t’’$,那么$t’=t’'$
  • 每个值都是标准形式:标准形式是指不存在$t\rightarrow t’$的$t$,一般语言会遵守这个
  • 标准形式都是值:不一定满足,这对于运行时错误很重要
  • 标准形式的唯一性:由确定性可得
  • 求值的终止性:复杂语言不一定满足。证明方法一般是找到一个状态上的函数,随着求值严格递减,且递减序列不可能无穷长

一个term如果是标准形式但不是值,则称为卡住,这时候程序来到了没有意义的状态 。

数学表达式的ML实现

简单类型

子类型

递归类型

多态

高阶系统

编辑本页

孙子平
孙子平
静态分析方向研究生