依存型意味論による前提投射の分析
理学専攻・情報科学コース
1740645
伊藤 友里菜1

より、前提を含めた投射現象に対して統一的に説明がはじめに
前提 (presupposition) は、自然言語の意味論の主要与えられる。しかし、投射仮説では、前提が新情報とな説明対象である。前提内容は、通常発話の背景情報して問いに答えを与えるような談話を扱うことはできを形成するもので、前提を引き起こす表現は前提トリない。すなわち、前提調節が必要とされる談話を扱うガーと呼ばれる。以下に、前提トリガーのひとつであことができない、という問題点がある。

る確定記述による例を示す。(1) では、前提内容としてフランスには国王がいることが含意される。

(1) The king of France is not bald.
⇝ There is a king of France.

また、前提を意味論的に扱う枠組みのひとつに、Sudo[3] による二次元理論 (two-dimensional theory)[4] に基づく分析がある。この分析では、ジェンダーに関する前提など一部の前提トリガーの真理条件を正しく記述するために、前提内容は、二次元理論を用いて主張内容

ここで注目すべきは、文 (1) において前提表現は否定表とは異なる次元で記述される。しかし、二次元理論を現に埋め込まれているにも関わらず、その内容が文か用いたことにより、この理論の特性として生じる束縛ら含意されることである。これは、投射現象と呼ばれ問題を解決することが求められた。Sudo [3] では、束る。投射現象とは、否定・様相・疑問文等の文構造に埋縛問題に対して、動的意味論 (DPL)[5] を用いることでめ込まれた際にも、その内容が含意されることをいう。

解決策を提示した。これにより存在量化子を含む文に前提は投射現象が確認され、前提投射 (presupposition

関しては説明がなされたが、一方で否定や全称量化子projection) の問題として様々な形式意味論の枠組みで研究が進められてきた。などを含む文に関しては DPL を用いても説明を与え

また、前提内容は通常背景情報を形成するため、前提が伝える情報は、聞き手にとって既に知っている情報 (旧情報) であることが望まれる。しかし、必ずしもそうである必要はない。(1) の発話を、フランスに国王がいるということを事前に知らずに聞いたとする。このときにも我々はフランスには国王がいるという内容をその場で理解し、文を解釈することができる。このように、前提を補って解釈することは、前提調節 (accommodation)と呼ばれる。前提調節が行われるときは、前提内容は聞き手にとって新情報として現れる。
本稿では、前提現象の扱いに関して近年注目されている研究について批判的に検討を行う。また、自然言語の証明論的意味論である依存型意味論を用いて、前提投射の分析を行う。

2

先行研究の問題点
前提の扱いは、語用論的扱いと意味論的扱いに大別できる。意味論的扱いでは、 前提は文構造や語彙の慣習的な意味の一部として生じるものと考えられるが、一方で、語用論的扱いでは、前提は純粋に文脈に依存するものだとされる。
前提を語用論的に扱う枠組みとして、Simons ら [1]による投射仮説に基づいた研究がある。投射仮説では、現在の談話で議論の的になっている問い [2] と命題との間の関連性に基づいて投射現象を説明する。これにられず、問題として残る。

3依存型意味論
依存型意味論 (以下 DTS)[6] は、依存型理論 [7] に基づく証明論的意味論のひとつで、前提を含めた投射現象を統一的に扱うことのできる枠組みである。依存型理論は、項に依存した型の表現が可能な体系で、関数型と直積型の一般化として、それぞれ Π 型と Σ 型を持つ。またいわゆるカリー = ハワード対応関係に基づいて、DTS は意味表示に依存型を用いた表示を持つ。以下に、(1) の DTS における意味表示を示す。
(((2) ¬wise π1 @1 :[x : entity
KoF(x)]))DTS の特徴点は、依存型理論を未指定項 @ により拡張した体系を持つことである。照応表現や前提トリガーは辞書においては @ を用いて表される。@ : A という形式では、型 A は @ に対するアノテーションであり、@ は型 A を持つ具体的な項がその位置に入るまでの項である。前提解消は、@ に対応する具体的な項を構築する過程で行われる。この過程は型理論での証明探索に対応している。

@ を含む意味表示から、@ を取り除いた完全な意味表示を得るために、DTS では型チェック・証明探索・@ の除去という段階を踏む。型チェックは、意味表示の適格性を保証する工程で、ここでその意味表示に @を含むものに関しては、前述の証明探索が呼ばれる。
図 1 に、意味表示 (2) に型チェックを行った結果を示す。
..
..
]
[]
x : entity
x : entity: type ♣ :KoF(x)
KoF(x)([]) [] (@)
x : entity
x : entity@1 ::KoF(x)
KoF(x)(ΣE)([])
x : entity
wise : entity → typeπ1 @1 :: entity
KoF(x)(ΠE)( ([]))
x : entity
wise π1 @1 :: type
KoF(x)(¬F )( ([]))
x : entity¬wise π1 @1 :: type
KoF(x)[[] 1
x : entity
KoF(x)
..
..
([])
(CON)
x : entity
wise : entity → type
π1 @1 :: entity
KoF(x)(ΠE)( ([]))
x : entity
wiseπ@::type1
1..
KoF(x)
.. D1
(¬F )
[]
( ([]))
x : entity
x : entity: type¬wise π1 @1 :: type
KoF(x)
KoF(x)(ΣF ), 1[]
x : entity
 u:


KoF(x)
( ([]))  : typex : entity¬wise π1 @1 :KoF(x)u:

図 3: 図 1 の最下段における前提調節の適用例
図 1: 意味表示 (2) に対する型チェック
図 1 では、右上の @ の規則により証明探索が呼び出される。証明探索によって、これまでの文脈から ♣ の位置に来る具体的な項を構築することは、実際にフランスの国王である存在を見つけることに等しく、この過でき、未指定項 @ によってマークされていた部分は、u を用いて置き換えられる。以下に @ を置き換えて最終的に得られる意味表示を示す。
[] x : entityu:
KoF(x)
¬wise (π1 u)(3)程で投射の導出が行われる。後は、構築した項で、@で置かれていた部分を置き換えることにより完全な意

また、同じ手順で図 1 の下から二段目の位置で前提調味表示を得る。このようにして、DTS では前提投射の節を行ったときに得られる意味表示を以下に示す。

によって具体的な項を構築する過程で行われる。

3.1

前提調節

[] x : entityu:
¬
KoF(x)

wise (π1 u)

導出は、@ による中間的な意味表示を経て、証明探索(4)

前提投射の導出は、理想的にはこれまでの文脈からここで、上記 2 つの意味表示の表現することが異なる証明項を構築することで行われるのが望ましいが、証点に注意をする。(3) では文の外側で前提調節が行なわ明探索が失敗することも考えられる。通常、証明探索れたため、“フランスには国王がいて、その人は賢くなに失敗した場合は、その意味表示は不整合であると判い”ということを表す意味表示になっている。一方で、断されるが、前提は必ずしもそうではない。これは、前提には前提調節があるためである。

DTS では、前提調節は証明探索に失敗した証明図から、構築できなかった証明項を適切な位置に仮定した証明図へと変換させることで行う [8]。以下に、証明項を Σ 型で仮定した前提調節の規則を示す。
..
.. D2
A : typeA true(@)@i : A..
.. D1
ϕ : type
⇝

..
.. D2
A : type[u:A..
.. D2nA : type u : A(@)@i : A..
.. D1 [u/@ : A]ϕ[u/@ : A] : type(ΣF ), n]ϕ[u/@ : A]: type

図 2: Σ-accommodation 規則
証明項は、型が type である位置で仮定される。したがって、文が埋め込み節を含む場合は、前提調節の行われる場所は複数考えうる。たとえば、図 1 においては、二箇所でこの規則が適用可能である。図 3 に、図1 の最下段でこの規則を適用したものを示す。
図 3 の最下段では、証明できなかった項を u として仮定している。したがって、変換前の証明図である図 1において、♣ であった部分は u を用いて埋めることが(4) では、文の内側で前提調節が行なわれたため、結果として “フランスには国王がいて、その人は賢い、というわけではない”ということを表す意味表示となる。
DTS では、前提調節の導出は、証明図を変換することで行い、前提調節を行う際の複数の解釈の可能性は、規則を適用する位置の違いによって説明をする。

参考文献[1] Mandy Simons, Judith Tonhauser, David Beaver, and Craige
Roberts. What projects and why. In Semantics and linguistictheory, Vol. 20, pp. 309–327, 2010.
[2] Craige Roberts. Information structure in discourse: Towards
an integrated formal theory of pragmatics. Working Papers inLinguistics-Ohio State University Department of Linguistics,
pp. 91–136, 1996.
[3] Yasutada Sudo. On the semantics of phi features on pronouns. PhD thesis, Massachusetts Institute of Technology,
2012.
[4] Lauri Karttunen and Stanley Peters. Conventional implicatures. In Choon Kyu Oh and David A. Dineen, editors, Syntax
and Semantics 11: Presupposition, pp. 1–56. Academic Press,
New York, 1979.
[5] Jeroen Groenendijk and Martin Stokhof. Dynamic predicatelogic. Linguistics and philosophy, Vol. 14, No. 1, pp. 39–100,
1991.
[6] Daisuke Bekki and Koji Mineshima. Context-passing and underspecification in dependent type semantics. In Modern Perspectives in Type-Theoretical Semantics, pp. 11–41. Springer,
2017.
[7] Per Martin-Löf. Intuitionistic Type Theory. Notes by G. Sambin. Bibliopolis, Naples, 1984.
[8] Koji Mineshima. Aspects of Inference in Natural Language.
PhD thesis, Keio University, 2013.