随着SupGen的临近，我会发布一些技术内容，这些内容可能会无人问津，因为它们并非那种无脑AI内容，但我还是想这么做。 以下是一些关于整体性和终结性的思考。 在 Agda（以及 Lean？）中，终止是通过“结构递归”来保证的，这意味着论元可以按“字典序”递减。你明白这是什么意思吗？嗯，我一开始也不明白。但实际上它很简单。假设你有一个这样的子句： foo : Nat → Nat foo (S a) (S b) (S c) (S d) = foo (S a) (S b) c (S (S (S d))) foo x = x 它即将终止吗？还是不会？如何判断？ 在阿格达，情况是这样的： 步骤0： - 左侧论证 0：（S a） - 右侧论证 0：（S a） - 这完全一样，所以，请检查下一个参数。 （注：LHS/RHS 分别指等式左侧/右侧） 第一步： - 左侧论证 1：（S b） - 右侧论点 1：（S b） - 这完全一样，所以，请检查下一个参数。 步骤二： - 左侧论点 2：（S c） - 右侧论点 2：c - 这个条款*较小*，因此该条款终止！ 好了，我们完成了。 简而言之，每当右侧出现递归调用时，只需将其参数与左侧的相应模式逐一比较，直到其中一个更小为止。 很简单，不是吗？ （我希望他们能那样解释……） 现在，请思考： foo：Pair -> Pair foo(Pair(S a)(S b)) = foo(P a(S(S(S b)))) foo x = x 该函数是否即将终止？ 嗯，根据 Agda 的说法……不！然而，显然情况并非如此，逻辑相同：由于第一个组件较小，第二个组件较大也就无关紧要了。看来 Agda 的检查器被硬编码为对参数进行分块处理。因此，即使这段语句能够终止，它也无法通过检查器。 我为什么会提到这件事呢？ 所以，我在审查 SupGen 的递归生成器时，发现通过一些修改，它可以变得更简洁*并且*更快。但这些修改有效吗？我进行了测试，令我惊讶的是，根据 Agda 的说法，SupGen 生成的程序是无法终止的。起初我以为是我的方法错了，但事实证明，是 Agda 错了。 现在你掌握了新的知识。 我相信这最终会对你有所帮助！
SupGen 用于生成终止递归调用的新算法更简单*而且*更通用！
