形式言語系の定義
フー、ここ2,3日四苦八苦していた問題にやっと目星がついた。プログラム言語をはじめとする形式言語の一般的定式化。とりあえず目標は：
- インスティチューション・フレンドリ
- 十分な一般性
形式言語系とは、組(Sign, Mod, T, ξ)であって：
- SignとModはインスティチューションと同様。Modを、Mod:Sign→Catという反変関手だと考えるとindexed圏。Σ∈|Sign|に対するModの値をMod[Σ]と書く。σ:Σ→Σ'に対するMod(σ)（reduct; リダクト）はσ*と書く。
- TはSign上のモナドで、実用的な多くのケースでベキ等モナド。正確には、T=(T, μ, η)。Tを構文生成モナド（syntax/sytactic production monad）、項形成モナド（term forming monad）と呼ぶ。
- ξは、Mod⇒Mod・T : Sign→Cat とう自然変換。つまり、ξΣ:Mod[Σ]→Mod[T(Σ)] の集まり。ξをモデル拡張自然変換または（モデルの）自然拡張と呼ぶ。
Modの値の圏をCatではなくてSetやOrdにすることもある。そのときも、離散圏、やせた圏と考えれば、Catの場合の議論が通用する。
形式言語系の具体例は後で出す。
Lが形式言語系のとき、L=(SignL, ModL, TL, ξL)のように書く。また、モナドの乗法と単位を明示するときは、（μT、ηTではなく）μL、ηLと記すことにする。
形式言語系Lがプログラミング言語の形式化だとして、プログラム（単純プログラム）と実装の概念を定義する。（モジュール概念は考え中、まだイマイチ。）
プログラム（単純プログラム）とは、モナドTによるKleisli圏の反対圏の射である。Kleisli圏の反対圏をプログラムの圏と呼び、ProgLと書く。つまり、p:Δ→Σ in ProgL ⇔ p:Σ→T(Δ) in SignLである。
指標Δに対して、その実装（実現モデル）とは圏Mod[Δ]の対象のことである。プログラムp:Σ→T[Δ]（Prog内ではΔ→Σ）があると、Δの実装A∈Mod[Δ]に対して、自然拡張ξを使ってξ(A)∈Mod[T(Δ)]が確定する。射pをreductすると、p*:Mod[T(Δ)]→Mod[Σ]が決まる。このreduct関手p*で、実装ξ(A)をMod[Σ]に送るとΣの実装が1つ定まる。この過程による、Mod[Δ]→Mod[Σ]は関手となる。この関手をプログラムpの意味だとする。
| ModTr | = | Sign | 、ModTr(Σ, Δ) = Functor(Mod(Σ), Mod(Δ))で定義される圏をモデル変換子（model transformer）の圏と呼ぶ。プログラムの意味Semは、Porg→ModTrという共変関手を定義する。ひとつのプログラムはモデル圏のあいだのひとつの関手を定義する。 |
今までの記号法だと、モナドTに対するT(Σ)がTermΣ、System(Σ, Γ)は、ProgにもModTrにも使っていたかもしれない。
それにつけても、「セオリーと証明の圏」とか、ほとんど正しいこと言っているようだな。
