依存型意味論による前提理論の形式化
理学専攻 情報科学コース 石下裕里 （指導教員：戸次大介）

1

はじめに

形式意味論では、自然言語の文の意味を論理式を用いて表す。その中でも、自然言語の前提現象については様々な分析が行われている。
文の「前提」とは、その文が発話可能であるために真でなければならない命題のことである。[6] たとえば、(1a) が発話可能であるためには (1b) が真である必要があり、(1b) は (1a) の前提であるとされる。

(1) a. The king of France is bald.
b. There is a king of France.
ある命題が前提か否かを判断するには、「前提投射」と呼ばれる性質を利用する。
前提投射 命題 φ が文 ψ の前提であるとき、ψ を否定文・蓋然文・条件文に埋め込んでも φ がその文に含意される。

(2) a. The king of France is not bald.
b. If the king of France is bald, he has a head.
c. If there is a king of France, the king ofFrance is bald.
(2a)〜(2c) は (1a) を否定文や条件文に埋め込んだ文である。(2a) は (1b) を含意するため、前提投射の定義より (1b) は前提である。また、(2b) も同様に (1b)を含意するため、(1b) は前提である。ところが、(2c)は (2b) と同様に条件文に埋め込まれているにもかかわらず、条件文の前件部に前提とする命題が述べられていることによって、(2c) 全体としては (1b) を含意しない。このように、前提の投射を止める構造をフィルターと呼ぶ。このような現象についても様々な分析が行われているが、その多くはモデル理論的意味論に基づいており、計算機での処理には向いていない。一方、証明論的意味論に基づく分析には、Martin-Löf型理論に基づくものがある。[2][4][3] しかしながら、いずれの前提理論も、照応関係といったその他の言語現象を同時に記述することは困難である。
そこで本研究では、複数の言語現象を同時に記述可能な依存型意味論 [1] を採用する。ただし、前提の記述に関しては述べられていないため、本研究では依存型意味論による前提理論の構築を目的とする。

2組み合わせ範疇文法

組 み 合 わ せ 範 疇 文 法（Combinatory CategorialGrammar, CCG）[5] は、語彙化文法の一種であり、統語・意味に関わる情報の大部分が辞書に記述される。
そのため、組み合わせ規則は比較的単純である。CCGの最も基本的な組み合わせ規則は、以下の関数適用規則である。“:” の左側は統語範疇と呼ばれ、言語学における品詞、プログラミング言語における型に相当する。一方、右側は意味表示を表している。

>

X/Y : f
Y : a
X : fa<Y : a3

依存型意味論とその拡張

3.1依存型X \Y : f
X : fa依存型は、Martin-Löf 型理論から生じた概念である。

··型は項に依存する項に依存する型は量化される·(Πx : A)B は型 A → B を、(Σx : A)B は型 A × B を一般化したものである

例えば、月日を考えるとき、日は 30 の場合や 31の場合が考えられる。これは日の集合が月に依存して決まると言える。これを依存型を用いて、(Σm :Month)Day(m) と記述する。

3.2

依存型意味論

依存型意味論（Dependent Type Semantics, DTS）
[1] は、依存型理論に基づいた自然言語の証明論的意味論の一種である。特徴としては、1) 動的であること、
2) 証明論的であること、3) 構成的であること、4) 到達可能性を説明可能であることの 4 つが挙げられる。
これらの特徴により、DTS では、他の意味論では困難であった複数の言語現象の統一的分析が可能となっている。例えば、(3) は複数の文を跨ぐ照応関係の例である。これを証明論的に分析するために、seli 関数と動的連言規則を導入している。

(3) [A man]i enterd. Hei whistled.
seli 関数 seli 関数はインデックス (i) に対応する先行詞を選択する関数であり、投射関数 π1 または π2 が適当な数だけ合成されたものである。
動的連言規則 S は文を表す統語範疇、M, N はその意味表示、c は先行文脈を表す。

S

CON JSMN

S(λc)(Σu : M c)(N ((c, u)))これらの規則及び前節の関数適用規則を適用すると、(3) は以下のように分析可能である。

A man entered.

øSCON JS(λc)(Σu : (Σx : Entity)M(x))E(π1 (u))

(λc)W(seli (c))

He whistled.

S(λc)(Σv : (Σu : (Σx : Entity)M(x))E(π1 (u)))W(seli (c, v))

ここでは、“whistle” の主体は型 Entity を持つ項 x であるため、seli = π1 π1 π2 となる。

a king of Franceisthere
N Pthere
there

If
S/S/S
(λp)(λq)(λc)(Πw : pc)(q((c, w)))

S \ N Pthere /S \ (S/N P )S \ (S/N P )(λp)(λz)(λc)p((λx)(λc))c(λp)(λc)(Σu : (Σx : E)KingOf (x, f ))(p(π1 (u))c)>S \ N Pthere(λz)(λc)(Σu : (Σx : E)KingOf (x, f ))

<S(λc)(Σu : (Σx : E)KingOf (x, f ))

>>the king of France is bald

S/SS(λq)(λc)(Πw : (Σu : (Σx : E)KingOf (x, f )))(q((c, w)))(λc)(B(π1 (sel(Σx:E)KingOf (x,f ) (c))))S(λc)(Πw : (Σu : (Σx : E)KingOf (x, f )))(B(π1 (sel(Σx:E)KingOf (x,f ) ((c, w)))))

図 1: 文 (2c) の検証
ば、文脈 c において前提が満たされると言える。

提案：選択関数の拡張

3.3

DTS では複数の言語現象の統一的分析が可能である
ことは前節で触れたが、前提理論については未だ明確な形式化はなされていない。DTS で前提理論を構築するにあたって、まず DTS における前提投射の定義を示し、その後 seli 関数の拡張を行う。
DTS における前提の投射とは「適当な seli を用いて、先行文脈 c のみから前提の取得が可能であること」と定義できる。前提を含む文が発話された時点でその前提は真であると仮定されるが、これは先行文脈 c に前提を表す型の証明が存在していなければならないという制約によって説明される。ただし、先行文脈のどの部分に含まれているかは発話された時点では不明であるため、sel 関数の添え字にはインデックス i の代わりに前提を表す論理式とする。以上を踏まえると、(1b)を前提として持つ文の型は sel(Σx:Entity)KingOf (x,f ) (c)を含む形となる。なお、sel 関数は前提トリガーとなる語の意味表示として表すものとする。

4

検証

前節で拡張した体系を用いて、前提投射の形式化が適切に行われていることを検証する。ただし、E, Bはそれぞれ Entity, Bald の省略形とする。
投射する例 (1a)4.1>

king of France

S/(S \ N P )/N(λn)(λp)(λc)(p(π1 (sel(Σx:E)nxc (c))))N(λx)(λc)KingOf (x, f )S/(S \ N P )(λp)(λc)(p(π1 (sel(Σx:E)KingOf (x,f ) (c))))

>

(ΠE)

4.2

c : Discourceπ  (c) : (Πx : E)((Σy : E)KingOf (y, f ))π  (c)f : (Σy : E)KingOf (y, f )f : E

投射しない例 (2c)

図 1 の最下段において、sel(Σx:E)KingOf (x,f ) ((c, w)) ≡ π1 (w)と定義可能である。これにより、sel 関数は先行文脈c には依存しない。すなわち、前提は条件文の前件によってフィルターされており、前提投射していないと考えられる。

5

まとめと今後の課題

本研究では、DTS によって自然言語の前提現象を適切に表す論理体系の構築を目的とし、seli 関数の拡張を行った。このことにより、前提の性質の一つである前提投射の証明論的な分析が可能となった。
しかしながら、今回は “the” という特定の前提トリガーにのみ着目し議論を進めたため、より多くの前提トリガーについて考察し理論に改良を加えていくことが今後の課題である。

参考文献

The>

(ΣE)

isbald(S \ N P )/(S \ N P )(S \ N P )(λp)(λx)(λc)pxc(λx)(λc)B(x)S \ NP(λx)(λc)B(x)The king of France

is bald

S/(S \ N P )S \ NP(λp)(λc)(p(π1 (sel(Σx:E)KingOf (x,f ) (c))))(λx)(λc)B(x)S(λc)(B(π1 (sel(Σx:E)KingOf (x,f ) (c))))

最 下 段 に お い て 、sel 関 数 は「 項 c か ら 、(Σx :E)KingOf (x, f ) 型の項を演繹する証明」を表すものである。すなわち、c : Discourse から (Σx :E)KingOf (x, f ) 型の項が以下のように導出可能なら[1] Bekki, D.: Dependent Type Semantics:framework, manuscript. (2012)

the[2] Carlström, J.: Interpreting Descriptions in Intensional Type Theory, Journal of Symbolic Logic
70(2), pp. 488-514. (2005)[3] Ishishita, Y. and Bekki, D.: Toward the formulation of presupposition by Illative Combinatory
Logic, in Logical Aspects of Computational Linguistics(7th international conference, LACL2012,Nantes, France, July 2012 Proceedings), pp. 74–85, Springer. (2012)[4] Mineshima, K.: A Presuppositional Analysis ofDeﬁnite Descriptions in Proof Theory, in JSAI
2007, LNAI 4914, pp.214-227. (2008)[5] Steedman, M. J.: The Syntactic Process (Language, Speech, and Communication), The MIT
Press, Cambridge (2000)[6] Strawson, P. F.: On Referring, Mind, New Series,
Vol. 59, No. 235, pp. 320-344. (1950)