一般形式言語理論のアンビアント・モデル圏

リボン言語やツリー言語（ひょっとしてグラフ言語も）含むような一般的な形式言語理論を展開するためのアンビアント〈アンビエント〉（あるいはユニバーサルな）モデル圏は何だろう？ と探していたが、余対角を持つ（あるいは余GS）デカルト圏（cartesian category with codiagonals / co-GS cartesian category）がいいような気がする。実際にはさらに、“余対角＝加法”にベキ等性を要求し、射は、加法や零を保存する必要がない、とする。実際の例ではデカルト閉になるが、デカルト閉性はそれほど使わない。もちろん、トレースも要求する。

上の条件を満たす具象的な圏としては、ω完備な順序集合（ω-complete partial order; ωCPO）がいいと思う。ここで、ω完備とは次の意味：

• Aが順序集合（PO set）、Xが基数≦ωであるAの部分集合のとき、Xには上限が存在する。

この定義なら、

1. ∨{} = 最小限
2. V{a, b} = a∨b
3. ∨{a, b, c} = a∨b∨c

のように、最小元と有限ジョインの存在が自動的に保証される。ちなみに、ω完備の意味が

• a₀≦a₁≦ ... ≦a_n≦ ... が無限列のとき、上限（極限）が存在する。

のときは、別に最小元と有限ジョインの存在を要求する。このときは、ωCPPOJ（ω-complete pointed partial order with joins）とでも呼ぶべき。だが、めんどくさいからωCPOはpointedかつwith joinsだとする。

射は単調でω連続（連続性から単調は出るから、実質は順序的な連続写像）。最小不動点が存在してコンウェイ作用素（conway operator）が作れる。よって、カザネスク／ステファネスク／ハイランド／長谷川の定理から、ωCPO（定義によってはωCPPOJ）はトレース付きデカルト圏。

項がωCPO（より一般には、トレース付きベキ等余対角付きデカルト圏）で意味付けできるようなセオリー（構文的セオリーと意味関手の組）が“形式的な形式言語理論”（CFLT; categorical formal language theory）。特定のアンビアント・モデル圏Aを固定して、A上のCFLTを対象として、CFLTの変換（または翻訳）を射とする圏ができる。Aを動かせば、indexed categoryになりそうだ。

ところで、トレース付きベキ等余対角付きデカルト圏はコゥゼン圏（Kozen圏）にかなり近い。概コゥゼン圏（almost Kozen category）がいいかな？