インスティチューションがうまくない理由

インスティチューションは、構文とモデルを区別する。もともとがモデル論だから当たり前だ。が、コンピュータでは、その構文領域もデータ領域としてモデルの世界に入り込む。ここが問題。

インスティチューションの構造を残しながらも、構文（項）がモデルの世界に入り込むメカニズムが必要だ。モデルMod[Σ]を関手圏A^Σとして定義するのがひとつの手かもしれない。圏Aは、定数係数のような外部環境のようなアーキテクチャのような、、、

         |

 --------+-------- モデルの世界（Mod[Σ]達が住んでいる）

         |

         |          ↑意味写像

         |

 --------+-------- 構文の世界（ΣやT(Σ)達が住んでいる）

         |

        ↑この面（この図の上下方向）で切ってみたら何が見える？

これは難しいなー。

[追記]

コンパイルの概念を最初から組み込むしかないかな。大きなラムダ式とかハロ多圏とかがヒントになるのかも知れない。

[/追記]