PFPL 笔记 - II Statics and Dynamics

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

Chapter 4 Statics ¶

Most programming languages exhibit a phase distinction between the static and dynamic phases of processing. The static phase consists of parsing and type checking to ensure that the program is well-formed; the dynamic phase consists of execution of well-formed programs. A language is said to be safe exactly when well-formed programs are well-behaved when executed.

一个语言如果是 safe 的，那说明 well-formed programs 在执行时是 well-behaved

书中介绍了一种语言 $\mathcal L \{\text{num str}\}$ 具有一些 statics：

这些推理都比较显然，略。

Lemma 4.1：Typing 的唯一性。对任何 typing context $\Gamma$ 和表达式 $e$ 只存在至多一个 $\tau$ s.t. $\Gamma \vdash e : \tau$

Lemma 4.2：类型反转。Suppose that $\Gamma \vdash e : \tau$ If e = plus(e1;e2) 我们可以退出 e1 : num 和 e2 : num。

Chapter 5 Dynamics ¶

TODO