【Programming Languages And Lambda calculi】2.2 ~ 2.3 定义中的省略,证明树中的归纳

2.2 定义中的省略

要注意包含省略(或是星号)的定义,因为它们包含着隐含的递归。

例如,
在这里插入图片描述
在第二个要素中,任意数量的W都是被允许的。如下是更加精确的定义:
在这里插入图片描述
像这样扩展后,我们可以发现证明W实例的时,必须相互证明Y的归纳要素。在实践中,Y的归纳要素通常很明显以至于我们经常省略,并专注于原始定义的证明。

定理 2.3 每一个W都包含 α

证明

  • 基本要素:

    • 要素 α

      论证成立

  • 归纳要素:

    • 要素 (βW0W1 . . . Wn)

      每一个Wi 都包含 α ,每一个W都包含至少一个 Wi ,因此论证成立。

下述的定理也易证,并且不用重新扩展成互导形式。

定理 2.4 对于任意 W ,每一个 β 的前面都有一个圆括号

练习 2.2

证明定理 2.4

题解
  • 基本要素:

    • 要素 α

      要素中不存在 β

  • 归纳要素:

    • 要素 (βW0W1 . . . Wn)

      在 β 前有圆括号,且 W0 ~ Wn 中若存在 β ,β 前也有圆括号,因此论证仍然成立。

    证毕。

2.3 证明树中的归纳

下述的定义定义了集合
△ P \bigtriangleup P P
读作“P 为Δ”(P is pointy)
在这里插入图片描述
一如往常,集合 ΔP 被定义为满足上述规则的最小集合。第一条规则定义了一个基本要素,第二个规则则为自指。

另一种定义 ΔP 这样的方法类似于证明树:
在这里插入图片描述
注意到 ΔP 出现在线的上方,线的底部有 ΔP 的 Δ证明树。这棵 Δ证明树 代表第二条自指定义。

这两种定义集合的方式同时定义了两个集合: 表明 ΔP 的集合以及 Δ证明树 的集合。
这两个集合都只是被递归定义的简单符号模式。

下为Δ证明树的例子:
在这里插入图片描述
现在我们可以写出有关于 ΔP 以及 Δ证明树 的证明:

定理 2.5 : 如果 P集合为Δ, 则它的证明树中含有奇数个
△ s \bigtriangleup s s
这个论证的证明集合证明 P 集合一样,用结构归纳法:

  • 基本要素

    • 要素 Δα

      完整的树包含 Δα,一条线以及一个勾号,总共一个 Δα, 因此论证成立

  • 归纳要素

    • 要素 Δ(P1 O・ P2)

      完整的树包含 Δ(P1 O・ P2),加上 ΔP1 ΔP2 的树。在递归中,ΔP1 的树为 Δ(P1 O・ P2)树的子结构,其 Δs 的数量为奇数。 同样,ΔP2 的树 Δs 的数量为奇数。两个奇数相加得到偶数个 Δs。但是完整的 Δ(P1 O・ P2)树还要加上一个 Δs ,最终 Δs 的总数为奇数,论证仍然成立。

猜你喜欢

转载自blog.csdn.net/qq_35714301/article/details/113792312