依存型意味論の証明探索とその実装
理学専攻・情報科学コース

1

はじめに：依存型意味論と照応・前提

依存型意味論 (Dependent Type Semantics, 以下DTS)[1] は、依存型理論 (Dependent Type Theory)[4]に基づく自然言語の証明論的意味論である。文の表す命
題に依存型理論の型を対応づけており、Π 型 (x:A) →[]x:A
BとΣ型を用いることによって文脈に依存しBた文の意味を表示することができる。
DTS では、照応・前提現象を未指定項 (underspecifiedterm) によって記述する。たとえば、A man entered.
He whistled. という 2 文を組み合わせた意味表示は、以下の図 1 のようになる。図 1 中の @ が未指定項であり、]  [
x:entityu:  v: man(x) 
enter(π1 (u))[

]()

x:entity
whistle π1 (@ :)man(x)
図 1: A man enterd. He whistled. の意味表示
照応代名詞や前提トリガーなど、照応現象を引き起こす[]
x:entity
語彙項目の意味表示に含まれている。@ :man(x)[]x:entityのは、@ に対するアノテーションである。
man(x)DTS を用いて照応解決・前提束縛の計算を行う際には、大きく分けて以下の 3 つの操作が必要である。

1. 文の意味表示に対する型チェック
2. @ の型に対する証明探索
3. 証明項による @ の置き換え
1 の型チェックでは、文の意味表示に対して型チェ
ッ[]x:entityクを行うことで、@ :となるときの文脈man(x)を特定する。たとえば図1 の例ならば、型チェックを]
 [x:entityu:
行うことで v : man(x)  という文脈のもとenter(π1 (u))[]
x:entity
で、@ :であることが分かる。
man(x)
2 の証明探索では、@ の型に対して証明探索を行う
ことで @ の型に対する証明項を見つける。図1 の例な[]
x:entity
らば、@ の型であるという型を持つ項とman(x)して π1 (v) が存在し、証明探索を行うことでこの項を見つけることができる。このとき、
1 において特定し] [x:entity
u:たv : man(x)  という文脈を参照することenter(π1 (u))
ができる。

佐藤 未歩

3 は、2 で判明した証明項で文の意味表示中の @ を置き換える操作である。この操作を @-Elimination という。図 1 の例ならば、@ に対する証明項である π1 (v)で @ を置き換えることによって、図 2 の意味表示を得ることができる。
]  [x:entity  u: v: man(x)  enter(π1 (u))
whistle (π1 (π1 (v)))
図 2: @ 解消後の意味表示
このように、図 1 の意味表示から図 2 の意味表示を得ることで照応解決となる。
本研究では、DTS のための型チェック・証明探索アルゴリズムについて考察し、プログラミング言語 Haskellを用いて実装を行った。さらに、日本語 CCG パーザ
lightblue[2] との接続を行うことで、日本語の文の入力に対して照応解決・前提束縛の計算を自動で行うことのできるシステムの構築を試みた。

2型チェックと証明探索

2.1

DTS の型推論・型チェック

依存型理論の型推論は一般に undecidable であるため、依存型理論の型推論を行うには決定可能な部分体系を用いる方法が知られている。Löh による Agda[3]の型推論の体系では、アノテーション構文を用いて型推論の及ばない部分式の型をあらかじめ指定することで、依存型の部分体系に対する型チェックを decidableに行うことを可能にしている。
DTS のための型チェックアルゴリズムは佐藤・戸次[6] によって定式化され、佐藤・戸次 [7] において実装されている。[6] では、DTS の体系を @ を含む体系と含まない体系の 2 つに分けて定義している。@ を含む体系を UDTT(Underspecified Dependent Type Theory)、含まない体系を DTT(Dependent Type Theory) という。文の意味表示に対する型チェックは UDTT のもとで行われる。UDTT の型規則（抜粋）を図 3 に示す。
UDTT の型規則の例として、(ΠI) 規則を以下の図4 に示す。(ΠI) 規則は Π 型に対する導入規則であり、DΓ ⊢ A :↓ s JDKtm ⇓ A′ Γ, x : A′ ⊢ M :↓ B(ΠI )Γ ⊢ λx.M :↓ (x:A) → B
図 4: (ΠI) 規則
規則の上段が満たされたとき、項 λx.M は型 (x:A) →B を持つ、という意味である。規則中に現れる Γ は型環境を表す。規則の上段に現れている JDKtm は @Elimination を行っている箇所である。(ΠI) 規則では、型 (x:A) → B の A が型 type または kind を持つかどΓ ⊢ M :↑ A(CHK )Γ ⊢ M :↓ ADΓ ⊢ A :↓ s1[Γ ⊢ M :↑DΓ ⊢ A :↓ s JDKtm ⇓ A′ Γ ⊢ A′ true(@)Γ ⊢ (@ : A) :↑ A

JDKtm ⇓ A′ Γ, x : A′ ⊢ B :↓ s2(ΣF )][x:AΓ⊢: ↑ s2
Bx:AB[]

Γ ⊢ π1 (M ) :↑ AΓ ⊢ M :↑(ΣE )x:ABDΓ ⊢ M :↓ ADΓ ⊢ A :↓ s JDKtm ⇓ A′ Γ, x : A′ ⊢ M :↓ B(ΠI )Γ ⊢ λx.M :↓ (x:A) → BDΓ ⊢ A : ↓ s1

JDKtm ⇓ A′ Γ, x : A′ ⊢ B :↓ s2(ΠF )Γ ⊢ (x:A) → B :↑ s2

JDKtm ⇓ M ′B[M ′ /x] ⇓ B ′ Γ ⊢ N :↓ B ′(ΣI )][x:AΓ ⊢ (M, N ) :↓B]
B[π1 (M )/x] ⇓ B ′Γ ⊢ π2 (M ) :↑ B ′(ΣE )Γ ⊢ M :↑ (x:A) → B Γ ⊢ N :↓ A B[N/x] ⇓ B ′(ΠE )Γ ⊢ M N :↑ B ′ただし、s, s1 , s2 ∈ {type, kind}

図 3: UDTT の型規則（抜粋）うか型チェックを行った後、その証明木に対して @Elimination を行うことで A の中の @ を取り除き、Bの型チェックを行う際の型環境に加えている。これにより、文の意味表示中に複数の @ がある場合でも、より深い位置に存在する @ から順に解消していくことが可能となっている。

2.2

DTS の証明探索

DTS の証明探索は、@ 規則において型チェックの一部として呼び出されるよう定義されている。@ 規則上段の Γ ⊢ A′ true が証明探索の呼び出される箇所である。
DTS のための証明探索アルゴリズムとして、[7] において以下のアルゴリズムが提案されている。
1. 証明探索を行うときの型環境とシグネチャの中から、Σ 型を持つ項を探す
2. 1 で見つかった項に投射を適用することで、Σ 型の項の第一要素・第二要素とその型を得る
3. 1,2 を型環境とシグネチャの中から Σ 型がなくなるまで繰り返す
4. 同じ型環境とシグネチャの中から、Π 型を持つ項を探す
5. 4 で見つかった項に関数適用できる項を 3 で得られた項の中から探し、関数適用した結果の項とその型を得る
6. 4,5 を型環境・シグネチャから Π 型がなくなるまで繰り返す
7. 1 から 6 の操作で得られた項に対応する型の中から、証明探索を行う型と一致する型を探し、その型に対応する項を返す
このアルゴリズムを用いることにより、(CHK) 規則、(CON) 規則、(VAR) 規則、(ΣE) 規則、(ΠE) 規則のみを特定の順序で用いることで証明探索が可能な型について、証明項を見つけることができる。

3

実装

DTS のための型チェック・証明探索アルゴリズムは[7] において実装されているが、[7] ではパーザとの接続はなされていなかった。そこで本研究では、CCG パーザ lightblue との接続が可能となるよう型チェック・証明探索アルゴリズムの再実装を行った。
パーザとの接続を考える上で [7] での実装と最も異なるのは、lightblue の出力の意味表示は de Bruijnindex[5] を用いていることである。de Bruijn index とは、変数を変数名で言及するのではなく、0 以上の自然数を用いて表す記法である。つまり、自然数 k は k番目に束縛された変数に対応する。
de[ Bruijn index[]] をx:entityentity用いると、という項はと書man(x)man(0)くことができる。
de Bruijn index を用いた DTS のための型チェック・証明探索アルゴリズムの実装を行う際に注意しなくてはならないのが、(ΠE) 規則や (ΣE) 規則などの代入操作を伴う規則である。たとえば (ΠE) 規則ならば、規則上段の B[N/x] という部分で代入操作が行われている。de Bruijn index を用いる場合、代入の際に変数の対応関係が崩れないよう注意する必要がある。具体的には、代入の際に代入する項の 0 以上の index に 1追加し、その項を代入し終えた項全体の項の 0 以上のindex を 1 下げる必要がある。このことに注意すれば、de Bruijn index を用いた DTS のための型チェック・証明探索アルゴリズムは [7] と同様の方法で実装することができる。

4

おわりに

本研究では、依存型意味論 (DTS) のための型チェック・証明探索アルゴリズムについて考察し、その実装を行った。さらに、日本語 CCG パーザとの接続も行った。
ただし、自然数型や枚挙型を含む Martin-Löf 型理論
全体の型チェック・証明探索をどのように実現するかについては、今後の課題としたい。

参考文献[1] Daisuke Bekki. Representing anaphora with dependent types. In Logical Aspects of Computational Linguistics, pages 14–29. Springer, 2014.
[2] Daisuke Bekki and Ai Kawazoe. Implementing Variable Vectors in a CCG Parser. In Proceedings ofLACL2016, C.Retore and S.Pogodalla (Eds), pp.5267, Springer, 2016.
[3] Andres Löh, Conor McBride, and Wouter Swierstra. A tutorial implementation of a dependently
typed lambda calculus. Fundamenta informaticae,102(2):177–207, 2010.
[4] Per Martin-Löf. Intuitionistic Type Theory, volume 17. Italy: Bibliopolis, Naples, 1984. Sambin,Giovanni (ed.).
[5] Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.
[6] 佐藤未歩, 戸次大介. 依存型意味論のための型チェックの実装に向けて. 言語処理学会第 22 回年次大会発表論文集, pp.761–764, 2016.
[7] 佐藤未歩, 戸次大介. 依存型意味論における型チェックの実装の試み. 第 30 回人工知能学会全国大会論文集, 北九州国際会議場, 2016/6/6–6/9.