PFPL 笔记 - III Functional Types

Practical Foundations for Programming Languages 是 Robert Harper 的一本书，而这是我写的笔记 3

Chapter 8 Function Definations and Values ¶

这一章我们尝试往 $\mathcal L \{\text{num str}\}$ 中引入函数。

首先尝试引入 First order 函数。我们直接引入两个 expression call[f](e) 和 fun[t1;t2](x1.e2; f.e) 分别为 call 和 defination

容易发现这样的定义并没有什么必要，为了将函数排除到 type 之外引入了不必要的额外的替换工作。所以引入 Higher Order Functions （箭头）

type arr(t1, t2) 记为 $\tau_1 \to \tau_2$ 为函数类型

exp lam[\tau](x,e)计为 $\lambda(x:\tau)e$ 为 abstraction

新的语言记做 $\mathcal L \{\text{num str} \to\}$

Chapter 9 Godel’s T ¶

$\mathcal L \{\text{nat} \to\}$ 哥德尔的 System T 为函数引入了递归的可能性。这个递归非常类似于数学归纳法：所有递归都是有限的。

表达式 rec(e;e0;x.y.e1) 称为原始递归。

Godel’s T 和之前介绍的语言都必定停机。

Chapter 10 Plotkin’s PCF ¶

$\mathcal L \{\text{nat} \rightharpoonup \}$ 是 Plotkin’s PCF。引入了一个 fix 操作，允许函数无限制的自我递归。

Plotkin’s PCF 是图灵完备的。