PL基础入门

PL基础入门

资源

• Stanford CS242 Programming Languages
• [POPL'22 Tutorial] Program Analysis via Graph Reachability: Past, Present, and Future

《类型和程序设计语言》

对照学习中文版《类型和程序设计语言》和英文版《Types and Programming Languages》

还记得最早学编程的时候，会去想函数是什么。而现在，脑海里自动出现什么调用栈，返回地址。也许类型系统是当初就应该学的。

第一部分 无类型系统

无类型系统是图灵完全的。当整个系统中只有函数的形式，一切都是函数的树的形式，信息也被存储在函数的树状结构中。

第三章 无类型算术表达式

本章讨论的是布尔和数的无类型演算。

• succ,pred,iszero共同组成了自然数相关的判断的基本元素。true,false,if-then-else，构成了bool类型和条件判断的基本元素。

相关概念：

• 元变量，有点类似语法中的非终结符，是一个可以用其他项代换的“变量”。
• 表达式，和项，这两个词现在可以替换使用。但是后面章节里，表达式的范围更大，因为除了包括语言中的表达式（项），还包括类型系统中的表达式等。
• 推导规则：写一个横线，上面写前提，下面写结论。没有前提的规则称为公理。我们这里的推导规则实际上是规则模式，因为前提和结论可以包含“元变量”，需要匹配出来，背后代表的是无限多个具体规则。
• 语法：定义一个集合，包含所有可能存在的项。书中用 归纳定义，推导规则定义，具体定义 三种方法定义了相同的集合。最后证明了这样定义出来的集合就是满足语法规则的最小集合。

最后书中证明了，这里定义的集合是满足这三个语法条件的最小的集合。此外，定义的过程中区分了常量出来。因此得到一个推论，每个项目要么是常量，要么形如succ t, pred t, iszero t 或 if t then t else t的形式。

项上归纳原理：可以以三种方式归纳证明一些关于项的定理：深度归纳、长度归纳、结构归纳。

形式化语义的三种方法：

• 操作语义：定义一个简单的抽象机器。抽象指将语言中的项作为状态。机器的行为由一个转换函数定义，要么转换要么声明机器已经停止。有时语义可以看作将t作为初始状态时达到的最后状态。这里描述的是小步语义。还有一种大步语义形式，有时称为自然语义。
• 指称语义：语义不只是机器状态，而且是某个数学对象。包括一个语义域的集合和将项映射到域中元素的解释函数。需要为语言特征寻找合适的语义域。有时候所选的语义域的性质可以推导出程序行为。由语义定义域的性质甚至可以得出在一个语言中有些事情是不可能发生的。
• 公理语义：公理方法用规则本身作为语言的定义，一个项的语义就是，从公理规则出发，我们能推导出的关于这个项的性质。

在1980年前后，操作语义逐渐成为主流。这本书也只用操作语义

语义和求值

布尔表达式的操作语义有如下几个部分：

• 语法部分
  • 项本身的语法
  • 值：它定义了项的一个子集，可以作为求值的最终结果
• 求值关系（也叫归约）
  • 如果抽象机器有某个状态，则此时可以按照该规则求值一步。

有三条求值关系，IfTrue，IfFalse和E-If。其中只有E-If有前提条件，且注意到求值关系->的定义的递归性：使用E-If规则时要求有前提t1 -> t2，而这里的箭头正是我们正在定义的求值关系，更精确地说是一步求值关系。

求值顺序：求值关系里可以蕴含求值顺序，比如书中仅允许if then else表达式对条件部分进行修改，并不允许先对then/else部分进行求值。

求值关系：一个项的pair可以说是一个关系，表示一个项可以推导为另外一个项。当我写下一个求值推导：t1 -> t2时，这里就蕴含了一个求值关系(t1,t2)。我们说，项的pair (t1,t2)在求值关系中。

规则被某个关系满足：规则有很多可能的实例（即将规则中的变量替换成具体的项）。如果一个关系符合/满足一条规则，对任何一个实例，则满足下面两个条件中至少一个：① 不符合前提：实例的前提不在关系中。②满足结论：实例的结论在关系中。

这里应该看反例，只有当两个条件都被违反的时候，我们才说一个关系不满足一条规则。实例的前提在关系中（违反第一条），实例的结论不在关系中（违反第二条）。就说明这个实例不符合这个规则。

一步求值关系->：一个最小的项上的二元关系，满足上面列出来的三个求值规则。当一个项\((t1,t2)\)的pair在求值关系里，我们称，求值推断 t1 -> t2 是可推导的。

求值树：可以把推导过程，按照横线上方是前提，下方是结论的方式写成一个倒着的树。由于只有E-If规则有前提，所以它是内部节点，另外两个规则是叶子节点。现在是细长的线，等后面有多前提的规则时它会更像树。

一步求值的确定性：如果t1 -> t2，且t1 -> t3，那么t2 == t3。表达的意思是：因为一步求值是确定的，则只会求出一个唯一的项。

对推理结构的归纳：这里用证明 一步求值的确定性 来解释这个证明方法。因为我们这里是关于推导关系的定理，我们看t1 -> t2的推导的根部。根部用的式子如果是IfTrue，那么t1必然是一个if-else的形式，而且前提条件为true。因为前提条件已经是true了，那么t1 -> t3的推导的根部不可能是If-False。因为前提条件true不能再进一步求值，那么t1 -> t3的推导的根部不可能是E-If。因为只剩下一个求值规则，那么t1 -> t3的推导的根部肯定也是相同的IfTrue，此时直接得到t2 == t3。

范式：如果一个项，不能再被求值规则继续求值，则这个项是范式。每个值（定义操作语义时，作为最终结果的项的集合）都是范式

书中中间还有一些别的内容：

• 习题中可以给语言扩充一个error项，这样总是可以继续求值，只不过最终可能求值到这个错误项，判断为错误。
• 本章介绍的表达式演算的具体实现。

第五章 无类型lambda演算

除了这种lambda演算之外，pi演算已经成为定义基于消息并发语言的语义核心语言。

函数（过程）抽象：借助参数命名表示某种一般的执行演算。在需要的时候实例化，提供参数的值。而lambda演算则用最可能纯的方式表示这种函数定义和应用。

lambda演算-项：①变量：x，②抽象：λx.t，③应用：t t

抽象语法和具体语法：注意表明写的语法和实际的语法树之间的差异。我们这里是以语法树为准。语法规则上，应用有左结合，函数抽象体尽可能向右拓展。

变量和元变量：真正在语言中，作为项的是变量。有时候为了抽象表示，用t表示所有语言中的项，此时是元变量。有时为了节约空间，定义简写s=λy.xy，这种也是元变量。

辖域，囿界：在λx.t中，λx是一个绑定器，辖域是t。t中出现的x是囿界的，被这个抽象所界定。而单独出现的则是自由变量。比如x在λy.xy中是自由的。

封闭项，组合子：一个不含自由变量的项是封闭项，也成为组合子。

操作语义：纯lambda演算的语义依赖于，将函数应用与参数的操作。表示为：(λx.t1) t2 -> [x -> t2] t1。这种方括号的形式表示代换。虽然只有一个操作，但也有不同的求值策略。

• 全beta规约（full beta-reduction）：任何时刻可以规约任何约式
• 规范（normal order）策略：最左边，最外面的约式第一个被规约。但是如果最外面的不能再规约，还是可以进一步规约抽象内部的。这个策略和下面的策略都能保证每个项单步归约是确定的。
• 按名（call by name）策略：不允许在抽象内部进行规约。
• 按值调用策略：只有最外面的能被规约，并且函数参数必须规约完毕为一个值。

lambda演算中的程序设计：labmda演算很强大，可以表示布尔类型，数值类型，以及相应的运算。注意我们描述的是编程语言的语义，这里不关心执行速度问题，关心的是编程语言的表达能力。谁能想到简单的纯lambda演算居然能做到这么多事情。后续拓展了原生的bool和数值类型后，也可以很方便地进行转换。但是，这个转换内遇到求值策略的时候有一些问题。但是，这种使用纯lambda的Church数值的系统，可以定义出和使用正常数值的运算系统的等价关系，即两边运算的结果是一样的，没有很明显的差别。

• 多参数：柯里化，即使用高阶函数，允许部分应用得到部分函数partial function。
• Church bool式：定义tru = λt. λf. t（两个参数选择前者）和fls = λt. λf. f（两个参数选择后者）。另外可以定义似乎没什么用处的test函数，以及逻辑运算函数，将逻辑运算转换为这种选择关系。
• 序对：pair = λf.λs.λb. b f s 参数依次是first second select。首先应用first和second，可以得到一个pair：λb. b f s，正好形成一个便于获取第一个还是第二个值的形式。这时候参数给一个tru或者fls就可以取第一个或者第二个了。但是，我们想要的是fst (pair v w)这种pair作为被应用的东西的形式。所以我们定义为fst = λp. p tru，转换一下。
• Church 数值 （丘奇数）：C0 = λs. λz. z参数分别是successor，zero，然后返回一个被应用了n次的zero项，表示做某件事情n次。设计一个scc函数、plus函数、求幂函数变得有些有挑战性。
  • Church数的减法比加法更困难：定义前驱函数就很困难。需要定义一个（n-1,n）的pair序列，用ss函数不断将序列推进。然后用数字自身的含义，即做某事情n次，应用在ss和(0,0)上，然后取n-1部分。

使用纯lambda演算的时候，如果有求值策略的限制，比如按值调用策略，那么就会导致有些操作无法化简，即使它可能和化简后的函数确实完全一样。完全一样的意思是，如果把没给完的参数都应用进去，无论参数是什么，两个函数得到的结果最终会一样。直观上会得到一团很复杂的函数，虽然代表一个很简单的东西，但是想要化简过去却很麻烦。

递归：发散组合式omega(λx. x x) (λx. x x)没有范式，能一直规约下去，因此称为发散的。想要编写递归，需要用到不动点组合式fix。递归编写的问题在于函数体，当你定义f = xxx的时候，xxx里面是不能用到f的，因为f还没被定义。首先，我们定义g = λf. xxx此时xxx里可以使用f，按照正常的递归函数的方式去定义。然后我们定义真正的f factorial = fix g即可。这种方法能工作的核心是，factorial n ->* (g factorial) n -> ([f -> factorial] xxx) n，这里就开始符合递归函数定义了，而且如果xxx里面化简时没有化简出带factorial的部分，则递归可以停止

形式化定义：形式化定义一个语言，复习之前的内容，包括定义语法上有哪些项，有哪些推导规则。

• 语法：定义V为变量名的集合。我们用递归定义项的集合。①单独变量名属于项。②如果t1属于项，x属于变量名集合中的合法变量名，则λx.t1也属于项 ③如果两个项的应用，也属于项。
• 自由变量集合：定义一个方便的函数FV(t)，表示t中的自由变量集合。比如单独的变量，没有被约束的变量。
• 推导规则-代换：直观的想法是把代换像乘法分配律一样深入到每个部分，然后如果最后只需要代换单个变量，是的话就代换。但是在变量命名上有一些问题。比如我们要代换x -> z：
  • ①如果发现要代换的值 x 突然有个界定 λx. t，此时就不应该继续进入代换了。
  • ②和上一个相反的错误：如果发现被代换进去的东西 z，本来是一个自由变量的，但是出现了一个λz. t，再代换里面的t，此时代换出来的z变成被lambda约束的变量了，这也不对。
  最后我们得到了避免捕捉的代换，遇到问题需要对变量z重新命名。我们称这种重新命名为alpha转化。
• 具体的操作语义：在定义求值关系上，细节决定了具体的求值顺序。根据写出来的规则不同，隐含着采用的是完全beta规约，规范序还是懒惰求值。

第九章 简单类型的lambda演算

注意到单独写一个项，如果不知道参数的类型，则有时也不知道函数体的类型。考虑参数类型被显式标注的语言，比如C语言。隐式标注的语言需要额外的类型推导算法，但并没有什么额外的不同。

类型上下文：我们用 \(\Gamma\) 表示类型上下文，即一系列类型的假设。然后用 \(\vdash\) 符号表示类型上下文的应用。 \(\Gamma \vdash t: T\) 的意思是，在类型上下文 \(\Gamma\) 中，项t的类型为T。假如有个函数λx.t2，当参数的类型是T1的时候，我们可以推导函数体的类型，把函数体中遇到的参数x假定为T1类型：

\[ \frac{\mathrm{x}: \mathrm{T}_1 \vdash \mathrm{t}_2: \mathrm{T}_2}{\vdash \lambda \mathrm{x}: \mathrm{T}_1 \cdot \mathrm{t}_2: \mathrm{T}_1 \rightarrow \mathrm{T}_2} \]

同时我们定义dom函数， \(dom(\Gamma)\) 表示被 \(\Gamma\) 界定的变量集合。

第十五章 子类型

子类型和其他孤立的语言特性很不一样，它对很多其他特性都有着影响。我们这里首先主要关注的是函数和结构体。

S是T的子类型记作S <: T。

约定子类型有自反性和传递性，即前序，preorder。往往子类型关系也会满足antisymmetry，即如果S <: T 且 S <: T 则 S == T，此时满足偏序关系，partial order。由于结构体有标签置换规则，即标签顺序不同的认作不同类型，但是是其他相同标签的子类型，所以我们这里讨论的不满足偏序。

安全代换原则：任何能用父类型的地方，也可以用子类型代换。子类型比父类型包含的信息量更多。

width subtyping：字段越多，越属于子类型。忘记字段时，相当于转为父类型。可以将一个结构体类型类型{x:Nat}理解为至少包含Nat类型的字段x的结构体类型集合。

Depth subtyping：允许结构体单个字段用子类型替换。

函数类型的子类型：子类型对参数的要求更低，即参数是原类型的父类型（逆变，contravariant），结果的要求更高，返回值是原来的子类型（协变，covariant）。

第十六章 子类型

算法子类型化

S-RCD将width/depth/perm结合的子类型定理：如下图所示。如果把字段看作集合，且把子类型关系看作相等，则结构体的子类型关系可以表示为集合的子集关系。

\[ \frac{\left\{1_i{ }^{i \in 1 . . n}\right\} \subseteq\left\{\mathrm{k}_j{ }^{j \in 1 . . m}\right\} \quad \mathrm{k}_j=1_i \text { implies } \mathrm{S}_j<: \mathrm{T}_i}{\left\{\mathrm{k}_j: \mathrm{S}_j{ }^{j \in 1 . . m}\right\}<:\left\{1_i: \mathrm{T}_i{ }^{i \in 1 . . n}\right\}} \]

根据这个可以得到判断两个类型是不是有子类型关系的算法：

subtype(S, T) = 
if T = Top, then true
    else if S = S1→S2 and T = T1→T2
        then subtype(T1, S1) ∧ subtype(S2, T2)
    else if S = {kj:Sj j∈1..m} and T = {li:Ti i∈1..n}
        then {li i∈1..n} ⊆ {kj j∈1..m}
            ∧ for all i there is some j ∈ 1..m with kj = li
                and subtype(Sj , Ti)
    else false.

子类型关系在实际应用中，会遇到不知在何处将类型变为子类型的情况。通过对推导树的观察可以发现，有一种改写方法可以把子类型化不断推迟到推导树末尾。这个过程中只有一种推导无法推迟，那就是函数的应用语句。我们更新应用规则，在应用时同步应用子类型关系。最终得到了推导包含子类型化语言的项的类型的算法。

《Advanced Topics in Types and Programming Languages》(ATTAPL)

第十章 基于约束的ML类型推导

这里有拓展版