Olegさんから話を聞く会

前編

4/24土曜は、Olegさんの話を聞く会を聞く為に東京に来ました。
朝方までPS2でパチンコのようなものをやった挙げ句、全然大学で眠れなかったとかいうのもあって、ただでさえ辛い早起きがウルトラ辛かったような気がします。

取りあえず最初の話は、Abstractな言語と、意味を与える為にある論理式をベースにしたような言語は実は両方向に変換出来るのだ！！そしてそれを可能にするのが限定継続です、という所まで持って行く為の導入を含めて色々。
(Abstract Categorical Grammer)

導入辺りの話は、例えば何か適当に型を付けて英語の文章を表す時にモンタギューなんとかを使うと

taro :: e -- eは個体の集まりを表すような型
hanako :: e
praised :: e -> e -> t -- tはpropを表す型のような何か

praised taro hanako -- hanako as Subject taro as Objectで、
-- 英語ぽく書くと Hanako praised Taro
-- 日本語ぽく書くと　花子が太郎を褒めた

多分図のようなモノで表すと
    /\
   /  \
  /    \
taro   /\
      /  \
     /    \
    /      \
praised    hanako

もう１つ

some person smile　ある人が笑ったというのは

person :: e -> t
smile  :: e -> t

∃(λx.person(x) & smile(x))

-- person(x) と smile(x)を満たすわけなので
-- x ∈ e
-- よって、∃∈(e -> t) -> t

ここまでが、多分割と普通の考え方に成っています。

もう一題
taro smile 太郎が笑ったというのは、

smile :: e -> t
taro  :: e

smile taro

     /\
    /  \
   /    \
 smile  taro

でも素直に"taro smile"と書けないものでしょうか?

smile :: e -> t
taro :: (e -> t) -> t

taro smile

これでも行けそうですね！！

この2つの間では

taro :: e
↓
taro :: (e -> a) -> a

な置き換えが起こっています。これがなんとCPS変換になってるのです。

とかいうのは割と都合の良い書き方になっているのですが、実際にCPS変換するというのはある話で詳細が
[ http://www.cs.rutgers.edu/~ccshan/brown/paper.pdf ]にあるらしいです。

で、ここまでの導入をもとに(当日は、当然ながらOlegさんがもっと丁寧にもっとまともに説明してくれました)Abstract Categorial Grammarsに滑り込むという感じでした。

話の内容はこの辺[ http://okmij.org/ftp/gengo/CAG-talk.pdf ]で、特にΣstr(こいつはsyntaxを表す)、Σabs(こいつが抽象な項を表す)、Σsem(これが意味を表す)の3つのうち、Σabs <-> Σsemにする為に良く在るshift/resetではなくてbubble/resetを入れたという感じになってます。

ここが面白いのですが、bubble/resetに慣れて無いので簡単な例で練習して雰囲気を掴まないとうーんというかかなりこの辺は理解出来ませんでした。

それから、これはぼくが勝手に疑問に思った話なのですが、
"If a man meet a woman,he smile her."
的なものがあって、こいつをlogicalに表現すると
∀m.man(m) -> (∃w.woman(w) & meet(w,m)) -> smile(w,m)
(smile(w,m)のwが変な所に出ているのは、この後この式を∃と∀の関係や二重否定除去とかしまくって一番外側に持ってくる的な話もあったのですが)
と普通はなるらしくて、これを
∀m.∃w.man(m) -> (woman(w) & meet(w,m)) -> smile(w,m)
とするのと何が違うんだろうなーとかいうのがあります。