高维参数性的立方范畴
Cubical Categories for Higher-Dimensional Parametricity
摘要：
Reynolds的关系参数化理论形式化了系统F的参数多态性，从而捕捉到多态类型的系统F程序总是将相关的输入映射到相关的结果的想法。本文表明，Reynolds理论可以看作是系统F的关系参数化理论在1维的实例化，该理论在所有高维，包括无穷维都成立。这个理论是制定的一个p维立方范畴，我们使用它来定义一个p维参数模型的系统F的任何p，其中p是一个自然数或无穷大的新概念。我们表明，每个p维参数模型的系统F产生分裂$λ$ 2纤维化的类型被解释为面地图和退化保持立方函子和条款被解释为面地图和退化保持立方自然变换。我们证明了我们的理论是“好”的，通过证明Bainbridge等人的PER模型是可导出的另一个一维实例，并且所有维度的所有实例都导出了参数模型预期结果的高维类似物，例如图引理以及初始代数和最终余代数的存在。最后，我们的技术开发解决了Ghani等人提出的一些重大技术问题。最近的bifibrational治疗的关系parametricity，这使我们能够澄清他们的方法，并加强他们的主要结果。一旦澄清，他们的双纤维框架，也可以被视为我们的理论的一维实例。
英文摘要：
Reynolds' theory of relational parametricity formalizes parametric polymorphism for System F, thus capturing the idea that polymorphically typed System F programs always map related inputs to related results. This paper shows that Reynolds' theory can be seen as the instantiation at dimension 1 of a theory of relational parametricity for System F that holds at all higher dimensions, including infinite dimension. This theory is formulated in terms of the new notion of a p-dimensional cubical category, which we use to define a p-dimensional parametric model of System F for any p, where p is a natural number or infinity. We show that every p-dimensional parametric model of System F yields a split $λ$ 2-fibration in which types are interpreted as face map- and degeneracy-preserving cubical functors and terms are interpreted as face map- and degeneracy-preserving cubical natural transformations. We demonstrate that our theory is "good" by showing that the PER model of Bainbridge et al. is derivable as another 1-dimensional instance, and that all instances at all dimensions derive higher-dimensional analogues of expected results for parametric models, such as a Graph Lemma and the existence of initial algebras and final coalgebras. Finally, our technical development resolves a number of significant technical issues arising in Ghani et al.'s recent bifibrational treatment of relational parametricity, which allows us to clarify their approach and strengthen their main result. Once clarified, their bifibrational framework, too, can be seen as a 1-dimensional instance of our theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
