2009-11-21 [長年日記]
λ. True Intensionality in Higher Order Logic
Logic and Engineering of Natural Language Semantics 6 (LENLS VI) での Reinhard Muskens 氏によるチュートリアル。
昨日の Haskell Night で紹介したMontagueのPTQのように自然言語の意味を形式的に考えることは形式的意味論と呼ばれて研究されていて、PTQはその最初期のものになる。
昨日PTQについて紹介して、今日このチュートリアルってのは偶然なのだけど、形式意味論の研究で僕がちゃんと知っているのはPTQくらいなので、最近はどんな感じなのかと思い、聞きに行ってきた。
タイトルの「Intensionality」というのは「内包」のことで、「内包」の取り扱いは形式的意味論を考える際のポイントの一つ。例えば、「明けの明星」と「宵の明星」はどちらも金星を指す、すなわち同じ外延を持つ言葉であるにも関わらず、「古代人は宵の明星を宵の明星だと信じていた」と「古代人は宵の明星を明けの明星と信じていた」は明らかに異なる意味を持っているので、「明けの明星」と「宵の明星」は異なる内包を持っていると言える。
チュートリアルのメモ
チュートリアルの最初の話は、PTQで〈s,t〉という型だった命題をprimitiveな型pとして扱う話。PTQだと「Mary believes that the cat is out if the dog is in.」と「Mary believes that the cat is in. 」から、「Mary believes that the dog is out.」を導出出来てしまうが、Maryは論理的に含意されることを全て推論可能とは限らない(imperfect reasoner)ので、これは一般には正しくない。そこで、命題の型としてpという型を導入して、必要に応じて〈s,t〉に変換する。それによって、前述のような誤った導出を出来なくする。
次の話はMoschovakisの「Fregeのsenseをalgorithms、Fregeのreferenceをvaluesと同一視する」というアイ ディアに基づいて、論理プログラムとして解釈する話。これまで、命題から可能世界の集合への関数を使って意味を形式化していたが、関数の代わりに、部分関数を表すニ項関係にする。 そして、意味公準(Meaning Postulates)を論理プログラム、命題をクエリーとして、Refutationをによって可能世界の集合を求める。自己言及的な命題ではRefutationが発散する。論理プログラムのRefutationの形で、実際の推論過程を取り込んでいるのが興味深い。
次は、命題をprimitiveとして扱うアプローチと似ているけど異なるアプローチの話。命題をprimitiveとして扱うのではなく、論理的に可能な世界を表す述語Ωを導入して、and/or/notなどの非論理定数はそれらの世界でのみ標準的な解釈をするようにする。
最後が、関係に基づいた高階の型理論の話。型として基本型とn≧0個のタプル型があって、関係に対してラムダ抽象とか適用とか出来て、解釈は内包と外延をうまく使い分けて定義されている。で、型〈〉で命題を、型〈〈〉〉で可能世界を扱ったりする。この論理は結構キモいけど面白かった。
α型の項の内包はDαの要素とするのだけど、D〈α1, …, αn〉の要素には外延というのがあって、これはDα1×…×Dαnの部分集合になる。 命題の型〈〉の内包の領域はD〈〉で、その外延の領域は一点集合のベキ集合になるので二点集合となり、これは{true, false}とみなせる。 可能世界の型〈〈〉〉の内包の領域はD〈〈〉〉、外延の領域は命題の領域D〈〉のベキ集合となる。
その他
@MoCo7さんに久しぶりにお会いし、また@kaleidotheaterさん、@zoeaiさん、@bon_jaさんといった方々に知りあうことが出来て良かった。 どうせなので、昨日の Haskell Night でのPTQの話についても紹介してみた。ただ、これは時間他の制約からかなりいい加減な紹介になっているので、専門の研究者に見られるのは恥ずかしいものがあるけど (^^;
それから、Combinatory Categorial Grammar (CCG) という範疇文法の一種を教えてもらった。
