# 依存型意味論によるモダリティと照応の統一的分析に向けて

飯村葵 戸次大介
お茶の水女子大学
\{g2020504, bekki\}@is.ocha.ac.jp

## 概要

本研究は，依存型理論に基づく自然言語の意味論である依存型意味論により，様相 (modality) の分析を試みる。依存型意味論は，照応などの複雑な言語現象を扱うことができる理論だが，モダリティとの関係に着目する研究は，ほとんどなされていない.本論文が対象とする Modal Subordination は，モダリティと照応が相互作用する言語現象であり, 両者を同時に分析可能な体系が必要となる。そこで，依存型意味論を様相型で拡張した Modal DTS を提案し， この枠組みの中で分析を与える.

## 1 はじめに

自然言語には様々な言語現象が存在しており，形式意味論では数多くの理論が分析を与えてきた. そのような理論の一つに, 本研究で採用する依存型意味論 (dependent type semantics, DTS) [1] がある. DTS は，依存型理論 (dependent type theory, DTT) [2] に基づいた自然言語の意味の理論である. 項と型が相互に作用しない単純型理論と異なり，DTT は「項に依存した型」を記述できる. たとえば，長さが $n:$ Int であるリスト $l: \operatorname{List}(n)$ を扱える.この例では，型 List $(n)$ が項 $n$ に依存するという点で依存型である. DTS は以上の性質を受け継ぎ，意味表示が DTT の型と対応するため，他の文の意味に依存して別の文の意味を扱うことができる。

Modal Subordination とは，モダリティを伴う談話における照応現象であり，Roberts [3] により指摘された. 形式意味論では Roberts [3] をはじめ, van Rooij [4] や Asher and McCready [5] など, 多数の分析が存在する. Modal Subordination の例を (1)(2) に示す.

(1) A wolf might come in. \# It growls.

(2) A wolf might come in. It would growl.

モダリティを伴う談話では，E タイプ照応 [6] が到達可能ではなくなることがある.たとえば，(1)では，代名詞 it が a wolf を指すことができず，利用可能な先行詞が存在しない. ${ }^{1)}$ 一方，2 文目にモダリティ wouldを加えた (2)では，そのような制約が生じない. would の使用により, 前半の文で might のスコープ内で導入された a wolf を, 代名詞 it が $\mathrm{E}$ タイプ照応の先行詞として参照できる.

DTS は照応解決 (anaphora resolution) や前提の束縛 (presupposition binding)を扱う理論だが，これまでモダリティの分析についてはそれほど多くの研究がなされているわけではない. たとえば文 (2) と，モダリティを含まない文 (3)を考える。

(2) A wolf might come in. It would growl.

(3) A wolf came in. It growled.

どちらの文も，代名詞 it は a wolf を参照可能だが, DTS による照応解決が可能なのは (3) のみである. (2)における might や would のような，モダリティを含む文の照応解決については，DTS 基づく分析が （田中ら [7] の研究を除けば）存在しない.

本研究は，DTS による Modal Subordination の分析を目的として，モダリティと照応を同時に扱うことができるよう，様相型である可能性 (possibility) と必然性 (necessity)をDTS に加え，拡張した体系である Modal DTS を提案する. 照応の理論であるDTS の特徴を活かし，一般的な照応解決に還元することを目指す. 次節で DTS における照応解決の仕組みを解説し，Modal DTS について概要を述べた後，分析例を示す。

## 2 依存型意味論による照応解決

型が項に依存しない単純型理論は，導入則と除去則により型を定義する。対して，依存型理論 (DTT) [2] は，導入則と除去則に形成則を追加して型の定義を行う．依存型の例として，本稿では紙面の都合上，П型と $\Sigma$ 型のみを解説する．Пは関数型,

$\Sigma$ は直積型の一般化で，それぞれ型に対する全称量化子と存在量化子のように振る舞う。 П型と $\Sigma$ 型の表記を図 1 に示す.

$
(x: A) \rightarrow B \quad\left[\begin{array}{l}
x: A \\
B
\end{array}\right]
$

図1 1 型（左）と $\Sigma$ 型（右）の表記

П 型は後件の型 $B$ において前件の型 $A$ をつ変項 $x$ に依存した型が， $\Sigma$ 型は第二要素の型 $B$ において第一要素の型 $A$ を持つ変項 $x$ に依存した型が，それぞれ構成可能である. 型 $B$ が変項 $x$ に依存しない場合，「項は証明に，型は命題に対応する」というカリー・ハワード同型対応により，П型と $\Sigma$ 型は, 一階述語論理の命題 $A \rightarrow B$ と $A \wedge B$ にそれぞれ対応する。 DTS は，未指定型 (underspecified type) [8] をDTT に加えることで照応解決を可能にする．例として (3) の文における照応解決，つまり，代名詞 it が a wolf を指す場合の過程を示す. 図 2 は (3) の意味表示である. $\pi_{1}$ は $\Sigma$ 型の第一要素を取り出す操作である。

$
\left[\begin{array}{c}
v:\left[\begin{array}{l}
u:\left[\begin{array}{l}
x: \text { entity } \\
\text { wolf }(x)
\end{array}\right] \\
\operatorname{comein}\left(\pi_{1}(u)\right)
\end{array}\right] \\
{\left[\begin{array}{l}
w @\left[\begin{array}{l}
z: \text { entity } \\
\neg \operatorname{human}(z)
\end{array}\right] \\
\operatorname{growl}\left(\pi_{1}(w)\right)
\end{array}\right]}
\end{array}\right]
$

図 2 (3) A wolf came in. It growled. の意味表示

意味表示の型は，DTT における type でなければならないという制約 (semantic felicity condition) があるため，型検査 (type checking) を行うことで，この制約を満たすか調べる. 型検査の過程で未指定項@ を具体的な証明に置き換える操作が，照応解決にあたる. 例では「何らかの entity z が ᄀ human (z) である」という型の証明項を探索することになり，この証明項が存在すれば前述の制約も満たされる。探索した証明項を型検査の証明図に代入した結果，得られる意味表示を図 3 に示す. このように，照応解決は証明探索 (proof search) の問題に還元される.

$
\left[\begin{array}{l}
v:\left[\begin{array}{l}
u:\left[\begin{array}{l}
x: \text { entity } \\
\operatorname{wolf}(x)
\end{array}\right] \\
\operatorname{comein}\left(\pi_{1}(u)\right)
\end{array}\right] \\
\operatorname{growl}\left(\pi_{1} \pi_{1}(v)\right)
\end{array}\right]
$

(3) A wolf came in. It growled. の照応解決結果

## 3 提案手法

本節では，DTS による Modal Subordination の分析を念頭に，DTSを様相型によって拡張した体系である Modal DTS を提案する (§ 3.1). 本手法は， possibility と necessity を加えるにあたり, Contextual Modal Type Theory [9] を一部採用する (§ 3.2). さらに Modal DTS の規則群を紹介し (§ 3.3), 次節の分析で必要な体系を構築する。

## 3.1 Modal DTS

Modal DTS は，既存の П 型と $\Sigma$ 型に possibility と necessity の型を加えた体系である．新たに定義する型として possibility に対応する $\diamond$ (dia) と (bkdia), necessity に対応する $\square$ (box) とロ (bkbox) を加える.

り表される。 とロは 2 文目の意味表示に作用し， $「 1$ 文目のモダリティが 2 文目の証明で使用できる条件」を与える役割を担う． $\Psi$ を文脈として図 4 に例を示す。

$
\left[\begin{array}{c}
v:\langle\Psi\rangle\left[\begin{array}{c}
u:\left[\begin{array}{l}
x: \text { entity } \\
\operatorname{wolf}(x)
\end{array}\right] \\
\operatorname{comein}\left(\pi_{1}(u)\right)
\end{array}\right] \\
\Delta \Psi[\Psi]\left[\begin{array}{l}
w @\left[\begin{array}{l}
z: \text { entity } \\
\neg \operatorname{human}(z)
\end{array}\right] \\
\operatorname{growl}\left(\pi_{1}(w)\right)
\end{array}\right]
\end{array}\right]
$

図 4 (2) A wolf might come in. It would growl. の意味表示

## 3.2 Contextual Modal Type Theory

Contextual Modal Type Theory (CMTT) [9] は, 直観主義様相論理 (Intuitionistic Modal Logic) に対して, 構成的な手法で, possibility と necessity に意味の説明を

CMTTの定義に従う. ととロの規則群を, CMTTが提案する Intuitionistic Contextual Modal Logic (ICML) と Contextual Possibility から取り入れる。

ICML は，直観主義様相論理の S4 を相対化した体系で，含意と Contextual Necessity $[\Psi] A$ を定義する.最も基本的な judgement は命題の真偽を示す $A$ true であり，命題が真であることを，示す手段として導入則，使用する手段として除去則を用いる。一方 Contextual Possibility は， possible world に対する存在量化を表す judgement として，A poss $\langle\Psi\rangle$ を新たに定義した体系である.

図 5 前件のモダリティが possibility である場合の型検査

## 3.3 規則群

Modal DTS における規則は，3つに分けられ

とロに関する規則である.

CMTT の構造規則は, poss 規則に加えて, hyp 規則 (hypothesis rule) と, ctxhyp 規則 (contextual hypothesis rule) がある. hyp 規則は，含意や様相演算子 (modal operator) の意味を説明するために不可欠な hypothetical judgement に由来する. CMTT において命題が任意の世界で真となる場合は $A$ valid という judgement で表す。ctxhyp 規則は， $A$ valid を文脈について相対化した Contextual Validity に由来する.

$
\frac{\Psi \text { ctx } \quad M: \text { type }}{\langle\Psi\rangle M: \text { type }}(\diamond F) \quad \frac{\Psi \text { ctx } \quad M: \text { type }}{[\Psi] M: \text { type }}(\square F)
$

図 $6 \diamond$ との形成則

図 $7 \diamond$ との形成則

$\diamond$ とに関する規則は，図 6 の形成則を新たに作成し，導入則と除去則を CMTT から取り入れる。 とロに関する規則は, 図 7 の形成則をはじめ, Modal DTS において独自に定義したものである. $(\square F)$ の $\sigma: \Psi$ と $(F)$ の poss $\langle\Psi\rangle$ が， § 3.1 で述べた「 1 文目のモダリティが 2 文目の証明で使用できる条件」にあたる部分となる。

## 4 Modal DTS による分析

本節では，Modal Subordinationを対象に，前節で提案した Modal DTS を用いて分析を与える。まず，談話関係 (discourse relation) を示し (§4.1)，これに基づく分析を行う。型検査の過程で証明探索に還元するという DTS の分析 (§2) に従い，解説する (§4.2).

## 4.1 談話関係

Modal Subordination は，対象の 2 文が図 8 に示す談話関係 ${ }^{2}$ に入ることで初めて可能となる. 1 文目と 2 文目にモダリティを伴うことが，談話関係に入る形式的な条件のため，(1)のように後件にモダリティを含まない場合や，2 文が離れる場合は，Modal Subordination が起きることはない.

図 8 Modal DTS における談話関係

## 4.2 分析例

本論文では分析例として，図 8 上段の規則を取り上げる。これは，前件が possibility の場合であり，具体的に以下の 2 文を対象とする.

(2) A wolf might come in. It would growl.

(4) A wolf might come in. It might growl.

図 5 に示したのは，この 2 文の型検査の一部である.

2）記号を縦に並べた記法は複数の規則を纏めたものである。

図 9 前件のモダリティが possibility である場合の証明探索結果

§2で述べた流れと同様に，まずは型検査を行う。意味表示の型が type であるという制約を満たすかどうか調べるため, 図 5 の証明図を下から追う. 最下段は，意味合成で得られた意味表示から，（ $\Sigma F)$ により取り出された, 第二要素にあたる 2 文目の意味表示である. DTTにおいて， $\Sigma$ 型の意味表示全体の型を type とするには第一要素と第二要素の型がそれぞれ typeでなくてはならない.

ここから，§3.3で新たに追加した規則群を適用する. 1 文目のモダリティ might は, として 2 文目に作用しており，このくが $\left({ }^{\circ} F\right)$ の適用で「 1 文目のモダリティが 2 文目の証明で使用できる条件」にあたる poss $\langle\Psi\rangle$ を与える. $(\square F)$ と $(\forall F)$ により， 2 文目の意味表示からモダリティ部分を分けられた後，@型の推論規則である@規則を適用する。図 5 の証明図より, poss $\langle\Psi\rangle$ 環境下において「何らかの entity z が h human (z) である」という型の証明項が存在すれば，型検査は全体の意味表示の型が type であるという制約を満たす。

証明探索を行なった結果が図 9 である. 2 文目は 1 文目に依存して良いことから，1文目の意味表示が利用できる。また，CMTT から採用した $(\diamond E)$ はモダリティが外れた 1 文目の意味表示を仮定する役割を担い，poss 規則は poss $\langle\Psi\rangle$ 環境に作用する. その結果，§2で説明した，モダリティを含まない証明探索に帰着する。つまり，Пと $\Sigma$ 規則のみを使用して「何らかの entity z が ᄀ human (z)である」という型の証明項を探索すれば良い，その際，「wolf ならば human でない」という情報を関数 $f$ として，文脈に用いる. ドット (.) は， CMTT の記法であり，左右でスコープを分ける.探索した証明項は型検査の証明図に代入される.未指定型に伴う変項 $w$ が再帰的に置き換えられた結果, 2 文目の代名詞 $i t$ の具体的な指示対象が判明し,図 10 の意味表示を得る. Modal DTS による照応解決は，以上である．前件のモダリティが necessity の場合は，付録 (A)を参照されたい。

図 10 照応解決結果

## 5 おわりに

本研究は，様相型である possibility と necessity を DTS に加え，拡張した枠組みとして，Modal DTS を提案した。拡張にあたり, CMTT から一部の規則群を採用した。さらに，Modal DTS を用いて Modal Subordination を対象とした分析を与え，モダリティを伴う照応の解決過程を示した。

今後の課題は，まず Modal DTS の様相論理としての形式的性質を明らかにすることが挙げられる。また, 形式意味論では, 動的意味論をはじめとして数多くの理論が Modal Subordination の分析を与えており,これらの理論と Modal DTS の経験的な比較を行う必要がある. さらに，Modal Subordination 以外のモダリティを伴う言語現象について，本分析が拡張できるかどうかも検討を要する。

## 謝辞

本研究は，JST CREST JPMJCR20D2，および JSPS

科研費 JP23H03452 の助成を受けたものである.

## 参考文献

[1] Daisuke Bekki and Koji Mineshima. Context-passing and underspecification in dependent type semantics. In Stergios Chatzikyriakidis and Zhaohui Luo, editors, Studies of Linguistics and Philosophy, pp. 11-41. Springer International Publishing, 2017.

[2] Per Martin-Löf. Intuitionistic type theory. Vol. 17. Bibliopolis, 1984.

[3] Craige Roberts. Modal subordination and pronominal anaphora in discourse. In Linguistics and Philosophy, Vol. 12, pp. 683-721. Springer, 1989.

[4] Robert van Rooij. A modal analysis of presupposition and modal subordination. In Journal of Semantics, Vol. 22, pp. 281-305. Oxford University Press, 2005.

[5] Nicholas Asher and Eric McCready. Were, would, might and a compositional account of counterfactuals. In Journal of Semantics, Vol. 24, pp. 93-129. Oxford University Press, 2007.

[6] Gareth Evans. Pronouns. Linguistic Inquiry, Vol. 11, pp. 337-362, 1980 .

[7] 田中リベカ, 戸次大介. 依存型意味論における modal subordination の記述の試み. 人工知能学会全国大会論文集. 2014 .

[8] Daisuke Bekki. A proof-theoretic analysis of weak crossover. In Proceedings of the 18th International Workshop on Logic and Engineering of Natural Language Semantics. 2021.

[9] Frank Pfenning Aleksandar Nanevski and Brigitte Pientka. Contextual modal type theory. In ACM Transactions on Computational Logic, Vol. 9, pp. 1-49. 2008.

## A 前件のモダリティが necessity である場合の照応解決

図 11 照応解決前の意味表示

図 12 照応解決後の意味表示

図 13 前件のモダリティが necessity である場合の型検査

図 14 前件のモダリティが necessity である場合の証明探索結果