Abstraction and invariance for algebraically indexed types
Abstraction and invariance for algebraically indexed types
复制标题
代数索引类型的抽象和不变性
DOI：
10.1145/2429069.2429082
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Atkey R
中科院分区：
文献类型：
--
作者：
Atkey R
Reynolds的关系参数性提供了一种强有力的方法来推理程序在数据表示变化下的不变性。雷诺理论有一系列令人眼花缭乱的应用，利用不变性产生“自由定理”，非居住结果和代数数据的编码。在计算机科学之外，不变性是贯穿数学和物理学许多领域的共同主题。例如，三角形的面积不会因旋转或翻转而改变。如果我们缩放一个三角形，那么我们缩放它的面积，保持两者之间的不变关系。变换下的属性是不变的，往往组织成组，与代数结构反映的可组合性和可逆性transformation.In本文中，我们调查的编程语言的类型是由代数结构，如几何变换组索引。其他示例包括由主体索引的类型（用于信息流安全）和由距离索引的类型（用于分析一致连续性属性）。根据雷诺兹，我们证明了一个一般的抽象定理，涵盖了所有这些情况。我们的抽象定理的后果包括自由定理表示的不变性的程序，类型同构的基础上不变性的性质，和不可定义的结果表明，当某些代数索引类型是无人居住或只居住的平凡的程序。我们在Coq中已经完全正式化了我们的框架和大多数示例。
Reynolds' relational parametricity provides a powerful way to reason about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds' theory exists, exploiting invariance to yield "free theorems", non-inhabitation results, and encodings of algebraic datatypes. Outside computer science, invariance is a common theme running through many areas of mathematics and physics. For example, the area of a triangle is unaltered by rotation or flipping. If we scale a triangle, then we scale its area, maintaining an invariant relationship between the two. The transformations under which properties are invariant are often organised into groups, with the algebraic structure reflecting the composability and invertibility of transformations.In this paper, we investigate programming languages whose types are indexed by algebraic structures such as groups of geometric transformations. Other examples include types indexed by principals--for information flow security--and types indexed by distances--for analysis of analytic uniform continuity properties. Following Reynolds, we prove a general Abstraction Theorem that covers all these instances. Consequences of our Abstraction Theorem include free theorems expressing invariance properties of programs, type isomorphisms based on invariance properties, and non-definability results indicating when certain algebraically indexed types are uninhabited or only inhabited by trivial programs. We have fully formalised our framework and most examples in Coq.