结构性归纳法

结构性归纳法是一种证明方法，用于数理逻辑（例如，在证明Łoś'定理）、计算机科学、图论和其他一些数学领域。它是对自然数的数学归纳法的概括，并可进一步概括为任意的诺特归纳法。

结构性递归是一种递归方法，它与结构性归纳的关系与普通递归与普通数学归纳的关系相同。结构性归纳法被用来证明某个命题P(x)对于某种递归定义的结构（如公式、列表或树）的所有x都成立。在结构上定义了一个有根有据的部分顺序（公式的子公式，列表的子列表，树的子树）。

结构归纳证明是证明该命题对所有最小结构都成立，如果该命题对某一结构S的直接子结构成立，那么它对S也一定成立。（从形式上讲，这就满足了基础良好的归纳公理的前提，该公理断言这两个条件足以使该命题对所有x都成立）。

结构递归函数使用同样的思路来定义递归函数：基例处理每个最小结构和递归规则。结构性递归通常通过结构性归纳来证明其正确性；在特别简单的情况下，归纳步骤往往被省略。

下面例子中的length和++函数是结构性递归的。例如，如果结构是列表，通常会引入部分排序<，其中只要列表L是列表M的尾部，L就<M。在这种排序下，空列表[]是xxx的最小元素。那么，某个命题P(L)的结构归纳证明由两部分组成。证明P([])是真的，以及证明如果P(L)对于某个列表L是真的，并且如果L是列表M的尾部，那么P(M)也一定是真的。

最终，根据函数或结构的构造方式，可能存在一个以上的基本情况和/或一个以上的归纳情况。

在这些情况下，某个命题P(l)的结构归纳证明包括证明P(BC)对每个基例BC都是真的，证明如果P(I)对某个实例I是真的，并且M可以通过应用任何一个递归规则一次从I得到，那么P(M)也一定是真的。

例子祖先树是一个众所周知的数据结构，显示一个人的父母、祖父母等（见图片为例）。它是递归定义的。在最简单的情况下，一棵祖先树只显示一个人（如果对他们的父母一无所知的话）；或者，一棵祖先树显示一个人，以及通过分支连接的他们父母的两个祖先子树（为了简化证明，使用简化假设，如果其中一个人是已知的，那么两个人都是）。

作为一个例子，通过结构归纳法可以证明以下属性：一棵延续g代的祖先树最多显示2g-1个人。在最简单的情况下，这棵树只显示了一个人，因此也显示了一代人；对于这样的树来说，该属性是真的，因为1≤21-1。

由于后者是整个树的一个子结构，所以可以假设它满足要证明的属性（又称归纳假设）。也就是说，可以假设p≤2g-1和q≤2h-1，其中g和h分别表示父亲和母亲的子树延伸的代数，p和q表示它们显示的人数。

在g≤h的情况下，整棵树延伸了1+h代，显示了p+q+1人，p+q+1≤（2g-1）+（2h-1）+1≤2h+2h-1=21+h-1，即整棵树满足21+h-1。

在h≤g的情况下，整个树延伸了1+g代，通过类似的推理，显示p+q+1≤21+g-1人，即在这种情况下整个树也满足该属性。

因此，通过结构归纳，每个祖先树都满足该属性。

作为另一个更正式的例子，考虑以下列表的属性。length(L++M)=lengthL+lengthM[EQ]。这里++表示列表连接操作，而L和M是列表。为了证明这一点，我们需要对长度和连接操作进行定义。

让(h:t)表示一个列表，其头部（xxx个元素）是h，其尾部（剩余元素的列表）是t，让[]表示空列表。长度和连接操作的定义是。length[]=0[LEN1]length(h:t)=1+lengtht[LEN2]。[]++list=list[APP1](h:t)++list=h:(t++list)[APP2]我们的命题P(l)是指当L为l时，EQ对所有列表M都是真的。

我们想证明P(l)对所有列表l都是真的。首先我们将证明P([])是真的；也就是说，当L恰好是L时，EQ对所有列表M都是真的。