形式言語理論
まず、Bekicの発音、 https://www.howtopronounce.com/bekic/ ベキクでいいようだ。関連する記事は、 http://d.hatena.ne.jp/m-hiyama-memo/20131001/1380609526 双コンウェイ圏の構造を探る http://d.hatena.ne.jp/m-hiyama-memo/20080527/1211875554 注目…
Σ = {1, +, -} E→ 1 | EE+ | E- Eを式（その定義は上の文法）として、 S→ E S→ SE P→ S | SEE+ SはEのシーケンスで、Pはプレフィックスから。Eの言語をL, Pの言語をL'として、ターゲット命題は L' = Prefix(L) M = Prefix(L) とすれば、 L'⊆M M⊆L' 2番目の証…
簡単な方法 合併： 正規表現の'|'があるので、それが合併 否定： DFAの終状態（受理状態）と非終状態（非受理状態）を入れ替える。NFAをDFAにする必要がある！ 共通部分： ド・モルガンの法則 集合差： L＼L' = L∩L'c 対称差： L△L' = (L＼L')∪(L'＼L) 直接…
Ψをアルファベットとする。（Σは総和に使うので） NΨ をN係数でΨから生成された可換モノイドとして、これをパリク格子と呼ぶことにする。パリク・ベクトル空間と呼ぶことが多いが、混乱の危険があるから。 Ψのクリーネスター＝自由モノイドからΨのパリク格子…
だいぶ分かってきた気がするのだけど、なんかパシッと分かった気がしない。フラストレーションがたまる状態に置かれている。スッキリしない、イライラする。キーワードは 二重圏、三重圏 コボルディズム、TQFT 豊饒プロ関手、圏的双加群 仮想二重圏＝fc複圏 …
オペレーション＝オペラッド射＝複射 をテンプレートと考えて、文法規則をテンプレートにより扱う。 形式言語 テンプレート ガード文字記号 定数ワイヤーラベル 文字記号（終端） 定数（ソリッド）ボックスラベル 変数記号（非終端） 穴ボックスラベル 規則…
http://www.diku.dk/hjemmesider/ansatte/henglein/papers/leiss2006.pdf http://www.sciencedirect.com/science/article/pii/0021869381901794 http://people.maths.ox.ac.uk/~hap/tancl07/tancl07-struth.pdf 加群を考えないほうがおかしいよなー。
マイヒル／ネロードの定理はメイヤーオートマトンに対するものとする。 エルブランの定理 マイヒル／ネロードの定理 定数記号 コンストラクタ記号 関数記号 コマンド・メソッド記号 述語記号 クエリー・メソッド記号 基礎項 コマンド列＝状態項≒プログラムコ…
オートマトン理論に出てくるε遷移。あれは割とダメだった。形式言語理論の文脈では便利だし十分だが、プログラム意味論としてはダメダメ。次のような概念が混同されてゴッチャになった結果がε遷移。 ブランク記号＝タイムフィラー、セリンガーの言う無音{記…
箇条書きでザッと。 マイヒル／ネロード（Myhill/Nerode）の定理は、Constructor-Command-Query分離した指標に対するモデルの構造定理である。 Xを状態空間、適当な圏のホムセットを考えて、コンストラクタ（の意味）は Hom(1, X)、コマンドの意味は Hom(X, …
項集合代数（termset algebra）＝コゥゼン代数 古い順： Σコゥゼン σ-順序代数 - 檜山正幸のキマイラ飼育記 メモ編 コゥゼン代数再び - 檜山正幸のキマイラ飼育記 メモ編 コゥゼン代数もっと - 檜山正幸のキマイラ飼育記 メモ編 項と項集合 - 檜山正幸のキマ…
サイクリックグラフだがほとんどツリーであるものを準ツリー(quasi-tree)と呼ぶことにした。準ツリーは非常に扱いやすい。それは、単純サイクル（僕は素サイクルと呼びたいのだが）が、逆行辺と1:1に対応するからだろう。サイクルがあっても、逆行辺（非順行…
ゾゾウスキ導分とゾゾウスキ共役 - 檜山正幸のキマイラ飼育記 : M+∨M- から“自由生成”した畳み込み積の半環 プレ圏、偏圏、パラ圏などと呼んでいたものがあるが、M+∨M-はその例。これに限らず、圏の「生成系と関係」としてパラ圏は頻出する。モノイドが素材…
http://d.hatena.ne.jp/m-hiyama/20131014/1381732864 の最後の部分の話。aが文字列でLが言語だとして、Lの語全体にaを左に連接する作用を ^a と書き、aによるブルゾゾウスキイ導分（Brzozowski derivative）を a~ と書く。すると、ガロアコネクションがある…
ウーン、ちゃんと書かないとやばいよなー、と思いつつ、極めてラフなメモ。近日中になんとかして、より詳しい記述をしたい。変数と項のペアを束縛と呼ぶことにする。x = t のようにイコールで書く。束縛の集合、ただし変数はすべて違うものを束縛セットと呼…
「letマップ付きグラフ」で、letマップ付きグラフは、結局はサイクルとシェアリングを持つグラフの表現だ、と述べた。逆に、サイクル／シェアリングを持つグラフから出発して、letマップ付きグラフを作ってみる。これにより、ふだん我々が使っている名前機構…
アレ、アレレ？形式言語理論の言語は、列とかツリーとかグラフとかの集合だけど、結局は関手圏なのではないか。GとHがグラフのとき、GからHへのグラフ準同型の集合は、準同型を関手とみなしてよいので、関手圏 [G, H] となる。形式言語理論のたいていの問題…
スピヴァック理論とかの刺激で、マイヒル／ネロードの定理がけっこう分かってきた。指標を圏、むしろ圏の表示（presentation）だと考える。具体的には有向グラフとパス同値関係のセット。有向グラフのルートノード／リーフノードと同じ定義で、圏のルート対…
ソフトウェア技術者の観点から言えば、「ソフトウェアのための集合論」だな。 数学の集合は茫漠としていて掴みどころがない。 全体集合U（universe）を決めて、その部分集合だけを考えるのが良い。 Uはデータの集合だが、アトムだけじゃなくて複合データも考…
アルファベット 列 列言語 列正規表現 列オートマトン 釣り合い列（balanced sequence） ツリーアルファベット（分岐ノード記号とリーフノード記号） ツリーシリアライズ ツリーパターン ツリー正規言語 連接と包囲（enclosing） 明瞭性（Bruggemann-Klein &…
Catyのレイフィケーションを整備してメタプログラミング環境を作る。そもそも何をレイフィケーションするのか？ -- メタレベルにある構造をキチンと定義する必要がある。最近、「メタレベルにある構造」をモグラ（MOGra）という名前で呼ぶことにした。Metaob…
こういう絵になる。NSは名前空間の略称。NSコンテナはいくつかの名前空間を保持する入れ物。NSソートは名前空間の種別。 NSコンテナにNSソート指定＝名前空間＝束縛セット＝置換＝コンテキスト 色々な用語が使われているが同じこと。束縛セット（単に束縛と…
「オートマトンの森田の定理」で、「いやー、むずかしい、難しい。」と書いているが、そのあと挫折してやめた。で、最近また再挑戦。「いやー、むずかしい、難しい。」少しだけ進展してるんだけどね。
項空間に代数構造が入るは入るので、これを項代数と呼んでおく。項代数の演算は、項構成子（コンストラクタ）となる。項空間は余代数構造も持っていて（たいていそういうもんだ）、項の分解とか項の特性とかが余代数構造を定義する。項集合空間はもっと代数…
デクスター・コゥゼン（Dexter Kozen）は、なんか独特の（あるいはクセのある）手法を使う。それで論文が読みにくい感じもするのだが、問題意識は今の僕にとってはピッタリだ。set constraintsとかtermset algebraとか再帰的な型を含むsubtypingとか。コゥゼ…
termグラフの圏ありき。 termツリーはtermグラフの特別なもの。 termツリーはテキスト表現を持つ。 「term=termツリー」か「term=termグラフ」かは文脈次第 termsetはtermの集合、ただしtermの普遍集合があり、その部分集合 term空間 = termset termset空間 …
項と項集合はもちろん違うのだが、コゥゼン（Kozen）の項オートマトンと項集合オートマトンとなると、区別がちょっとわかりにくくなる。項集合の全体はコゥゼン代数（termset algebla）となるが、項の全体はそれほどハッキリした代数構造は持たない。まー、…
http://ttic.uchicago.edu/~pl/classes/CMSC336-Winter08/lectures/lec10.pdf に、次の推論規則が載っていた。 「Xは型です」を X type と書くことにして、 Δ, α type |- τ type ---------------------- Δ |- ∀α.τ Δ, α type; Γ |- e : τ ------------------…
最近考えている手順： スクリプトから有向グラフを作る。あるいは最初から有向グラフが与えられる。 すべてのワイヤー（有向辺＝パイプ）に型注釈を付ける。このとき型付け規則（typing rules）を使う。 限量子で束縛されていた型変数を名前を変えて自由変数…
非対称グラフ単一化って、オートマトンの模倣構成問題だったのだ。メモリを気にしなければ、ノード間の対応（模倣辺）を全部覚えておいて、ダイクストラ法を使えばいい。メモリを使わないように、覚えておかなくていい（後で使わない）記録を削除しようとす…
