这个表达式。一般而言，表达式的值在编译时难以确定，因此编译时的类型检查采取稳妥的 策略，从而可能拒绝了一些没有不良行为的程序。基本递归论的一个结论是：预测运行时类 型错误是程序的一个不可判定性质。 本书将集中在可静态确定类型的语言上，即每个程序短语必须有一个类型。除了极端情 况外，类型可以从其语法形式有效地确定。第3章讨论的语言的语法将由一组定型规则来定 义，而不是用上下文无关文法。每个良形(well formed)短语都有一个类型，一遍扫描可确 定短语的类型。其中没有局部声明的标识符的类型可以从某个符号表得到。 集中于静态类型化语言的原因是，把注意力集中到良类型的程序上，不必考虑有类型错 误的程序，因而不必考虑运行时的类型检查。只考虑良类型的程序可以使程序设计语言的理 论比较简单。考虑静态类型化语言的另一个理由是，它允许对表达式的值进行一定程度的推 理，这对无类型语言或运行时才能检查类型的语言是不可能的。 1.4归纳法 1.4.1表达式上的归纳 本书包含许多归纳证明。最常用的是基于表达式结构的归纳和基于证明的长度或结构的 归纳。本节介绍一些归纳法，对于大家己经熟悉的两种自然数归纳法，下面直接给出定义。 自然数归纳（形式1）为了证明对每个自然数n,P()为真，只要完成下面两步证明就 足够了。 (1)证明P(0)为真： (2)对任何自然数m,证明，若P(m)为真，则P(m+1)也为真。 自然数归纳（形式2）为了证明对每个自然数n,P()为真，只要完成下面的证明就足 够了： 对任何自然数m,若P()对所有的i<m都为真，则P(m)也为真。 只要有方法把每一棵树联系到一个自然数，就可以使用自然数归纳法来证明树的性质。 也可以为树和一些其他数学对象类阐述独立的归纳原理，最关键的问题是要能够为一类数学 对象安排一个适当的次序，使得每个对象可以从最小对象经过有限步的构造得到。直观上， 这类次序允许写出一种无限证明的形式，最终覆盖所关心的每一个对象。首先考虑表达式上 的归纳。 通常用文法来定义表达式集合，如： e::=01vle+ele*e 假定V是变量符号的无穷集合，该文法中的ⅴ表示V的任何元素都是一个表达式。由这个 文法产生的表达式都有一棵分析树，可以由对分析树的高度进行归纳来证明表达式的性质。 更精确地说，如果P是表达式的一种性质，那么可以定义自然数的一种性质Q如下： Q(m)≌t分析树t.如果height()=n并且t是e的分析树，那么P(e)为真。 注意，即使某些表达式的分析树多于一棵时，这也是一个合理的自然数性质。要想得到更加 清楚的证明方式，还是应该为表达式使用一种专门的归纳形式。下面使用自然数归纳证明的 本质步骤来解释这种形式的归纳证明。 假设要证明表达式上的性质P,并且像上面那样定义了自然数上的一个性质Q。如果使 用自然数归纳法来证明Vn.Qn),那么首先必须为高度是0的分析树直接证明P。然后在高 度至少为1的分析树中，假定对其各子树对应的表达式，P都成立。就上面所给的文法而言， 对于0,1和变量，必须直接证明P。对于形式为(e1+e2)和(e1*e2)的复合表达式， 可以假定P对子表达式e1和2都成立。由此分析可以得出基于表达式结构的归纳，其形式 >7 这个表达式。一般而言，表达式的值在编译时难以确定，因此编译时的类型检查采取稳妥的 策略，从而可能拒绝了一些没有不良行为的程序。基本递归论的一个结论是：预测运行时类 型错误是程序的一个不可判定性质。 本书将集中在可静态确定类型的语言上，即每个程序短语必须有一个类型。除了极端情 况外，类型可以从其语法形式有效地确定。第 3 章讨论的语言的语法将由一组定型规则来定 义，而不是用上下文无关文法。每个良形（well formed）短语都有一个类型，一遍扫描可确 定短语的类型。其中没有局部声明的标识符的类型可以从某个符号表得到。 集中于静态类型化语言的原因是，把注意力集中到良类型的程序上，不必考虑有类型错 误的程序，因而不必考虑运行时的类型检查。只考虑良类型的程序可以使程序设计语言的理 论比较简单。考虑静态类型化语言的另一个理由是，它允许对表达式的值进行一定程度的推 理，这对无类型语言或运行时才能检查类型的语言是不可能的。 1.4 归纳法 1.4.1 表达式上的归纳 本书包含许多归纳证明。最常用的是基于表达式结构的归纳和基于证明的长度或结构的 归纳。本节介绍一些归纳法，对于大家已经熟悉的两种自然数归纳法，下面直接给出定义。 自然数归纳（形式 1）为了证明对每个自然数 n，P(n)为真，只要完成下面两步证明就 足够了。 （1）证明 P(0)为真； （2）对任何自然数 m，证明，若 P(m)为真，则 P(m+1)也为真。 自然数归纳（形式 2）为了证明对每个自然数 n，P(n)为真，只要完成下面的证明就足 够了： 对任何自然数 m，若 P(i)对所有的 i < m 都为真，则 P(m)也为真。 只要有方法把每一棵树联系到一个自然数，就可以使用自然数归纳法来证明树的性质。 也可以为树和一些其他数学对象类阐述独立的归纳原理，最关键的问题是要能够为一类数学 对象安排一个适当的次序，使得每个对象可以从最小对象经过有限步的构造得到。直观上， 这类次序允许写出一种无限证明的形式，最终覆盖所关心的每一个对象。首先考虑表达式上 的归纳。 通常用文法来定义表达式集合，如： e ::= 0 | 1 | v | e + e | e ∗ e 假定 V 是变量符号的无穷集合，该文法中的 v 表示 V 的任何元素都是一个表达式。由这个 文法产生的表达式都有一棵分析树，可以由对分析树的高度进行归纳来证明表达式的性质。 更精确地说，如果 P 是表达式的一种性质，那么可以定义自然数的一种性质 Q 如下： Q(n)  ∀分析树 t.如果 height(t) = n 并且 t 是 e 的分析树，那么 P(e)为真。 注意，即使某些表达式的分析树多于一棵时，这也是一个合理的自然数性质。要想得到更加 清楚的证明方式，还是应该为表达式使用一种专门的归纳形式。下面使用自然数归纳证明的 本质步骤来解释这种形式的归纳证明。 假设要证明表达式上的性质 P，并且像上面那样定义了自然数上的一个性质 Q。如果使 用自然数归纳法来证明∀n.Q(n)，那么首先必须为高度是 0 的分析树直接证明 P。然后在高 度至少为 1 的分析树中，假定对其各子树对应的表达式，P 都成立。就上面所给的文法而言， 对于 0，1 和变量 v，必须直接证明 P。对于形式为（e1 + e2）和（e1 ∗ e2）的复合表达式， 可以假定 P 对子表达式 e1 和 e2 都成立。由此分析可以得出基于表达式结构的归纳，其形式