言語処理学会 第30回年次大会 発表論文集（2024年3月）

依存型意味論によるモダリティと照応の統一的分析に向けて
飯村葵 戸次大介
お茶の水女子大学{g2020504, bekki}@is.ocha.ac.jp

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

1

はじめに達可能ではなくなることがある．たとえば，(1) では，代名詞 it が a wolf を指すことができず，利用可
1）一方，2 文目にモダリ能な先行詞が存在しない．
ティ would を加えた (2) では，そのような制約が生じない．would の使用により，前半の文で might のスコープ内で導入された a wolf を，代名詞 it が 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 のような，モダリティを味論 (dependent type semantics, DTS) [1] がある．DTS含む文の照応解決については，DTS に基づく分析がは，依存型理論 (dependent type theory, DTT) [2] に基づいた自然言語の意味の理論である．項と型が相互 （田中ら [7] の研究を除けば）存在しない．
本研究は，DTS による Modal Subordination の分析に作用しない単純型理論と異なり，DTT は「項に依を目的として，モダリティと照応を同時に扱うこと存した型」を記述できる．たとえば，長さが 𝑛 : Intができるよう，様相型である可能性 (possibility) と必であるリスト 𝑙 : List(𝑛) を扱える．この例では，型List(𝑛) が項 𝑛 に依存するという点で依存型である． 然性 (necessity) を DTS に加え，拡張した体系である
Modal DTS を提案する．照応の理論である DTS のDTS は以上の性質を受け継ぎ，意味表示が DTT の特徴を活かし，一般的な照応解決に還元することを型と対応するため，他の文の意味に依存して別の文目指す．次節で DTS における照応解決の仕組みをの意味を扱うことができる．
解説し，Modal DTS について概要を述べた後，分析
Modal Subordination とは，モダリティを伴う談話
例を示す．
における照応現象であり，Roberts [3] により指摘された．形式意味論では Roberts [3] をはじめ，van2 依存型意味論による照応解決
Rooij [4] や Asher and McCready [5] など，多数の分型 が 項 に 依 存 し な い 単 純 型 理 論 は，導 入 則 と析が存在する．Modal Subordination の例を (1)(2) に除去則により型を定義する．対して，依存型理論示す．
(DTT) [2] は，導入則と除去則に形成則を追加して型(1) A wolf might come in. # It growls.の定義を行う．依存型の例として，本稿では紙面の(2) A wolf might come in. It would growl.
都合上，Π 型と Σ 型のみを解説する．Π は関数型，モダリティを伴う談話では，E タイプ照応 [6] が到

1） 文頭に置かれた「#」は続く文が不適切であることを示す― 408 ―

This work is licensed by the author(s) under CC BY 4.0(https://creativecommons.org/licenses/by/4.0/).

Σ は直積型の一般化で，それぞれ型に対する全称量化子と存在量化子のように振る舞う．Π 型と Σ 型の表記を図 1 に示す．

[(𝑥 : 𝐴) → 𝐵
図1

𝑥:𝐴

提案手法

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 は，既存の Π 型と Σ 型に possibility とうカリー・ハワード同型対応により，Π 型と Σ 型

necessity の型を加えた体系である．新たに定義するは，一階述語論理の命題 𝐴 → 𝐵 と 𝐴 ∧ 𝐵 にそれぞれ対応する．DTS は，未指定型 (underspeciﬁed type) [8]型として possibility に対応する ◇ (dia) と ◆ (bkdia)，necessity に対応する □ (box) と ■ (bkbox) を加える．

を DTT に加えることで照応解決を可能にする．例

might や would のようなモダリティは，◇ と □によとして (3) の文における照応解決，つまり，代名り表される．◆ と ■ は 2 文目の意味表示に作用し，詞 it が a wolf を指す場合の過程を示す．図 2 は (3)「 1 文目のモダリティが 2 文目の証明で使用できるの意味表示である．𝜋1 は Σ 型の第一要素を取り出条件」を与える役割を担う．Ψ を文脈として図 4 にす操作である．

例を示す．

[][]


𝑥 : entity 
𝑢:
 𝑣: ⟨Ψ⟩ wolf(𝑥)

comein(𝜋(𝑢))1[]  𝑧 : entity  ◆Ψ [Ψ]  𝑤@ ¬ human(𝑧)  
 

 
 growl(𝜋1 (𝑤))
 

 

 𝑢 : 𝑥 : entity  
 
 𝑣:
 wolf(𝑥)comein(𝜋1 (𝑢))  []       𝑤@ 𝑧 : entity ¬ human(𝑧)        growl(𝜋1 (𝑤)) 
図 2 (3) A wolf came in. It growled. の意味表示

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

意味表示の型は，DTT における type でなければならないという制約 (semantic felicity condition) があ

3.2

Contextual Modal Type Theoryるため，型検査 (type checking) を行うことで，このContextual Modal Type Theory (CMTT) [9] は，直観制約を満たすか調べる．型検査の過程で未指定項@

主義様相論理 (Intuitionistic Modal Logic) に対して，構を具体的な証明に置き換える操作が，照応解決にあ成的な手法で，possibility と necessity に意味の説明をたる．例では「何らかの entity z が ¬ human (z) であ与える理論である．Modal DTS における ◇ と □ はる」という型の証明項を探索することになり，このCMTT の定義に従う．◇ と □ の規則群を，CMTT が証明項が存在すれば前述の制約も満たされる．探索
した証明項を型検査の証明図に代入した結果，得ら提案する Intuitionistic Contextual Modal Logic (ICML)れる意味表示を図 3 に示す．このように，照応解決は証明探索 (proof search) の問題に還元される．
[]
𝑥 : entity  𝑢:  𝑣 :  wolf(𝑥)
comein(𝜋1 (𝑢))   growl(𝜋1 𝜋1 (𝑣))
図3(3) A wolf came in. It growled. の照応解決結果と Contextual Possibility から取り入れる．
ICML は，直観主義様相論理の S4 を相対化した体系で，含意と Contextual Necessity [Ψ] 𝐴 を定義する．
最も基本的な judgement は命題の真偽を示す 𝐴 trueであり，命題が真であることを，示す手段として導入則，使用する手段として除去則を用いる．一方
Contextual Possibility は，possible world に対する存在量化を表す judgement として，𝐴 poss ⟨Ψ⟩ を新たに定義した体系である．

― 409 ―

This work is licensed by the author(s) under CC BY 4.0(https://creativecommons.org/licenses/by/4.0/).

..
.

[..
.
Ψ : type poss ⟨Ψ⟩..
.
][𝑧 : entity𝑧 : entity: typeposs ⟨Ψ⟩ 𝑡𝑟𝑢𝑒
¬ human(𝑧)¬ human(𝑧)[] 𝑤@ 𝑧 : entity¬ human(𝑧)  : type poss ⟨Ψ⟩ growl(𝜋1 (𝑤))


[]

𝑧 : entity[Ψ]  𝑤@¬ human(𝑧)  : type poss ⟨Ψ⟩⟨Ψ⟩  growl(𝜋1 (𝑤)) []𝑧:entity[Ψ]  𝑤@◆Ψ¬ human(𝑧)  : type⟨Ψ⟩ 
 growl(𝜋1 (𝑤))
図53.3](@)( □ 𝐹)( ◇ 𝐹)(◆𝐹)

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

規則群

Modal DTS による分析

4

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

本節では，Modal Subordination を対象に，前節でる．CMTT の 構 造 規 則，◇ と □ に 関 す る 規 則，提案した Modal DTS を用いて分析を与える．まず，◆ と ■ に関する規則である．

談話関係 (discourse relation) を示し (§ 4.1)，これに基CMTT の構造規則は，poss 規則に加えて，hyp 規則づく分析を行う．型検査の過程で証明探索に還元す(hypothesis rule) と，ctxhyp 規則 (contextual hypothesis

るという DTS の分析 (§ 2) に従い，解説する (§ 4.2)．

rule) が あ る．hyp 規 則 は，含 意 や 様 相 演 算 子(modal operator) の意味を説明するために不可欠な

4.1

談話関係hypothetical judgement に由来する．CMTT においてModal Subordination は，対象の 2 文が図 8 に示す

命題が任意の世界で真となる場合は 𝐴 valid という談話関係2）に入ることで初めて可能となる．1 文目

judgement で表す．ctxhyp 規則は，𝐴 valid を文脈にと 2 文目にモダリティを伴うことが，談話関係に入ついて相対化した Contextual Validity に由来する．

る形式的な条件のため，(1) のように後件にモダリティを含まない場合や，2 文が離れる場合は，ModalΨ 𝑐𝑡𝑥 𝑀 : type(◇𝐹)⟨Ψ⟩𝑀 : type

Ψ 𝑐𝑡𝑥 𝑀 : type(□𝐹)[Ψ] 𝑀 : type

Subordination が起きることはない．
□𝑀◇ 2□□ 𝑀1 ;𝑀◇ 2◇ 𝑀1 ;

図 6 ◇ と □ の形成則

𝜎:Ψ..
.

𝑀 : type poss ⟨Ψ⟩(◆𝐹)◆Ψ 𝑀 : type𝑖𝑖𝑀 : type■Ψ 𝑀 : type

図8(■𝐹)

図 7 ◆ と ■ の形成則

Modal DTS における談話関係

分析例

本論文では分析例として，図 8 上段の規則を取◇ と □ に関する規則は，図 6 の形成則を新たに作成し，導入則と除去則を CMTT から取り入れる．
◆ と ■ に関する規則は，図 7 の形成則をはじめ，
Modal DTS に おい て 独 自 に 定 義 し た も の で あ る．
(■ 𝐹) の 𝜎 : Ψ と (◆ 𝐹) の poss ⟨Ψ⟩ が，§ 3.1 で述べた「 1 文目のモダリティが 2 文目の証明で使用できる条件」にあたる部分となる．

4.2

□
𝑀
◇ 2
□
≡ □ 𝑀1 × ■𝑀
◇ 2≡ ◇ 𝑀1 × ◆り上げる．これは，前件が possibility の場合であり，具体的に以下の 2 文を対象とする．
(2)

A wolf might come in. It would growl.

(4)

A wolf might come in. It might growl.

図 5 に示したのは，この 2 文の型検査の一部である．
2） 記号を縦に並べた記法は複数の規則を纏めたものである．

― 410 ―

This work is licensed by the author(s) under CC BY 4.0(https://creativecommons.org/licenses/by/4.0/).

] 1[
 𝑢 : 𝑥 : entity ′𝑣 :
wolf(𝑥)
[]
1comein(𝜋1 (𝑢)) 𝜎:Ψ..
 𝑢 : 𝑥 : entity .
𝑣 : ⟨Ψ⟩ wolf(𝑥)[]𝑧 : entity comein(𝜋1 (𝑢)) ′′(𝜋1 𝜋1 (𝑣 ), 𝑓 (𝜋1 (𝑣 ))) :¬ human(𝑧)[]( 𝑝𝑜𝑠𝑠 )𝑧 : entity′′⟨ 𝜎, (𝜋1 𝜋1 (𝑣 ), 𝑓 (𝜋1 (𝑣 ))) ⟩ :poss ⟨Ψ⟩¬ human(𝑧)[]𝑧 : entity′′′𝑙𝑒𝑡𝑑𝑖𝑎( 𝑣, ⟨Ψ, 𝑣 ⟩.⟨𝜎, (𝜋1 𝜋1 (𝑣 ), 𝑓 (𝜋1 (𝑣 )))⟩ ) :poss ⟨Ψ⟩¬ human(𝑧)( ◇ 𝐸 ), 1

図 9 前件のモダリティが possibility である場合の証明探索結果§ 2 で述べた流れと同様に，まずは型検査を行う．

探索した証明項は型検査の証明図に代入される．

意味表示の型が type であるという制約を満たすかど

未指定型に伴う変項 𝑤 が再帰的に置き換えられた結うか調べるため，図 5 の証明図を下から追う．最下果，2 文目の代名詞 it の具体的な指示対象が判明し，段は，意味合成で得られた意味表示から，(Σ𝐹) によ

図 10 の意味表示を得る．Modal DTS による照応解り取り出された，第二要素にあたる 2 文目の意味表

決は，以上である．前件のモダリティが necessity の示である．DTT において，Σ 型の意味表示全体の型場合は，付録 (A) を参照されたい．

を type とするには第一要素と第二要素の型がそれぞれ type でなくてはならない．
ここから，§ 3.3 で新たに追加した規則群を適用する．1 文目のモダリティ might は，◆ として 2 文目に作用しており，この ◆ が (◆ 𝐹) の適用で「 1 文目のモダリティが 2 文目の証明で使用できる条件」にあたる poss ⟨Ψ⟩ を与える．(□ 𝐹) と (◇ 𝐹) により，][ 𝑢 : 𝑥 : entity wolf(𝑥) 𝑣: ⟨Ψ⟩  comein(𝜋1 (𝑢)) [Ψ] ◆Ψgrowl( 𝑙𝑒𝑡𝑑𝑖𝑎(𝑣, ⟨Ψ, 𝑣 ′ ⟩.⟨𝜎, 𝜋1 𝜋1 (𝑣 ′ )⟩) )⟨Ψ⟩
図 102 文目の意味表示からモダリティ部分を分けられた












照応解決結果後，@型の推論規則である@規則を適用する．図 5の証明図より，poss ⟨Ψ⟩ 環境下において「何らかのentity z が ¬ human (z) である」という型の証明項が存在すれば，型検査は全体の意味表示の型が type でおわりに5

本研究は，様相型である possibility と necessity をDTS に加え，拡張した枠組みとして，Modal DTS をあるという制約を満たす．
証明探索を行なった結果が図 9 である．2 文目は提案した．拡張にあたり，CMTT から一部の規則1 文目に依存して良いことから，1 文目の意味表示群を採用した．さらに，Modal DTS を用いて Modalが利用できる．また，CMTT から採用した (◇ 𝐸) は

Subordination を対象とした分析を与え，モダリティモダリティが外れた 1 文目の意味表示を仮定する役を伴う照応の解決過程を示した．

割を担い，poss 規則は poss ⟨Ψ⟩ 環境に作用する．その結果，§ 2 で説明した，モダリティを含まない証今後の課題は，まず Modal DTS の様相論理としての形式的性質を明らかにすることが挙げられる．ま明探索に帰着する．つまり，Π と Σ の規則のみを使た，形式意味論では，動的意味論をはじめとして数用して「何らかの entity z が ¬ human (z) である」と多くの理論が Modal Subordination の分析を与えておいう型の証明項を探索すれば良い．その際，「 wolfり，これらの理論と Modal DTS の経験的な比較を行ならば human でない」という情報を関数 𝑓 として，う必要がある．さらに，Modal Subordination 以外の文脈に用いる．ドット (.) は，CMTT の記法であり，モダリティを伴う言語現象について，本分析が拡張

左右でスコープを分ける．

できるかどうかも検討を要する．

― 411 ―

This work is licensed by the author(s) under CC BY 4.0(https://creativecommons.org/licenses/by/4.0/).

謝辞
本研究は，JST CREST JPMJCR20D2，および JSPS科研費 JP23H03452 の助成を受けたものである．

参考文献[1] Daisuke Bekki and Koji Mineshima. Context-passing andunderspeciﬁcation in dependent type semantics. In Stergios Chatzikyriakidis and Zhaohui Luo, editors, Studiesof Linguistics and Philosophy, pp. 11–41. Springer International Publishing, 2017.
[2] Per Martin-Lö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 andmodal subordination. In Journal of Semantics, Vol. 22,
pp. 281–305. Oxford University Press, 2005.
[5] Nicholas Asher and Eric McCready. Were, would, might anda compositional account of counterfactuals. In Journal ofSemantics, 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 weakcrossover. 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.

― 412 ―

This work is licensed by the author(s) under CC BY 4.0(https://creativecommons.org/licenses/by/4.0/).

付録
A

前件のモダリティが necessity である場合の照応解決[] 𝑢 : 𝑥 : entity 
 𝑣: [Ψ] wolf(𝑥) comein(𝜋1 (𝑢)) 


[]


𝑧 : entity


[Ψ]
𝑤@
 ■Ψ
¬ human(𝑧)  ⟨Ψ⟩   growl(𝜋1 (𝑤))
図 11[]
 𝑢 : 𝑥 : entity 
 𝑣: [Ψ] wolf(𝑥) comein(𝜋1 (𝑢)) 
 ■Ψ [Ψ] growl( 𝑙𝑒𝑡𝑏𝑜𝑥(𝑣, 𝑣 ′ .(𝜋 𝜋 (𝑐𝑙𝑜(𝑣 ′ , 𝜎))) ) 1 1
⟨Ψ⟩


図 12

照応解決前の意味表示

1𝜎:Ψ
..
[]
.
𝑧 : entity[]: type
𝑧:entity¬ human(𝑧)𝑡𝑟𝑢𝑒¬ human(𝑧)[] 𝑤@ 𝑧 : entity : type¬
human(𝑧) growl(𝜋1 (𝑤))


[]

𝑧 : entity[Ψ]  𝑤@
¬ human(𝑧)  : type⟨Ψ⟩ growl(𝜋1 (𝑤))[]𝑧:entity
[Ψ]  𝑤@¬ human(𝑧)  : type■Ψ⟨Ψ⟩  growl(𝜋1 (𝑤))
..
.

..
.
Ψ : type

照応解決後の意味表示(@)( □ 𝐹)( ◇ 𝐹)( ■ 𝐹 ), 1

図 13 前件のモダリティが necessity である場合の型検査2[] 𝑢 : 𝑥 : entity 1 [Ψ]wolf(𝑥)𝑣 ′ :: 𝜎:Ψ comein(𝜋1 (𝑢)) 

[][]


𝑥:
entity𝑥: entity  𝑢:𝑢:
wolf(𝑥)wolf(𝑥)𝑣 : [Ψ] 𝑐𝑙𝑜(𝑣 ′ , 𝜎) :  comein(𝜋1 (𝑢))  comein(𝜋1 (𝑢)) ..
.
[]𝑧 : entity( 𝜋1 𝜋1 (𝑐𝑙𝑜(𝑣 ′ , 𝜎)), 𝑓 (𝜋1 (𝑐𝑙𝑜(𝑣 ′ , 𝜎))) ) :¬ human(𝑧)[]𝑧:entity′′′𝑙𝑒𝑡𝑏𝑜𝑥( 𝑣, 𝑣 .(𝜋1 𝜋1 (𝑐𝑙𝑜(𝑣 , 𝜎)), 𝑓 (𝜋1 (𝑐𝑙𝑜(𝑣 , 𝜎)))) ) :¬ human(𝑧)図 14( 𝑐𝑡 𝑥ℎ𝑦 𝑝 )( □ 𝐸 ), 2

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

This work is licensed by the author(s) under CC BY 4.0(https://creativecommons.org/licenses/by/4.0/).