混乱の原因と課題

モナド セオリー論 論理 本編ネタ インスティチューション 課題

\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{\text{ in } }

指標の圏の上の構文モナドのクライスリ圏を考えるのが基本。だが、圏とその反対圏を同時に考えて、ストリング図を使うと混乱しがち。

ストリング図の併置は直和か直積を表すが、それは向き（反対圏かどうか）によって解釈が変わる。

Mが構文モナドのとき、

  • M-手続きは、クライスリ圏の反対圏の射
  • M-コードは、モナドの基礎圏のM-結果的射〈M-resultic morphism〉
  • M-手続きの圏は \mathrm{Proc}(M/\mathcal{S}) := \mathrm{Kl}(M/\mathcal{S})^{\mathrm{op}}

次が重要：

  1. \mrm{Proc}(M) の射 p は対応するコード p^\downarrow を持つ。コードはプログラミング言語によるソースコードだと思ってよい。
  2. コードは \cat{S} 内のM-結果的射である。
  3. \cat{S} は余デカルト圏である。
  4. \mrm{Proc}(M) はデカルト圏である。
    1. \mrm{Proc}(M) は終対象 \mrm{Void} = {\bf 0}^\mrm{op} を持つ。
    2. \mrm{Proc}(M) は直積 \oplus を持つ。\mrm{Void} を単位対象とする対称モノイド積である。
    3. \mrm{Proc}(M) は対角 \Delta_\Sigma を持つ。自然変換になる。
    4. \mrm{Proc}(M) は終射 !_\Sigma を持つ。自然変換になる。

問題は、\mrm{Proc}(M) に対するトレースの定義だ。