proof net を用いたランベック計算の実装に向けて渡辺成美

1（指導教員：戸次大介）

はじめに

A : xi・・
A:φI/i
B/A : λxψ

自然言語の構文解析として様々な手法が提案されている。Categorial Grammar(CG) では、各語の統語範疇を辞書から引き出し、その統語範疇の列に推論規則を適用することで文を解析する。統語派生を推論とみなし、統語範疇を論理式、辞書を公理の集合、統語規則を推論規則と考えるのである。証明に成功したとき、構文解析ができたとされる。CG はコンピュータに処理をさせやすいという点で優位である。CG の拡張されたものとして Lambeck Categorial Grammar(LCG)がある。Morrill(2011) は LCG と対応した proof net による構文解析アルゴリズムを提案している。本研究ではこれに基づいた日本語の構文解析器の実装を目指す。
実装のための言語として Prolog を用いる。論理型言語である Prolog は CG と相性が良いと考えられる。

2

図 2. 意味論を含めたランベック計算のための自然演繹

3

Lamek Categorial GrammaridΓ ⇒ A ∆(A) ⇒ BCut∆(Γ) ⇒ B

A, Γ ⇒ C\RΓ ⇒ A\C

図 3.proof net の木への変換関数
proof frame はシーケント計算と対応する。ただしランベック計算が問題として抱えている擬似的曖昧性が、proof net には存在しない。シーケント A1 , ..., An ⇒ A0
は h| A◦0 |, | A•1 |, ..., | A•n |i で表される。

∆(A, B) ⇒ D•L∆(A, B) • D

A• と A◦ は相補的であり（A• = A◦ 、A◦ = A• ）、その間にリンクを結ぶことができる。このリンクは互いに交差しない。また、/◦ や \◦ のから伸びる葉のうち、最左の葉と最右の葉を繋げることはできない。リンクが全て繋げられ、proof net が正しく形成される
とき、そのシーケントはランベックシーケント計算で導出可能な定理である。
例として、「太郎が手紙を書く」の構文解析を行う。
戸次 (2010) に基づいて辞書を以下のように定義する：

Γ ⇒ A ∆(C) ⇒ D\L∆(Γ, A\C) ⇒ D

Γ ⇒ A ∆(C) ⇒ D/L∆(C/B, Γ) ⇒ DΓ, B ⇒ C/RΓ ⇒ C/BΓ ⇒ A Γ ⇒ B •RΓ, ∆ ⇒ A • B

図 1. ゲンツェン流シーケント計算の規則
ランベックシーケント計算においてカット除去が成り立つことを証明されている。また、カット以外の規則はその上段における各型がいずれも下段の部分型であるという性質を持つ。そのため各定理はその部分論理式のみを含む証明を持つ。後ろ向き連鎖証明探索(backward chaining proof search) の際に探索空間が有限であるので、あるシーケントが定理であるかどうかは決定可能である。
単語とその型は辞書の中に定義される。この時生成される言語は有限集合である。
ランベック計算の自然演繹的表現として、以下が与えられる。普通自然演繹に順序の区別はないが、このランベック計算のための自然演繹では順序が存在する。意味論は λ 計算により引き出される。シーケント Γ ⇒ Aが導出可能なとき、そしてその時に限り、そのシーケントはランベック計算の定理である。
・・・・
A : φ A\B : χE\B : (χ φ)

A : xi・・A:φI\iA\B : λxψ

Proof net

proof net では証明を図で表記する。木 | AP | は、図3 の変換に従って定義される、型 AP の木である。

ランベック計算の型の集合 F は以下のように定義される：
F ::= P | F • F | F \F | F/F
LCG ではゲンツェン流シーケント計算を行う。/、\、• についてのシーケントを得るための体系が定義されている。。規則としてカット規則、恒等規則 id、論理規則がある。
A⇒A・・・・
A:φ B:ψ
I•
A • B : (φ, ψ)

太郎

:

N Pnc

:taro

手紙::

N Pnc
N Pnc \N Pga::

tegamiid:::

N Pnc \N Po
N Po \(N Pga \Sv,5,k,stem )Sv,5,k,stem \Sv,5,k,term

:
:
:

id
λxλy(kaku(x, y))idがを書
く

この文に一致するシーケントは、
N Pnc , N Pnc \N Pga , N Pnc , N Pnc \N Po ,N Po \(N Pga \Sv,5,k,stem ), Sv,5,k,stem \Sv,5,k,term ⇒ Stermである。このシーケントの導出は図 4 に与えられる。

・・・・
B/A : χ A : φ
E/
B : (χ φ)

図 4.「太郎が手紙を書く」の導出

31

及び並列の助詞「と」は以下のように表される：が:(N P \T1 )/(N Pga \T1 ):idと:(T1 \T1 ) /T1:

λxλy[(x ∧ y)]「が」の T1 と「と」の T1 はプログラム中では異なる変数として識別される。図 7 では T1 に N Pnc 、T2に Sterm が代入されている。「太郎と次郎が走る」の意味論として (2a) が導かれ、これは (2b) に縮約される。
図 5.semantic trip
意味論は図 5 に従って A◦0 から順に移動していくことで引き出される。A◦0 に戻ることで終了する。図 4 の場合 (1a) が導かれ、(1b) に縮約される。
(1) a.(id((λxλy(kaku (x, y))(id tegami))(id taro)))b.(kaku(tegami taro))

4

proof net を用いた prolog による実装

上記の構文解析アルゴリズムを用いたプログラムがMorrill(2011) により提供されている。そのアルゴリズ
ムは以下の通りである：
process α
G, [Li | Ls], α, F, X
ST ART
SHIF T[S0◦ ], [], α, [S0◦ ], ∅[Li | G], Ls, α, F, X
0G, [], α ⊕ α , F, X
LEX,where α:AG, f ringe(| A• |](F ) ), α0 , F ⊕ [| A• |](F ) ], X[], [], [], F, X
accept EN Db.

5[Li | G], [Lj | Ls], α, F, X
REDU CE
G, Ls, α, F, X ∪ {(i, j)}

いて subtend せず、F にあるものの間の各 pathは axiom links X と共にいくつかの ℘-link のedges のうち両方を横切る。
G：メインスタック。まだ試されていない葉を含む

書::

N Po \(N Pga \Sv,5,k,stem )N Pga \(N Po \Sv,5,k,stem )::λxλy(kaku(x, y))λxλy(kaku(x, y))

上記の proof net ではかき混ぜ規則を表現することができないため、拡張する必要がある。proof net のリンクは互いに交わらないと書いたが、条件付きで交わることを許すことにより、かき混ぜ規則を実現できるかもしれない。また現在素性に対する扱いが弱く、変数を入れることができない。日本語の活用に柔軟に対応するには、素性についてより正確に記述できる構造にする必要がある。

X:proof net 上にこれまでに立てられたリンクの集合

図 6. 構文解析アルゴリズム解析
このプログラムでは型に変数が存在せず、そのため例えば ‘and’ の辞書を以下のように記述する必要がある：and : (N C\N C)/N C : λxλy[(y ∧ x)]((N \S)\(N \S))/(N \S)λxλyλz[(y z) ∧ (x z)]

6(((N \S)/N )\((N \S)/N ))/((N \S)/N )λxλyλzλw[(y z w) ∧ (x z w)]...
(T \T )/T の形を取るものが数多く並び、冗長である。
また日本語の構文解析を考えた時、助詞を扱うのに同じ問題が挙がる可能性がある。
これを踏まえて、本研究では型に変数を用いることができるようにした日本語構文解析器を実装した。図 6の LEX の適用の際、単語 A に含まれる変数 T1 , ..., Tnに、他の単語の変数と重ならないように番号を付けなおす。REDUCE で変数が他の型と結びつけられたとき、Ls および G 中のそれと同じである変数は書き換えられる。このようにして変数が処理される。
素性は型の中に含めて扱う。このとき格助詞「が」andまとめと今後の課題

書

Ls:補助スタック。
α:まだ見られていない単語
F :語彙選択によってこれまでに立てられた proof net::((λzλw(z ∧ w) jiro ) taro))(hashiru (taro ∧ jiro))

proof net による構文解析アルゴリズムを用いて、日本語の解析を行うことができた。現在日本語のかき混ぜ規則に対応していない。
「太郎が手紙を書く」と「手紙を太郎が書く」の両方を解析するには、辞書に以下の二つがなければならない：

ただし Li と Lj は相補的であり、frame F におand図 7.「太郎と次郎が走る」の導出
a. (( id (λy( id (λx(hashiru x ) y))))

(2)

参考文献
[1]

Glyn V.Morrill (2011) Categorial Grammar
Logical Syntax, Semantics, and Processing ,Oxford[2]

戸次大介 (2010) 日本語文法の形式理論 - 活用::

体系・統語構造・意味合成、くろしお出版

32