依存型意味論によるモダリティと照応の統一的分析に向けて
飯村 葵（指導教員：戸次大介）
はじめに1

DTS に新たに追加する規則群は 3 種類に分けられる．
CMTT の構造規則，◇ と □ に関する規則，◆ と ■ に関する規則である．CMTT の構造規則は，ContextualPossibility に由来する poss 規則，hypothetical judgement に由来する hyp 規則，Contextual Validity に由来する ctxhyp 規則である．◇ と □ に関する規則は，形成則を新たに作成し，導入則と除去則を CMTT から取り入れる．◆ と ■ に関する規則は，Modal DTSにおいて独自に定義したものである．

自然言語には様々な言語現象が存在しており，形式意味論では数多くの理論が分析を与えてきた．そのような理論の一つに，本研究で採用する，依存型意味論(dependent type semantics, DTS)[1] がある．DTS は依存型理論 (dependent type theory, DTT)[2] に基づく自然言語の意味論である．本研究は，DTS により，様相 (modality) の分析を試みる．DTS は，照応など複雑な言語現象を扱う理論だが，モダリティとの関係に着目する研究はあまりなされていない．
本稿が対象とする modal subordination は，モダリティを伴う談話における照応現象であり，Roberts [3]により指摘された．modal subordination の例を (1)(2)に示す．

(1)

A wolf might come in. #It growls.

(2)

A wolf might come in. It would growl.

提案手法

2.1

Modal DTS

Modal DTS による分析

3.1

談話関係

□
M2
◇□
□ M1 ;
M2◇◇ M1 ;

≡≡

□
M2
◇
□
□ M1 × ■M2◇◇ M1 × ◆図 1: Modal DTS における談話関係

3.2

分析例

本稿では分析例として，図 1 上段の規則を取り上げる．これは，前件が possibility の場合であり，具体的に以下の 2 文を対象とする．ここでは，意味表示における後件のモダリティをまとめて，図 2 のように扱う．
π1 は組の第一要素を取り出す操作である．

Modal DTS は，既存の依存型に possibility と necessity の型を加えた体系である．新たに定義される型
は，possibility に対応する ◇ (dia) と ◆ (bkdia)，necessity に対応する □ (box) と ■ (bkbox) が該当する．
might や would のようなモダリティは，◇ と □ により表される．◆ と ■ は 2 文目の意味表示に作用し，「1文目のモダリティ内の命題の証明が，2 文目の証明で使用できる条件」を与える役割を担う．
2.2

3

modal subordination は，対象の 2 文が図 1 に示す談
話関係に入ることで初めて可能となる．記号を縦に並べた記法は，複数の規則を纏めたものである．1 文目と2 文目にモダリティを伴うことが，談話関係に入る形式的な条件のため，(1) のように後件にモダリティを含まない場合や 2 文が離れる場合は，modal subordinationが起きることはない．

モダリティを伴う談話では，E タイプ照応 [4] が到達可能ではなくなることがある．たとえば，(1) では，代名
詞 it が E タイプ照応の先行詞として a wolf を指すこ
1とはできない．
一方，2 文目にモダリティ would を加えた (2) では，would の使用により，前半の文で might のスコープ内に導入された a wolf を，代名詞 it が E タ
イプ照応の先行詞として参照できる．
本研究は，DTS による modal subordination の分
析を念頭に，モダリティと照応を同時に扱うことができるよう，様相型である可能性 (possibility) と必然性(necessity) を DTS に加え，拡張した体系として ModalDTS を提案する．照応の理論である DTS の特徴を活かし，一般的な照応解決 (anaphora resolution) に還元することを目指す．

2

規則群

2.3

(2)

A wolf might come in. It would growl.

(3)

A wolf might come in. It might growl.
] x : entity v: ⟨Ψ⟩
wolf(x)
comein(π(u))
]  [ 1z:entity ◆Ψ [Ψ]  w@ ¬ human(z)  ⟨Ψ⟩
growl(π1 (w))


[ u:

図 2: 照応解決前の意味表示

Contextual Modal Type Theory

Modal DTS の ◇ と □ は，Contextual Modal Type
2Theory (CMTT)[5] の定義に従う．
CMTT は，直観主義様相論理 (Intuitionistic Modal Logic) に対して，構成的な手法で possibility と necessity に意味の説明を与える理論である．◇ と □ の規則群を，CMTT が提案する Intuitionistic Contextual Modal Logic (ICML)と Contextual Possibility から取り入れる．

DTS は，未指定型 (underspeciﬁed type)[6] を DTTに加えることで照応解決を可能にする．文の意味表示の型は，DTT における type でなければならないという制約 (semantic felicity condition) がある．そのため，型検査 (type checking) を行うことで，この制約を満たすか調べる．型検査の過程で，未指定項@を具体的な証明に置き換える操作が，照応解決にあたる．
対象となる 2 文の型検査を図 3 に示す．前述の制約を満たすか調べるため，図 3 の証明図を下から追う．

1 文頭に置かれた「#」は続く文が不適切であることを示す
2 付録 (C) を参照されたい

1

[..
.
Ψ : type poss ⟨Ψ⟩..
.
z : entity]¬ human(z)[[: typez : entity

z : entity¬ human(z)] ..
.]poss ⟨Ψ⟩ true w@
¬ human(z)  : type poss ⟨Ψ⟩growl(π1 (w))[] z : entity[Ψ]  w@¬ human(z)  : type poss ⟨Ψ⟩⟨Ψ⟩growl(π1 (w))[] z : entity[Ψ]  w@◆Ψ¬ human(z)  : type⟨Ψ⟩
growl(π1 (w))(@)( □ F )
( ◇ F )

( ◆F )

図 3: 前件のモダリティが possibility である場合の型検査
最下段は，図 2 に示した照応解決前の意味表示で第二要素にあたる 2 文目の意味表示である．DTT において，Σ 型の意味表示全体の型を type とするには，第一要素と第二要素の型がそれぞれ type でなくてはならない．1 文目のモダリティ might は，◆ として 2 文目に作用しており，この ◆ が (◆ F ) により「 1 文目のモダリティが 2 文目の証明で使用できる条件」にあたる poss ⟨Ψ⟩ を与える．(□ F ) と (◇ F ) により，2文目の意味表示からモダリティ部分を分けられた後，@型の推論規則である@規則を適用する．図 3 の証明
図より，poss ⟨Ψ⟩ 環境下において「何らかの entity zが ¬ human (z) である」という型の証明項が存在すれば，型検査は全体の文の意味表示の型が type であるという制約を満たす．
証明探索を行った結果は，付録 (A) を参照されたい．
2 文目は 1 文目に依存して良いことから，1 文目の意味表示が利用できる．また，CMTT から採用した (◇ E)
はモダリティが外れた 1 文目の意味表示を仮定する役割を担い，poss 規則は poss ⟨Ψ⟩ 環境に作用する．その結果，モダリティを含まない一般的な証明探索に帰着する．つまり，依存型の規則のみを使用して「何らかの entity z が ¬ human (z) である」という型の証明項を探索すれば良い．その際，「wolf ならば human でない」という情報を関数 f として文脈に用いる．ドット (.) は，CMTT の記法であり，左右でスコープを分ける．
探索した証明項は型検査の証明図に代入される．未指定型に伴う変項 w が再帰的に置き換えられた結果，2 文目の代名詞 it の具体的な指示対象が判明し，図 4の意味表示を得る．Modal DTS による照応解決は，以上である．前件のモダリティが necessity の場合は，付録 (B) を参照されたい．
[] x : entity v: ⟨Ψ⟩  u : wolf(x)comein(π1 (u))
[Ψ]◆Ψgrowl( letdia(v, ⟨Ψ, v ′ ⟩.⟨σ, π1 π1 (v ′ )⟩) )
⟨Ψ⟩

4

おわりに

本研究は，様相型である 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 underspeciﬁcation in dependent type semantics.
In Stergios Chatzikyriakidis and Zhaohui Luo, editors, Studies of Linguistics and Philosophy, pp. 11–41.
Springer, 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] Gareth Evans. Pronouns. Vol. 11, pp. 337–362. 1980.
[5] Frank Pfenning Aleksandar Nanevski and Brigitte
Pientka. Contextual modal type theory. In ACM
Transactions on Computational Logic, Vol. 9, pp. 1–49. 2008.







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

図 4: 照応解決後の意味表示

2

付録

A

前件のモダリティが possibility である場合の証明探索]  1
x : entity
wolf(x)v′ :comein(π(u))
1[] 
1σ:Ψ
x : entity..
u:. [wolf(x)v : ⟨Ψ⟩ ]z : entity
comein(π1 (u))′′(π1 π1 (v ), f (π1 (v ))) :¬ human(z)[]( poss )z : entity⟨ σ, (π1 π1 (v ′ ), f (π1 (v ′ ))) ⟩ :poss ⟨Ψ⟩¬ human(z)[]z : entity
letdia( v, ⟨Ψ, v ′ ⟩.⟨σ, (π1 π1 (v ′ ), f (π1 (v ′ )))⟩ ) :poss ⟨Ψ⟩¬ human(z)[ u:( ◇ E ), 1

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

B

前件のモダリティが necessity である場合の照応解決
1..
.
Ψ : type

σ:Ψ..
..
.
[].
[]
z : entity: typez : entity¬ human(z)true¬ human(z)[] z : entity
 w@ ¬ human(z)  : typegrowl(π1 (w))[] z : entity[Ψ]  w@
¬ human(z)  : type⟨Ψ⟩growl(π1 (w))[] z : entity[Ψ]  w@
¬ human(z)  : type■Ψ⟨Ψ⟩
growl(π1 (w))(@)( □ F )
( ◇ F )

( ■ F ), 1

図 6: 前件のモダリティが necessity である場合の型検査2] x : entity1 [Ψ]
wolf(x)v ′ ::
σ:Ψ
comein(π1 (u))
[] 
] [
x : entity
x : entityu:u:
wolf(x)clo(v ′ , σ) : wolf(x)v : [Ψ] comein(π1 (u))
comein(π1 (u))..
.
][z : entity′( π1 π1 (clo(v , σ)), f (π1 (clo(v ′ , σ))) ) :¬ human(z)][z : entity
letbox( v, v ′ .(π1 π1 (clo(v ′ , σ)), f (π1 (clo(v ′ , σ)))) ) :¬ human(z)[ u:

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

3( ctxhyp )( □ E ), 2

CModal DTS における規則群（抜粋）

C.1

Π型
ii

x:A..
.
B : type

A : type

A : type(ΠF ),ix:A..
.
M : B

M : (x: A) → B(ΠI),i(x: A) → B : type

N :A(ΠE)

λx.M : (x: A) → B

M N : B[N/x]

Σ型

C.2

i

A : type

x:A..
.
B : type(ΣF ),i

M : (x : A) × B(ΣE)(M, N ) : (x : A) × B(ΣE)

π1 (M ) : A

π2 (M ) : B[π1 (M )/x]

CMTT の構造規則
u :: A[Ψ]..
.
σ:Ψ∆ ; (Γ, x : A, Γ′ )
(hyp)

σ:Ψ

(ctxhyp)x:A

C.4

M : (x : A) × B

N : B[M/x](ΣI)(x : A) × B : type

C.3

M :A

M :A(poss)⟨σ, M ⟩ : A poss⟨Ψ⟩clo(u, σ) : A◇型
ΨΨ ctx(◇ I)(◇ F )⟨Ψ⟩M : type

C.5

M : ⟨Ψ⟩A

E : A poss⟨Ψ⟩M : typei

x:A..
.
E : B poss⟨Θ⟩(◇ E),idia(E) : ⟨Ψ⟩Aletdia(M, ⟨Ψ, x⟩.E) : B poss⟨Θ⟩

□型i

Ψ ctx

Ψ..
.
M :A

M : type(□ F )(□ I),i[Ψ]M : type

C.6i

M : [Ψ]Au :: A[Ψ]..
.
N :C(□ E),ibox(Ψ.M ) : [Ψ]Aletbox(M, u.N ) : C

◆型i

M :◆A
M :A

M : type poss⟨Ψ⟩(◆ I)(◆ F )◆Ψ M : type

C.7

x:A..
.
N :B

(◆ E),ibkdia(M ) : ◆ A

casedx (M, N ) : B■型iiσ:Ψ
..
.
M : type(■ F ),i

M :■A
M :A(■ I)■Ψ M : typex:A..
.
N :B(■ E),ibkbox(M ) : ■ A

4casebx (M, N ) : Bi