编程中的归纳法与无类型算术表达式基础

### 编程中的归纳法与无类型算术表达式基础 #### 1. 归纳法原理 归纳法证明在编程语言理论以及大部分计算机科学领域中无处不在。许多证明都基于以下几个重要原理： - **自然数的普通归纳原理**：假设 $P$ 是关于自然数的谓词，如果 $P(0)$ 成立，并且对于所有的 $i$，$P(i)$ 能推出 $P(i + 1)$，那么 $P(n)$ 对于所有的自然数 $n$ 都成立。 - **自然数的完全归纳原理**：假设 $P$ 是关于自然数的谓词，如果对于每个自然数 $n$，在已知所有 $i < n$ 时 $P(i)$ 成立的情况下，能证明 $P(n)$ 成立，那么 $P(n)$ 对于所有的自然数 $n$ 都成立。 - **字典序归纳原理**：对于自然数对的字典序定义为：$(m, n) ≤ (m′, n′)$ 当且仅当 $m < m′$ 或者 $m = m′$ 且 $n ≤ n′$。假设 $P$ 是关于自然数对的谓词，如果对于每一对自然数 $(m, n)$，在已知所有 $(m′, n′) < (m, n)$ 时 $P(m′, n′)$ 成立的情况下，能证明 $P(m, n)$ 成立，那么 $P(m, n)$ 对于所有的自然数对 $(m, n)$ 都成立。字典序归纳原理是嵌套归纳证明的基础，并且可以推广到三元组、四元组等情况。 下面用表格总结这些归纳原理： | 归纳原理 | 条件 | 结论 | | --- | --- | --- | | 自然数的普通归纳原理 | $P(0)$ 成立，且 $\forall i, P(i) \Rightarrow P(i + 1)$ | $P(n)$ 对所有 $n$ 成立 | | 自然数的完全归纳原理 | $\forall n$，已知 $\forall i < n, P(i)$ 成立能推出 $P(n)$ | $P(n)$ 对所有 $n$ 成立 | | 字典序归纳原理 | $\forall (m, n)$，已知 $\forall (m′, n′) < (m, n), P(m′, n′)$ 成立能推出 $P(m, n)$ | $P(m, n)$ 对所有 $(m, n)$ 成立 | #### 2. 无类型算术表达式语言介绍 为了严谨地讨论类型系统及其性质，我们需要先处理编程语言的一些更基础的方面。这里介绍一种简单的包含数字和布尔值的语言，它虽然简单，但可以用来引入几个基本概念，如抽象语法、归纳定义和证明、求值以及运行时错误的建模。 该语言包含以下几种语法形式： - 布尔常量 `true` 和 `false` - 条件表达式 `if t then t else t` - 数字常量 `0` - 算术运算符 `succ`（后继）和 `pred`（前驱） - 测试操作 `iszero`，当应用于 `0` 时返回 `true`，应用于其他数字时返回 `false` 这些语法形式可以用以下语法规则来概括： ```plaintext t ::= terms: true constant true false constant false if t then t else t conditional 0 constant zero succ t successor pred t predecessor iszero t zero test ``` 在这个语法中，`t` 是一个元变量，它是占位符，代表某个特定的项，但它不是对象语言（我们正在描述其语法的简单编程语言）的变量，而是元语言（用于描述的符号）的变量。 以下是一些程序示例及其求值结果： - `if false then 0 else 1;` 求值结果为 `1` - `iszero (pred (succ 0));` 求值结果为 `true` 求值结果总是布尔常量或数字（对 `0` 进行零次或多次 `succ` 操作的嵌套应用），这样的项被称为值，它们在项的求值顺序的形式化中起着特殊的作用。 #### 3. 表达式语法的定义方式 该语言的语法有几种等价的定义方式： - **归纳定义**：项的集合 $T$ 是满足以下条件的最小集合： 1. $\{true, false, 0\} \subseteq T$ 2. 如果 $t_1 \in T$，那么 $\{succ t_1, pred t_1, iszero t_1\} \subseteq T$ 3. 如果 $t_1 \in T$，$t_2 \in T$，$t_3 \in T$，那么 `if t1 then t2 else t3` $\in T$ - **推理规则定义**：项的集合由以下规则定义： ```plaintext true ∈ T false ∈ T 0 ∈ T t1 ∈ T succ t1 ∈ T t1 ∈ T ```