言語処理学会 第21回年次大会 発表論文集 (2015年3月)

依存型意味論における型推論の定式化と実装
佐藤 未歩

1

戸次 大介

2,3,4

1

お茶の水女子大学理学部情報科学科
g1120522@is.ocha.ac.jp
2
お茶の水女子大学大学院人間文化創成科学研究科
bekki@is.ocha.ac.jp
3
国立情報学研究所
4
独立行政法人科学技術振興機構, CREST

1

はじめに：依存型意味論 (DTS)

依存型意味論 (DTS)[1] は、自然言語の証明論的意味論の 1 つである。形式意味論においては、モンタ
ギュー意味論 (MG) や談話表示理論 (DRT) のようなモデル理論的意味論が主流である。DTS では、文の意味をモデルを媒介して定義するのではなく、その文が正しいために何が必要か、そして、その文が正しいときに何が言えるかという、推論を媒介した定義を与えている。結果的に、文の含意関係を、モデルを参照せずに直接計算することができる。それに加えて、照応解決および前提の束縛が proof search の問題に還元されるという特徴がある。
たとえば、A man entered. He whistled. という 2文の意味表示はそれぞれ、図 1 と図 1 のようになる。
2 文を組み合わせた意味表示は、図 3 のようになる。

]x:entity u:λc. man(x) enter(π1 (u))λc.whistle(@1 c)

図 1: A man entered.

図 2: He whistled.

[[x:entity

照応解決に対応する。DTS は型理論に基づいていることから、@i の型を推論することができる。@i はその型を持つ項によって置き換えられる。上の例では、
@1 は型

⊤ []

x:entity  u:  → entity
man(x)  enter(π1 (u))
を持つ。この型を持つ証明項には、λc.π1 π2 c がある。
これは 1 文目の entity を取り出すものであり、a manが先行詞であるという読みに対応している。
一方、he の先行詞は a man ではなく、local contextの中に存在する場合も考えられるが、その場合には別の証明項が与えられる。このように先行詞の曖昧性は、ある型に対して複数の異なる証明項が存在することに対応している。
DTS のこのような形式化は、DRT 等のモデル理論的な談話理論に対し、次のような利点を備えている。

1. 照応解決に推論が必要となる場合、たとえばbridgeing のようなケースは、厳密には DRT では扱うことができないが、DTS では proof searchの枠組みの中で世界知識を用いることは自然である。

]  u:
 v: man(x)  
λc. 
enter(π1 (u))
whistle(@1 (c, v))

2. 照応や前提の先行詞が entity 以外であるケース、たとえば叙実動詞の前提のように先行詞が命題の形をとるような場合なども同様に扱える。
3. DRT における推論は、様々なシステムが提案されているが、いずれも first-order fragment に限られる。しかし、DTS では most などの GQ を含む higher-order ケースについても推論を行うことができる。

図 3: A man entered. He whistled.
ここで、変数 c は local context と呼ばれ、先行する文の証明項が与えられる。ただし、先行する文が存在しない場合は、初期 context として () (unit) が与えられる。また、@1 は underspecified term と呼ばれ、意味表示のうちで聞き手にとって未知の意味表示である。代名詞や前提トリガー（上の例では He ）は、意味表示に必ず @i を含み、その内容を推定することが以上の議論は、DTS が基づいている Dependent
Type Theory[2] に underspecified term を加えた体系において、型推論が可能であるという前提に基づいている。しかしながら、依存型理論において、一般に型― 461 ―Copyright(C) 2015 The Association for Natural Language Processing.
All Rights Reserved.

M↑vn::= n|type

neutral term
the type of types

|
|

kind⊤

the type of type
top|
|
|

⊥()
(x:v)
→ v′
[]

bottomunit
dependent functional type

|

x:v
v′

dependent sum type

|
|

λx.v
(v, v ′ )lambda abstraction
pair::= x|cvariables
constants|||

underspecified terms
functional application
projection@inv
πi nM↓

推論は undecidable であるため、Agda[3] における型推論のように、構文的に制限された、依存型の部分体系を用いる必要がある。
本研究では、DTS のための型推論、型チェックアルゴリズムを定式化し、プログラミング言語 Haskell を用いて実装した。この体系は、Σ-type、@i を含むものであり、自然言語の意味表示を記述することができる。

自然言語における型推論の問題点

Löh[3] による Agda の型推論の体系においては、アノテーション構文を用いて、型推論が及ばない部分式の型をあらかじめ指定することで、一部の構文に対して型チェック、さらにその一部の構文に対して型推論を decidable に行うことを可能にしている。
しかし、Löh[3] の体系には Σ-type や @i が存在しないため、型規則を拡張する必要がある。さらに、自然言語の意味表示においては、Löh[3] の (ΠE) 規則だけでは、図 3 のようなケースにおいて @1 の型を推論することができない。なぜならば、図 3 において @1 の型が推論できるという直感は、以下の (1)∼(6) の推論に基づいているが、⌈(2),(5) より⌋ という部分は Löh[3]の (ΠE) 規則では実現できないからである。
(1) whistle の型は entity → type であること(2) したがって、@1 ((), v) の型は entity であること(3) () の型は ⊤ であること] [x:entity u:(4) v の型は man(x)  であること
enter(π1 (u))

variableconstant symbol|||

the type of types
dependent functional typefunctional application

type(x:M↓ ) → M↓M
[ ↑ M↓ ]

|

x:M↓
M↓

|||

(M↑ , M↑ )πi M↑
M↓ : M↓

pairprojections
annotated term

||()
⊤unit
top type|⊥

bottom type

dependent sum type::= M↑

inferable terms

||

λx.M↓
(M↓ , M↓ )lambda abstraction
pair

|

@i

underspecified term

図 5: inferable term, checkable term の定義

図 4: neutral term, value の定義

2::= x|c(5) したがって、((), v) の型は


⊤ []



x:entity  u:  であることman(x)  enter(π1 (u))(6) (2),(5) より、@1 の型は

⊤ []

x:entity  u:
  → entity であるman(x)  enter(π1 (u))
これは、(ΠE) 規則では application の関数部分を最初に評価するため、関数部分である @1 の型が判明しなけれは、その先の推論は行わないようになっているからである。このように、Löh[3] の体系を拡張し、(1)∼(6)の推論を実現する上では、いくつかの技術的課題が存在している。

3DTS のための型チェック・型推論
アルゴリズム本研究において定義した体系は、Löh[3] の体系に基づき、DTS のための新たな構文をいくつか追加した体系となっている。この体系では、項は inferable term（型推論可能な項）と checkable term（型チェック可能な項）に分かれている。ただし、型推論可能ならば型チェック可能である。また、値は neutral term と valueの 2 つに分かれている。inferable term と checkableterm、neutral term、value の詳細は図 4, 図 5 のように定義されている。本研究では inferable term に定数 c、type、dependent sum type、projection、pair、― 462 ―Copyright(C) 2015 The Association for Natural Language Processing.
All Rights Reserved.

[L] Γ ⊢σ M :↑ v [L′ ](CHK )[L] Γ ⊢σ M :↓ v [L′ ][L] Γ ⊢σ M :↑ (x:v) → v ′ [L′ ] [L′ ] Γ ⊢σ N :↓ v [L′′ ] v ′ [N/x] ↠β v ′′(ΠE )[L] Γ ⊢σ M N :↑ v ′′ [L′′ ][L] Γ ⊢σ N :↑ v [L′ ] [L′ ] Γ ⊢σ M :↓ v → v ′ [L′′ ](→E )[L] Γ ⊢σ M N :↓ v ′ [L′′ ][[L] Γ ⊢σ M :↓ v [L′ ] v ′ [M/x] ↠β v ′′ [L′ ] Γ ⊢σ N :↓ v ′′ [L′′ ]
(ΣI )
[]
x:v
[L] Γ ⊢σ (M, N ) :↓[L′′ ]′v[[L] Γ ⊢σ M :↑x:v
v′[L] Γ ⊢σ M :↑x:v][L′ ]v′[L] Γ ⊢σ π1 M :↑ v [L′ ]

(ΣE )

]
[L′ ] v ′ [π1 M/x] ↠β v ′′[L] Γ ⊢σ π2 M :↑ v ′′ [L′ ](ΣE )(i : ) ∈/L(ASP)[L] Γ ⊢σ @i :↓ v [L, (i : v)](i : v) ∈ L(ASP)[L] Γ ⊢σ @i :↓ v [L]

図 6: 型推論・型チェック規則 (抜粋)

unit、top、bottom を新たに追加し、checkable term にpair、underspecified term、application を追加した。
Löh[3] の体系では、application は inferable term であり、型推論が可能な項として定義されている。しかし、先述したように、Löh[3] での application に対する規則である (ΠE) 規則だけでは、図 3 のようなケースにおいて @1 の型を推論することはできない。図
3 の中には @1 (c, v) という application が現れ、関数部分 @1 は inferable ではなく、(ΠE) 規則では先に関数部分を評価するため、関数部分が inferable でないapplication に型をつけることはできないからである。
一方で、application 全体の型が分かっており、かつ、引数部分の型が inferable である場合には、関数部分の型は定めることができるはずである。つまり関数部分の型は、引数部分の型を受け取り、application 全体の型を返すような関数型となると考えられる。以上のような推論を実現するためには、application を checkable termに追加し、引数部分を先に評価する (→E) 規則を追加する必要がある。このとき、application は checkableterm と inferable term の両方に存在することになる。
型推論、型チェックの各規則は図 6 のようになっている。これらの規則において、各規則のト記号の前後に現れている [L] は、各 @i がどのような型を持つかを保持する環境を表しており、アスペランド環境と呼ばれる。照応解決などにおいて重要な @i は、@1 , @2 , . . .のように異なる pronoun の数だけ現れ、型推論・型チェック規則の実行に伴いアスペランド環境は更新されていく。実際にアスペランド環境に対する操作を行うのは型チェック規則の中の (ASP) 規則である。この規則が呼び出された際には、引数として呼び出された@i に対する型割当がアスペランド環境の中に入っている場合はアスペランド環境を更新せず、入っていない場合には型チェックの際に呼び出された型をその @iに割り当てるようにアスペランド環境を更新する。この操作を行うことによって、未知であった @i の型を定めることができる。

4実装

DTS による自然言語の意味表示のための型推論アルゴリズムを、プログラミング言語 Haskell を用いて実装した。DTS における preterm（型のついていない項）は、Haskell 上で Preterm というデータ型を用意し、その型の値コンストラクタとして DTS の各構文を定義した。また、型推論は typeInfer という関数、型チェックは typeCheck という関数をそれぞれ定義しており、その型は図 7 のようになっている。
typeInfer と typeCheck の両方に引数として渡している 3 つのリストはそれぞれアスペランド環境、型環境、シグネチャを表現している。アスペランド環境
は前節でも述べたように @i の型を保持する環境であり、@i の番号 i (Int) と対応する型 (Preterm) のペアのリストである。型環境は変数の型を保持する環境であり、変数名 (String) と対応する型 (Preterm) のペアのリストである。シグネチャは定数の型を保持する環境であり、定数名 (String) と対応する型 (Preterm)のペアのリストである。これら 3 つの環境の中で、アスペランド環境と型環境は型チェック・型推論の実行時に更新されていくが、シグネチャは実行の前に与えておくことが前提となっており、基本的に更新されることはない。
型推論を実行する関数 typeInfer では、3 つの環
境と型推論を行う項を受け取り、型推論の結果として返ってきた型と、更新されたアスペランド環境のペアを返している。その際型推論が失敗することもありうるので、失敗つき計算を表現するために Maybe モナドを用いている。型チェックを実行する関数 typeCheck
では、3 つの環境と項と型を受け取り、与えられた項が与えられた型を持つかを確かめ、与えられた型を持つ場合のみアスペランド環境を返している。typeCheck
でも typeInfer と同様の理由から Maybe モナドを用いており、型推論・型チェックに失敗した場合はどちらも Nothing が返る。
application に対する型チェック規則である (→E) 規― 463 ―Copyright(C) 2015 The Association for Natural Language Processing.
All Rights Reserved.

typeCheck :: [(Int, Preterm)] -> [(String, Preterm)] -> [(String, Preterm)] -> Preterm -> Preterm -> Maybe [(Int, Preterm)]
typeInfer :: [(Int, Preterm)] -> [(String, Preterm)] -> [(String, Preterm)] -> Preterm -> Maybe (Preterm, [(Int, Preterm)])

図 7: 型推論・型チェックの型
sig :: [(String, Preterm)]
sig = [("whistle", Imp (Con "entity") Type), ("entity", Type), ("man", Imp (Con "entity") Type), ("enter", Imp (Con "entity") Type)]
preTerm1 :: Preterm
preTerm1 = Sigma "v" (Sigma "u" (Sigma "x" (Con "entity") (App (Con "man") (Var "x"))) (App (Con "enter") (Proj One (Var "u"))))(App (Con "whistle") (App (Asp 1) (Pair Unit (Var "v"))))
typeTest :: Maybe [(Int, Preterm)]
typeTest = typeCheck [] [] sig preTerm1 Type

図 8: テストプログラム
ghci> typeTest
Just [(1,Imp (Conj Top (Sigma "u" (Sigma "x" (Con "entity") (App (Con "man") (Var "x"))) (App (Con "enter") (Proj One (Var "u")))))(Con "entity"))]

図 9: テスト結果
則では、application の関数部分の型は、dependentfunctional type ではなく、依存関係のない implication となっている。よって (→E) 規則の実装では、関数部分の型が、引数部分の型から結果の型への implication と一致するかどうか、パターンマッチを用いて判定すればよいと考えられる。しかしそのような実装
では、application の関数部分の型が dependent functional type になっている場合、型チェックに失敗してしまう。というのは、Löh[3] の体系では application に対する型チェック規則は (CHK) 規則のみであるので、application に対して型チェックを行った場合、実際には型推論、すなわち (ΠE) 規則が適用されている。しかし、(→E) 規則が追加された体系では、applicationに対する型チェックの際には (CHK) 規則は適用されず、(→E) 規則のみが適用される。このため、関数部分の型が dependent functional type である場合には前述のパターンマッチに合致せず、型チェックに失敗してしまう。この問題を解消するためには、application の関数部分の型が inferable であるかどうかを確かめる必要があり、inferable であったら (ΠE) 規則、inferable でなかったら (→E) 規則を適用すればよい。
この考えに基づき、(→E) 規則は、まず (ΠE) 規則を実行し、失敗した場合には (→E) 規則を実行するよう実装を行っている。これにより、@i を含む applicationの型推論・型チェックが可能になる。
このアルゴリズムのテストとして、図 8 のようなテストプログラムを作成した。このプログラムは、第1 節で述べた A man entered. He whistled. という文に対応する意味表示が型 type を持つという条件で型チェックを実行することにより、代名詞 he の意味表示中の @1 への型割当を含むアスペランド環境を返す。
このプログラムを実行することによって、@1 の型を自動的に推論することができる。実行結果は図 9 のようになっており、これは理論的予測と一致する。

5

おわりに

本研究では、依存型意味論 (DTS) の部分体系に対する型チェック、型推論のアルゴリズムを提示し、実装した。この体系は部分体系ではあるものの、依存型Π、Σ、underspecified term @i を含むもので、自然言語の意味論を展開するために十分な記述力を備えている。DTS では照応・前提の他にも、慣習的含みなど幅広い言語現象が @i を用いて説明されており [4]、本研究のアルゴリズムの適用が期待される。また、自然数型や等号型を含む、より豊かな体系に本研究のアルゴリズムを拡張することが考えられるが、今後の課題としたい。

参考文献[1] Bekki, Daisuke. 2014. Representing Anaphora withDependent Types. In Logical Aspects of Computational Linguistics (8th international conference,LACL2014, Toulouse, France, June 2014 Proceedings), N.Asher and S.Soloviev (Eds), LNCS 8535,
pp.14-29, Springer, Heiderburg.
[2] Martin-Löf, Per. 1984. Intuitionistic Type Theory.
vol. 17. Naples: Italy: Bibliopolis.
[3] Löh, A., C.McBride, and W.Swierstra. 2010. A Tutorial Implementation of a Dependently Typed Lambda
Calculus. Fundamenta Informaticae - Dependently
Typed Programming, Vol. 102, No. 2, pp. 177-207.
[4] Bekki, Daisuke and Eric McCready. 2014. CI via
DTS. In Proceedings of LENLS11, pp.110-123.

― 464 ―

Copyright(C) 2015 The Association for Natural Language Processing.
All Rights Reserved.