プログラミング言語概念の定義

プログラミング言語をひとつ与えることは、結局は指標を与えることと同じで、問題は指標から自由圏を作る一種の閉包演算<->のほうだな。どのような種類の自由圏（エルブラン圏、項集合）を与えるかがプログラミング言語構文の特徴付けになる。

閉包演算<->はモナドだが、<->自体がプログラミング言語なのではなくて、プログラミング言語のメタ規則だから、一連のプログラミング言語族を定義する機構。1つのプログラミング言語はメタ構文モナド<->と指標Σの対で決まる。意味論の値の圏をCとすると、Σ→U(C) （Uは忘却）と <Σ>→C が随伴となるのだから、指標圏Signと意味圏の圏Semのあいだの随伴対がメタ構文規則を与えることになる。

となると、Sign上の自由生成圏関手F:Sign→Semと忘却関手U:Sem→Signの対がプログラミング言語族概念に対応するのだろう。意味論sは、s:F(Σ)→C in Sem という射。だから、Σのすべての意味論は Sem＼F(Σ) という余スラント圏をなす。

同じSign上に別な対F':Sign→Sem'、U':Sem'→Signがあると、別なプログラミング言語概念ができる。異なるプログラミング言語概念を繋ぐには、Sem→Sem'という関手が必要になる。あるいはSemもSem'も含むような大きな意味圏の圏SEMを使うとか。

通常、指標圏Signはグラフの圏として定義するが、プレ圏（precategory）の圏としてもいい。そうすれば、忘却関手は実は何も忘却しないで、埋め込み関手となる。忘却／自由生成の対が、埋め込みとレトラクトになっている。事情は簡単になる。Sign⊆Precat、Sem⊆Cat。プレ圏上の合同も使えるな、ウン。