bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

"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 \$
  • 射 恒等射以外
    • 自然変換  L': X*(X \backslash Y) \to \mu Y が適用できるところ
      • μYはYを展開して得られるものの最大不動点。ここでμはモナド(ということにしたい)
    • 同型射 X + \$ \to \$ \$ + X \to \$
    • 同型射 \mu \$ \to \$

ちなみに

  • AND述語: ||&e_1 e_2|| = e_1 \backslash e_1 e_2
  • NOT述語: ||!e_1 e_2|| = (e_1' +' e_2' +' ... ) \backslash e_2 where e'i ≠ e1 なのTBD. 定義めんどくせー)

解きたい問題

 LC(-, \$) \subseteq PEG(-, \$)かどうか。
where

    •  LC(-, \$) LC内の任意の対象から$への射の全集合
    •  PEG(-, \$) PEG内の任意の対象から$への射の全集合

解答

To be developed ハゲワラ

*1:Mati Pentus, Lambek Grammars Are Context Free (1993), In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science. PDF

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。