AI 中文总结
本研究将完整基础本地状态（FGLS）视为计算效应，通过证明其单子存在非有限计算得出该单子非有限的结论，并引入其有限子单子，为后续通过等式公理化理解FGLS奠定基础。
AI 中文摘要
完整基础本地状态（Full Ground Local State，FGLS）指可动态分配的可变状态，允许存储基础值与引用，是许多命令式算法的关键组成部分，可实现（循环）数据结构。本研究将完整基础本地状态视为一种计算效应，聚焦于一个特定的指称模型：Kammar等人提出的以位置集合为索引的集合上的可能世界单子。我们解决了关于该FGLS单子的一个未决问题：它是否是有限的？通过证明该单子中存在非有限计算，我们得出FGLS单子并非有限的结论。随后，我们引入Kammar等人单子的一个有限子单子，给出其具体描述，并证明它为FGLS提供了充分的语义。所构建的子单子为未来通过适用于程序推理的等式公理化来理解FGLS铺平了道路。
英文摘要
Full ground local state (FGLS) refers to dynamically allocated mutable state that allows storing ground values and references. It is a key ingredient in many imperative algorithms as it enables (cyclic) data structures. In this work, we treat full ground local state as a computational effect, focusing on one particular denotational model: Kammar et al.'s possible worlds monad on sets indexed over sets of locations. We resolve an outstanding question regarding this FGLS monad: is it finitary? We show that the FGLS monad is not finitary by showing the existence of non-finitary computations in the monad. We then introduce a finitary submonad of Kammar et al.'s monad, give it a concrete description and show that it provides an adequate semantics for FGLS. The submonad we construct paves the way to understanding FGLS in the future via an equational axiomatization suitable for program reasoning.
