圏論で図式変形を厳密に：e-graphの操作的意味論への道
How to prove equations using diagrams, part 1
e-graphは等式推論を高速化するデータ構造だが、その操作を数学的に厳密に捉える試みは少ない。本稿では、圏論の「initial functor」を用いて図式の変形規則を定式化し、可換四角形の貼り合わせ法則を機械的に証明する。将来のe-graphの圏論的意味論に向けた第一歩。
圏論は、図式の有効な操作を簡潔に記述するために不可欠であることがわかるだろう。
- henearkr
とても興味深い！！
一つ細かい指摘ですが、J字型の図式Dに対して、JはDの「インデックス圏」または「スキーム」であって、記事に書かれているような「形状」ではありません。
- boldslogan
最近ファンクターとか非記号的論理とかいう概念に偶然出会ったんだが、何かおすすめはないかな？