circ-Kleisli構成の別な例

あれれれ、Cを集合圏として、(×, 1)でモノイダル構造を与える。共変ベキ関手Powと、sigleton埋め込み{-}:I→Powと∪:Pow(Pow)→Pow でモナドを考える。

circ-Kleisli構成を考えると、状態遷移も出力も非決定的な順次機械の圏ができる。射は、A×X→Pow(B×X) で、これが遷移と出力を記述する。B=1ならば、非決定性のオートマトンだ。余分配Pow(A)×Pow(B)→Pow(A×B)は具体的な状況では自明だ。余対角が本質ではないな、こりゃ。

対称モノイド圏とモナドがあれば、かなり一般的にいける構成かな。それに、非決定性機械α:A×X→Pow(B×X)を射A→B と考えていいのはうれしい。指標Σがあると、Σの基礎項とかコンテキストの全体とかが決まるが、これはΣが定義する入出力メッセージの集合だから、Σ|→Mes(Σ)のようにして関手が決まる。Mes(Σ)は入力とする非決定性機械で実行系をモデル化するのは自然だ。

話がうまくいきそうだ。circ-Kleili構成はめっけもんのようだ。