循环交换

先处理一格的全部k，还是先处理一轮k的全部格 ​

源矩阵累加为

for i in range(0,3):
  for j in range(0,5):
    for k in range(0,2):
      C[i,j] := C[i,j] + A[i,k]*B[k,j]

交换内两层后得到真正可执行的另一份代码：

for i in range(0,3):
  for k in range(0,2):
    for j in range(0,5):
      C[i,j] := C[i,j] + A[i,k]*B[k,j]

两份代码都处理30个三元组。源先完成C[0,0]的两次累加，再处理C[0,1]；目标先给第0行所有C加上k=0的项，再加k=1的项。只要A、B与C不别名，每个C槽自己的k顺序没有改变，不同C槽之间可交换。

30次累加的实际结果 ​

取

C初始全零。两份循环均得到

例如C[1,3]先加 $3\cdot 4=12$，再加 $4\cdot 9=36$，合计48。若C初始不是零，结果应再加上各槽的原值；交换并没有插入清零，也没有把累加改成赋值乘积。

原图的45条带类型边都发生在同一 $(i,j)$ 的两个k之间，距离为(0,0,1)。新次序i、k、j把它变为(0,1,0)，仍为正。这里给出的距离式对任意非负m、n、k尺寸及互不别名的A、B、C都成立；参考程序的30实例报告则只认证这一个已实例化形状，二者的量词不同。

第一个分量翻负，结果真的改变 ​

考虑同一个3×5数组A，初始全部为0，只执行以下六次写入：

for i in range(1,3):
  for j in range(1,4):
    A[i,j] := A[i-1,j+1] + 1

源的写入结果按 $(1,1),(1,2),(1,3),(2,1),(2,2),(2,3)$ 列为

原因是A[2,1]读取刚算出的A[1,2]=1，A[2,2]读取刚算出的A[1,3]=1，末格读取未写过的A[1,4]=0。

边 $(1,2)\to (2,1)$ 的距离为(1,-1)，源词典序为正；交换成j、i后变成(-1,1)，为负。目标在第1位就写A[2,1]，第2位才写它需要的A[1,2]，所以前者读到旧0。全部六格结果变成 $[1,1,1,1,1,1]$。反例不是“缓存较慢”，而是程序数值错误。

参考程序将源坐标归一化为 $(u,v)=(i-1,j-1)$，故拒绝报告为 $(0,1)\to (1,0)$、目标编号2→1、RAW见证对象a的槽7。坐标平移不改变距离，正文和输出描述的是同一条边。

范围相依时不能只交换两行for ​

若原域是 0<=j<i<n 的三角形，直接把for j搬到外层而保留上界i，会引用尚未绑定的i；把上界随意改成n又会执行额外点。合法变换需要重新求目标域及循环界。本页限定矩形域，因此不以这两份简单For模板处理三角循环。

长度为零是另一种真实输入。任一维为空时，两种次序都不执行赋值，最终内存原样返回；但解释器经过的空循环外层数量可能不同。结论是内存相同，不是控制开销相同，更不是在每个输入上加速。

生成器和验证器分别做什么 ​

interchange(p,order)先检查order确为维度的排列，拒绝重复、漏维和布尔值冒充整数，再从内向外搭建For链。下载IR的一条For记录是 (for,变量,下界,上界,正步长,子树)；叶子emit执行固定源体，不能携带一份被改写的算术表达式。界表达式只有整数、已绑定变量、加法和min。绑定名不重复、上界只读外层变量、步长为正，故每层执行有限，整个有限语法树终止。

验证器采用翻译验证理路翻译验证Translation validation · Per-run translation validation · 编译翻译验证给无环有限位算术IR建立良构检查、总解释器与全输入验证器，证明接受可靠性，并用四位溢出反例拒绝错误优化。接口，检查产生器这一次实际交付的IR：

1. 从源P重新求完整身份表、合法地址和冲突图，不信任目标附带的边表。
2. 检查IR语法和绑定；解释其For结构，列出实际emit产生的身份。每次emit先检查“已输出数+体内语句数”不超过源实例数T，超出立即拒绝，不生成这批坐标或记录。其余每个身份须在源域内，全部身份恰出现一次。缺点、重复点、额外点均拒绝。
3. 把目标出现位置写成按源编号索引的rank数组。对每条源边a→b检查 rank[a]<rank[b]。失败返回边、存储见证和两个目标编号；成功返回完整rank数组。

第一步给出真实约束，第二步给出实例双射，第三步给出保持证据。保持定理由此作用于这一个P、IR对。输出报告不是另一份程序的通行证；尺寸、视图、源体或IR变化后必须重验，执行的对象须仍是已经检查的对象。参考程序的run也可执行覆盖正确但依赖不合法的IR，专供复算上述反例；发布路径应先要求validate接受。

为什么不用枚举整数值 ​

循环控制、地址和实例内容已固定。验证器检查的是所有内存值都共同遵守的读写顺序，因此不需要从负无穷到正无穷枚举输入。此前逐槽的独立交换引理已经覆盖了这项无限量化；只对几组矩阵输出作比较则没有这层证明。

精确图规模可能很大。沿用前页A、F、T、e，另记Q为目标IR语法长度、K为解释For的实际栈分派次数、U为这些分派中计算全部界表达式的总节点访问数。验证总时间可保守写为

目标展开在每批emit前受T上限约束，因此即使外来IR重复发出实例，最多物化T条记录。目标身份哈希与复制包含坐标维数，其 $O(dT)$ 工作已由F覆盖；脚本先生成整型rank数组，逐边查询不再反复哈希长坐标。空间除源图外还计目标身份、rank、IR和深度栈。空域可能仍走许多外层循环，K不能从T=0推成0。公共执行器还复制全部初始存储并保存每次写的轨迹，其费用另加总槽数和轨迹长度；本式是验证费用，不是运行目标的费用。

共同终点要求交付IR、rank数组和实际矩阵。迁移时把A改为C前6槽的共享视图：原本合法的i、k、j如今会倒置新RAW边。请先求边再运行，解释为何“同样循环文本、同样维度排列”不足以沿用先前接受报告。