如下： 结构归纳（形式1）为了证明对某个文法产生的任意表达式e,P()为真，只要完成下 面两步证明就足够了。 (1)对每个原子表达式e,证明P(e)为真： (2)对直接子表达式为e1,e4的任何复合表达式e,证明，如果P(e)(=l,k)都 为真，那么P(e)也为真。 对于上面所给文法，则有下面的模板： 目标：对每个表达式e,证明P(e)。 归纳基础：证明P(O)和P(1),并对任何变量v证明P(v)。 归纳步骤：证明，对任何表达式e1和e2,若P(e1)和P(e2)为真，则P(e1+e2)和P(e1*e2) 也为真。 还有另一种形式的结构归纳，它在归纳假设中包含了所有的子表达式，只不过这种区别 不像自然数归纳那样强调。 结构归纳（形式2）为了证明对某个文法产生的任意表达式e,P()为真，只要完成下 面的证明就足够了： 对任何表达式e,若P(e')对e的任何子表达式e'都成立，则P(e)也成立。 形式1和形式2的区别在于，形式2的归纳假设包含了所有的子表达式，并非只是直接 子表达式。 可以把自然数归纳的两种形式看成是结构归纳对应形式的特殊情况。请看文法 n:=0|succ n 直观上说，n的后继succ n是n+l。每个自然数都可以用该文法写出来，并且对于该文法， 表达式上的两种归纳形式正好对应到自然数上的两种归纳形式。 1.4.2证明上的归纳 基于证明结构的归纳和基于表达式结构的归纳本质上是一样的。在许多方面，两者都是 树上的归纳形式。在论述证明结构上的归纳之前，先回顾一般证明系统的一些公共的基本概 念。 希耳伯特风格的证明系统由公理和推理规则组成。证明系统的公理是一个公式，它被定 义成可证明的。推理规则用来表达：若某一组公式可证，则另一个公式也可证。证明是一个 结构化的对象，它由公式来构造，这些公式遵循由一组公理和推理规则确定的约束。下面将 完整地描述证明。 公理和推理规则通常写成模板，它们中的每一个都代表某种形式的所有公式或证明步 骤。例如，相等性的自反公理 e=e (ref) 叫做“带元变量e的模板”。这个公理模板断言，每个形式为e=e的等式是一个公理。例如， 只要x,y和3都是良形表达式，那么x=x,y=y和3=3都是公理。通常，推理规则模板 的形式是 A,…4 B 其含义是，如果公式A1,,An都可证，那么公式B也可证。把公式A1,…,An的证明合起来 就形成公式B的证明。例如，相等性的传递规则可以写成 e1=e2e2=e3 (trans) e1=e3 88 如下： 结构归纳（形式 1） 为了证明对某个文法产生的任意表达式 e，P(e)为真，只要完成下 面两步证明就足够了。 （1）对每个原子表达式 e，证明 P(e)为真； （2）对直接子表达式为 e1,…, ek的任何复合表达式 e，证明，如果 P(ei)（i=1,…, k）都 为真，那么 P(e) 也为真。 对于上面所给文法，则有下面的模板： 目标：对每个表达式 e，证明 P(e)。 归纳基础：证明 P(0)和 P(1)，并对任何变量 v 证明 P(v)。 归纳步骤：证明，对任何表达式 e1和 e2，若 P(e1)和 P(e2)为真，则 P(e1 + e2)和 P(e1 ∗ e2) 也为真。 还有另一种形式的结构归纳，它在归纳假设中包含了所有的子表达式，只不过这种区别 不像自然数归纳那样强调。 结构归纳（形式 2）为了证明对某个文法产生的任意表达式 e，P(e)为真，只要完成下 面的证明就足够了： 对任何表达式 e，若 P(e′)对 e 的任何子表达式 e′都成立，则 P(e)也成立。 形式 1 和形式 2 的区别在于，形式 2 的归纳假设包含了所有的子表达式，并非只是直接 子表达式。 可以把自然数归纳的两种形式看成是结构归纳对应形式的特殊情况。请看文法 n ::= 0 | succ n 直观上说，n 的后继 succ n 是 n +1。每个自然数都可以用该文法写出来，并且对于该文法， 表达式上的两种归纳形式正好对应到自然数上的两种归纳形式。 1.4.2 证明上的归纳 基于证明结构的归纳和基于表达式结构的归纳本质上是一样的。在许多方面，两者都是 树上的归纳形式。在论述证明结构上的归纳之前，先回顾一般证明系统的一些公共的基本概 念。 希耳伯特风格的证明系统由公理和推理规则组成。证明系统的公理是一个公式，它被定 义成可证明的。推理规则用来表达：若某一组公式可证，则另一个公式也可证。证明是一个 结构化的对象，它由公式来构造，这些公式遵循由一组公理和推理规则确定的约束。下面将 完整地描述证明。 公理和推理规则通常写成模板，它们中的每一个都代表某种形式的所有公式或证明步 骤。例如，相等性的自反公理 e = e (ref) 叫做“带元变量 e 的模板”。这个公理模板断言，每个形式为 e = e 的等式是一个公理。例如， 只要 x，y 和 3 都是良形表达式，那么 x = x，y = y 和 3 = 3 都是公理。通常，推理规则模板 的形式是 B A An ... 1 其含义是，如果公式 A1, …, An 都可证，那么公式 B 也可证。把公式 A1, …, An 的证明合起来 就形成公式 B 的证明。例如，相等性的传递规则可以写成 1 3 2 3 1 2 e e e e e e = = = (trans)