ωCPO（可算完備順序集合）で考える形式言語理論 - 檜山正幸のキマイラ飼育記 (はてなBlog)

Brzozowskiさんの発音を調べたりしたのは、Brzozowski導分への興味が再燃したからです。

「再燃」と書いたのは、だいぶ前にもBrzozowski導分を使おうとしていたからです。詳しい話は割愛しますが、形式言語理論をプログラム理論のなかに埋め込もうとしていた時期があります。形式言語理論のめぼしい結果はプログラム理論から再現できるだろうと思っていたし、今でもそう思っています。

以下、僕の印象に残っていることだけ、かなり断片的な話をします。

ベキ等可換モノイドの圏

形式言語理論自体を構文論と意味論に分けることができます。意味論の舞台となる圏についてだけ考えます。形式言語とは、自由モノイドMの部分集合なので、その全体はベキ集合 Pow(M) となります。Pow(M) には、集合の合併による足し算と、Mの演算に由来する掛け算が入ります。とりあえず、足し算（集合の合併）だけ考えます。すると、この足し算はベキ等になり、空集合が零元（足し算の単位元）となります。

以上の状況を一般化して、ベキ等可換モノイドの圏ICM（idempotent commutative monoids）を考えます。対象はもちろんベキ等可換モノイドで、射は半線形写像です。半線形の条件は：

f(x + y) = f(x) + f(y)
f(0) = 0

半線形を単に「線形」と言ってしまうこともあるので注意してください。

足し算を可算無限まで考えたいことがあるので、可算無限例 x₀, x₁, ... に対して、それらの和を Σ_ix_i のように書きます。このような無限和の存在は一般には保証されないので、条件として可算総和可能性を入れた圏をωICMとします。ωICMの射は次の条件を満たす写像です。

f(Σ_ix_i) = Σ_if(x_i)

圏ωICMは、圏ICMの部分圏と考えることができます。より正確には、ωICMは、ICMへの忘却関手を持ちます。

順序構造とωCPO

Aがベキ等可換モノイドのとき、次のようにして順序を定義できます。

x≦y ⇔ x + y = y

足し算のベキ等性があるので、順序がwell-definedであることは簡単に示せます。半線形写像が順序に関する単調写像になることも分かります。これは、圏ICMから順序集合の圏Ordへの標準的な関手があるということです。

x₀≦x₁≦ ... が順序集合内の上昇鎖（上昇しないで停留してもかまわない）として、これらの上限（最小上界）を sup_i x_i とか lub x_i とか書きます。任意の可算上昇鎖（ω上昇鎖）が上限を持つような順序集合をω完備順序集合と呼びます。

AとBがω完備順序集合で、順序に関する単調写像fが、次の条件を満たすときω連続と呼びます。

f(sup_ix_i) = sup_if(x_i)

この条件さえあれば、fの単調性は仮定しなくても出てきます。

ω完備順序集合を対象として、ω連続写像を射とする圏をωCPO（ω-complete partial order）とします。ωCPOは、順序集合の圏Ordへの忘却関手を持ちます。

ωICMの対象と射を順序構造として解釈することにより、ωICM→ωCPO という関手ができます。この関手は充満忠実なので、ωICMをωCPOの部分圏と考えることができます。

ナスター／タルスキー（Knaster-Tarski）の定理とハマりどころ

ωCPOの対象のなかには、ωICMの対象とはみなせないものが含まれます。一般のωCPOに最小元の存在は保証されません。最小元があっても、ωCPOの射が最小元を保存するとは限りません。任意の x, y∈A（AはωCPO)に対して最小上界 x∨y の存在も保証されません。ωICMの対象は、最小元としての零と最小上界としての和を持ち、ωICMの射はそれらを保存します。

ωCPOの対象で、最小元を持つものだけを集めて部分圏を作ります。ただし、射が最小元を保存することは保証しません。この圏をωCPO_⊥としましょう。圏ωCPO_⊥では、次のナスター／タルスキーの定理が成立します。

任意の射 f:A→A に対して、fの最小不動点 p∈P、f(p) = p が存在する。
fの最小不動点は、⊥≦f(⊥)≦f(f(⊥))≦ ... の上限で与えられる。

もう少し一般化して、f:C×A→A に対して、c∈C を固定しての最小不動点p、f(c, p) = p を構成することができて、c|→p という対応もωCPO_⊥の射となります。

さて、ωICM⊆ωCPO_⊥ なので、ωICMでもナスター／タルスキーの定理やその拡張が成立します。しかし、ωICMの射は最小元を保つので、f(⊥) = ⊥ となり、最小不動点が自明となり無意味だ、と、僕は長いことそう思い込んでいました。

違うのです！ f:C×A→A の形の射のCをパラメータとした最小不動点は、p:C→A という射です。確かに、p(⊥) = p(0) = 0 ですが、pに0以外の値を入れれば、非自明な最小不動点が現れます。現実には、c≠0 である p(c) を考えるので、ωICMでもナスター／タルスキーの定理は意味があり、ちゃんと役に立つのです。

デカルト構造と不動点構造

ωCPO_⊥もωICMも、普通の直積でデカルト圏になります。ωICMは、可換モノイドの圏であることから余デカルト構造も持ち、結果的に双デカルト圏です。

ωCPO_⊥でナスター／タルスキーの定理（の拡張版）が成立し、部分圏ωICMでも同様です。ナスター／タルスキーの定理により構成される最小不動点演算子は圏論的に望ましい性質を持つので、KSHH（カザネスク／ステファネスク／ハイランド／長谷川）定理によりトレースを構成可能です。つまり、ωCPO_⊥はトレース付きデカルト圏、ωICMはトレース付き双デカルト圏です。

「ゾゾウスキ導分とゾゾウスキ共役」で出した、言語に対する左連接オペレーターL_αやゾゾウスキ導分D_αは、ωICM内の射として解釈可能です。ゾゾウスキ共役（随伴）の議論をするには、ホムセットに順序構造が必要ですが、ωICMのホムセットは標準的な順序構造を持ちます。

L_αとD_αは共役（随伴）対なので、

L_α(D_α(x))≦x
x≦D_α(L_α(x))

は成立するのですが、ゾゾウスキ共役はより強い条件になっていて、

x=D_α(L_α(x))

です。

左連接オペレーターL_αとゾゾウスキ導分D_αは、随伴対よりは強く、可逆対よりは弱い条件であるEPペア条件を満たしています。これにより、単なる随伴よりは強い結果が出せるはずですが、あんまりよく分かってないです。

形式言語理論全体の構成

形式言語理論の構文論を記述する圏は、記号（構文的変数）の集合を対象として、文法（生成規則の集合）を射とする圏です。左線形文法だけを考えると、圏は（半）線形性を持ち双デカルト圏となります。より一般的な場合でも、デカルト圏にはなります。再帰性からトレースも定義できて、トレース付きデカルト圏を構成できます。

形式言語の意味論とは、文法（あるいは指標）の圏からωICMやωCPOへの関手です。この関手はデカルト構造もトレースも保存するので、トレース付きデカルト圏の準同型関手と言えます。反変関手のときもあります。実際、ゾゾウスキ導分を使って構成された関手は反変です（射の向きの解釈に依存はしますが）。

同一の構文的な圏（文法／指標の圏）の上で複数の意味論関手を考えて、それらの関係を議論することは形式言語理論の課題でしょう。ゾゾウスキ導分による関手と、ゾゾウスキ共役の関係は、特に重要な事例です。随分と前にある程度調べて、それから放置状態だったんですが、もう少し詳しく知りたいなー、とかまた思ったりしている今日このごろ。