同构递归与等价递归类型的语义表达力研究
编程语言
2024-11-20 v5
摘要
递归类型以额外的表达力扩展了简单类型 lambda 演算（STLC），使其能够进行发散计算并编码递归数据类型（例如列表）。递归类型有两种表述：同构递归（iso-recursive）与等价递归（equi-recursive）。关于同构与等价递归在类型推断方面影响的相对优势已有充分研究。然而，这两种表述的相对语义表达力至今仍不明确。本文研究带有同构与等价递归类型的 STLC 的语义表达力，证明这些表述具有同等的表达力。事实上，我们证明它们都与仅带项级递归的 STLC 表达力相当。我们将这些同表达力结果表述为这三种语言（带同构递归、带等价递归以及带项级递归的 STLC）之间三个典型编译器的完全抽象性。我们对语言的选择使我们能够在简单类型接口与递归类型接口交互时研究表达力。三个证明均依赖于一种称为近似反向翻译（approximate backtranslation）的证明技术的类型化版本。综上，我们的结果表明带同构与等价递归类型的 STLC 之间在语义表达力上并无差异。本文聚焦于简单类型设定，但我们相信我们的结果可扩展到如 System F 等更强大的类型系统。
引用
@article{arxiv.2010.10859,
title = {On the Semantic Expressiveness of Iso- and Equi-Recursive Types},
author = {Dominique Devriese and Eric Mark Martin and Marco Patrignani},
journal= {arXiv preprint arXiv:2010.10859},
year = {2024}
}