计算效应的关系参数性
Relational Parametricity for Computational Effects
摘要：
根据Strachey的说法，如果多态程序应用独立于其应用的类型实例化的统一算法，则多态程序是参数化的。雷诺兹提出的关系参数性概念是这一思想的一种可能的数学表述。关系参数性为建立数据抽象性质、证明数据集等价性和建立程序等价性提供了有力的工具。这些性质已经在纯函数环境中得到了很好的研究。然而，许多程序表现出计算效果，并且不被关系参数化的标准理论所解释。在本文中，我们开发了一个基本的框架，扩展的概念关系参数化的程序设计语言的影响。
英文摘要：
According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. Relational parametricity provides a powerful tool for establishing data abstraction properties, proving equivalences of datatypes, and establishing equalities of programs. Such properties have been well studied in a pure functional setting. Many programs, however, exhibit computational effects, and are not accounted for by the standard theory of relational parametricity. In this paper, we develop a foundational framework for extending the notion of relational parametricity to programming languages with effects.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
