进入递归接口证书路线，下载标准库核验器。运行python或python -O加文件名，都会只向stdout输出相同JSON；检查不依赖assert。

你要交的是有限构造图、对集封闭证书或能重走的失败路径。打印几层无限展开可以帮助检查例子，却不能代替完整查询。

一、给出两份完整输入 ​

本单元记录字段只读，Top是子类型的上界，在等价检查时仍是独立标签。固定输入为

S = μX. {
  next: X,
  get: Top -> Int,
  tag: Bool
}

S2 = μY. {
  next: {
    next: Y,
    get: Top -> Int,
    tag: Bool
  },
  get: Top -> Int,
  tag: Bool
}

T = μY. {
  next: Y,
  get: Int -> Top
}

S2的两个记录都显式给出get与tag，不能只插一个缺字段的next壳。下载器examples中的tuple AST与这三份语法相同。

按递归类型编图理路正则递归类型等价Regular recursive type equality · Equi-recursive type equality把有μ绑定的闭合类型压成有限构造图，检查相同无限展开并交出互模拟对集或有限区分路径，拒绝纯别名循环。，μ与绑定变量形成别名边，再将别名边压到构造头。提交S的5节点图、S2的10节点图及T的4节点图。附件graphs给完整编号、端口与根；基础类型按语法出现保留，不把两次Int自动合成一个节点。

二、证明单周期与双周期相同 ​

检查S等价S2。把S根配到S2外层，又把同一S根配到S2内层；next继续回到已登记对。两组get方法的domain/result分别配Top/Int，两组tag配Bool。完整队列访问10对、生成10条子义务，pairs就是成功证书。

对这份证书另跑verify。解释为什么只保留根对会失败：根的get子对尚未入证书，即使next能循环，也没有完成全部字段义务。这里不要求图同构；不同节点数的图依然可以描述同一无限类型树。

迁移为

Deep = μY. {
  next: {next: Y, get: Top -> Int, tag: Int},
  get: Top -> Int,
  tag: Bool
}

S与Deep在根处还没有冲突。提交失败路径next、tag；末端是Bool与Int。若只检查根或只追next环，会错过这个差异。进一步把异常字段放到更多层以后，说明为何任何事先固定的展开深度都不是通用判定法。

三、等价失败，替代仍可能成功 ​

检查S等价T时，根字段集合就不同，等价失败。但按递归子类型规则理路递归结构子类型判定Recursive structural subtyping · Equi-recursive subtyping algorithm在有限递归类型图上展开有方向的替代义务，以只读记录宽度和函数域逆变生成闭合证书，并返回带方向的有限失败路径。，S<:T通过。

提交四对义务：根s<:t；方法s_get<:t_get；T的Int域<:S的Top域；S的Int结果<:T的Top结果。根next后继回到根对，两个右Top叶无需更多后继，合计4对/4子义务。

把方向改为T<:S，返回根缺目标字段tag。不能把“子类型是一种相似关系”作为反向推理；接受方向正是哪个接口要被兑现。

四、方法参数变化必须反映在路径方向里 ​

把S的get输入改Bool，得到

Bad = μX. {next: X, get: Bool -> Int, tag: Bool}

重算Bad<:T。get/domain义务将左右角色交换，末端要求Int<:Bool，因此失败。输出path应为get、domain，conflict中的left/right应为Int/Bool。仅写“Bool与Int不同”不足以验证你是否实现了逆变。

在这个例子中，T的调用者允许向get传整数，而Bad的方法只承诺Bool。再把Bad的域恢复Top但把结果改Bool：这次Bool<:Top仍成立，因此不应因为“结果变了”就无条件拒绝。修改目标T的结果为Int后，同一Bool结果才在get/result处失败。分别提交两次判断及其方向。

五、先验收递归输入本身 ​

以下输入都要有明确处置：

• μX.X：纯别名环，拒绝
• μX.μY.X：仍没有构造观察，拒绝
• {next:μY.Y}：虽然外层有记录，子类型仍含无观察循环，拒绝
• μX.μY.Int：两个不用的绑定可以压掉，接受为Int
• μX.(μX.{next:X})→X：内层next回内层μ，结果X回外层μ；把绑定改成outer/inner应保持等价
• 有自由X的类型：不属于本闭合接口，拒绝

入口拒绝与“不等价”是不同输出层次。不能把μX.X作为普通待比较图，让重复对规则把它与Int等同。本实现的选择也不同于把无构造递归另定义成底类型的模型。

六、核验缓存、证书与成本 ​

对字段包含next循环、但tag不匹配的同一输入连续调用两次，结果都必须失败。第一次临时登记的对不许变成第二次的成功缓存。对返回证书删掉必要子对、篡改冲突编号或换一个不能走的端口，也必须被独立verify拒绝。

主JSON含9类图/证书拒绝，加上5类不合法AST、绑定遮蔽与空用绑定检查。额外自查从完整节点对关系逐轮删除不满足条件的对，独立对照队列结果；这不是让同一个solve自己证明自己。

提交时把编图与对比较的成本分开：A个AST出现的作用域链查找保守O(1+A²)；归一化后N节点/E边、p个义务对、最大出度d，比较O(1+N+E+p(1+d))，工作空间O(1+N+E+p)。等价p≤nm，域可能反向的子类型p≤2nm。失败路径只在终点沿父指针生成，不每步复制长路径。

所有结论限定于本单元明确的闭合、可观察、不可变结构类型。没有求自由变量替换，也没有实现任意运行语言的强制转换、可变引用安全或一般类型同构。