"CFG⊆PEG?" Proofathon（略して CPon）作業メモ

文脈自由文法（CFG）から生成される言語と、解釈表現文法（PEG）にて解釈される言語の関係についてのopen problem をみんなで証明してみるオンラインでのバーチャルな会合。参考↓

ノリで参加してみたけど、楽しかったのです。

概要

当初は、PEGのチェッカとかジェネレータとかこさえたりへんちくりんな反例考えてみたり、とかいうまっとうな（？）方向での参加を考えていたのですが、途中でLingrの部屋のログを読み返してて

kinaba
連接 e1 e2 はだいたい e1>>=e2 で、選択 e1|e2 や e1/e2 はだいたい e1 `mplus` e2 で、
リストモナドにすればCFGでMaybeモナドにすればPEGになると思うんですけど
そういう方向でHaskellerやカテゴラーが頑張ってどうにか何か示す未来を期待

とかいう発言から、あーそういやCFGって圏論的にどうなの？とか超脱線気味に思い始め…
歴史の浅いPEGとは違って、どうせ過去に誰か仕事してんだろ、と思っていろいろぐぐってたら、Lambek計算とCFGがequivalentらしい*1事を発見。ぶっちゃけ最終的に、これが自分の一番の成果だったという話も。

なので、そこから急速に方針転換。他の人たちと全く趣を異に、Lambek計算の圏とPEGの圏を比較して何とかしようというアプローチを取ってみた。

でも結論としては、問題の定式化（っぽいもの）をしただけで終わってしまいました。
以下はその痕跡。勢いでやったので、細かいところとか多分いろいろありそうな気はしますが、ひとまず今日の作業メモということで。

圏の定義

基本的に、* が連接、+ が選択に対応。この2つの間には分配則 X*(Y+Z) → X*Y+X*Z が成り立つ。
各規則は冪によって表現される。終端での受理を便宜的に$で表す。（例えば、A→b は追加で b → $ があるという想定）

圏 $LC$ ：Lambek計算で受理できる型の圏

対象
- 任意の終端記号∈Σ_Tと任意の非終端記号∈Σ_N
- 任意の対象X, Yに対して：
  - $X*Y$ : ふつーの直積からsymmetryをとったもの
  - $X+Y$ : ふつーの直和
  - $X \backslash Y$ : 左冪
  - $Y/X$ : 右冪
- $i$ : * の単位（左＝右）
- $\$: X + \$ \simeq \$ + X \simeq \$$
射恒等射以外
- 自然変換 $L: X*(X \backslash Y) \to Y$ が適用できるところ
- 自然変換 $R: (Y/X)*X \to Y$ が適用できるところ
- 同型射 $X + \$ \to \$$ 、 $\$ + X \to \$$

圏 $PEG$ ：PEGとPELの圏

対象
- 任意の終端記号∈Σ_Tと任意の非終端記号∈Σ_N
- 任意の対象X, Yに対して：
  - $X*Y$ : ふつーの直積からsymmetryをとったもの
  - $X+'Y$ : ふつーの直和からsymmetryをとったもの
  - $X \backslash Y$ : 左冪
- $i$ : * の単位（左＝右）
- $\$: X + \$ \simeq \$ + X \simeq \$$
射恒等射以外
- 自然変換が適用できるところ
  - μYはYを展開して得られるものの最大不動点。ここでμはモナド（ということにしたい）
- 同型射 $X + \$ \to \$$ 、 $\$ + X \to \$$
- 同型射 $\mu \$ \to \$$