一句话：提出证明子类型关系相对于类型安全完备性的方法，证明 Amber 规则不完备，并给出可靠完备且 O(mn) 的等递归子类型算法。
子类型关系的可靠性已有成熟证明技术，但相对类型安全的完备性缺乏通用处理框架。本文提出陈述并证明子类型关系关于类型安全完备性的技术，并应用于等递归（iso-recursive）子类型。作者引入“对失败推导的归纳”这一新证明方法。利用该技术，他们证明等递归类型常用子类型规则——Amber 规则——关于类型安全不完备：存在可安全视为子类型的等递归类型 τ1、τ2，但 τ1 ⩽ τ2 不可由 Amber 规则推导。为此，文章定义新的算法化等递归子类型规则，证明其关于类型安全既可靠又完备；并实现算法，优化至 O(mn) 时间，其中 m 为类型中 μ-项数量，n 为类型规模。
Well-known techniques exist for proving the soundness of subtyping relations with respect to type safety. However, completeness has not been treated with widely applicable techniques, as far as we’re aware. This article develops techniques for stating and proving that a subtyping relation is complete with respect to type safety and applies the techniques to the study of iso-recursive subtyping. A new proof technique, induction on failing derivations, is provided that may be useful in other domains as well. The common subtyping rules for iso-recursive types—the “Amber rules”—are shown to be incomplete with respect to type safety. That is, there exist iso-recursive types τ 1 and τ 2 such that τ 1 can safely be considered a subtype of τ 2 , but τ 1 ⩽ τ 2 is not derivable with the Amber rules. New, algorithmic rules are defined for subtyping iso-recursive types, and the rules are proved sound and complete with respect to type safety. The fully implemented subtyping algorithm is optimized to run in O ( mn ) time, where m is the number of μ-terms in the types being considered and n is the size of the types being considered.
@article{LigattiBN17,
title = {On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types},
author = {Jay Ligatti and Jeremy Blackburn and Michael Nachtigal},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {39},
number = {1},
year = {2017},
doi = {10.1145/2994596}
}