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.

翻译：递归类型扩展了简单类型λ演算（STLC）的表达能力，使其支持发散计算并编码递归数据类型（如列表）。递归类型有两种构造方式：同构递归类型与等价递归类型。两者的相对优势在类型推理方面已得到充分研究，但它们在语义表达能力上的差异至今尚不明确。本文研究含同构递归类型与等价递归类型的STLC的语义表达能力，证明这两种构造具有相同的表达能力。实际上，我们证明它们与仅含项级递归的STLC表达能力等价。我们通过构造这三种语言（含同构递归类型、等价递归类型及项级递归的STLC）之间的三个典范编译器的完全抽象性来表述这些等价性结果。语言选择的核心在于，我们可研究在简单类型接口与递归类型接口交互下的表达能力差异。三个证明均依赖一种称为近似反向回溯的证明技术的类型化版本。综合结果表明，含同构递归类型与等价递归类型的STLC在语义表达能力上不存在差异。本文聚焦于简单类型设定，但我们相信该结论可推广至更强大的类型系统，如System F。