Types and Programming Language
这篇博客是Pierce, Benjamin C.在2002年出版的《Types and Programming Languages》的阅读笔记。
无类型系统
无类型数学表达式
书中首先给出一个语言的语法说明。语法说明的目标是给出“terms”集合$\mathcal{T}$的描述。文中采用了如下3种等价的描述：
- 归纳地描述：给出一系列类似“如果$t_1,\dots\in\mathcal{T}$，那么$\dots\in\mathcal{T}$”的规则，并且强调$\mathcal{T}$是满足这些规则中最小的。$t$之类的变量被称为元变量
- 推理规则：类似归纳，只是每个规则采用“一条横线，上方是若干前提，下方是结论”来描述,“最小的”这个要求通常隐含。没有前提的规则称为公理，推理规则则是公理和真规则（有至少一个前提）。公理有时候不需要横线。有些推理规则实际上是规则模式，因为它可能包含元变量，对应了一系列甚至无穷个具体规则
- 具体地描述：定义集合序列，并指出这一无穷集合的并就是$\mathcal{T}$
由上面的规则可以看出，对于一个term，它也肯定是推理规则中的某个给出。因而：
- 我们可以定义term上的函数，并按情况讨论递归地给出函数定义
- 我们可以按情况讨论term，进而归纳地给出其性质的证明
可以通过下面的3种方式定义语义：
- 操作语义：定义一个抽象的机器，并给出一个状态转移函数。机器从初始状态（可以是一个term），不断地进行状态转移（化简term），直至停机。有时可以给出一个语言的多个操作语义，从而便于理解或实现
- 指称语义：定义一个解释函数，从term映射到语义域（数学中的对象，如数或函数）
- 公理化语义：首先定义term的含义（而非先给出程序的行为）。相较更容易挖掘不变性
早期研究（70年代及之前）认为操作语义劣于其他。之后操作语义由于其简洁更受欢迎。本书主要使用操作语义。于是本书依照推理规则的形式给出了求值规则。注意：对于嵌套的term，必须从最外层开始求值（不应对内层嵌套term求值）。求值规则可以分为两类：
- 计算规则：进行实际的计算
- 一致性规则：决定那一子部分先计算
一个规则的实例是指将规则中的每个元变量一致地替换为某term的结果（包括结论和前提）。一个关系满足一个（求值）规则是指对于每个规则的实例，要么结论在关系中，要么存在一个前提不在关系中（这里的关系是指化简前后的两个term）。书最后定义了单步求值关系为满足所有求值规则的最小关系，记作$*\rightarrow *$。多步求值关系是单步求值关系的自反、传递闭包，记作$*\xrightarrow{*}*$。
将多个规则实例彼此组合在一起，形成树状结构，其中上方的叶子节点由公理实例组成，内部节点由真规则实例组成，这种结构被称为推导树。
通过按推导归纳可以证明求值的诸多性质，如：
- 确定性：如果$t\rightarrow t’,t\rightarrow t’’$，那么$t’=t’'$
- 每个值都是标准形式：标准形式是指不存在$t\rightarrow t’$的$t$，一般语言会遵守这个
- 标准形式都是值：不一定满足，这对于运行时错误很重要
- 标准形式的唯一性：由确定性可得
- 求值的终止性：复杂语言不一定满足。证明方法一般是找到一个状态上的函数，随着求值严格递减，且递减序列不可能无穷长
一个term如果是标准形式但不是值，则称为卡住，这时候程序来到了没有意义的状态 。
数学表达式的ML实现
简单类型
子类型
递归类型
多态
高阶系统
