動的意味論における上書き問題
理学専攻・情報科学コース
はじめに1るため、Kamp and Reyle (1993) によって提案された DRTを Classical DRT と呼ぶ。
λ-DRT などの拡張された DRT は、各語にラムダ式を用いた意味表示を与え、それらを組み合わせることで文の DRSを獲得する。最終的に構築される DRS は等しく、合成性を満たしたまま Classical DRT と同等の分析を行える。

形式意味論は、文の意味をどう定義するかによって、大きく二つに分類することができる。一つは、モデルの下で評価される真理条件を文の意味とするモデル論的意味論、もう一つは、その文が正しいと判断するために必要な証拠とその推論過程を文の意味とする証明論的意味論である。
モデル論的意味論の中で、E タイプ照応などの動的な現象を取り扱うよう設計された理論としては、談話表示理論 (DRT, Discourse Representation Theory; (Kamp andReyle 1993)) や動的述語論理 (DPL, Dynamic PredicateLogic; (Groenendijk et al. 1996)) などが挙げられる。証明論的意味論では、依存型理論 (DTT, Dependent Type Theory; (Martin-Löf 1984)) を用いてそれらの現象を分析する試みがいくつか提案されている。
上に挙げた理論のうち、DPL と DRT は、Groenendijket al. (1996) で述べられている通り、経験的に等価であることが知られている。また、Ahn and Kolb (1990), Fernando(2001) では、DRT と依存型による分析は同等のものであり、交換可能であると述べられている。このことから、DRT,DPL と依存型による分析は等価な理論であり、各言語現象について同様に振るまうように思われる。
本稿では、意味表現の導出過程や理論の振るまいについて、これらの動的意味論と依存型による分析が異なるものであることを主張する。

DPL は、Groenendijk and Stokhof (1991) によって提案された動的意味論で、割り当て関数のペアを用いて一階述語論理の式を評価する理論である。また、量化動的論理 (QDL,Quantificational Dynamic Logic;(Harel 1984)) の言語を用いて一階述語論理の式を書き換えることもでき、その式を解釈しても結果は変わらないことが保証されている。本稿
では書き換えた後の式を DPL 式と呼ぶ。
以下に DPL で使用する言語の定義を示す。
Definition 1 (DPL 言語).
(i) 変項を v, 定項を c とすると、項 t は以下の通り：
t ::= c|v(ii) n 項述語を P とすると、原子式 A は以下の通り：
A ::= ∃v|P t1 ...tn(iii) 複合論理式 ϕ は以下の通り：
ϕ ::= A|A; ϕ|¬(ϕ)|¬(ϕ1 ); ϕ2
これらの式は、以下のように解釈される。
Definition 2 (割り当て関数による解釈). af を入力の割り当て関数、g を出力の割り当て関数とする：
f [[P (x1 , ..., xn )]]g ≡ f = g ∧ (f (x1 ), ..., f (xn )) ∈ I(P )f [[∃x]]g ≡ f [x]gf [[¬ϕ]]g ≡ f = g ∧ ¬∃h f [[ϕ]]hf [[ϕ; ψ]]g ≡ ∃h f [[ϕ]]h[[ψ]]g
これらの定義を用いることで、自然言語の文から DPL 式までは以下のように変換される。

本章では、形式意味論の中で、動的な現象を扱うものを紹介する。動的意味論の中から談話表示理論 (以下, DRT)と動的述語論理 (以下, DPL) を、依存型を用いた分析から依存型意味論 (Dependent Type Semantics(Bekki andMineshima 2017), 以下 DTS) を取り上げる。

2.1

談話表示理論 / DRT

DRT は、Kamp and Reyle (1993) によって提案された、Discourse Representation Structure (以下, DRS) と呼ばれる箱型の意味表示を持つ動的意味論である。以下に、自然言語の文と意味表示である DRS の対応を示す。
(1)

(2)

a. A man read a book.
b. ∃x∃y(man(x) ∧ book(y) ∧ read(x, y))c. ∃x; ∃y; man(x); book(y); read(x, y)
依存型意味論 / DTS

2.3

a. A man read a book.

DTS は、Bekki and Mineshima (2017) によって提案された証明論的意味論であり、依存型理論を用いた分析の一つである。DTS は Π 型と Σ 型を持ち、主にこの 2 つの型を用いて意味表示を構築する。Π 型は関数型に、Σ 型は直積型に対応している。以下に、自然言語の文と意味表示の対応を示す。

xyb.

動的述語論理 / DPL

2.2

動的な現象を扱う形式意味論2

簗有紀子

man(x)book(y)read(x,y)(1b) の上段にある変数 x, y のことを談話指示子と呼び、下段にある述語 man(x), book(y), read(x,y) を条件と呼ぶ。
DRS は談話指示子の集合と条件の集合のペアによって構成される。この DRS は、述語 man を満たす談話指示子 x と述語 book を満たす談話指示子 y が存在し、それらの談話指示子が述語 read の関係にあることを表している。
DRT は合成性の原理を満たさないことで知られている。
合成性の原理を満たすように拡張された DRT として、Compositional DRT (Muskens 1996, Haug 2013), Relational
DRS による拡張 (van Eijck and Kamp 1997, van Eijck
2001), λ-DRT (Bos et al. 1994, Kohlhase et al. 1995) などが挙げられる。以降、これらの拡張された DRT と区別す

(3)a. A man read a book.

[] x : entity
v:
man(x) u: [] y : entity
book(y)read(π1 π1 u, π1 π2 u)b.

3

動的意味論の問題点

3.1

上書き問題

合成性を満たすよう拡張された DRT では、以下の定義に沿って DRS 同士を結合する。

1

Definition 3 (DRS 同士の結合). a
K1 = (U1 , Con1 ), K2 = (U2 , Con2 ) を DRS とする：
K1 ; K2 = (U1 ∪ U2 , Con1 ∪ Con2 )しかしこの定義では、同じ名前の談話指示子 y を持つ DRS同士を結合する以下のような場合に、それらが同一視されてしまうという問題が生じる。これを上書き問題と呼び、この問題は Zeevat (1989) によって指摘された。
(4)

DTS ではこれら二つの問題は生じないのだが、本節ではその理由を述べていく。
DRT や DPL は個体を表すのに変数を用いており、変数名を用いてそれらを識別していた。しかし DTS はそれらを意味表示内の位置で識別するため、変数の衝突は起こらない。このため、例え分配読みであっても正しい意味表示を導出することができ、上書き問題は生じ得ない。
また DTS は、動的意味論のような束縛ではなく単純型付
きラムダ計算と同様の束縛方法を採用している。そのため、関数適用によって変数がコピーされても束縛状態は保たれる。以下がその例である。

xyz

xyyz

P(x)
Q(y)
R(y,z)=
P(x) ;
R(y,z)Q(y)λ-DRT などの拡張された DRT はこの問題に対応すべく様々な定義を導入している。これによって一見この問題は解決したかに思えたが、Yana et al. (2017) によって分配読みの文 (5) ではこの問題が生じてしまうことが指摘された。
(5)

(9)

Bill and Sue own a donkey.

4a. x; ∃x; P (x)c. x; ∃x; P (x); ∃x; Q(x)Vermeulen (1993) は、値がシーケンスの割り当て関数を採用し、これを解決しようとした。この拡張によって確かに情報は失われず保全されるが、シーケンス内の情報を自由に取り出すことはできないため、このような状況で正しく照応解決を行うことはできない。よって、この拡張においても依然として問題は解決していない。
複製問題

(7)

a.

...
x...

⇒René Ahn and Hans-Peter Kolb. Discourse representation meets constructive mathematics. In Papers from the Second Symposium onLogic and Language. Akademiai Kiado, 1990.
Daisuke Bekki and Koji Mineshima. Context-passing and underspecification in Dependent Type Semantics. In Modern Perspectives in Type
Theoretical Semantics, pages 11–41. Springer, 2017.
Johan Bos, Elsbeth Mastenbroek, Scott Mcglashan, Sebastian Millies,
and Manfred Pinkal. A compositional DRS-based formalism for NLP
applications. In In International Workshop on Computational Semantics, pages 21–31, 1994.
Tim Fernando. A type reduction from proof-conditional to dynamic
semantics. Journal of Philosophical Logic, 30(2):121–153, 2001.
Jeroen Groenendijk and Martin Stokhof. Dynamic predicate logic. Linguistics and Philosophy, 14(1):39–100, 1991.
Jeroen Groenendijk, Martin Stokhof, and Frank Veltman. Coreferenceand modality. In The Handbook of Contemporary Semantic Theory,pages 179–216. Blackwell, 1996.
David Harel. Dynamic Logic, pages 497–604. Springer Netherlands,Dordrecht, 1984.
Dag T. T. Haug. Partial dynamic semantics for anaphora: Compositionality without syntactic coindexation. Journal of Semantics, 31:
274–294, 2013.
Hans Kamp and Uwe Reyle. From Discourse to Logic: Introduction
to Model-theoretic Semantics of Natural Language, Formal Logic andDiscourse Representation Theory. Springer, 1993.
Michael Kohlhase, Susanna Kuschert, and Manfred Pinkal. A TypeTheoretic Semantics for lambda-DRT. In Proceedings of the TenthAmsterdam Colloquium, pages 479–98, 1995.
Per Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984.
Reinhard Muskens. Combining Montague semantics and discourse representation. Linguistics and Philosophy, 19:143–186, 1996.
Jan van Eijck. Incremental dynamics. Journal of Logic, Language andInformation, 10(3):319–351, 2001.
Jan van Eijck and Hans Kamp. Representing discourse in context. In
Johan van Benthem and Alice ter Meulen, editors, Handbook of Logicand Language. MIT Press, 1997.
C. F. M. Vermeulen. Sequence semantics for dynamic predicate logic.
Journal of Logic, Language and Information, 2(3):217–254, 1993.
Yukiko Yana, Daisuke Bekki, and Koji Mineshima. Variable handling:
DRT and DTS. submitted, 2017.
Henk Zeevat. A compositional approach to discourse representation
theory. Linguistics and Philosophy, 12:95–131, 1989.

...
P ...
 Q(x)P∨B...
xb.

...

⇒...
Q(x)

(8)

まとめ参考文献

関数適用の際に変数が複数箇所にコピーされ、それらの束縛状態が異なってしまうことを複製問題と呼ぶ。この問題は Kohlhase et al. (1995) によって指摘された。(7) は DRTの、(8) は DPL の例である。
λP.

[]
x:A[]u:D(y : B) → P 
E(y)P ∨C

x:A[] 
 (w : B) → u : D

E(y)


[]  u:D∨CE(y)

本稿では、二つの問題を通じて、DRT や DPL の分析とDTS の分析が等価ではないことを示した。
DRT や DPL は代入や α 変換などの操作について、一階述語論理などの通常の論理とは異なる独自の定義を採用しており、これが上書き問題や複製問題の一因となっている。
だが、DRT や DPL が動的な束縛によって照応解決を行う限り、そのような特殊な定義を採用することは避けられない。
一方 DTS では、代入や α 変換などの操作は通常の論理と同様に振る舞う。DTS は照応解決に証明探索を用いるため、動的に束縛する必要はないからである。

b. ∃x; Q(x)3.2a. λP. b.

上書き問題は DRT に対して指摘されたものだが、DPL でも同様の状況が考えられる。(6a) と (6b) を結合すると (6c)の式が得られるが、中央の x の情報は失われている。

(6)

DTS における二つの問題

3.3...
Q(x)∨B

a. (λP.¬(∃x; P ); P ) Q(x)b. ¬(∃x; Q(x)); Q(x)(7) と (8) のどちらにおいても引数の中にある x は自由変数だが、関数適用後は、前方の x は束縛され後方の x はそのまま、という束縛状態のズレが生じている。
このズレは関数適用と解釈の順序に大きな影響を与える。
具体的には、(7b) は (7a) を β 簡約したものなので意味的に等しいはずだが、(7b) と (7a) を解釈すると異なる意味になる。本来であれば関数適用と解釈は順序に依らず結果が変わらないはずなので、このような状況は望ましくない。

2