PFPL笔记

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

第一章 Syntactic Objects 句法对象 ¶

The structural, or abstract, syntax is concerned with the structure of phrases, specifically how they are composed from other phrases. At this level a phrase is a tree, called an abstract syntax tree, whose nodes are operators that combine several phrases to form another phrase.

structural or abstract, syntax 与短语的结构有关，特别是它们是如何由其他短语组成的。 在这个级别上，phrase 是一棵树，称为抽象语法树，其节点是将几个短语组合成另一个短语的运算符。

The binding structure of syntax is concerned with the introduction and use of identifiers: how they are declared, and how declared identifiers are to be used. At this level phrases are abstract binding trees, which enrich abstract syntax trees with the concepts of binding and scope.

语法的 binding 结构与标识符的引入和使用有关：如何声明它们，以及如何使用已声明的标识符。在这个级别上，短语是抽象绑定树，它用绑定和范围的概念丰富了抽象语法树。

AST ¶

for example,

2 + (3 * x)
plus(num[2];times(num[3];x))

考虑我们希望证明某个属性 properity $\mathcal P(a)$ 对所有给定类型的 ast $a$ 都成立，只需要考虑生成 $a$ 的所有方式，并证明该属性在每种情况下都成立

So, in the case of the sort Exp just described, we must show

1. The property holds for any variable, x, of sort Exp: P(x).
2. The property holds for any number, num[n]: for every $n \in \mathbb N, \mathcal P($ num[n] $)$
3. Assuming that the property holds for $a_1$ and $a_2$, show that it holds for plus($a_1; a_2$) and times($a_1; a_2$): if $\mathcal P(a_1)$ and $\mathcal P(a_2)$, then $\mathcal P($ plus($a_1; a_2$) $)$ and $\mathcal P($ times($a_1; a_2$) $)$

Abstract binding trees ABT ¶

抽象绑定树 abt 丰富了 ast，使其能够引入新的变量和参数，称为绑定，具有指定的重要范围，称为作用域。

Chapter 2 Inductive Definitions ¶

An inductive definition of a judgment form consists of a collection of rules of the form

$$\dfrac {J1 \quad...\quad J_k}{J}$$

in which $J1 \quad...\quad J_k$ and $J$ are all judgments of the form being defined.

for example

$$\dfrac {}{\text{zero nat}}$$

$$\dfrac {a\text{ nat}}{\text{succ}(a)\text{ nat}}$$

Modes ¶

We already know that Theorem 2.4. For every a nat and b nat, there exists a unique c nat such that sum(a;b;c)

对任意 a, b nat 存在 c 有 a + b = c

The statement that one or more arguments of a judgment is (perhaps uniquely) determined by its other arguments is called a mode specification for that judgment. For example, we have shown that every two natural numbers have a sum according to Rules (2.9). This fact may be restated as a mode specification by saying that the judgment sum(a; b; c) has mode (∀, ∀, ∃). The notation arises from the form of the proposition it expresses: for all a nat and for all b nat, there exists c nat such that sum(a; b; c).

If we wish to further specify that c is uniquely determined by a and b, we would say that the judgment sum(a; b; c) has mode (∀, ∀, ∃!), corresponding to the proposition for all a nat and for all b nat, there exists a unique c nat such that sum(a; b; c).

If we wish only to specify that the sum is unique, if it exists, then we would say that the addition judgment has mode (∀, ∀, ∃≤1), corresponding to the proposition for all a nat and for all b nat there exists at most one c nat such that sum(a; b; c).

A given judgment may satisfy several different mode specifications. For example, addition also has the mode (∀, ∃≤1, ∀), stating that the sum and the first addend uniquely determine the second addend, if there is any such addend at all. Put in other terms, this says that addition of natural numbers has a (partial) inverse, namely subtraction.

Chapter 3 Hypothetical and General Judgments ¶