记忆化流图专门化

可以把专门化状态看成一张加工单：“现在处理 H，n=3、i=1、a=3、b=3”。这张单已经足够决定循环条件为真，但不能算出 y，因为 x 尚未到。生成器便留下 y:=3*y+3，然后制作下一张静态状态更新后的加工单。

同一张单再次出现时，不需要再造一份代码，只让新跳转接回已有标签。真正增长的是不同加工单的数量，而不是源码里有几个循环。只有一个循环也可能产生无限多张不同的单；有循环但静态状态始终相同，反而只需一个有限的残余环。

固定三轮，保留输入 x ​

沿用前页仿射流图：E 设置 i=0、a=2、b=1、y=x；H 检查 i<n；B 顺序执行 y:=a*y+b、a:=a+1、b:=b+2、i:=i+1，再回 H；R 返回 y。取 n=3，D={x,y}，S={n,i,a,b}。

初始键是 E[3,0,0,0]，方括号依次写 n、i、a、b。E 发出 y:=x；得到 H[3,0,2,1]。第一次 H 已知0<3，只跳向 B[3,0,2,1]。B 留下 y:=2y+1，然后静态地更新到 H[3,1,3,3]。下一轮留下 y:=3y+3，再下一轮留下 y:=4*y+5。

第三轮后 H[3,3,5,7] 的比较为假，只到 R[3,3,5,7]。参考器按发现顺序命名，实际输出为：

r0: y := x;       goto r1
r1:               goto r2
r2: y := 2*y+1;   goto r3
r3:               goto r4
r4: y := 3*y+3;   goto r5
r5:               goto r6
r6: y := 4*y+5;   goto r7
r7:               goto r8
r8: return y

手算三次更新得到 y=24x+29。x=4 时 y 依次为4、9、30、125；x=−2 时为−2、−3、−6、−19。生成器发出的是上述九块代码，没有把它进一步代数合成为一条24*x+29，所以不要把手算化简声称为已经实施的优化。

两边都执行九个基本块。源有16次赋值和19次二元原语运算：四次循环比较，每轮五次算术；残余有4次赋值和6次原语运算。计数不含读取变量、跳转、代码生成和大整数位成本，因而不是机器耗时比。控制块没有减少，是这里保留块间对应的有意选择。

同一个 J 必须有两个版本 ​

动态输入 p 决定 T 的 k:=2 或 F 的 k:=5，随后都到 J 计算 y:=k*x。初始 k=0。专门化器登记 E[0]、T[0]、F[0]、J[2]、J[5] 五个键，残余条件仍读取 p；两个 J 分别乘2和5。

x=4 时，p 非零走 J[2] 返回8，p=0 走 J[5] 返回20。若缓存只用标签 J，第一次登记的 J[2] 会吞掉 J[5]；参考器把 F 的边故意重定向到 J[2]，实际得到错误的8。正确的状态关系也会在汇合点报告：源 k=5，却进入证书写着 k=2 的残余块。

完整静态存储可能含已经不会再读取的变量，导致额外版本。本页不做活跃静态投影，因为删掉键的某个分量必须另证以后再也不需要它。仅仅因为两次测试返回一样，就合并静态状态，无法支撑一般正确性。

源发散和生成器发散是两件事 ​

纯静态程序 L: goto L 的静态存储始终相同。首次登记 L 后，处理后继立即命中已有键，输出 r0: goto r0，生成过程结束。源与残余都无限跳转。若生成器把“所有静态控制”理解为必须先跑完这个循环，就永远无法交出 Q；本实现明确避免那种压缩策略。

另一程序从 i=0 开始，在未知整数 x 下循环 if i<x，真分支执行 i:=i+1，假分支返回 i。每个具体整数 x 都只循环 max(0,x) 次，但若 i 为 S，生成器要处理 H[0]、H[1]、H[2]、……。对每个固定 i，未知 x 仍可能更大，所以两路都要保留。记忆化没有相同键可复用，变体集合无限。

参考器以12个已登记状态为教学预算，实际报告 budget_exhausted，并给出下一请求的 R[i=3]；它不返回缺边的半成品程序。这个有限实验本身不是无穷性证明，无穷性来自上述对任意 i 都能继续产生 H[i+1] 的论证。把 i 主动加入 D 并重新分析后，静态存储为空，仅有 E、H、B、R 四个残余块，运行时循环保留，输入5返回5。

逐块对应足以保持返回和发散 ​

先证明表达式引理。设源存储 σ 的静态部分等于 σS，动态部分等于残余存储 τ。结构归纳表明，在 σ 中求 e，与在 τ 中求 reduce(e,σS) 得到同一整数：常量不变，静态变量换成其真实值，动态变量由相等的 τ 读取，二元原语的归纳结论由相同的纯总操作保持。

对源块中的赋值顺序归纳。静态赋值用该引理得到真实新值，只更新专门化时的 σS；残余无需保存它。动态赋值在两边写入同一结果，其他动态变量仍相等。于是到块尾，两边的动态存储对应，更新后的静态存储也与源一致。return 的值相等；静态 if 选出的边与真实条件一致；动态 if 留下的条件在两边求得相同真假值。

在每个残余块入口建立关系：证书的源标签等于当前源标签，证书的完整静态存储等于源静态部分，残余全部动态变量等于源动态部分。入口初始化建立关系，上面的块级论证保持它。每个非返回源块恰对应一个非返回残余块，每个返回块同时结束且结果相同。

因为块内表达式与赋值都有限且总定义，无限源运行必经过无限多个块；一一对应给出无限残余运行，反方向也一样。这里没有用“只比较正常返回”忽略发散，也没有无限多个源静默步骤被压成零个残余步骤的漏洞。证明以专门化成功生成完整有限 Q 为前提，不声称生成器对所有合法输入都会结束。

哪些条件保证生成过程结束 ​

从入口键出发，按上述生成规则闭合得到键集合 K。每次处理一个键只扫描一个有限源块，所有静态运算都终止；同一键只处理一次。因此在忽略资源预算的数学算法中，K 有限就保证生成终止。反之，每个输出块对应不同键，若闭包无限，穷尽队列的算法就不可能产生有限完整结果。

一个可检查的充分条件是：源标签有限，且对这次固定静态输入，每个静态变量在所有被生成的键上只能取有限多个值。若变量 j 至多有 dⱼ 个值，键数至多为源标签数乘以各 dⱼ 的积。这个积可能很大；有限不等于划算。条件必须覆盖生成器保留的动态分支两侧，而不能只看某个测试输入实际走过的路径。

全动态二分始终是保守的终止退路：静态存储为空，每个源标签最多一个版本，已知输入通过入口常量赋值固化。它可能几乎不省运行工作。只动态化某一个不断增长的变量未必够，其他静态计数仍可能产生无限版本；每次改变二分都要重新闭合赋值约束，再重新检查变体边界。

输出敏感成本与参考器的边界 ​

设处理了 k 个键，全部对应源块的语法大小之和为 W，静态变量数为 s，残余代码大小为 R。每个块至多请求两个后继，复制及构造完整静态键需 O(s)。在整数、变量名与哈希访问按单位成本计的模型里，生成时间为 O(W+ks)，空间为 O(R+ks) 加源程序、二分分析和队列；队列长度至多 k。实际大整数的求值、复制表示、哈希、比较和字面量输出都按位长另计，不能把巨大已知整数当作免费常量。

参考器还保存完整证书、执行轨迹和访问过的运行状态，这些是教学验证开销，不包含在只发出 Q 的工作量中。它用重复的完整确定性状态证明一个可见循环；达到执行步数预算但未重复时只报告 prefix_only，不把有限前缀叫作发散证书。源—残余逐块比较可以找错，有限测试仍不能代替上面的全运行证明。

s-m-n 定理理路s-m-n 定理s-m-n theorem · Parameter theorem把程序的部分输入有效固化为新程序索引的参数化定理。允许总能结束的固参包装器：把已知输入写入代码，剩下的工作以后交给解释器。本页选择积极计算静态部分，因此需要额外的有限键条件；两者不矛盾。终点任务要求交出实际残余程序、逐块对应、错误缓存见证和动态化后的重试结果，而不只给“结果看起来一样”的结论。