日々の流転

λ. ロバ文と依存型と

「Every farmer who owns a donkey beats it.」のような文をロバ文(donkey sentence)といい、一階述語論理の限量子では適切に量化出来ない例として良く知られている。が、ふとこれは依存型の存在するある種の型理論で「∏x:(∑f:Farmer. ∑d:Donkey. own(f,d)). beat(p1(x), p1(p2(x)))」みたいに表現すればいいじゃんと気づいた。

でも、喜んだのは一瞬だけで、調べたらそんなアイディアは Ranta さんらによってとうにやりつくされているのでした。俺なんかがふと思いつく程度のアイディアは誰かにやられていて当たり前だけどね。たはは。

しかし、強力な型理論で自然言語の意味論を扱うのは結構面白そうだ。それに、考えてみればMontagueの理論は個体,真理値,内包的指標からなる単純型付きラムダ計算に基づいていると言えるわけで、この方向は必然だったとも思う。

λ. 鳳梨酥

台湾のお土産らしい。