递归类型语义表达能力的机械化比较
摘要：递归类型将简单类型的λ演算（STLC）扩展为具有额外表现力的能力，使其能够进行发散计算并编码递归数据类型（例如列表）。存在两种形式的递归类型：iso-递归和等价-递归。关于iso-递归和等价-递归对类型推断的影响的相对优势已有大量研究。然而，这两种形式的相对语义表达能力迄今为止仍不清楚。本文研究了带有iso-递归和等价-递归类型的STLC的语义表达能力，并证明了这些形式具有相同的表达能力。实际上，我们证明它们与只具有项级递归的STLC具有相同的表达能力。我们将这些等价表达结果用三种语言之间的三个经典编译器（具有iso-递归类型和等价-递归类型的STLC以及具有项级递归的STLC）之间的完全抽象的方式来阐述。我们所选择的语言选择允许我们研究在简单类型和递归类型接口上进行交互时的表达能力。这三个证明都依赖于一种称为近似反向翻译的有类型版本的证明技术。综合我们的结果表明，STLC具有iso-递归类型和等价-递归类型之间在语义表达能力上没有区别。在本文中，我们专注于简单类型的设定，但我们相信我们的结果可以推广到更强大的类型系统，例如System F。
作者：Dominique Devriese, Eric Mark Martin, Marco Patrignani
论文ID：2010.10859
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-29