“综合练习要求重算交换图的三元素闭包，提交唯一幂等图的两个严格自环，再加入两个方向不相接的严格规则，交出空图的原调用词和实际两步循环。另将严格边改成弱边，分别说明算法输出、具体程序事实及还缺哪…”
形式陈述
不要求任务个数每步减少
一个任务可能拆出多个子任务，所以任务数不是可靠的倒计时。本页把每个任务映到自然数大小，整个工作池表示为有限多重集，也叫bag。它忽略排列顺序，却保留出现次数：{3,3,1}含两份3，与{3,1}不同。记M(n)为n的次数，⊎按次数相加，减法仅在逐项可减时使用。
沿用良基下降证明终止的接口。定义新bag M′严格小于旧bag M，记M′≺ₘM，当且仅当可以写成
其中X非空，且
Z是原样保留的部分，X是删除的出现，Y是添加的出现。Y可以为空；同一份被删的大元素可以支配多个新元素，不要求从Y到X的单射。例如{2,2,2,2}≺ₘ{3}。这是Dershowitz–Manna多重集扩张在自然数通常顺序上的实例。[1, §II]
程序使用此序，需要每个真正继续执行的步骤都终止、产生有限个新任务，并使整个bag严格下降。未执行任何任务的无限空转不满足该条件。任务处理的异常、外部输入及并发等待若属于运行语义，也必须另外规定，不能仅证明“处理完以后下降”。本页只考虑每步选一份任务并完成有限替换的纯工作池。
一个可返回证书的判定器
取消两边相同的出现，令
在自然数全序下，判定恰好是
这是一份大删除可支配全部新增，不是每个删除都必须大于每个新增。等价地，找到出现次数不同的最大数d，检查M(d)>M′(d)；完全相同的bag不严格下降。
下载器先排序两份出现列表，再用双指针取消相同值。相等时两指针一起前进并记入Z；较小的一侧独自前进，记入该侧残余；最后附上未扫完的尾部。每轮已处理前缀恰分成公共出现与两边残余，未处理的相同值仍可能在后方相遇。算法返回Z、X、Y及最大差异，独立验证器重建两条bag等式并检查支配条件。
直觉
大任务消失，小任务可以增多
判断先看最大的重要差异。即使新增了很多大小2的任务，只要删掉一个大小3，且所有更大的任务未变，这次仍算进展。若最大的不同大小反而出现得更多，就不能用这个序作证。
因此“任务数下降”“所有任务大小之和下降”和“多重集下降”是不同条件。任务总和增加不反驳多重集证书；多重集证书也不会自动提供一个小的运行步数界。
例子与边界
从{3,1}实际执行到空池
规定规则：选到n>0，就删除它并添加n+1份n−1；选到0则直接删除。每次只替换被选任务，其他出现都保留。对n>0，所有新增大小n−1都小于n；对n=0，新增为空。因此任意合法选择都使bag下降。
从{3,1}开始，先处理3得到{2,2,2,2,1}。任务数从2增至5，大小总和从4增至9，却有证书Z={1}、X={3}、Y={2,2,2,2}。只盯任务数或总和会错过这一步进展。
附件分别执行“选最大任务，平局取较早ID”与“选最小任务，平局取较早ID”。每份新增任务都有新出现ID，两条轨迹均恰好44步清空工作池；最大任务优先的峰值为26份，最小任务优先的峰值为7份。终止证明不依赖这两个特定策略，但空间峰值确实依赖调度。
44可以独立复算。设处理单份n及其全部后代需要T(n)步，则
依次得到T(1)=3、T(2)=10、T(3)=41。两棵任务树互不共享，故总数T(3)+T(1)=44。这个递推是本例规则的额外信息；仅知道某个多重集序下降，并不能自动写出同一个递推。
重复值不能随手去重
旧bag {3,3,1}变成{3,2,2,1}，应取消一份3和一份1，留下X={3}、Y={2,2}，所以下降。如果先把输入变成set，两份3的信息就消失，已不是原来的任务池。
旧{2,1}变成新{2,1,0}时，公共部分就是旧bag，X为空，故不下降。尤其把错误规则1→{1,0}用于工作池，虽然每步都新添一个更小的0，却一直保留那份1；不断选择1会产生无限执行。“新增项里有更小的”并不是定义要求的删除与支配。
允许无限新增会破坏模型
规则3→无限多份2不是合法一步。每个新任务虽更小，但结果已不再是有限bag，单次替换也未必能完成。实数大小同样不能直接替代自然数：{1}、{1/2}、{1/3}、…构成无限严格下降链。
一般偏序上的多重集扩张仍有良基定理，但“取最大的残余元素”可能无定义；本页判定器只接受自然数。调用者不能把不可比较的资源向量随便编码成整数，再宣称保留了原来的支配关系。
推论与应用
最大差异判据为什么完整
若取消后的X非空且所有Y元素小于maxX，直接取这份Z、X、Y就是定义的见证，充分性成立。
反过来，假设原定义存在某份见证Z₀、X₀、Y₀。因为X₀有限且非空，令d=maxX₀。每个新增y都小于某个x≤d，所以所有Y₀元素严格小于d；因此d的出现数净减少，所有比d大的出现数都未变。取消公共项后，最大的差异仍是d且位于删除一侧，正是判定器的接受条件。
这个证明也解释了为什么不能把支配要求改成一对一配对。一个d可以提供任意有限多个更小元素的见证，仍保证最大差异在删除方向。
自然数bag的良基性
设存在从非空M₀开始的无限下降链。令K=maxM₀。每次只能以更小数替换被删数，故以后所有元素都不超过K。记录固定长度向量
最大差异判据说明每步都按从左到右的词典序严格下降。固定有限个自然数坐标的词典序良基：第一坐标只能下降有限次，随后稳定；从此第二坐标只能下降有限次，逐项下去后所有坐标都会稳定，与每步严格下降矛盾。空bag没有更小bag，也不可能开始无限链。
于是上述工作池每条合法执行都终止。这里K只用于证明，不需要实际分配K+1个计数槽；K再大，判定器仍仅处理出现列表。一般良基底序的原始证明使用有限分支树与König引理，本页给自然数情形的直接证明，适用边界明确。[1, §II]
判定成本与执行成本分别核算
旧、新bag分别有p、q份出现，比较排序后双指针线性扫描。按固定字长大小比较计，总时间O(1+(p+q)log(p+q+1))，附加空间O(p+q+1)，包括返回的完整证书。空输入也有常数入口工作。若大小为任意长整数，还要另计比较其位串的费用。
独立证书验证可用频数表重建两条等式，再计算maxX并扫描Y；在期望常数散列表访问模型下需O(p+q+1)。它核验给出的下降见证，不必重新排序。
附件为了教学，对每个工作池步骤都重新生成并核验完整bag证书，并可保存全部状态。若第t步前后共aₜ份出现，这些复查的时间为O(Σₜ[1+aₜlog(aₜ+1)])，轨迹空间O(1+Σₜaₜ)。这不是高性能任务调度器的成本；只执行已证明的替换规则可以省去逐步证书重算。步数预算耗尽会明确报告资源限制，不能当作非终止结论。
综合练习要求交44步的出现身份与两种峰值，再把一条替换改为1→{1,0}并定位第一份失败证书。大小变化终止分析转向另一种输入：跨调用参数之间的大小关系图，追踪能否接成无限下降线程。
参考资料
- Nachum Dershowitz、Zohar Manna，Proving Termination with Multiset Orderings，ICALP1979，LNCS71，pp.188–202；§II，印刷pp.189–191：多重集扩张、良基定理及全序排序判定。相同研究发表于CACM22(8)，pp.465–476。本文引用页码对应所链ICALP版本。
- Jayadev Misra，Multiset Ordering; A Theorem of Manna and Dershowitz，2014，pp.1–2：取消公共项后的定义及带出现身份的证明。工作池规则、44步和两个峰值为本文自己的可执行实例。