やったこと

申し込みをした

https://jssst-ppl.org/workshop/2018/

申し込んだので否応にも論文を書かねばならぬ。ならぬのである。

東工大に行った

少し予定時間に遅れる。日本橋駅が複雑すぎるのが悪い。局所的な密度がヤバすぎる。あと西8号館Wは施錠されており、入るのが難しかった。結局ドアが開いた隙に侵入することになった。不穏すぎる。そのせいでさらに遅れて、新屋さんの話の冒頭を聞き損ねた。もったいない。

新屋さんの曖昧な文脈自由文法の特徴付けの話を聞いた。話を聞いてようやく言語の母関数の意味合いが理解できた。一度ちゃんと自分でも計算してみたい。

あと、木言語は木の集合だという非常に自明で重要な示唆を得た。今、木言語を勉強すれば前よりも理解できる気がする。

そのあとはなぜか鍋を囲んだ。gfnさんの中の人に会えて良かった。Macrodownのモチベーションを本人から聞いてようやく理解できた。なるほど。

南出先生という方がいたのだけど、この人は中々面白い人だと思った。というかアトミックグループの人じゃん。どうりでググった履歴があるわけだ。ちゃんと記憶しような。南出先生のゼミの学生が先読みをもつ正規表現のdenotationalな定式化——恐らく正規表現からその言語を直接的に近い方法で計算するような方法を研究しているらしい。なんとなく方法は思いつくのだけど、敢えてそれをテーマにするのは面白いなと思う。

帰り道は直感主義論理について調べていた。理由は今回のセミナーの主催の鹿島先生という方がその手の研究をしているらしく、しょっちゅう話に出てきたから。実際直感主義論理についてググると鹿島先生の書いた資料が出てくる。なのでそれを読んだら結構分かるような気がした。多分leanを少し触れて定理証明支援系の感覚を理解したからだと思う。シークエントによる証明は定理証明支援系がやってることじゃん、みたいな。クリプキモデルも面白いと思った。あれが必要なのは、ゲーデルの不完全性定理のせい？

総括すると様々な示唆を得られて良かった。