代数的プログラム意味論

TQFTとの類似を考えたプログラム意味論は幾何的プログラム意味論とでも言えるだろう。最近、代数的な定式化にも傾いている。本質は同じだけど。

プログラム	代数
状態空間	加群
プログラム	多元環
状態点	加群の生成系
インストラクション	多元環の生成系
遷移系	多元環上の加群

境界付き遷移系を考えると、空間的境界（順次実行の両端のデータ型）がブール代数、時間的境界（メッセージングプロトコル）が非可換多元環になっている。遷移系が空間的境界（開始状態と終了状態）を持ち、時間的境界も持つなら、2つのブール代数といくつかの非可換多元環を係数域（作用団）とする加群になる。

加群の射が模倣となるのは、各種の係数域の作用と射が交換することで表現されるのだと思う。

このような観点から言うと、Kleene Algebra with Test とか Kleene Algebra with Domains とかも、ブール代数を係数域にしている加群、多元環として説明できると思う。