このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

Categorical Formal Language Theories

形式言語理論 TQFT XML 課題

TQFTつうか、TQFTの一般化であるCategorical General Field Theoriesにならって、Categorical Formal Language Theoriesを定義したい。

準備

まず、アンビエント（ユニバーサル）なモデル圏としてはωCPOを採用。しかし、枠組みとしてはトレース付きベキ等余対角付きデカルト圏なら何でもいい。もうひとつのアンビエント圏として、ソート付き集合（sorted sets）の圏が必要。ソート付き集合の圏は余インデックスされた圏（coindexed category）となる；以下に定義。

集合Sを固定してSorted[S]は、集合Xとσ:X→Sの組(X, σ)を対象として、ソート割り当てσを保存する写像の圏。f:S→Tがソート集合の写像とする。(X, σ)がS-ソート付き集合のとき、T-ソート割り当てτ:X→Tを τ:=σ;f で定義できる。これにより、共変関手 f*=Sorted[f]:Sorted[S]→Sorted[T]が定義できる。よって、Sorted[-]はSet上に余インデックスされた圏となる。余インデックス構造を使わずに、最初から平坦な圏を定義をすることもできる。

別な見方として、集合Sを離散圏とみなして、関手圏SetSを作るとS-集合の圏になる。S |→ SetS は、圏の圏の上のSet前層の圏だと思えばよい。（一般的な話題としても、“圏の圏の上の前層の圏”は面白そう。）

CFLTの定義

アンビエント・モデル圏はωCPOに固定するとして、CFLT（Categorical Formal Language Theory）を定義するには、指標Σの概念が必要。指標Σはソート集合Sとソート付き演算子の集合Oを持つ。固有指標Σ以外に共通指標Γは前もって固定しておく。Γには、対角、余対角、終対象、対称などの“ジャンクション”が含まれる。固有指標Σに共通指標（実はメタ指標、指標構成子、指標生成関手だが）Γを作用させてΓ(Σ)を作り、絶対指標Γ(Σ)から構文圏（syntactic category）を作る。

指標から構文圏を作る方法は2通りある。1つは自由構成（free construction）を行う方法。もう１つは項モナドを使う方法。自由構成では、例えば、指標から自由双デカルト圏などを作る。モナドを使う場合は、モナドが作用するアンビエント圏としてソート付き集合全体の圏を使い、変数圏Vも使う。Vは余デカルト圏でSorted[S]上の具象圏（直和を保存する忘却関手を持つ）である。

項モナドTermΣ(X) （X∈|V|）は、Sorted[S]=SetS上で定義される（直和に関する）可換モナドで、Kleisli圏に直和モノイド構造（つまり余デカルト構造）が入る。このKleisli圏に、直和に関するトレースを入れて、トレース付き余デカルト圏とする。反対圏ならば、トレース付きデカルト圏となる。

項モナドを使う方法は、自由構成よりはるかに一般的（そのぶん複雑）で、自由構成で作った圏は、項モナド構成の特殊なケースと圏同値になる（はず）。さらに、指標Σから構文圏Syn(Γ(Σ))=SynΓ(Σ)=Syn(Σ)を作る操作がおそらくはモナドで、このSynモナドのKleisli圏が、構文圏のあいだの変換を定義する。

CFLT間の射と同値性

アンビエント・モデル圏をωCPOとして、関手M:Syn(Σ)→ωCPO が意味関手（semantic functor）だとは、トレース付きベキ等余対角付き圏としての（共変または反変の）関手のこと。M:Syn(Σ)→ωCPO、N:Syn(Δ)→ωCPO が2つの「構文圏＋意味関手＝CFLT」だとして、構文圏の変換Φ:Σ→Δ（SynのKleisli圏の射）とする。CFLTの射を次のように定義する。

  • Φの持ち上げSyn(Σ)→Syn(Δ)を同じ記号Φで表すとして、MとΦ;Nが、Syn(Σ)→ωCPOの関手となる。別に自然変換α::M⇒Φ;N : Syn(Σ)→ωCPO があるとき、Φとαの組をCFLTの射とする。

特に、(Φ, α):M→N、(Ψ, β):N→M で、ΦとΨが構文圏の圏同値を与え、β=α-1となり、αが（同時にβが）意味関手の自然同値になっているとき、2つのCFLT MとNは同値と呼ぶ。

インデックスされた圏としてのCFLT圏

固有指標の全体を対象類として、適当なSynモナドのKleisli射を射とする圏をベース圏と考えて、インデックスされた圏（indexed category）を作れる。指標Σに対して、関手圏ωCPOSyn(Σ)を考える。構文圏のあいだの構文翻訳関手F:Σ→Δがあると、ωCPOSyn(Δ)→ωCPOSyn(Σ) が誘導される。

以上の状況は、固有指標の圏Signの上にCFLT[-] = ωCPOSyn(-)がインデックスされた圏となることを示す。ΣごとにSen(Σ)をうまく定義できれば、インスティチューションになる（はず）。

課題

すべてのCFLTからなる圏CFLT、あるいはCFLT[-]を考察の対象とする。始対象、終対象はなんだろう。指標Σ（圏だと解釈できる）と変数圏Vをなにか固定したときを詳しく調べる。指標の種類による違い／影響、Vの影響など。