CHAPTER 2 Formalizing Program Syntax

Concrete Syntax

程序定义来自程序语言，程序语言定义来自它的语法。语法描述了哪些短语是结构正确的。语义（semantics）表达了程序的意义（mean）。从concrete syntax，规定了哪些字符序列是可接受的。

举例算术运算，我们使用文法（grammar）来表述，给出 BNF，这部分理解，略过。

我们用得到的最重要的工具将会是inductive definitions，用来解释如何从小集合构造大集合。更一般的表示法，是一组 inference rules来定义一个集合。被定义的集合一般习惯为符合所有规则的最小集。举例，给出与上面算术运算 BNF 等价的inference rules定义。\(Exp\)表示所求集。水平线表示推理，之上为真，则之下为真。

Abstract Syntax

讲了 Concrete Syntax 后，放下它，本书剩余部分关注的是 abstract syntax，它是语言定义的真正核心。现在语言是 abstract syntax trees 抽象语法树，对应 Coq 中的 inductive type 定义或者 Haskell 中的 algebraic datatype 定义。这样的类型可通过用类型枚举它们的 constructor functions（构造函数）。

对应的构造函数，这些构造函数定义了\(Exp\)。

诀窍：将具体语法（方便写出）表示法在头脑中分解为抽象语法（方便理解）

注意，将 inductive type 每个构造函数对应一个子句？否则构造函数将不完整。同时注意终止条件（Coq 称为 primitive recursion 原初/初始递归）。

Structural Induction Principles

在本书中，我们不会过多地讨论自然数的证明，而是基于将自然数视为一个简单的归纳定义集，基于结构化归纳提出一个更一般，更强大的概念，这种归纳在形式上包含数学归纳（包含数学归纳！？）。

通过对集合的归纳定义，我们得到了一个证明集合中所有元素的某些谓词的归纳原理（归纳定义和归纳原理的相关性）。需要一种 proof obligation per rule。其实还是比较了解的，就是使用谓词的形式来表示定义。

• 结论用谓词表示
• 前提用谓词表示，并假定前提的 True，即 inductive hypothesis（归纳前提）。

理论，\(\forall e ∈ Exp, ⌈e⌉ ≤ |e|\)，用机器去证明。

这种极小化证明的确如作者所说吓到我了，作者认为定理的验证检查是一种适合机器而不是人的活动，省略一些血腥的细节，这些细节将在伴随的 Coqcode 中找到。

Decidable Theories

这个还蛮重要的，可判定理论。

（这个不太明白。。）

徐老师的解答

这段文字很简练，没有前因后果，所以费解，实际上，简单说，它的意思是：对于问题 f，如果存在一个程序（=机器），对于输入 f，这个程序是会运行停止的。那么，这个 f 就是可判定的，T 的意思是可判定问题的集合。所以，写成 f 属于 T

一些情况下，我们需要填充完整的证明细节，最常见的情况是证明目标符合 decidable theory。根据可计算理论，我们思考某种选择问题，在限制条件下能推断出什么。

Theories 的 Decidablity 判定非常简单（handy，张手就来）。只要我们的目标属于可判定理论的集合，我们就可以通过使判定程序

（机翻）注意半环理论的适用性与线性算术理论的适用性是不可比拟的。也就是说，有些目标是可以证明的，有些只能通过半环理论证明，有些只能通过林耳算法证明。

归纳到可判定问题，交给计算机

Simplification and Rewriting

• Simplification：“代入”已有的 theorem 来简化或者得到中间性质。

• Rewriting：“重写”成不同的表现形式（同样是利用已有的理论），来达到目标的样子（接近证明或者是想要得到其他形式的性质）。