“记录字段重排不改变结果，但把变成会改变展开树。后一种变化可能仍允许有方向的结构子类型替代，它不是等价。”
形式陈述
有环接口也必须保持替代方向
子类型问S能否放在期待T的位置，记S<:T。给类型加上递归之后，检查可能绕回旧问题：记录的next字段再次要求S<:T。算法需要接受有根据的循环证书，同时继续核查其他字段，不能把“见过这对”当作整次查询已经成功。
本页的输入是两个有限、有根的构造图。节点为Int、Bool、Top、箭头或只读记录；箭头有domain/result两个端口，记录有有限个互异字段标签，边指向本图节点，允许有环。没有未解析的变量或μ别名。下载器也提供从闭合μ语法编图的入口；其绑定、纯别名环拒绝与展开图等价页相同。
图表示可逐层观察的equi-recursive类型。没有可写字段、引用、交/并、有界量化、依赖类型或名义继承。本页规定的<:是下面结构规则的最大关系；它不是为任意语言求值器自动证明值集合包含或程序上下文安全的万能判定器。[1，§§3–4]
一步必须交出的子义务
对方向明确的一对(S,T)，按以下互斥顺序检查：
- T是Top时直接满足，不要求S也为Top
- 两者是同一基础类型时满足；不同基础类型不满足
- 两者是箭头S₁→S₂、T₁→T₂时，必须同时有T₁<:S₁及S₂<:T₂
- 两者是记录时，T的每个字段必须在S中，且同名字段满足S(ℓ)<:T(ℓ)
- 其余构造组合不满足
例如Int<:Top成立，Top<:Int不成立。记录中S可以多字段，因为只读T接口不访问它们；函数域却要把两端翻转，因为期待T的调用者会提供T₁，而实际S函数必须接受它。结果方向保持不变。
令Φ(R)收集当前构造条件满足、且所有子义务均在R中的节点对。R⊆Φ(R)是一份可闭合的候选证书；将所有这种R取并，得到本页的子类型关系。Φ单调：扩大R只会让更多子义务成立。函数域翻转的是有序对，不是对R取补，所以不会破坏这项单调性。
这个定义允许无限递归观察，但只在真正处理构造子之后使用循环假设。不要向Φ加入无守卫的传递规则。 若允许用S<:U与U<:T直接协归纳地证明S<:T，取所有节点对作关系便可让每个错误判断不断引用自身，Int<:Bool也会“成立”。传递性应从结构规则证明，或另用受控的归纳层；不能直接把常见推理规则全部放进同一个最大不动点。[2，引言、§§4–5]
直觉
递归记录多一个字段，方法反而要少挑参数
考虑两份完整类型
T的使用者只知道next与get。S多出的tag不会碍事；调用者给get一个Int，S的get能接收Top范围内的任意输入，当然也包括Int；它返回Int，又满足调用者仅要求Top的结果接口。
next处再次遇到S<:T，这只说明递归部分回到了同一义务。方法参数和结果仍要独立检查，最后所有分支一起闭合，才能接受根判断。
例子与边界
主例四对闭合，反向立即失败
把S、T的根分别记s、t，方法节点记s_get、t_get。成功证书包含四个有方向的义务：
| 对 | 当前检查 | 必需后继 |
|---|---|---|
| s<:t | T字段为get、next，S均提供 | s_get<:t_get；s<:t |
| s_get<:t_get | 箭头 | T的Int域<:S的Top域；S的Int结果<:T的Top结果 |
| T的Int域<:S的Top域 | 右边Top | 无 |
| S的Int结果<:T的Top结果 | 右边Top | 无 |
两个末端虽然都写成Int<:Top，却来自不同语法出现，附件保留为两对节点。访问4对、生成4条子义务，队列清空后交付完整关系。
反向T<:S不成立，因为作为目标的S还要求tag，而T没有。输出根部missing-target-field:tag即可；没有必要展开next到某个深度，也不能把前向成功倒过来用。
改窄方法参数会改变答案
将S的get输入改成Bool，其余字段不动：
现在S_bad<:T的get/domain子义务是Int<:Bool，而不是Bool<:Int。根记录仍提供全部字段，next仍形成可回到根的环，失败来自一个具体方法边界。附件返回路径get、domain，末端有序构造对为(Int,Bool)。
在这个方法接口中，期待T的调用者可以传整数7；一个只接收Bool的方法不能以静态规则承诺接住它。有限义务路径解释了方向错误，但一般不成立的结构子类型判断未必都能构造成某个运行语言的具体反例，尤其当相关类型没有值时；本页不混淆这两项结论。
重复对不意味着可以提前发布成功
队列把每个新对登记一次，逐个检查本地条件和全部后继。登记的含义是“本次查询已经安排检查”，不是“这个对子在任意上下文里已证明成功”。只有本次队列全部检查完，候选对集才是一份成功证书。
例如递归记录的next分支可以绕回根，另一个tag分支却在Bool与Int处失败。如果把刚登记的根先写入跨查询的成功缓存，这次查询失败后又不撤回，下次就可能无条件接受同一错误输入。下载器每次solve创建新的队列和登记表，只有返回的完整成功证书可另作验证与缓存；图身份、版本与判断方向也必须包含在缓存合同里。
遇到右边Top时没有后继义务，即使左图很复杂也可以在该对停止。但输入图仍要先合法：不能因为根要检查S<:Top，就静默接受S里越界的边、重复字段或未解析的别名环。
推论与应用
工作队列给出最大关系中的判定
算法从根对开始，广度优先处理。每一对按形式规则生成唯一的一组必需后继；字段按标签查找，函数domain显式交换两个子节点。只有此前未登记的新对入队，并保存父对及规则端口。无本地规则可用时，沿父链返回冲突证书。
成功时取全部已登记对为R。每一对都经过检查，所有后继仍在R，所以R⊆Φ(R)，根属于最大关系。这证明算法的可靠性；环之所以能关闭，是整份关系封闭，不是单独一次递归调用返回了true。
若根本来属于最大关系，则每个必需后继也属于它。沿队列生成顺序归纳，算法不可能产生本地冲突。两图分别有n、m个节点，域翻转后有序对可处于G×H或H×G，最多2nm对；每对只入队一次，所以算法终止并成功。这给出相对于本页结构关系的完备性。
失败父链上的每一步都是父义务成立所必需的子义务，末端却不满足任何本地规则。沿有限链反推，根也不成立。函数域步骤会改变当前方向，验证器因此重走规则，不把一串字段名当成左右图上始终同向的路径。
传递性来自结构，而不是无穷套规则
自反性可取所有同节点对：基础类型相同，记录字段齐全，箭头两项后继仍是同节点对，故关系封闭。
要证传递，令C由存在U使S<:U且U<:T的所有对(S,T)组成。若T为Top直接满足；否则U也不可能凭Top规则绕过T的外形，相关构造必须匹配。基础类型相同；记录有labels(T)⊆labels(U)⊆labels(S)，每个字段的两段关系给出C中的子对。箭头的域有T₁<:U₁<:S₁，因此(T₁,S₁)在C；结果有S₂<:U₂<:T₂，因此(S₂,T₂)在C。于是C⊆Φ(C)，得到S<:T。
这份证明也适用于环，因为它一次证明关系封闭，没有对无限类型做错误的有限语法归纳。在本页这些结构构造下，互为子类型又迫使基础标签、字段集合和所有对应子节点双向匹配，因而恰好等于展开树等价。可写字段、交并或其他类型算子加入后，需要重新核查这项结论。
实际成本与迁移
设归一化两图共N=n+m节点、E条边，本次访问p对，最大出度d。下载器先核图并建字段字典，随后每对扫描至多d项后继。在字长节点/标签与期望常数散列表操作下，时间O(1+N+E+p(1+d))，空间O(1+N+E+p)，p≤2nm。没有把域翻转之后的反向对误算成已经检查过的正向对。
从μ语法开始还要加编图费用。附件采用显式栈和持久作用域链，A个语法出现的保守时间O(1+A²)、空间O(A)；不会靠Python递归栈偷偷限制可接受展开深度。证书验证重新枚举全部必需后继，保持同阶时间；失败路径在发现冲突后才沿父链生成。
综合练习要求交S<:T的四对关系、反向缺字段证书及S_bad的get/domain方向轨迹，并修改第二层字段而非只换节点编号。这个判定器可作为类型检查器的一个部件；类型检查器整体的进展/保持、运行时记录布局和强制转换仍各有自己的证明接口。
参考资料
- Roberto M. Amadio、Luca Cardelli，Subtyping Recursive Types，TOPLAS15(4)，1993，pp.575–631；作者版§4.1正则方程、§4.2计算规则与有限搜索、§4.3可靠性和完备性。本页采用闭合、可观察图，并显式加入只读记录的语法定向字段义务。
- Nils Anders Danielsson、Thorsten Altenkirch，Subtyping, Declaratively: An Exercise in Mixed Induction and Coinduction，2010，引言、§§4–5：树上结构子类型与不能把传递规则无守卫地协归纳解释的原因。本文只用结构最大关系，不实现论文的混合归纳/协归纳声明系统。