Scenes：一种用于可变状态的元逻辑代数
Scenes: A Meta-Logical Algebra for Mutable State
查看机构详情
- University of York（约克大学）
- University of Aarhus（奥胡斯大学）
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
本文提出场景（scene）代数结构，用于刻画状态空间中的变量集，支持基于透镜的元逻辑属性分析，并无需语法即可表征自由/约束变量，进而推导并行组合的推理原则。
中文摘要 AI 辅助
在组合验证中，对可变状态空间进行建模并精确描述变量在程序中的操作方式是一个基本问题。尽管我们可以利用程序的嵌入抽象语法进行此类分析，但这与浅嵌入方法相悖，并阻碍了高效的证明自动化。另一方面，透镜（lenses）和棱镜（prisms）为状态建模提供了优雅的代数基础，它们具备足够的结构以支持元逻辑程序分析，而无需深度嵌入。然而，透镜作为复杂的代数对象，难以轻松地组合、互补或集合收集。在本文中，我们贡献了一种伴随的代数结构，称为场景（scene），它使我们能够刻画状态空间中的变量集或坐标集。场景直观上对应于透镜的集合，但像透镜一样，它们是纯语义的代数对象。我们证明了场景为我们提供了足够的结构来刻画基于透镜的元逻辑属性，如独立性和等价性。此外，我们引入了场景空间（scene space）的概念，类似于向量空间，它使我们能够恢复类似集合的代数结构。最后，我们展示了场景如何使我们能够在不依赖语法的情况下刻画表达式和程序的自由变量与约束变量，并通过推导并行组合算子的推理原则来展示其在程序推理中的应用。
英文摘要
Modelling of mutable state spaces and precisely describing how variables are manipulated in a program is a fundamental problem in compositional verification. Though we can make use of the embedded abstract syntax of a program for such analysis, this runs contrary to the shallow-embedding approach, and hampers efficient proof automation. On the other hand, lenses and prisms provide an elegant algebraic foundation for modelling state, which provide sufficient structure to provide meta-logical program analysis, but without requiring a deep embedding. Nevertheless lenses, as complex algebraic objects, cannot easily be combined, complemented, or collected in sets. In this paper we contribute an accompanying algebraic structure called the scene, which allows us to characterise the set of variables, or coordinates, in a state space. Scenes intuitively correspond to sets of lenses, but like lenses they are purely semantic algebraic objects. We demonstrate that scenes provide us with sufficient structure to characterise the lens-based meta-logical properties, like independence and equivalence. Moreover, we introduce the notion of a scene space, analogous to a vector space, which allows us to recover a set-like algebraic structure. Finally, we show how scenes allow us to characterise the free and bound variables of expressions and programs, without any need for syntax, and demonstrate their use for reasoning about programs by deriving reasoning principles for the parallel composition operator.
