ステパノフ理論：正則型

STLのステパノフが『プログラミング原論』という変な本を書いている。昔から持っていたが読んでなかった、変だから。少し読もうかと思った。『原論』の内容をステパノフ理論と呼ぶことにする。

正則型（regular type）とは、

• 計算可能で全域な等号述語を持っている。
• コピー操作（コピーコンストラクタ）を持っている。
• 代入操作を持っている。

これは次のような代数構造だろう。

• 生成 i: 1→ T
• 破棄 !: T→1
• 複製 Δ: T→T×T
• 右自明演算 ◁:T×T

なお、記号「◁」は、Unicode Character 'WHITE LEFT-POINTING TRIANGLE' (U+25C1) だ。

複製と破棄は、直積に関してコモノイドになっている。生成は、1上の自明なコモノイドからのコモノイド射になっている。これは、モノイドの破棄（discharger, deletion）が自明モノイドへのモノイド射になっているのと同じ。

右自明演算は破壊的代入で、Tを状態とする加群が作れて、双モノイド上のメイヤー加群となることだと思う。まだちゃんと確認してないけど。