高階依存型理論を用いた自然言語の意味論構築に向けて中野悠紀

1(指導教員：戸次大介)
例えば、Montague 流の “every” の語彙項目は CG（から方向性を省略した体系) においては以下のようになる。

はじめに

高階依存型理論の研究は Martin-Löf 型理論にさかのぼるが、自然言語への応用については Ranta(1994) などがあり、その後も様々な拡張が行われている。自然言語の意味論には高階依存型理論によって解決しうる問題がいくつかあるが、本研究は高階依存型理論を用いたCG(Categorial Grammar) を提案する。

2` λQ.λP.∀x(P (x) → Q(x)) : (N P → S) → ((N P → S) → S)

これは Martin-Löf の体系では以下のように表される。
(λQ)(λP )((Πx : N P )((Πy : P (x))Q(x))) : (ΠQ : (Πx : N P )S)((ΠP : (Πx : N P )S)S)N P : set とすると、“every” の導出は次のようになる。

Martin-Löf 型理論(Πx : N P )((Πy : P (x))Q(x)) : S
ΠI(λP )((Πx : N P )((Πy : P (x))Q(x))) : ((ΠP : (Πx : N P )S)S)ΠI(λQ)(λP )((Πx : N P )((Πy : P (x))Q(x))) : (ΠQ : (Πx : N P )S)((ΠP : (Πx : N P )S)S)Martin-Löf 型理論 (Martin-Löf 1975、1984) は依存型を持つ型理論である。命題 (prop) と集合 (set) を区別しなければ、次の4 つの判定を持つ。
def

一番上の部分で S ≡ set でなければ ΠF 規則が適用でdef
A:set
 a:Aきないので、S ≡ set と仮定すると図 1 のように導出できる。

a=b:A
A=B:set

3

1

2

1

P : (Πx : NP )set

x : NP

Q : (Πx : NP )set

x : NP

各型はそれぞれ、形成規則 (formation rule)、導入規則(introduction rule)、除去規則 (elimination rule)、等号規則 (equality rule) と呼ばれる 4 組の推論規則を持つ。Martin-Löf 型理論を用いて論理記号を解釈すると次のようになる。
A&B = (Σx : A)B : propfor

for

3for

defforA : set, B(x) : prop (x : A)

(x : N P )..
..
N P : set S : set ΠF, 1(Πx : N P )S : set

A : prop, B : prop(∀x : A)B(x) = (Πx : A)B(x) : propA ∨ B = A + B : prop

図 1:Martin-Löf を用いた “every” の導出

しかし、S ≡ set と仮定して(Πx : N P )S : setを導出す
ると、

A : prop, B : prop(∃x : A)B(x) = (Σx : A)B(x) : propA ⊃ B = (Πx : A)B : prop

ΠEΠE
Q(x) : set
ΠF(Πy : P (x))Q(x) : set
NP : setΠF, 1(Πx : NP )((Πy : P (x))Q(x)) : set
ΠI, 2(λP )((Πx : NP )((Πy : P (x))Q(x))) : ((ΠP : (Πx : NP )set)set)
ΠI, 3(λQ)(λP )((Πx : NP )((Πy : P (x))Q(x))) : (ΠQ : (Πx : NP )set)((ΠP : (Πx : NP )set)set)
P (x) : setforA : set, B(x) : prop (x : A)

A : prop, B : prop

CG の論理的解釈

defS ≡ set なので set : set という判定が成り立つ必要があるが、これは Martin-Löf 型理論において妥当な判定

3.1 提案CG(Steedman 1996) において統語素性 (Syntacticfeature) は統語範疇をより詳しく指定する上で非常にではない、という問題がある。
問題 2
また、“runs” が主語に三人称単数かつ主格しか取らないことを示したいとするならば、“runs” は「(3&s)&
nom」という統語素性に依存しているので、“runs”から主語が「(3&s)&nom」であることを指定できなければならない。つまり “runs” の型 (意味表示) 側に「(3&s)&nom」という情報を持ち、「John, runs `run(John) : S 」は証明可能で「I, runs ` run(I) : S 」は証明できない体系を考える必要がある。また、この 3や s や nom は統語範疇 N P の統語素性なので統語範疇 N P に依存しているはずである。したがって、２つ目の問題点として “runs” 側から「(3&s)&nom」を指定でき、3 や s や nom が N P に依存しているような依存関係を “runs” の型の側で表現する方法を必要とする。

重要である。統語素性はそれぞれの統語範疇で異なり、統語範疇 N P は統語素性として「格」「人称・数」などを持つ。そしてそれぞれの値として「格」は「nom + acc」を、「人称・数」の場合は「x&s」(x は人称の値であり、例えば三人称ならば 3) を持つ。例えば、“John” が統語素性に三人称単数主格を持つならば、その統語素性の値は「(3&s)&nom」となる。また、統語範疇 N P は N Pの統語素性しか持たないので、統語範疇 N P と N P の統語素性の間には依存関係があると考えられる。
統語素性を持たない文法では、ほとんどの文は非文にならない。例えば、動詞 “runs” の主語は統語素性「(3&s)&nom」を持つ N P でなければならないが、統語素性を考えなければ、統語素性「(1&s)&nom」を持
つ “I” や統語素性「(3&s)&acc」を持つ “Him” などが“runs” の主語になることができ、本来非文であるはずの “I runs” や “Him runs” という文が文法的となってしまう。
しかし、CG と論理学や代数との対応に関する研究において、統語素性まで含めた CG が扱われたことはない。そこで、本研究では依存型を用いて統語素性を表現する手法を提案する。
3.2 問題点依存型を用いて統語素性を表現するには 2 つの問題点がある。
問題 14λ-cube を用いた解決手法

4.1 Barendregt の λ -cube
λ-cube とは、8 つの型理論 (λ →, λ2, λω, λω, λP,
λP 2, λP ω, λC = λP ω) の総称であり、図 2 の様な立方体で表される。型、項、判定と推論規則の大部分は8 つのシステムで共通であり、システムの違いは次の(s1 , s2 ) 規則において (s1 , s2 ) に現れうる型や種にある。
Γ ` A : s1 Γ, x : A ` B : s2
Γ ` (Πx : A.B) : s2

s1 , s2 は ∗, 上を動き、∗ とは型全体の集まりである種を表し、 とは種全体の集まりを表す。
8 つのシステムでそれぞれ (s1 , s2 ) は図 3 のようにな

45` NP : . ` S : ` NP : . ` S : ..
..
.
.
π1(S, S) ` NP :  ` S : 
Q : (Πα : NP.S), P : (Πα : NP.S)x : NP ` (Πy : P (x).Q(x)) : S..
(, S)..
` NP : . ` S : Q : (Πα : NP.S), P : (Πα : NP.S) ` (Πx : NP.(Πy : P (x).Q(x))) : S..
ABS.
Q : (Πα : NP.S) ` (λP : (Πα : NP.S).(Πx : NP.(Πy : P (x).Q(x))))) : ((ΠP : (Πα : NP.S).S))ABS` (λQ : (Πα : NP.S).(λP : (Πα : NP.S).(Πx : NP.(Πy : P (x).Q(x))))) : (ΠQ : (Πα : NP.S).(ΠP : (Πα : NP.S).S))` NP : . ` S : ..
.

図 4:λ-cube を用いた語彙項目 “every” の導出` (λr : (Σz : N P.(Σy : (Σx : 3.s).nom)).run(p(r))) : (Πr : (Σz : N P.(Σy : (Σx : 3.s).nom)).S)` run(p(hJohn, hha, bi, cii)) : S` hJohn, hha, bi, cii : (Σz : N P.(Σy : (Σx : 3.s).nom))

AP P

図 5:run(p(hJohn, hha, bi, cii)) : S の導出る。このうち λP は Martin-Löf 型理論に対応する。

4.3 問題 2 の解決へ向けて
λω が複数の種を持つよう新しく拡張したシステムでは、統語範疇 S や統語範疇 N P という種の他に、統語素性の種 F を持つとする。三人称を表す型を 3、単数を表す型を s、主格を表す型を nom とする。この時“John runs” が文法的となることの導出を考える。つ

図 2:λ-cube
System(s1 , s2 )λ→(∗, ∗)λ2(∗, ∗)(, ∗)λP(∗, ∗)(∗, )

λP 2(∗, ∗)(, ∗)λω(∗, ∗)λω(∗, ∗)λP ω(∗, ∗)λP ω = λC(∗, ∗)まり、` N P : , ` S : , ` F : , ` John : N P,` a : 3, ` b : s,` c : nom` 3 : (Πz : N P.F ), ` s : (Πz : N P.F ), ` nom : (Πz : N P.F )であるときrun(John) : S となることを示す。
まず、統語素性の型である(Πz : N P.F )が種であることは次のように証明できる。

(∗, )(, )(, ∗)(, ∗)(, )(∗, )(, )(∗, )(, )` F :  ` NP :  w` NP : x : N P ` F :  (, )` (Πz : N P.F ) : 

図 3:各システムにおける (s1 , s2 ) 規則

三人称単数、主格の “John” は次のように導出される。
a:3 b:sΣIha, bi : (Σx : 3.s)c : nomΣIJohn : N P hha, bi, ci : (Σy : (Σx : 3.s).nom)
ΣI
hJohn, hha, bi, cii : (Σz : N P.(Σy : (Σx : 3.s).nom))

4.2 問題 1 の解決手法“every” の語彙項目を λ-cube の体系で考えると、` (λQ : (Πα : N P.S).(λP : (Πα : N P.S).(Πx : N P.(Πy : P (x).Q(x)))))“runs” は、次のように表す。

: (ΠQ : (Πα : N P.S).(ΠP : (Πα : N P.S).S))` (λr : (Σz : NP.(Σy : (Σx : 3.s).nom)).run(p(r))) : (Πr : (Σz : NP.(Σy : (Σx : 3.s).nom)).S)となる。“every” の導出の過程で、次の π1 のような証明木が現れるので、すると図 5 のようにrun(p(hJohn, hha, bi, cii)) : S となる。
さらに、

` NP : . ` S : ..
.

hJohn, hha, bi, cii : (Σz : N P.(Σy : (Σx : 3.S).nom))ΣEp(hJohn, hha, bi, cii) : N P` NP : . ` S : ..
.

Q : (Πα : NP.S), P : (Πα : NP.S) ` P : (Πα : NP.∗)w
Q : (Πα : NP.S), P : (Πα : NP.S), x : NP ` P : (Πα : NP.∗)AP P
Q : (Πα : NP.S), P : (Πα : NP.S), x : NP ` P (x) : ∗となる。しかし、p(hJohn, hha, bi, cii) : NP がJohnと等価であることを示さなければ、run(John) : S は証明できない。

π15

Q : (Πα : N P.S), P : (Πα : N P.S) ` P : (Πα : N P.∗)を 示 す に
def

まとめと今後の課題

本 研 究 で は 高 階 依 存 型 理 論 を 用 い て CategorialGrammar を拡張する上での問題点を指摘し、λ-cubeを用いた解決策を示した。
今後の課題としては、λω を拡張したシステムの体系を考案すること、そのシステム上でp(hJohn, hha, bi, cii) : NPがJohnと等価であることを示すこと、また “every” を定め、“Every student runs” のような文が文法的な文として導出されるかなどを検証することが挙げられる。

defは S ≡ ∗ でなければならない。S ≡ ∗ と仮定し、(s1 , s2 ) 規則に (S, S), (, S), (, ) を使うことで、図4 のように語彙項目 “every” を導出できる。
考察def
この導出においては S ≡ ∗ であり、` N P : と ` S :  を axiom に追加する必要がある。また、Martin-Löf は λP なので図 2 より (S, S),(S, ) しか使うことができないので、set : set という判定が必要という結論になった。この導出で使う (s1 , s2 ) 規則は(S, S), (, S), (, ) であるので、図 2 より CCG の計算には λω が必要ということになる。つまり、[2] における Martin-Löf の定式化では Categorial Grammarを表現することはできない。
また、ここまでは統語範疇 S と N P のみを考えていたが、他の統語範疇も踏まえるならば、統語範疇の数だ
け (S,) (N P ,) (N ,) (CON J,)... というような規則が必要になると考えられる。λω では (s1 ,) のs1 には ∗ か  しか入らなかったが、s1 に複数の種類(S や N P など) の種か  が現れるシステムが必要であり、したがって λω を拡張する必要がある。

参考文献[1] Barendregt,H. 1992, Lambda calculi with types.
In S. Abramsky, D. M. Gabbay, and T.S.E.
Maibaum (Eds.), Handbook of Logic in Computer
Science, Volume 2 Background: ComputationalStructures. pp.117–309,Oxford Science Publications.
[2] Ranta,A. 1994, Type-Theoretical Grammar. Oxford University Press.
[3] 龍田真, 1992, 「型理論」, 近代科学社.
[4] 戸次大介, 2010, 「日本語文法の形式理論−活用体系・統語構造・意味合成−」, 日本語研究叢書 24, く
ろしお出版.
46