“综合练习要求交44步的出现身份与两种峰值，再把一条替换改为1→{1,0}并定位第一份失败证书。大小变化终止分析转向另一种输入：跨调用参数之间的大小关系图，追踪能否接成无限下降线程。”
形式陈述
输入图必须对每次实际调用成立
大小变化分析追踪“下一次调用的某个参数不大于或小于这次的哪个参数”。它使用自然数不能无限严格下降，但不要求下降总发生在同一个参数位置。[1]
本页固定有限个过程名，每个f有a_f个自然数参数。状态是(f,v₁,…,vₐ)。一步选择一条满足guard的调用规则，经过有限、正常结束的计算后转到下一状态；没有可用规则时正常返回。所有可能选择都属于待证明的运行。这个模型不含隐藏的内部无限循环、阻塞I/O或公平调度假设。
每条可能调用f→g都给一张a_f×a_g的大小图。源参数i到目标参数j的标签只有三种：
- 0：不知道两者的大小关系，不代表它们不相等
- W：目标参数不大于源参数，即vᵢ≥v′ⱼ
- S：目标参数严格小于源参数，即vᵢ>v′ⱼ
W不是“相等”。给图的人必须证明每条边在该调用guard成立时可靠。少写一条真实边可能使分析失败，多写一条不成立的S边则可能错误证明终止。下载器检查图的维数和标签，并不能自动验证任意源程序的算术。
本页从任意过程的任意合法自然数状态讨论终止，所以把所有给出的调用图都纳入分析。若只关心一个入口，可先可靠地排除不可达过程；仅从某次测试没走到一条分支，不能把它删掉。
连续调用怎样合成
对G:f→g和H:g→h，合成G;H:f→h。对每对源i、终点k，枚举g的中间参数j：两段都存在才构成路径；任意一段为S则该路径为S，两段均为W则为W。存在S路径就保留S，否则有W路径便保留W，全无则记0。[2, Definition5.1]
例如vᵢ≥v′ⱼ且v′ⱼ>v″ₖ，推出vᵢ>v″ₖ。合成中的严格边因而仍可靠。多次合成描述参数路径：只要路径上至少有一次严格下降，整体就严格下降。这一含义也证明合成结合律；改变括号不改变可连接的路径和是否出现S。
闭包C包含所有非空可连接调用词的合成图。它不是反射闭包，不能无条件加入表示零次调用的恒等图；否则连无递归程序也会凭空多出一个没有严格下降的“循环”。
有限幂等判据
一张自返图G:f→f若满足G;G=G，称为幂等图。判据是：
C中每一张幂等自返图，都有至少一条i→i的S边。
判据恰好等价于以下图性质：任何无限的可连接调用图序列，其分层参数图中都存在一条线程，从某层开始每次沿边走到下一层，并经过无限多个S。线程可在参数位置间移动，不要求每一层都有S。
在可靠图和自然数参数的前提下，这个图性质推出程序终止。若判据失败，只说明这些摘要没有建立该性质；失败图的重复调用词未必能由具体程序的guard实现。
直觉
下降可能换到另一个参数上
考虑
text
f(x,y):
if x == 0: return y
else: tail-call f(y,x-1)x>0的guard保证x−1仍是自然数。下一次的第一个参数等于旧y，第二个参数严格小于旧x，因此图为x→y′标S、y→x′标W。两个同名参数之间都没有边，不能只盯一个固定位置。
把图合成两次，x经过y′回到x″时严格下降，y经过x′回到y″时也严格下降。线程保存的是“哪份大小事实传到哪里”，不是仅统计每张图有几个下降箭头。
例子与边界
三张闭包图给出完整证书
以源行、目标列均按(x,y)排列，0表示无边，交换图G及其后续合成为
继续合成不会产生第四张图：G⁴=G²，此后在后两张之间交替。唯一幂等图为G²，两个对角线均为S，所以判据通过。附件给出三图及“第0图与自身合成得到第1图”等父引用，可以重算整个闭包，而不只相信一个true标志。
实际轨迹从(2,5)出发为
随后正常返回3。有限轨迹只是例子；对所有自然数输入的结论来自图可靠性和幂等判据。这个例子也能另用x+y作排名，SCT并不要求它是唯一可能的终止证明。
每个调用各有严格边仍然不够
增加两种非确定规则：x>0时可转(x−1,y+1)，y>0时可转(x+1,y−1)。分别只保留必然成立的边，得到
A、B各有一个严格对角线，也各自幂等。但A;B为空图：A追踪到的第一个参数，在B里没有继续边。空图与自身合成仍为空，没有严格自环，故整个集合不通过。
这里还可以交出具体非终止证书：(1,1)选A到(0,2)，再选B回(1,1)，两步无限重复。每个guard都合法。它解释了为何必须检查全部闭包中的幂等图，不能只检查原始调用或每张图是否有S。
摘要太弱也会失败
对只执行x>0→x−1的自然数循环，若分析只保留W自环而忘掉真实的严格性，W图幂等却没有S，判据失败。原程序仍明显终止。这与上一个真实两步循环有不同结论：失败摘要是需要补事实或换证明方法的提示，不自动给出可执行无限运行。
零参数过程也有边界：仅有f()→g()而g返回，非空闭包无自返图，判据真且运行终止；再加g()→f()，便出现0×0幂等自返图，没有任何可下降参数，判据失败。加入零次调用恒等图会把前一个正确结果误判掉。
推论与应用
为什么检查有限图就够
先证明一个有限颜色的无限序列引理。把每对自然数索引i<j染成有限种颜色之一。先取一个索引，再在其后索引中保留与它同色的无限子集；总能找到这样的颜色，因为有限个有限集合的并仍有限。在保留集合里取下一个索引，继续缩小无限尾集。每个选出索引到后续所有选出索引的颜色已经固定。
这些固定颜色只有有限种，必有某一种在无限多个选出索引上出现。只保留那些索引，它们任意一对都有同一颜色。这是此处需要的无限Ramsey形式；构造是存在性证明，不是让编译器真的遍历无穷序列。
现在假设判据通过，却有无限调用图序列。用区间[i,j)的合成图给(i,j)着色。图种类有限，所以存在无限索引集，其任意区间合成都是同一个G。三个递增索引给G;G=G；相邻区间的接口又说明G为f→f。因此G有严格自环i→i。每个相邻选中区间中都存在实现此边、至少含一个S的参数路径，把它们接起来就得到无限下降线程，与自然数良基性矛盾。[3, Theorem4.12的Ramsey机制及§4.3的SCT特例]
反方向，若有坏幂等图G，取生成它的非空调用词w，无限重复w。假如该分层图有无限下降线程，在每个词边界观察其参数位置。有限个位置中，某个位置会无限复现；可选两次复现，使中间经过S。于是某个正次数的G合成有严格自环，而幂等性给所有正次幂都等于G，矛盾。因此w的重复确实不满足抽象线程性质。这个证明没有宣称w能通过具体guard。
工作队列、证书与终止
算法把原始图放入集合及队列。取出一张新图G，与当前集合中的H分别尝试G;H和H;G；只有接口相接才合成，只把此前未见的新图入队。每张图连同源、目标一起判重，不跨过程名混合。
始终保持：集合中的每张图都有一个非空原调用词作为来源。实现不复制整条词，而记录原始图编号或两个更早图的父引用，形成有限推导DAG。队列处理结束时任意可组合二图的结果都已在集合中；结合生成不变量，所得正是非空路径闭包。随后逐个检查自返幂等图及S对角线。
设过程数r、最大元数k，可能的有类型图最多r²3^(k²)张，所以不断加入新图必停止。输入一张0×0图仍是一张图，不是“没有这个调用”。本实现保留全部图，不把较强图按包含关系随意剪掉再只检查幂等者；这种混用可能删去需要检查的坏证据。[3, §4.3]
验证器还检查原始图全在集合中、父引用向前、每次合成相符、集合对合成封闭，以及幂等列表和判断完整。只验证推导DAG里已有图的来源而不检查闭包完整性，可能漏掉A;B那张坏空图。
实现成本与可迁移终点
设输入图数e，实际闭包有c张。稠密矩阵合成最多做k³个中间路径检查；标签和维数验证至多k²。工作队列对图对作常数次尝试，在固定字长标签/过程标识和散列表判重模型下，时间为
空间为O(1+r+(e+c)(1+k²))，包括原始矩阵、闭包、队列和常数大小父引用。显式输出调用词若长W，还需O(W+1)输出工作；推导DAG共享不等于展开后字符串免费。完整闭包证书重检也做图对合成，保持同阶上界。有限可终止不代表多项式规模，3^(k²)提示了参数数目带来的增长。
综合练习要求重算交换图的三元素闭包，提交唯一幂等图的两个严格自环，再加入两个方向不相接的严格规则，交出空图的原调用词和实际两步循环。另将严格边改成弱边，分别说明算法输出、具体程序事实及还缺哪份证明。对可变长任务集合，可改用多重集下降证书；其任务增长语义与这里固定元数的调用接口不同。
参考资料
- Chin Soon Lee、Neil D. Jones、Amir M. Ben-Amram，“The Size-Change Principle for Program Termination”，POPL2001，pp.81–92，官方发表记录：原始提出与发表信息。
- Peter Møller Neergaard，The Size-Change Principle of Termination，Brandeis大学讲义，§3大小图与可靠性、Theorem4.2、Definition5.1合成、Theorem5.4闭包判据及证明，PDF pp.12–16。本文取自然数状态与全部过程入口的明确教学模型。
- Amir M. Ben-Amram，Size-Change Termination, Monotonicity Constraints and Ranking Functions，2010，§4.3、Theorem4.12：有限闭包、无限Ramsey证明机制、SCT幂等严格自环特例及剪枝警告。一般monotonicity constraints另含其他方向约束，不能直接沿用本页局部判据。