プログラムの変更可能な状態を表す代数Scenes
Scenes: A Meta-Logical Algebra for Mutable State
この論文をやさしく読む
ひとことで言うと
プログラムの状態変数を、構文に頼らず意味論的な代数として扱うsceneという構造を提案します。
何に役立つ？
状態を変更するプログラムの性質や並列合成を、合成的に証明するための理論的な道具になります。
この研究の面白いところ
レンズの利点を保ちながら、変数の集合のように扱うためのscene空間を作り、自由変数や束縛変数も構文なしに特徴付けます。
どこまで分かった？
要旨で示されるのは代数的な性質と推論原理です。実装した証明器の速度や大規模プログラムへの適用結果は記載されていません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
変更可能な状態空間をモデル化し、プログラムが変数をどう操作するかを正確に記述することは、合成的なプログラム検証の基本的な問題である。解析にはプログラムの抽象構文を埋め込んで使うこともできるが、それは浅い埋め込みという方法と相いれず、証明の効率的な自動化を妨げる。一方、レンズとプリズムは、深い埋め込みを必要とせずに、メタ論理的なプログラム解析に十分な構造を持つ、状態をモデル化するための代数的基盤を与える。しかし複雑な代数的対象であるレンズは、容易には結合、補集合の構成、集合としての収集ができない。 本論文は、そのための補助的な代数構造であるsceneを提案する。これにより状態空間の変数または座標の集合を特徴付けられる。sceneは直感的にはレンズの集合に対応するが、レンズと同様、純粋に意味論的な代数的対象である。sceneが独立性や同値性といった、レンズに基づくメタ論理的な性質を特徴付けるために十分な構造を持つことを示す。さらにベクトル空間に類似するscene空間を導入し、集合に似た代数構造を再び得る。最後に、構文を使わずに、式やプログラムの自由変数と束縛変数をsceneで特徴付けられることを示し、並列合成演算子に関する推論原理を導いて、プログラムについての推論に使えることを示す。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-24（UTC）
- 最新改訂
- 2026-09-24 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-24 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
著者のコメント
Submitted to MFCS 2026, rejected. Plan to revise and resubmit elsewhere
arXiv ID: 2609.29380 ／ 要約の誤りについて