部分方向性組み合わせ論理の計算論的性質
尾崎博子

1(指導教員：戸次大介)

はじめに

4

Bekki (2010) では、コンビネータ K は用いられていないが、コンビネータの依存関係を明らかにするために以下のように定める。
K
K/ : (A/B)/\A K\ : (A\B)/\A
CL では B が S, K から導出できることが知られているので、Bekki (2010) における B/ が S, K から導出できるかを確かめてみると、図 1 より導出できないことが分かる。
そこで次のように S を変更すると、B/ が S/ , K\ から導出できることが分かる (図 2)。
S/ : (A/C)/(B/C)/\(A/B\C)
S
S\ : (A\C)\(B\C)/\(A\B/C)
B\ についても同様であり、以上より依存関係が成立するコンビネータの組み合わせが明らかになった。

言語処理の分野における形式的な文法理論として組み合わせ範疇文法 (CCG: Steedman (2000)) がある。
CCG は頑健な構文解析に使われている一方で、言語学的には適切な制約を与えることが知られている。
Bekki (2010) では CCG と論理体系の関係を明らかにするために、部分方向性組み合わせ論理（Subdirectional Combinatory Logic）という形式体系を提案した。部分方向性組み合わせ論理は、組み合わせ論理(CL) の拡張であり、ランベック計算のように関数適用の二つの方向性を区別する体系である。しかし、部分方向性組み合わせ論理の計算論的性質はまだ示されていない。
本研究の目的は、部分方向性組み合わせ論理の計算論的性質を明らかにすることである。Bekki (2010) では Steedman (2000) のコンビネータを用いて、CCGを部分方向性組み合わせ論理上の一体系として位置付けている。しかし、組み合わせ論理において成立するコンビネータ間の依存関係が、この論理においては方向性の区別により成立しない場合があるため、その場合を考慮に入れなければならない。
そこでまず始めに依存関係が成立するコンビネータの組み合わせを明らかにしたうえで、システムの正当性を示すために必要とされている 1) Subject-reduction、2) 合流性、3) 停止性、等の計算論的性質を証明する。

25

 B
/ f g x B
\ f g x S
/ f g x S
\ f g x

K
/ x y

K
\ x y

K// : (A/B)/A K\/ : (A\B)/AK/\ : (A/B)\A K\\ : (A\B)\A(他のコンビネータについても同様)

6(<)

略記法

(γ は型の要素)(c はコンビネータ)

ΔN :BΓ, Δ  M N : AΓ  M : A\B≡τ /σM N

def

(<>)

≡def≡

f  (g  x)→(f  x) (g  x)→(f  x) (g  x)

→x→x

CLCLCLCL

Subject-Reduction

つまり、この性質は簡約前と後で値の型が変わらないことを示している。この性質を部分方向性組み合わせ論理で証明するために、コンビネータ K, S についてこの性質が成立するかを確かめる。証明方法は Hindleyand Seldin (2008) を参考にした。B についてはコンビネータの依存関係より示す必要はない。
CLΔ, Γ  M N : A

τ /\σ→CLK
/ X Y → X の場合

deff  (g  x)

CLx | c | Λ Λ | Λ ΛΔN :B→CL

Subject-ReductionΓ  X : τ で X → X の時、Γ  X : τγ | τ /τ | τ \τΓ  M : A/Bc (c はコンビネータ)

Subject-Reduction とは以下のような性質である。

構文、型規則、略記法

型規則 (>)→CL※以下では証明の構想のみを述べる。なお、詳細については尾崎・戸次 (2011) を参照。

このようにコンビネータに方向性を持たせた組み合わせ論理を部分方向性組み合わせ論理と言う。

式 Λ ::=

CLc

部分方向性組み合わせ論理

構文 型 τ ::=簡約規則

部分方向性組み合わせ論理の簡約規則を次のように定める。
x→ x

組み合わせ論理の direction → に方向性を持たせ、/ と \ に分けると、各コンビネータから複数の種類が生じる。例えば組み合わせ論理におけるコンビネータ
K : A → (B → A) には以下の４つが対応する。

3

コンビネータの依存関係

or

τ \σ

M Nor

M N

(<)

or(>)

(<>)
(>)



15

K/ : (x/y)/\x

X:xK/ X : x/y
K
/ X Y

Y :y:x（他の K, S についても同様）

(A/C)/(B/C)\((A/B)/C)
(<>)

(<)

K/ = ((A/B)/C)/(A/B)

K/ = ((A/C)/(B/C)\(A/B)/C)/(A/B)/\(A/C)/(B/C)\((A/B)/C)\((A/C)/(B/C)\(A/B)/C)/(A/B)
S/ = ((A/C)/(B/C)/(A/B))\(((A/B)/C)/(A/B))\(((A/B)/C)/(A/B))/((A/C)/(B/C)\(A/B)/C)/(A/B)(<>)((A/C)/(B/C)/(A/B))\(((A/B)/C)/(A/B))\(((A/B)/C)/(A/B))
B/ = (A/C)/(B/C)/(A/B)

図 1: B/ の導出（失敗例）(<>)

S/ = (A/C)/(B/C)/((A/B)\C)

K\ = ((A/C)/(B/C)/(A/B)\C)\(A/B)/\(A/C)/(B/C)/((A/B)\C)
S/ = ((A/C)/(B/C)/(A/B))/(((A/B)\C)/(A/B))/\((A/C)/(B/C)/(A/B)\C)\(A/B)((A/C)/(B/C)/(A/B)\C)\(A/B)(<>)

K\ = ((A/B)\C)/(A/B)((A/C)/(B/C)/(A/B))/(((A/B)\C)/(A/B))(>)

B/ = (A/C)/(B/C)/(A/B)

図 2: B/ の導出
以上より部分方向性組み合わせ論理におけるSubject-Reduction の性質を証明できた。

定義 1-2 RT2 /T1 (t) の時 t は停止し、RT1 (s) ⇒ RT2 (t s)合流性（Church-Rosser の定理）

定義 1-3 RT2 \T1 (t) の時 t は停止し、
RT1 (s) ⇒ RT2 (t s)

7

合流性を示すためには以下の Church-Rosser の定理を証明すればよいとされている。

次に以下の補題を示す。
補題 2 x1 : T1 , · · · , xn : Tn  t : T かつ
v1 , · · · , vn について RT1 (v1 ), · · · , RTn (vn ) が成り立つ時 RT ([x1 → v1 ] · · · [xn → vn ]t)

Church-Rosser の定理
 を 1 回以上の簡約とすると
M  M1 , M  M2 ならば、ある N について、Mi  N (i = 1, 2)

上の補題 2 が成り立つと以下の性質が証明できる。
強正規化性

つまり、この性質は値のどこから簡約をかけても最終結果は同じになることを示している。
証明の準備としてまず以下の３条件を満たす関係 ⇒ t : T ならば t は停止する
証明方法は Pierce (2002) を参考にし、t の構成に関する帰納法を用いて証明した。以上より部分方向性組み合わせ論理における強正規化性を証明できた。

CL（これ以降「並行変換」）を考える。

1. M → N ならば M ⇒ N
CLCLCLCL9

2. M ⇒ N ならば M  N
3. M ⇒ Mi (i = 1, 2) ならば Mi ⇒ N (i = 1, 2)
CL

まとめと今後の課題

本研究では部分方向性組み合わせ論理におけるコンビネータの依存関係を示し、システムの正当性を示すために必要な Subject-Reduction、合流性、正規化定理という３つの計算論的性質を証明した。
今後の課題としては、部分方向性組み合わせ論理の妥当性が証明できたので、正規形（正規化した形）を計算しながら解析をする解析器の構築などを考えている。

CL

次に、簡約の並行変換を以下のように値の形ごとに定義する。

(C1) x ⇒ x
CL(C2) c ⇒ cCL(C3) K/ M1 M2 ⇒ N1 (ただし M1 ⇒ N1 )参考文献

(C4) K\ M1 M2 ⇒ N1 (ただし M1 ⇒ N1 )Bekki, D. (2010) “Combinatory Categorial Grammar
as a Substructural Logic — Preliminary Remarks—”, In the Proceedings of LENLS 7, JSAI International Symposia on AI 2010. Campus Innovation
Center, Tokyo, pp.70–83.

CLCL

CLCL

(C5) S/ M1 M2 M3 ⇒ (N1 N3 ) (N2 N3 )
(C6)

CL



S\ M1 M2 M3 ⇒ (N1 N3 ) (N2 N3 )CL(ただし (C5),(C6) では Mi ⇒ Ni (i = 1, 2, 3))

Hindley, J. R. and J. P. Seldin. (2008) LambdaCalculus and Combinators: an Introduction. Cambridge University Press.

CL(C7) M1 M2 ⇒ N1 N2 (ただし Mi ⇒ N1 (i = 1, 2))
CL

CL

上のように定義した並行変換 ⇒ が条件 1, 2, 3, をPierce, B. C. (2002) Types and Programming Languages. The MIT Press.

CL満たすことを示し、合流性の証明とする。証明方法は
高橋 (1991) を参考にし、M の構成に関する帰納法を使った。以上より部分方向性組み合わせ論理における合流性を証明できた。

8Steedman, M. J. (2000) The Syntactic Process (Language, Speech, and Communication). The MIT
Press.

停止性（正規化定理）

高橋正子, 1991. 「計算論 — 計算可能性とラムダ計算—」, 近代科学社.

停止性を示すには、正規化定理を証明すればよい。
強正規化性とは式を任意の順序で簡約していっても必ず有限ステップで停止するという性質である。まず、以下のような定義を設定する。

尾崎博子, 戸次大介. 2011. 「部分方向性組み合わせ論理の計算論的性質とその証明」, Technical Report ofDepartment of Information Science, Ochanomizu
University, OCHA-IS 10-2, February 7th, 2011.

定義 1-1 RA (t) の時 t は停止する (A は基本型)

16