組合せ子 L の非循環性
Acyclicity of combinator L
岩見 宗弘 †
Munehiro Iwami

1.

はじめに

組合せ子論理 (combinatory logic) は, λ 計算と同様に,任意の項 (計算機上のプログラムに相当) が関数である体系である [1]. λ 計算と密接な関係があり, 計算モデルとして重要である. 書換え規則 Sxyz→xz(yz), Kxy→xを持つ組合せ子 (combinator) S, K は, それぞれ, λ 項
λxyz.xz(yz), λxy.x に対応している. 全ての計算可能(帰納的, λ 表現可能) 関数は, 組合せ子 S, K だけで記述できる. 特に, 組合せ子論理は, 関数型プログラミング言語の効率的な実装に応用されている.
Barendregt は, 組合せ子 S は停止性を持たないことを示した [1]. Bergstra らは，組合せ子 S の非循環性(acyclicity) を示した [2]．Klop は, λ 計算と組合せ子論理の違いが循環書換え (cyclic reduction) にあることを示した [4]. λ 計算において, 有限かつ循環書換えを含む書換えグラフ G(M ) (すなわち, 書換え → により項 Mから得られる項全体の集合) から M →M 0 → · · · →M を満たす項 M を見つけることは困難ではない. しかしながら, 組合せ子 S, K だけに基づく組合せ子論理において,G(M ) が有限かつ循環書換えを含む項 M は存在しない.
さらに，Waldmann は, 組合せ子 S の非循環性を拡張し，組合せ子 S の非基底ループ性 (non-ground loopingness)を示し, 組合せ子 S のみから成る項が正規形を持つか否かを決定する手続きを与えている [10]．Probst らは, 書換え規則 Jxyzw→xy(xwz) を持つ組合せ子 J の停止性を示した [5]. 組合せ子 I, J は, λ 計算を制限した体系である λI 計算と密接な関係を持つ [1]. Ketema らは, 循環書換えは, 未定義な項であると考え, 全てが定義されているときは, 循環書換えは存在しないと主張した [3]. 正
確には, 正則 (orthogonal) 項書換えシステム (TRS) が,弱停止性を持つならば非循環性を持つことを示した. 組
合せ子論理の書換え規則は, 定数と二項演算記号で簡単に正則 TRS として表現することができる [9].
Sumllyan は，書換え規則 Lxy→x(yy) を持つ組合せ子 L を提案した [6]．Statman は，組合せ子 L の語の問題 (word problem) が決定可能であることを示した [8].
さらに，Sprenger らは，組合せ子 L の語の問題に対する効率的な決定可能アルゴリズムを与えた [7].
組合せ子 L のみから成る項 LL(LL) を書換え規則
Lxy→x(yy) で書換えると次のような無限書換え列が得られる [7].
LL(LL) → L(LL(LL)) → L(L(LL(LL))) →L(L(L(LL(LL)) → · · · → Ln (LL(LL)) → · · · .
したがって，組合せ子 L は停止性 (強正規性) を持たない．
本稿では, Bergstra ら [2] と同様の手法により，書換え規則 Lxy→x(yy) を持つ組合せ子 L の非循環性を示† 島根大学 総合理工学部, e-mail: munehiro@cis.shimane-u.ac.jp

す．さらに, 本結果の有用性を示すために, 次の 2 つの関係が決定可能であることを示す.
(1) 書換え規則 Lxy→x(yy) による書換え → の反射推移的閉包 →∗ は決定可能である.
(2) R = M0 →M1 → · · · を組合せ子 L のみから成る項上の無限書換え列とする. このとき, 関係 M ∈ R は決定可能である.

2.

準備

本稿の定義は, 文献 [2] に準ずる. 組合せ子論理ついては，文献 [1] の弟 7 章を参照して頂きたい．
抽象書換えシステム hA, →i は, 集合 A と A 上の二項関係 → で定義される [9]. →+ は, → の推移的閉包,→∗
は, → の反射推移的閉包である. = は, → により生成される同値関係である. 構文的等式を, ≡ で表す. A 上の書換
え a→+ a を循環 (cyclic) であるという．a ∈ A が正規形であるとは, a→b となる b ∈ A が存在しないときをいう. A 上の書換え → が, 無限書換え列 a0 →a1 →a2 → · · ·を持たないとき, 停止性を持つという.
A 上の書換え戦略 (strategy) は, M →∗ F (M ) を満たす写像 F ：A→A である. したがって, M が正規形ならば, F (M ) ≡ M . A 上の 1 ステップ書換え戦略
は, 次の条件 (1), (2) 満たす写像 F ：A→A である. (1)
M が正規形ならば, F (M ) ≡ M , (2) それ以外のとき,M →F (M ). 戦略 F が次の条件を満たすとき, ChurchRosser(CR)-戦略と呼ぶ. 任意の M, M 0 ∈ A に対して,
M = M 0 =⇒ ∃n, m ∈ N [F n (M ) ≡ F m (M 0 )].
L-項の集合 CL(L) を次のように帰納的に定義する．
(1) L ∈ CL(L), (2) s, t ∈ CL(L) ならば，(st) ∈ CL(L).
以下では, A = CL(L), 書換え規則 Lxy→x(yy) による CL(L) 項上の書換えを二項関係 → とする.

3.

組合せ子 L の非循環性

本節では，Bergstra ら [2] と同様の手法により，組合せ子 L の非循環性を証明する．
L-項の長さと重みを次のように定義する．これらは，
文献 [2] の S-項の長さと重みの定義中の 組合せ子 S をL に置き換えたものである．
定義 1 s ∈ CL(L) とする．s の長さ | s | を次のように定義する．(1) | L |= 1, (2) | (st) |=| s | + | t |. s の重み k s k を次のように定義する．(1) k L k= 1, (2)k (st) k= 2 k s k + k t k.
補題 2 s, t ∈ CL(L) とする．(1) s→t ならば，| s |≤| t |,(2) s→t かつ | s |=| t | ならば，s 中の L-リデックス
Lxy が書換えられ，このとき，y = L である．

(証明) 組合せ子 L の書換え規則と L-項の定義より, 自明.
¤

補題 3 C[ ] を L-文脈, すなわち，1 つのホールを含む L項とする．このとき，k s k > k t k ならば，k C[s] k >k C[t] k．

(証明) k s k>k t k と仮定し，L-文脈 C[ ] の構造に関する帰納法により示す．C[ ]=¤ のとき；自明．C[ ]=(M C 0 [ ])のとき；k C[s] k=2k M k+k C 0 [s] k, k C[t] k=2k M k +k C 0 [t] k. 帰納法の仮定より，k C 0 [s] k>k C 0 [t] k．したがって，k C[s] k > k C[t] k. C[ ]=(C 0 [ ]M ) のとき；k C[s] k= 2k C 0 [s] k+k M k, k C[t] k = 2k C 0 [t] k+k M k.
帰納法の仮定より，k C 0 [s] k>k C 0 [t] k．したがって，k C[s] k>k C[t] k.
¤
次に本稿の主定理を証明する.
定理 4 L-項において，循環書換えが存在しない．

(証明) 循環書換え M0 →M1 →M2 → · · · →Mn ≡ M0(n ≥ 1) が存在すると仮定する．このとき，| M0 |=|Mn |. 補題 2 (1) より，| M0 |=| M1 |=| M2 |= · · · =|Mn |. 補題 2 (2) より， 循環書換え中で書換えられるすべての L-リデックスは，LxL の形をしている．しかしながら，k LxL k = 5 + 2 k x k, k x(LL) k = 3 + 2k x k. よって，k LxL k>k x(LL) k が成り立つ．補題 3より，k M0 k > k M1 k > k M2 k > · · · > k Mn k =k M0 k. よって，矛盾する．
¤補題 5 R = M0 →M1 → · · · を CL(L) 上の無限書換え列とする. このとき, ∀n∈N , ∃m∈N [| Mm |> n].

(証明) n0 ∈ N に対して, ∀m ∈ N [| Mm |≤ n0 ]と仮定する. このとき, R の無限部分書換え列 R0 =
Mm0 →Mm0 +1 → · · · が存在し, ある定数 n1 ≤ n0 に対して, | Mm0 | ≤ | Mm0 +1 | · · · ≤ | Mm0 +m1 | (= n1 ) =| Mm0 +m1 +1 | (= n1 ) = · · · を満たす. 長さ n1 の L-項は有限個であるから, R は循環書換えを含む. これは, 定理 4 に矛盾する.
¤
本稿の主定理の有用性を示すために, 次の定理を証明する.
定理 6 (1) 書換え規則 Lxy→x(yy) による書換え → の反射推移的閉包 →∗ は決定可能である.
(2) R = M0 →M1 → · · · を CL(L) 上の無限書換え列とする. このとき, 関係 M ∈ R は決定可能である.

(証明) (1) M, N ∈ CL(L) とする. M →∗ N が成立するか否かが決定可能であることを示す. 補題 5 より, Mから始まる N の長さを超えるまでのすべての書換え列を考える. このとき, M から始まるすべての有限書換え列に N が属するかを確認することが可能である. (2)n0 =| M | とする. 補題 5 より, n0 ∈ N に対して, ∃m0 ∈N [| Mm0 |> n0 ]. | Mm0 |> n0 から, R の無限部分書換
え列 R0 = Mm0 →Mm0 +1 → · · · に対して, M 6∈ R0 . Rの有限部分書換え列 R00 = M0 →M1 → · · · →Mm0 −1 に対して, M ∈ R は決定可能である.
¤Bergstra らは, λ 計算に対して, 次のような定理を示している [2]. Λ を λ 項の集合とする.
定理 7 ([2]) Λ 上に再帰的な CR-戦略が存在する.

定理 8 ([2]) Λ 上に 1 ステップ CR-戦略が存在する. しかしながら, 再帰的ではない.

CL(S) を, 組合せ子 S のみから成る S-項の集合とす
る. Bergstra らは, 集合 Λ を CL(S) へ制限し, さらに組合せ子 S の非循環性を応用し, 次の定理を示している[2].
定理 9 ([2]) CL(S) 上に再帰的な 1 ステップ CR-戦略が存在する.
我々は, 定理 4 の組合せ子 L の非循環性の応用として,次の予想を与える.
予想 10 CL(L) 上に再帰的な 1 ステップ CR-戦略が存在する.

4.

むすび

本稿では, Bergstra らと同様の手法により，書換え規則
Lxy→x(yy) を持つ組合せ子 L の非循環性を示した．さらに, 本結果の有用性を示すために, 次の 2 つの関係が決定可能であることを示した. (1) 書換え規則 Lxy→x(yy)による書換え → の反射推移的閉包 →∗ は決定可能である. (2) R = M0 →M1 → · · · を組合せ子 L のみから成る項上の無限書換え列とする. このとき, 関係 M ∈ R は決定可能である.
今後の課題は, 組合せ子 L のみから成る項上に再帰的な 1 ステップ CR-戦略が存在することを示すことである.

参考文献[1] H. P. Barendregt, “The Lambda Calculus, Its Syntax and Semantics,” Elsevier, Amsterdam / NewYork, 1984.
[2] J. Bergstra and J. W. Klop, “Church-Rosserstrategies in the lambda calculus,” TheoreticalComputer Science, 9, pp.27–38, 1979.
[3] J. Ketema, J. W. Klop and V. van Oostrom,“Vicious circles in orthogonal term rewriting systems,” Electronic Notes in Theoretical Computer
Science, 124, pp.65–77, 2005.
[4] J. W. Klop, “Reduction cycles in combinatory
logic,” To H. B. Curry: Essays on Combinatory
Logic, Algebra, Lambda Calculus and Formalism,Academic Press, pp.193–214, 1980.
[5] D. Probst and T. Studer, “How to normalize theJay,” Theoretical Computer Science, 254, pp.677–681, 2001.
[6] R. Smullyan, “To Mock a Mockingbird,” Knopf,
New York, 1985.
[7] M. Sprenger and M. Wymann-Böni, “How to decide the lark,” Theoretical Computer Science, 110,pp.419–432, 1993.
[8] R. Statman, “The word problem for Smullyan’slark combinator is decidable,” J. Symbolic Computation, 7, pp.103–112, 1989.
[9] Terese, “Term rewriting systems,” Cambridge
University Press, 2003.
[10] J. Waldmann, “The combinator S,” Information
and Computation, 159, pp.2–21, 2000.