“本页的输入是两个有限、有根的构造图。节点为Int、Bool、Top、箭头或只读记录；箭头有domain/result两个端口，记录有有限个互异字段标签，边指向本图节点，允许有环。没有未解析的…”
形式陈述
判定的是展开树，不是变量替换
沿用递归类型的equi-recursive解释：类型与展开一层的结果视为相同。问题是，两份有限写法是否描述同一棵可能无限的类型树？一棵树的同一模式可以每层重复，也可以每两层重复，文字长度不同不能直接回答。[1，§§1.3、4.1]
本页固定闭合类型文法
记录字段有限、标签互异且只读，字段排列不影响类型。μ按词法作用域绑定变量，可以遮蔽外层同名变量；所有变量必须有绑定。本页把Top作为一个明确的构造标签；在等价问题中，它不与Int或任意其他类型相同。
只接收可观察的递归类型：沿μ展开与变量回指走，必须有限步遇到Int、Bool、Top、箭头或记录构造子。这个要求也作用于每个可达子类型。μX.X及{next:μY.Y}都拒绝；μX.{next:X}和μX.X→Int允许。这里的条件是递归展开能露出构造子，不是归纳数据的严格正性，也不是程序运行的终止性。
输入中没有待求解的自由类型变量。算法不找MGU，也没有通过删除有限项合一的occurs check来“修好”一个类型错误。无限展开等价、有限项可合一与一般类型同构是三个不同问题。
把绑定变成有限的边
编译器给每个语法出现分配节点。基础类型是零出边构造节点；箭头带domain、result两个端口；记录带各字段标签的端口。μ节点只指向其主体，变量节点只指向它实际绑定的μ节点，这两类叫别名边。
遍历变量时沿当前作用域链寻找最近的同名绑定。退出内层绑定不改变外层环境。因此μX.(μX.{next:X})→X中，记录里的X回到内层μ，箭头结果的X回到外层μ；把所有同名X连到一个全局节点会改变类型。
随后解析每个节点的别名链。若它最终到构造节点，就缓存这个头节点；若尚未遇构造子便回到当前路径上的旧别名节点，报告纯别名环。把构造节点的每条子边改为其目标的头节点，得到有限构造图。图的有向环仍保留，只有不产生任何类型观察的别名环被拒绝。
这种图可以反复展开，却不需要真的复制无限多层。沿有限端口词，例如next、next、get、domain，总能在有限图上走出同一串观察。它的展开只有有限多种不同的子树形状，所以称为正则树。[1，§4.1.3–4.1.5]
等价证书的接口
设两份构造图为G、H。候选关系R由节点对(u,v)组成，必须含两根，且对每一对满足：
- 两节点构造标签相同；Int、Bool、Top分别只与自身匹配
- 箭头的domain与domain、result与result后继分别仍在R
- 记录的字段标签集合相同，每个同名字段的后继仍在R
它是保留节点标签的互模拟。存在这样的有限R，当且仅当两图展开成相同类型树。成功输出R；失败输出一个有限端口词，以及沿词到达的一对不兼容构造或字段集合。失败词是类型结构的观察，不必是某段运行程序的反例。
直觉
绕一圈与绕两圈，可以描述同一层层结构
令
另一份完整有限语法为
S每经过next就回到自己；S₂先经过外层和内层记录，第二次next才回到外层。无论沿next走多少次，看到的都是相同三个字段、相同get方法类型和Bool标签，所以应判等价。
证书不用宣称“已经检查无穷多层”。它检查有限对集的一步义务，并保证下一步仍回到这份对集。环提供可重复使用的证明位置，未检查的其他字段仍须真正检查。
例子与边界
工作队列实际要做什么
从根对入队，同时记录它没有父对。每次取出一对，先检查当前构造和字段，再生成全部同名子对。此前未见过的子对入队，保存首次发现它的父对与端口；已见过者不重复入队。遇冲突即沿父链返回有限失败词；队列清空则全部已访问对构成成功证书。
不使用有向图同构。S图有一个递归记录节点，S₂图有两个，节点数就不同；互模拟允许一个节点分别与多个节点配对。共享程度、分配编号和μ变量名也不是展开树的可见标签。
附件不做构造节点合并，S编成5个构造节点，S₂编成10个。除一对/两对递归记录外，两份写法各自保留方法及基础类型出现。根查询恰访问10对、生成10项子义务，最终闭合。这个精确数取决于公开的逐出现编图方式，不是所有等价检查器都必须产生10对。
分支里隐藏的差异仍必须检查
把S₂的内层tag改成Int，外层tag仍为Bool，得到
根字段相同；沿next也先看到一个看似熟悉的递归记录。但端口词next、tag到达Bool与Int，所以不等价。只沿next环确认“能回去”，然后跳过同一节点的其他字段，会漏掉这项差异。
广度优先队列首次到达某节点对的路径最短。因为每个待证分支是必需条件，最先出队的冲突便给最短的冲突节点深度；它不声称是最短字符串编码，也不把记录字段缺失再算成一次真实可执行字段访问。
不能只展开某个固定深度
任给检查深度d，可以造一个类型前d层都返回Bool，到第d+1层才把tag换成Int。有限截断相等不能证明整个无限展开相等。有限节点对闭包却不同：它已把当前输入的所有可达义务处理完，后续不会出现新对。
本页拒绝μX.X，因为它没有根构造观察。Amadio–Cardelli原文在更大的类型模型中另把这种表达式解释为底类型；那是另一种明确选择，不是本算法把它与所有类型匹配的理由。[1，§5.1]
记录字段重排不改变结果，但把{a:Int,b:Bool}变成{a:Int}会改变展开树。后一种变化可能仍允许有方向的结构子类型替代，它不是等价。
推论与应用
编图为何保留展开含义
变量边由词法环境决定，等价于展开时用对应μ类型作无捕获替换；没有以同名字符串代替绑定身份。别名链只跳过μ与变量，不跳过构造子或字段，因此压缩前后每次有限构造观察相同。
对有限端口词长度归纳：空词读到同一头构造；多一个端口时，压缩图沿该构造的对应子边跳到子类型头，再用归纳假设。所有别名链有限，保证每个观察步骤有定义。由此原类型展开与压缩图展开完全一致，无须给运行时递归值选最小或最大解释。
有限关系的可靠性与完备性
若算法成功，所有加入的对子最终都检查过。取这些对为R，每一对的构造兼容且所有子义务仍在R，满足上述互模拟合同。对任意有限端口词归纳，两边具有相同节点标签、相同可选端口，因而展开树相同。这证明成功不只是“没有碰巧遇到错误”。
反过来，若两根展开树相同，任一同名端口后继的展开也相同。算法从根开始，只能加入这样的对，所以不可能遇构造或字段差异。两图分别有n、m个节点，最多nm对；每对只入队一次，故队列必清空。若结果失败，其父链则直接指出一处展开标签差异。三条结论共同给出判定、终止和两类证书的完整接口。
验证器对成功证书重新检查根成员、所有对的构造以及全部子义务是否仍在证书中；缺一个必要后继就拒绝。失败证书则从根逐端口重走，末端必须真有声称的冲突。访问次数或“passed=true”不替代这些检查。
把成本按实际表示计入
设两份输入AST按出现次数计共A个节点。附件用持久作用域链，变量查找至多走A层，故编图时间保守为O(1+A²)；记录标签排序、合法性检查和别名解析均被此界覆盖。作用域链、待处理栈、原始图及头缓存共O(A)空间。输入本身若以共享结构编码，本接口的A仍按展开的语法出现计算，不能把重复处理共享子项的成本抹去。
归一化构造图共有N=n+m个节点、E条端口边；本次访问p个节点对，最大构造出度为d。先建字段字典，队列与证书重检在字长标签及期望常数散列表访问下分别需O(1+N+E+p(1+d))时间，工作空间O(1+N+E+p)。广度父指针每对只存一次，失败时才反向展开一条路径，避免在每次入队复制整条路径。p≤nm；空记录或零出边基础类型仍有入口与节点检查工作。
这些证书适合类型检查器的循环判等、错误定位和缓存验收。它不证明类型中必有一个有限运行值，也不证明所有该类型程序终止。综合练习要求交S/S₂的图与10对关系，再用完整S_deep输入复算next、tag失败词。
参考资料
- Roberto M. Amadio、Luca Cardelli，Subtyping Recursive Types，TOPLAS15(4)，1993，pp.575–631；所链作者排版版共57页，§1.3循环展开等价、§4.1.3–4.1.5正则方程及编图、§4.2.3等价判定、§5.1无构造递归的底解释。章节定位不把作者版页码冒充期刊页码。
- Nils Anders Danielsson、Thorsten Altenkirch，Subtyping, Declaratively: An Exercise in Mixed Induction and Coinduction，2010，§§2.3、3–4：逐层观察、递归绑定与无限树。本页记录扩展、别名拒绝及返回证书的队列实现为明确的教学构造。