一句话：证明带 iso- 与 equi- 递归类型的 STLC 语义表达力相同，且都等价于项级递归 STLC。
递归类型扩展了简单类型 lambda 演算（STLC），使其支持发散计算并编码递归数据类型（如列表）。递归类型有两种表述：iso-recursive 与 equi-recursive。它们在类型推断上的相对优劣已有充分研究，但二者的语义表达力关系尚不清楚。本文研究带 iso- 与 equi- 递归类型的 STLC 的语义表达力，证明这两种表述具有相同的表达力；事实上，它们都与仅含项级递归的 STLC 等表达力。作者将这三个语言之间的规范编译器（STLC with iso-recursive types、STLC with equi-recursive types 与 STLC with term-level recursion）的 full abstraction 作为等表达力结果的形式化表述，从而能够研究在简单类型接口和递归类型接口下交互时的表达力。三个证明均依赖一种带类型的 approximate backtranslation 技术。结果表明，带 iso- 与 equi- 递归类型的 STLC 在语义表达力上没有差异。本文聚焦简单类型设置，但作者相信结果可推广到 System F 等更强类型系统。
Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-recursive. The relative advantages of iso- and equi-recursion are well-studied when it comes to their impact on type-inference. However, the relative semantic expressiveness of the two formulations remains unclear so far. This paper studies the semantic expressiveness of STLC with iso- and equi-recursive types, proving that these formulations are equally expressive. In fact, we prove that they are both as expressive as STLC with only term-level recursion. We phrase these equi-expressiveness results in terms of full abstraction of three canonical compilers between these three languages (STLC with iso-, with equi-recursive types and with term-level recursion). Our choice of languages allows us to study expressiveness when interacting over both a simply-typed and a recursively-typed interface. The three proofs all rely on a typed version of a proof technique called approximate backtranslation. Together, our results show that there is no difference in semantic expressiveness between STLCs with iso- and equi-recursive types. In this paper, we focus on a simply-typed setting but we believe our results scale to more powerful type systems like System F.
@article{paperbot2708,
title = {On the Semantic Expressiveness of Iso- and Equi-Recursive Types},
author = {Dominique Devriese and Eric Mark Martin and Marco Patrignani},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:14)2024}
}