Representing Generalized Quantifiers and Modalities
in Dependent Type Semantics
理学専攻・情報科学コース

1

はじめに自然言語の一般化量化子やモダリティは、形式意味論においてモデル論的な枠組みで盛んに研究されてきた。
一方、依存型理論 (Martin-Löf 型理論 [2], 以降 MLTT)
による自然言語の分析が発展してきている [5, 3, 1]。
MLTT は形式意味論で従来標準的であった単純型理論を拡張した体系で、その高い表現力により、これまで適切な扱いが困難であった照応・前提現象の分析に成功している。この枠組みではモデルを参照せずに直接文間の含意関係を計算できることから、近年では Coqなどの定理証明支援系を用いた意味処理も試みられている。しかし MLTT による個々の言語現象の分析は、まだ非常に少ないのが現状である。そこで本研究では、
依存型意味論 (以降 DTS)[1] の枠組みを採用し、英語の量化表現 most とモダリティ表現 might/would に意味表示を与えた。

2依存型意味論 (DTS)DTS は MLTT に基づく自然言語の意味論である。
単純型理論に対する MLTT の特徴的な点は、型が項に依存しうることである。たとえば、項 n : N の値に依存する長さ n のリストの型として、List(n) という型を考えることができる。また、MLTT は型構成子 Π, Σをもつ。型 (Πx : A)B(x) は関数型の一般形であり、型と項に依存関係がない場合は A → B と同一視される。
型 (Σx : A)B(x) は直積型の一般形であり、依存関係がない場合は A × B と同一視される。Curry-Howard
対応（型＝命題、項＝証明）より、型 (Πx : A)B(x) は全称量化 (∀x : A)B(x) と、型 (Σx : A)B(x) は存在量化 (∃x : A)B(x) と見なせる。
DTS はこの体系を @ オペレータで拡張し、自然言語における照応・前提現象の説明を可能にしたものである。DTS における文の意味表示の例を示す。ただし型 E は個体の型 Entity の略記である。
(1)

a. A man entered.
b. (λc)(Σv : (Σx : E)Man(x))Enter(π1 v)(2)a. Every man entered.
b. (λc)(Πv : (Σx : E)Man(x))Enter(π1 v)(1b) や (2b) のような関数的な命題は動的命題と呼ばれ、その返り値である静的命題と区別される。動的命
題は前方談話の静的命題の証明項（local context 、以下コンテキスト）を引数として受け取る。与えられたコンテキストのもとで得られる静的命題は、文の真偽と関係づけられる。すなわちある文が特定の文脈で真であるとは、与えられたコンテキストの下でその文の意味表示である静的命題に証明が存在するとき、つまり静的命題に対応する型に証明項が存在するときまたそのときのみであるとされる。
コンテキストは、文に照応表現や前提トリガが出現した際に参照される。以下に、照応表現である代名詞

田中 リベカを含む文の意味表示を示す。

(3)

a. He smiled.
b. (λc)Smile(@γ→E (c))

ただし変数 γ はコンテキスト c の型を表すものとする。
項 @γ→E はコンテキストを受け取り個体を返す関数であり、型は γ → E である。
談話の意味表示は、動的連言によって構築される。
def

M ; N ≡ (λc)(Σu : M c)N (c, u)
これより、(1a)(3a) の 2 文からなる談話の意味表示は(4) のように記述される。
(4) (λc)(Σu : (Σv : (Σx : E)Man(x))′Enter(π1 v))Smile(@γ →E (c, u))@ オペレータの型の γ ′ を推定し、型 γ ′ → E をもつ
具体的な項を構成して置換する操作が照応解決に対応する。ここではたとえば項 (λc)π1 π1 π2 (c) を構成することが可能であるため、代名詞 he が a man を指すような意味表示が得られる。

3

量化表現 most
量化表現 most は次のような多様な振る舞いを示す。

• 内的に動的である• 存在に関する前提をもつ• ロバ文が weak/strong reading をもつ• 保存性・右上方単調性をもつ
これに加え、素朴な分析では proportion problem が起こることが指摘されている。Sundholm (1989) は
MLTT の枠組みで量化子 most の意味表示を与えており、この問題を回避する定式化を提案している [6]。しかし一方で、proportion problem が起きない代わりに定義の統一性が欠如してしまうという問題があった。
また、most のもつ照応や前提に関する性質までは意味表示に反映されていなかった。
本研究では、上記の問題を解決する意味表示を与えた。Weak reading の際の意味表示を示す。
[[mostweak ]](A, B) =γ→|(Σx:E)Axc|≥1(c))+1(λc)(Σk : N)(k ≥ [ π1 (@]+1 ∧2(Σf : M (k) → (Σx : E)Axc)(E-injection(f )∧(Πz : (Σx : E)Axc)((Σy : M (k))eq((Σx : E)Axc, z, f y)
↔ B(π1 z)(c, z))))[ ] や M の定義は [6] に従う。また | | や ≥, E-injectionの定義は [7] を参照。
DTS における名詞句の扱いでは定義の統一性の問題は回避されるため、上記の意味表示では統一性を保ちつつ proportion problem を回避することに成功している。また、コンテキストの受け渡しを考慮することで内的に動的となっており、ロバ文内部の照応も説明される。さらに、@ オペレータによって存在に関する前提を記述している。most の前件部の名詞句が指す集合は空でないという前提が、@ の型として記述されている。これらの振る舞いを保持したまま、strongreading に対応する意味表示も同様に与えられる。
また most の意味表示をもとに、more than n, atleast n, n, exactly n, fewer than n (ただし n は threeなどの数を表す単語) の意味表示を与えた。このうち、at least n と n は同じ真理条件をもつが、照応に関する振る舞いが異なることが指摘されている。以下の例
で部屋に 15 人の子どもが入っていったという状況を考えると、前者では代名詞 they が 15 人全員を指示するのに対し、後者では 10 人の子どもを指示する。本
研究で与えた意味表示では、このような照応に関する振る舞いの違いも記述されている [8]。

(5) [At least ten kids/Ten kids]i walked into theroom. Theyi were making a lot of noise.
さらにこれらの量化表現について、与えた意味表示が保存性や単調性を満たすことを証明した。以下に保存性の定義を示す。
定義 任意の A, B : (Πx : E)(Πc : γ)type について, 与えられたコンテキスト c のもとで量化表現 Q が保存的であるとは、以下が成立することである：
Q(A, B)c に証明項が存在する ⇐⇒Q(A, (λx)(Ax; Bx))c に証明項が存在する

4

様相表現 might/would

様相表現 might/would の意味表示を与えるに際し、様相従属 [4] という現象に注目した。様相従属はモダリティが照応に影響を及ぼす現象である。

(6) [A wolf]i entered. Iti growled.
(7) [A wolf]i might enter. #Iti growled.
(8) [A wolf]i might enter. Iti would growl.
(6) では、2 文目の代名詞 it が 1 文目の名詞句 a wolfを指示しうるが、(7) のように 1 文目に様相表現が出現するとこの照応は許されない。一方、(8) のように後続文にも様相表現が出現した場合は (6) と同様、代名詞 it は a wolf を指示しうる。ここで、(8) の 2 文目は以下のような意味をもつとされている。
(9) If [a wolf]i entered, iti would growl.
前件部の命題は、前方で様相表現を伴って導入された命題である。2 文目の意味を正しく解釈するためには前件部の命題を補う必要があるため、ここでは照応として分析する。
DTS で様相表現の意味を記述するにあたり、可能世界の概念を導入する。W を世界の型とし、動的命題をw : W とコンテキスト c を受け取り静的命題を返す関数とする。また、個体の型 E を世界に依存する型 Ew として再定義し、述語についても Man : (Πw : W)(Ew →type) などとする。また、認識的到達可能性関係を Repiとする。これにより、可能性/必然性はそれぞれ以下のように定義される。

♢Mdef

≡

(λwc)(Σw′ : W)(Repi ww′ ∧ M w′ c)

□M

def

(λwc)(Πw′ : W)(Repi ww′ → M w′ c)≡

また、動的連言と動的含意を以下のように定義する。

M ;NM ▷Ndef

≡

def

≡

(λwc)(Σu : M wc)N w(c, u)(λwc)(Πu : M wc)N w(c, u)

これらを用いて、様相表現 might/would の意味表示を以下のように与える。

[[might]](A) = (λwc)(♢(↓ (@i c) ; A)wc∧(ΣP : κb)(↓ P =κ ↓ (@i c) ; A))[[would ]](A) = (λwc)(□(↓ (@i c) ▷ A)wc∧(ΣP : κb)(↓ P =κ ↓ (@i c) ; A))
ただし、κ は W → γ → type の、κ
b は W → γ → rpropの略であり、rprop は type の部分型である。また、↓ (·)
はκ
b 型の命題を κ 型の命題へと対応づける関数であり、@ の型 γ → κb は省略している。
この意味表示から (8) のような照応解決が可能である。また、個体の型を世界 W 型の項に依存する型としたことにより、(7) の照応は正しく失敗する [9]。

5まとめ

本研究では、依存型意味論の枠組みで量化表現 mostと様相表現 might/would の意味表示を与えた。いずれも照応・前提や推論など複数の側面をとらえた意味記述を行った。また、可能世界に関する記述を行うために枠組みの拡張を行った。
本研究で扱った現象は、形式意味論で研究されてきた一般化量化子やモダリティの振る舞いの一部である。
たとえば most に関しては、more than half との意味の違いや不可算名詞に対する量化なども問題とされる。
より多様な現象に対応した意味表示への拡張は、今後の課題とする。

参考文献[1] Bekki, D.: Representing Anaphora with Dependent Types, In LACL2014 (2014)[2] Martin-Löf, P.: Intuitionistic Type Theory, Bibliopolis Naples (1984)[3] Ranta, A.: Type-Theoretical Grammar, Oxford
University Press (1994)[4] Roberts, C.: Modal Subordination and Pronominal Anaphora in Discourse, Linguistics and Philosophy (1989)[5] Sundholm, G.: Proof Theory and Meaning, In
Handbook of Philosophical Logic (1986)[6] Sundholm, G.: Constructive Generalized Quantifiers, Synthese (1989)[7] Tanaka, R., Nakano, Y., Bekki, D.: Constructive Generalized Quantifiers Revisited, In
LENLS10 (2013)[8] Tanaka, R.: A Proof-Theoretic Approach toGeneralized Quantifiers in Dependent Type Semantics, In ESSLLI2014 Student Session (2014)[9] Tanaka, R., Mineshima, K., Bekki, D.: Resolving Modal Anaphora in Dependent Type Semantics, In LENLS11 (2014)