数理解析研究所講究録
第 1604 巻 2008 年 60-68

60

組合せ子の非循環性と非停止性*(Acyclicity and Non-Termination of Combinators)
島根大学総合理工学部 岩見宗弘 (Munehiro Iwami)Interdisciplinary Faculty of Science and Engineering, Shimane University
Matsue, Shimane, Japan, 690-8504
e-mail: munehiro@cis.shimane-u.ac.jp

概要

Sumllyan は, 書換え規 J $Lxyarrow x(yy)$ を持つ組合せ子 と書換え規則 $Oxyarrow y(xy)$を持つ組合せ子 $O$ を提案した. 本稿では最初に, Bergstra らの手法を一般化した組合
せ子の非循環性に対する十分条件を与える. その十分条件を用いて, 組合せ子 と $O$の非循環性を示す. 次に, 組合せ子 $O$ は停止性を持たないことを示す.
$L$$\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}$

$L$

1

はじめに

) は, Curry[3] により考案され, 帰納的関数の研究において歴史的に重要な役割を果たしてきた計算体系であり, 論理や計算の基礎として重要である. 組合せ子論理の計算対象は, 組合せ子 (combinator) と呼ばれる 2 つの定数 $S,$ $K$ と関数適用から構成される項であり, 2 つの計算規則 $Sxyzarrow xz(yz)$ と $Kxyarrow x$ だけを持つ.
組合せ子論理は 計算と深い関連があり, その性質や 計算との対応関係について様々な研究が行われている [1, 3, 6]. また, 組合せ子論理は関数型プログラミング言語の効率的組合せ子論理 (combinatory$10\dot{}c$$\lambda$$\lambda$

な実装に応用されている.
Klop は 計算と組合せ子論理の違いの 1 つが循環書換え (cyclic reduction), つまり, 項$M$ から同じ項 $M$ へ到達するような書換え $Marrow M’arrow\cdotsarrow M$ にあることを示した [8]. 書に基づく $M$ の書換えグにより項 $M$ から得られる項全体の集合を書換え関係
換え計算においては, $G(M)$ が有限かつ循環書換え
ラフと呼び, $G(M)$ と記す. このとき,を含むような項 $M$ が存在する. その一方で, 組合せ子論理においては, $G(M)$ が有限でありかつ循環書換えを含むような項 $M$ は存在しない [8].
組合せ子 $K$ のみからなる計算体系を考えると. どのような計算も停止する、 したがって, 組合せ子 $K$ のみからなる計算体系は循環性を持たない. 一方, 組合せ子 のみからなる計算体系は非停止性を持つ (停止性を持たない)[11 ため, 循環性を持つか否かは自明ではない. そこで Bergstra らは組合せ子 $S$ が非循環性 (acyclicity) を持つ (循環性を持たない ことを示した [2]. 近年, Waldmann は, 非循環性より強い性質である非基礎ループ性$\lambda$$arrow$$arrow$$\lambda$

$S$

$)$

’This paper is an extended abstract and the detailed version will be published elsewhere.

61(non-ground loop) を提案し, 組合せ子 が非基礎ループ性を持つことを示した. さらに,組合せ子 のみから成る項が正規形を持つか否かを決定する手続きを与えている [22].
一般の項を扱う計算モデルとして, 項書換えシステム (TRS) がよく知られている. 組合
せ子論理や組合せ子の書換え規則は, 項書換えシステムとして見倣すことができる. 項書
換えシステムに対する非循環性についても様々な研究が行われている. Plaisted は TRS の非循環性が一般的に決定不能であることを示している [15]. 一方, Ketema らは正則 TRS
が弱停止性を持つならば非循環性を持つことを示している [7]. また, 非循環性をより強くした性質として非ループ性 (non-loop) があるが, Middeldorp らは書換え規則が 1 つのTRS の場合でさえ非ループ性が決定不能であることを示している [12]. 彼らの非ループ性の決定不能性の証明から, 書換え規則が 1 つの TRS の非基礎ループ性も決定不能であることが分かる. また, 部分システムの性質から全体システムの性質が導かれることをモジュラ性と呼ぶが, 正則 TRS において非循環性がモジュラであること [9] や, (等式付)TRS の
非循環性と非ループ性 (non-loop) のモジュラ性についての研究も Midde\’idorp らにより行われている [13].
項書換えシステムでは, 様々な書換え規則を一般的に取り扱う. 同様に, 様々な書換え規則を持つ組合せ子を考えた場合, その性質はどのようになるのであろうか. このため,組合せ子 $S,$ $K$ 以外にも, 論理学における構造に関する推論規則 [17] に関連する組合せ子$B,$ $C,$ $W$ や計算と密接な関係を持つ組合せ子 等, 様々な組合せ子に関する研究が行われている [16, 6]. また, 組合せ子 $L,$ $O$ で Turing の不動点組合せ子 $U[1]$ を表すことができる [18]. 組合せ子の書換えが停止性を持つ場合はその非循環性は自明であるが, 非停止性を持つ組合せ子の循環性は明らかでない場合も多い.
単純な書換え規則を持つ組合せ子であるが停止性を持たない組合せ子として, 書換え
規則 $Lxyarrow x(yy)$ を持つ組合せ子 がある [18]. 組合せ子 が停止性を持たないことはSprenger ら等により示されている [19, 20]. また, 単純な書換え規則 $Oxyarrow y(xy)$ を持つ組
合せ子 $O[18]$ は本稿で示すように停止性を持たない. これらの組合せ子の書換え規則は,
弱停止性と強停止性が一致するクラスに含まれるため [10, 21], Ketema らの結果 [7] を利用して非循環性を示すことも出来ない.
本稿では, 組合せ子 及び組合せ子 $O$ に着目し, 循環性や循環性に関連する性質について調べる. 上記のように, 組合せ子に基づく計算体系において循環性は非常に重要な性質と考えられる. このため, 単純な書換え規則を持つ組合せ子の循環性について考察を行うことは,計算や組合せ子に基づく計算体系やその関連性について考察する上で重要で
$S$

$S$

$J$

$\lambda I$

$L$

$L$

$L$

$\lambda$ある.

本稿は次のように構成される. 第 3 節では, Bergstra ら [2] の手法を一般化した組合せ子の非循環性に対する十分条件を与える. その十分条件を用いて, 組合せ子 と $O$ の非循環性を示す. 第 4 節では, 組合せ子 $O$ が停止性を持たないことを示す.
$L$

2

準備
本稿の定義は文献 [2], [22], [21.] に準ずる.

62

2.1

抽象書換えシステム

は集合 $A$ と $A$ 上の二項関係で定義される.
の逆関係
抽象書換えシステム
ははを又はにより表す.
の反射推移的閉包である.
の推移的閉包,$=$ はにより生成される同値関係である. 構文的等式を で表す. $A$ 上の書換え $aarrow^{+}a$を循環 cyclic) であるという. $A$ 上の書換えが循環書換えを持たないとき, 非循環性を持っ (acyclic) という. $a\in A$ が正規形であるとは, $aarrow b$ となる $b\in A$ が存在しないときをいう. $A$ 上の書換えが無限書換え列を持たないとき, 停止性を持つという.
$\langle A,$$arrow^{-1}$$arrow$$arrow\rangle$$arrow^{+}$$arrow$$arrow^{*}$$arrow$$arrow$$arrow$$\equiv$$arrow$$($$arrow$

2.2$arrow$$a_{0}arrow a_{1}arrow a_{2}arrow\cdots$

組合せ子論理組合せ子論理ついては文献 [1] の第 7 章及び文献 [3], [6] を参照して頂きたい.
以下では, 記号 $Z$ をある組合せ子とする. 変数の加算無限集合を とする.
$Z$$\{Z\}$ 上の項の集合 $CL(\{Z\}, \mathcal{V})$ を次のように帰納的に定義する.
(1)
に対して,
$(st)\inCL(\{Z\}_{;}\mathcal{V})$$Z\in
CL(\{Z\},\mathcal{V}),$$t\in
CL(\{Z\},\mathcal{V})$ならば$x,$(2) $s,$. 変数を含まない項
を $Z$-項といい, $Z$-項全体の集合を $CL(Z)$ で表す. $Z$-文脈, すなわち,個以上のホールを含む $Z$-項の集合 $CL(\{Z,$ 口 を次のように帰納的に定義する. (1) $Z\in CL(\{Z, \square \}),$ $(2)$$\square \in CL(\{Z, \square \}),$ (3) $s,t\in CL(\{Z, \square \})$ ならば $(st)\in CL(\{Z, \square \})$ .
つのホー) を含む Z文脈を $C[]$ で表す. $(st)$ を括弧を省略して単に $st$ と書く. 括弧は左結合である, すなわち,
は $(\cdots(s_{1}s_{2})\cdots s_{n})$ を意味する. 代入
を から $CL(Z)$ への写像とする. 代入の定義域 $Dom(\sigma)=\{x\in \mathcal{V}|\sigma(x)\not\equiv x\}$ は有限である. 書換え規則 $Zx_{1}\cdots x_{n}arrow t$ は組
合せ子 $Z$ が持つ方向付けられた等式であり, 次の条件を満たす. 変数
は互いに
$t\in
CL(\emptyset,\{x_{1},\cdots,x_{n}\})$$Zx_{1}\cdotsx_{n}arrowt$による $CL(Z)$ 上の書換
相異なりかつ. 書換え規則$Z$えある -文脈 $C[],$を次のように定義する :$B_{n}\in CL(Z)$ に対して,$s\equiv C[ZB_{1}\cdots B_{n}]$ かつ $t\equiv C[t\{x_{1}arrow B_{1}, \cdots, x_{n}arrow B_{n}\}|$ .
このとき, $ZB_{1}\cdots B_{n}$ を Z- リ
デックスという. 以下では, $A=CL(Z)$ , 二項関係を書換え規則 $Zx_{1}\cdots x_{n}arrow t$ による$CL(Z)$ 上の書換えとする. 書換え
を循環 (cyclic) であるという. 書換え
が循環
書換えを持たないとき, 組合せ子 $Z$ は非循環性を持つ (acyclic) という. $C[]$ を $Z$-文脈,をループ (loop) という. 書換え
を代入とする. 書換え
がループを持たないとき, 組合せ子 $Z$ は非ループ性を持つという. 書換え $tarrow^{+}C[t]$ を基礎ループ (ground
が基礎ループを持たないとき, 組合せ子 $Z$ は非基礎ループ性を
loop) という. 書換え持つという. 本稿で使用する組合せ子と書換え規則を次の表 1 にまとめる.
$(\{Z\}\cap \mathcal{V}=\emptyset)$$\mathcal{V}$$\forall x\in \mathcal{V},$

$0$

$\})$

$1$

$s_{1}s_{2}\cdots s_{n}$$\sigma$$\triangleright$$\mathcal{V}$$\sigma$$x_{1},$$sarrow t\Leftrightarrow$$arrow$$B_{1},$$\cdots,$$x_{n}$$\cdots,$$arrow$$tarrow^{+}t$$\sigma$$tarrow^{+}C[t\sigma]$$arrow$$arrow$$arrow$

3

組合せ子の非循環性に対する十分条件

TRS の非循環性は一般に決定不能である [15], [14]. しかしながら, 書換え規則が 1 つのTRS の非循環性の決定可能性問題は未解決であると考えられる. 文献 [12] の最後 (p.126)
でも Plaised の結果 $[15|$ を書換え規則が 1 つの TRS へ強めることが可能か不明であると述べられている. また, Dauchet [4], Lescanne [11], Geser ら [5] により, 書換え規則が 1 つの TRS の停止性の決定不能性と相対決定不能性 (relative undecidability) に関する研究が

63

表 1: 組合せ子と書換え規則 ([18])

行われている. これらの手法は, 書換え規則の右辺 $B(\cdots)$ の根記号 $B$ が左辺 $A(\cdots)$ には出現しない TRS $\{A(\cdots)arrow B(\cdots)\}$ を構成するため, 書換え規則が 1 つの TRS の非循環性の決定可能性問題に対して, 直接適用できないと考えられる. したがって, 組合せ子の
非循環性の決定可能性問題も未解決であると考えられる.
本節では, Bergstra ら [2] の手法を一般化し組合せ子が非循環性を持つための十分条件を与える. この十分条件を用いて組合せ子 と $0$ の非循環性を示す. 以下では, 記号 $Z$ を書換え規則を持つ組合せ子とする.
文献 [2] では, 組合せ子 の非循環性を示すために -項に対して長さと重みを定義している.
-項に対する長さと重みを同様に定義する.
$L$$Zx_{1}\cdots x_{n}arrow t$

$S$

$S$

$Z$

定義 3.1 $s\in CL(Z)$ とする.の長さを次のように帰納的に定義する. (1) $|Z|=1_{\dot{J}}$(2) $|(st)|=|s|+|t|$ .
の重みを次のように帰納的に定義する. (1) $\Vert Z\Vert=1,$ $(2)$
$|s|$

$s$

$s$

$\Vert(st)\Vert=2\Vert s\Vert+\Vert t\Vert$$\Vert s\Vert$.

定義 3.2 組合せ子 $Z$ の条件を以下のように与える.
$n)$ に対して,(1) $Zx_{1}\cdots x_{n}arrow t,$ $\forall B_{i}\in CL(Z)(i=1,$$\cdots,$$B_{1},$$\cdots,$ $x_{n}arrow B_{n}\}|$$|ZB_{1}\cdots B_{n}|\leq|t\{x_{1}arrow$.

(2) $s\equiv C[\Delta]arrow C[\Delta’]\equiv t$ かつ $|s|=|t|$ ならば

表 1 の書換え規則を持つ組合せ子 $L,$ $O,$

$S$$\Vert\Delta\Vert>\Vert\Delta’\Vert$($\Delta$は Z- リデックス).

は次のように定義 32 の条件を満たす.

組合せ子 $L(1)|LB_{1}B_{2}|=1+|B_{1}|+|B_{2}|\leq|B_{1}|+|B_{2}|+|B_{2}|=|B_{1}(B_{2}B_{2})|$ .

(2)$sarrow t$

とする.

ある

$B_{1},$と表される. このとき,$C[]$$B_{2}\in CL(L)$ に対して,$|s|=|t|$ を満たすならば,$s\equiv C[LB_{1}B_{2}],$$B_{2}\equiv L$$t\equiv C[Bi(B_{2}B_{2})|$が成立することを $L$ -文脈の構造に関する帰納法により示す.
のとき ; $s\equiv LB_{1}B_{2}arrow B_{1}(B_{2}B_{2})\equiv t$ . $|s|=1+|B_{1}|+|B_{2}|=|B_{1}|+$$2|B_{2}|=|t|$ より, $|B_{2}|=1$ , すなわち, $B_{2}\equiv L$ である.

$\bullet$$C[]\equiv\square$$\bullet$$C[]\equiv(B_{3}C’[])$ のとき; このとき, $s\equiv(B_{3}C’[LB_{1}B_{2}]arrow(B_{3}C’[B_{1}(B_{2}B_{2})])\equiv t$ .
$|s|=|t|$ から $|C’[LB_{1}B_{2}]|=|C’[B_{1}(B_{2}B_{2})]|$ . 帰納法の仮定から,.
$C[]\equiv(C’[]B_{3})$ のとき ; 前項と同様.
$B_{2}\equiv L$$\bullet$

64

したがって, 任意の $B_{1}\in CL(L)$ に対して,$\Vert LB_{1}L\Vert>\Vert B_{1}(LL)\Vert$

を示せばよいが,これは $\Vert LB_{1}L\Vert=5+2\Vert B_{1}\Vert>3+2\Vert B_{1}\Vert=\Vert B_{1}(LL)\Vert$ より成立する.

組合せ子 $O(1)|OB_{1}B_{2}|=1+|B_{1}|+|B_{2}|\leq|B_{2}|+|B_{1}|+|B_{2}|=|B_{2}(B_{1}B_{2})|$.

(2) $sarrow t$ とする. ある$B_{2}\in CL(O)$ に対して, $s\equiv C[OB_{1}B_{2}],$ $t\equiv C[B_{2}(B_{1}B_{2})]$と表される. このとき, $|s|=|t|$ を満たすならば, $B_{2}\equiv O$ が成立することを $O$ -文
脈 $C[]$ の構造に関する帰納法により示す.
$B_{1},$$\bullet$$\bullet$のとき ; $s\equiv OB_{1}B_{2}arrow B_{2}(B_{1}B_{2})\equiv t$ . $|s|=1+|B_{1}|+|B_{2}|=|B_{1}|+$$2|B_{2}|=|t|$ より, $|B_{2}|=1$ , すなわち, $B_{2}\equiv O$ である.
$C[]\equiv\square$$C[]\equiv(B_{3}C’[])$ のとき; $s\equiv(B_{3}C’[OB_{1}B_{2}])arrow(B_{3}C’[B_{2}(B_{1}B_{2})])\equiv t$. $|s|=|t|$から $|C’[OB_{1}B_{2}||=|C’[B_{2}(B_{1}B_{2})||$ . よって, 帰納法の仮定から. $B_{2}\equiv O$ .
$\bullet$$C[]\equiv(C’[]B_{3})$ のとき; 前項と同様.

したがって, 任意の $B_{1}\in CL(O)$ に対して, $\Vert OB_{1}O\Vert>\Vert O(B_{1}O)\Vert$ を示せばよい
が, これは, $\Vert OB_{1}O\Vert=5+2\Vert B_{1}\Vert>3+2\Vert B_{1}\Vert=\Vert O(B_{1}O)\Vert$ より成立する.

組合せ子 $S(1)|SB_{1}B_{2}B_{3}|=1+|B_{1}|+|B_{2}|+|B_{3}|\leq|B_{1}|+|B_{3}|+|B_{2}|+|B_{3}|=$$|B_{1}B_{3}(B_{2}B_{3})|$.

(2) 組合せ子 $L,$ $O$ の場合と同様にして, すべてのかつ $|s|=$ 団を満たす と に対
$s\equiv
C[SB_{1}B_{2}S],$$t\equiv C[B_{1}S(B_{2}S)|$ が成立する. さらに, 任意のして,$B_{2}\in CL(S)$に対し, $\Vert SB_{1}B_{2}S\Vert=9+4\Vert B_{1}\Vert+2\Vert B_{2}\Vert>3+4\Vert B_{1}\Vert+2\Vert B_{2}\Vert=\Vert$$sarrow t$

$s$

$t$

$B_{1},$$B_{1}S(B_{2}S)\Vert$となる.

補題 3.3 $s,$ $t\in CL(Z)$ とする.
$|s|\leq|t|$$($.

$sarrow t$

かつ組合せ子 $Z$ が定義 82 の条件を満たすならば,

証明 組合せ子 $Z$ の書換え規則と $Z$ -項の定義かつ定義 32 (1) より自明$)$

補題 34 $C[]$ を Z-文脈とする. このとき

(証明)$\Vert s\Vert>\Vert t\Vert$$\Vert s\Vert>||t\Vert$

口

ならば $\Vert C[s]\Vert>\Vert C[t]\Vert$ .

と仮定し $Z$ -文脈 $C[|$ の構造に関する帰納法により示す.

$C[|\equiv\square$のとき; 自明.

$C[]\equiv(MC’[])$ のとき ; $\Vert C[s]\Vert=2\Vert M\Vert+\Vert C’[s]\Vert,$ $\Vert C[t]\Vert=2\Vert M\Vert$$+\Vert C’[t]\Vert$. 帰納法の仮定より 1 $C’[s]\Vert>\Vert C’[t]\Vert$ .

したがって $\Vert C[s|\Vert>\Vert C[t]$ $[$$C[]\equiv(C’[|M)$ のときも同様に示すことができる.

$\square$

次に本節の主定理を示す.
定理 35 定義 S.2 の条件を満たす組合せ子 $Z$ は, $CL(Z)$ 上で非循環性を持っ.
証明 循環書換え $M_{0}arrow\Lambda f_{1}arrow M_{2}arrow\cdotsarrow M_{n}\equiv M_{0}(n\geq 1)$ が存在すると仮定する. このとき, $|M_{0}|=|M_{n}|$ . 補題 33 より, $|M_{0}|=|M_{1}|=|M_{2}|=\cdots=|M_{n}|$ . 定義 32(2) から,$M_{1}\equiv C[\Delta|arrow C[\Delta’]\equiv M_{i+1}$ かつ $|M_{i}|=|M_{i+1}|$ より$\Vert\Delta\Vert>\Vert\Delta’\Vert(i=0,1, \cdots, n-1)$ .
$($

$)$

補題 3.4 より, $\Vert M_{0}\Vert>\Vert M_{1}\Vert>\Vert M_{2}\Vert>\cdots>\Vert M_{n}\Vert=\Vert M_{0}\Vert$ . よって矛盾する.

口

したがって, 定理 35 から次の結果が得られる.

65

系 36 $Z\in\{L, O, S\}$ とする. このとき, 組合せ子 $Z$ は $CL(Z)$ 上で非循環性を持つ.

例 37 表 1 の書換え規則を持つ組合せ子 $Z\in\{H, M, W, W^{1}, W^{*}, W^{**}\}$ はそれぞれ$CL(Z)$ 上で次のような循環書換えを持つ.
$HHHHarrow HHHH_{f}MMarrow MM_{f}WWWarrow WWW_{f}W^{1}W^{1}W^{1}arrow W^{1}W^{1}W^{1},$ $W^{*}$$W^{*}W^{*}W^{*}arrow W^{*}W^{*}W^{*}W^{*},$ $W^{**}W^{**}W^{**}W^{**}W^{**}arrow W^{**}W^{**}W^{**}W^{**}W^{**}$ .

しかしながら, これらの組合せ子は, 次のように定義 32 の条件を満たさないから定理 3.5 の反例ではない.
かつ $|s|=|t|$ であるが, $\Vert HB_{1}HB_{3}\Vert=10+4\Vert$$s\equiv C[HB_{1}HB_{3}]arrow C[B_{1}HB_{3}H]\equiv t$$\bullet$$B_{1}\Vert+\Vert B_{3}\Vert\not\simeq 5+8\Vert B_{1}\Vert+2\Vert B_{3}\Vert=\Vert B_{1}HB_{3}H\Vert(B_{1}, B_{3}\in CL(H))$

かつ同$\bullet$$s\equiv C[\Lambda fM|arrow C[MM|\equiv t$$\bullet$$s\equiv C[WB_{1}W]arrow C[B_{1}WW]\equiv t$$=$固であるが,$s\equiv C[W^{1}W^{1}B_{2}|arrow C[B_{2}W^{1}W^{1}|\equiv t$

MM .

$\Vert\not\simeq\Vert$$\Vert$.

かつ $|s|=|t|$ であるが,$B_{2}\Vert\not\simeq 3+4\Vert B_{2}\Vert=\Vert B_{2}W^{1}W^{1}\Vert(B_{2}\in CL(W^{1}))$$s\equiv C[W^{*}B_{1}B_{2}W^{*}|arrow C[B_{1}B_{2}W^{*}W^{*}|\equiv t$$\bullet$MM

かつ $|s|=$ 団であるが, $\Vert WB_{1}W\Vert=5+2\Vert B_{1}\Vert\not\simeq$$3+4\Vert B_{1}\Vert=\Vert B_{1}WW\Vert(B_{1}\in CL(W))$$\bullet$$\Vert$.

$\Vert W^{1}W^{1}B_{2}\Vert=6+\Vert$.

かつ同 $=|t|$ であるが, $\Vert W^{*}B_{1}B_{2}W^{*}\Vert=$$9+4\Vert B_{1}\Vert+2\Vert B_{2}\Vert\not\simeq 3+8\Vert B_{1}\Vert+4\Vert B_{2}\Vert=\Vert B_{1}B_{2}W^{*}W^{*}\Vert(B_{1},$$CL(W^{*}))$.

$s\equiv C[7V^{**}B_{1}B_{2}B_{3}W^{**}|arrow C[B_{1}B_{2}B_{3}W^{**}W^{**}]\equiv t$$\bullet$$B_{2}\in$

か っ $|s|=|t|$ であるが,$\grave$$\Vert W^{**}B_{1}B_{2}B_{3}W^{**}\Vert=17+8\Vert B_{1}\Vert+4\Vert B_{2}\Vert+2\Vert B_{3}\Vert\not\simeq 3+16\Vert B_{1}\Vert+8\Vert$$B_{2}\Vert+4\Vert B_{3}\Vert=\Vert B_{1}B_{2}B_{3}W^{**}W^{**}$

4I$(B_{1},$ $B_{2},$$B_{3}\in CL(W^{**}))$.

組合せ子 $O$ の非停止性

前節で示したように, 組合せ子 $L,$ $O,$ $S$ は非循環性を持つ. 組合せ子が停止性を持てば,非循環性を持つことは明らかであるため, 組合せ子 $L,$ $O,$ $S$ が停止性を持たないときに初めて, 前節の結果が自明な結果ではないといえる.
組合せ子 $S$ が停止性を持たないことは文献 [1, 22] により示されている. また, 組合せ
子 $L$ が停止性を持たないことは文献 [19, 20] により示されている. しかしながら, 組合せ
子 $O$ の非停止性についてはまだ知られていない. そこで, 本節では, 組合せ子 $O$ が停止
性を持たないことを示す.

定義 41$OX_{n}$.

$X_{0},$ $X_{1},$$\ldots\in CL(O)$

補題 42 任意の自然数 $k,$$n$を次のように帰納的に定義する. (1) $X_{0}\equiv OO,$ (2) $X_{n+1}\equiv$に対して, ある $O$ -文脈 $C[]$ が存在して, $X_{k}X_{n^{arrow+}}C[X_{n}X_{n+1}|$ .

66に関する帰納法で示す. $k=0$ のとき, $X_{0}X_{n}\equiv OOX_{n}arrow X_{n}(OX_{n})\equiv_{\wedge}Y_{n}X_{n+1}$
より明らか. $k=l+1$ のとき, $X_{l+1}X_{n}\equiv OX[X_{n}arrow X_{n}(X_{i}X_{n})$ . 帰納法の仮定より, ある$O$ -文脈 $C’[]$ に対して,$XiX_{n}arrow^{+}C’[X_{n}X_{n\neq 1}]$ が成立する.
したがって, $X_{n}(X_{l}X_{n})arrow^{+}$

(証明)

$k$

$X_{n}(C’[X_{n}X_{n+1}])$.

口

定理 43 組合せ子 $0$ は $CL(O)$ 上で停止性を持たない.

(証明) 補題 42 を繰り返し用いることにより, 次のような無限書換え列が得られる.
$X_{0}X_{0}arrow^{+}C_{0}\lceil X_{0}X_{1}\rceil$$arrow^{+}C_{0}[C_{1}\lceil X_{1}X_{2}\rceil]$$arrow^{+}C_{0}[C_{1}[C_{2}[X_{2}X_{3}]]]$$arrow^{+}\cdots$

したがって, 組合せ子 $O$ は $CL(O)$ 上で停止性を持たない.

5$\square$

むすび

本稿では組合せ子 $L$ と $O$ の非循環性を示した. 組合せ子 と $O$ は, Sumllyan[18] により提案された比較的単純な書換え規則を持つ組合せ子であるが, それらの非循環性は知られていなかった. また, 組合せ子 $O$ の非停止性も示した. 非停止性は組合せ子 については従来から知られていたが, 組合せ子 $O$ については著者の知る限り従来示されていな
$L$

$L$

かった.

本稿および先行研究の結果を以下の表にまとめる.
表 2: 組合せ子が持つ性質($\bullet$: 本研究, $O$ : 成立,$\cross$: 不成立, ◎: 予想, ?: 未解決)

今後の課題は, 組合せ子 $O$ の非基礎ループ性を示し, 組合せ子 $S$ と $O$ の非ループ性を解析することである. 組合せ子 $O$ は $SI$ で表すことが可能である. さらに, 書換え規則

67$Oxyarrow y(xy)$ の右辺 $y(xy)$ の部分項 $(xy)$と書換え規則 $Sxyzarrow xz(yz)$ の右辺 $xz(yz)$ の部
分項 $(yz)$ には類似性がある. したがって, 組合せ子 $O$ の非ループ性の解析手法は組合せ
子 $S$ の非ループ性の解析にも有用であると予想される.

参考文献[1] H. P. Barendregt, ’‘The Lambda Calculus, Its Syntax and Semantics,” 2nd revised
edition, North-Holland, 1984.
[2] J. Bergstra and J. W. Klop, ”Church-Rosser strategies in the lambda calculus,”
Theoretical Computer Science, 9, pp.27-38, 1979.

[3] H. B. Curry and R. Feys, “Combinatory Logic,” Vol.1, North-Holland, 1958.
[4] M. Dauchet, “Simulation of Turing machines by a regular rewrite rule,” TheoreticalComputer Science, 103(2), pp.409-420, 1992.

[5] A. Geser, A. Middeldorp, E. Ohlebusch and H. Zantema, ”Relative undecidability interm rewriting, Part 1: The termination hierarchy,” Information and Computation,
178(1), pp.101-131, 2002.
[6] J. R. Hindley and J. P. Seldin, ”Introduction to Combinators and -calculus,” Cambridge University Press, 1986.
$\lambda$[7] J. Ketema, J. W. Klop and V. van Oostrom, “Vicious circles in orthogonal term
rewriting systems,” Electronic Notes in Theoretical Computer Science, 124, pp.6577, 2005.
[8] 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.

[9] J. W. Klop, V. van Oostrom and F. van Raamsdonk, “Reduction strategies andacyclicity,“ Rewriting, Computation and Proof: Essays Dedicated to J. -P. Jouannaud on the Occasion of his 60th Birthday, LNCS, 4600, pp.89-112, 2006.
$[10|$

J. W. Klop, “Term Rewriting Systems,” Handbook of Logic in Computer Science,Vol. 2, Oxford University Press, pp.1-116, 1992.

[11] P. Lescanne, “On termination of one rule rewrite systems,” Theoretical Computer
Science, 132(2), pp.395-401, 1994.
[12] A. Middeldorp and B. Gramlich, “Simple termination is difficult,” Applicable Algebra in Engineering, Communication and Computing, 6, pp.115-128, 1995.

68[13] A. Middeldorp and H. Ohsaki, “Type introduction for equational rewriting,” Acta
Informatica, 36(12), pp.1007-1029, 2000.

[14] E. Ohlebusch, “Advanced Topics in Term Rewriting,” Springer-Verlag, 2002.
[15] D. A. Plaisted, “The undecidability of self-embedding for term rewriting systems,”
Information Processing Letters, 20, pp.61-64, 1985.

[16] D. Probst and T. Studer, “How to normalize the Jay,” Theoretical Computer Science,
254, pp.677-681, 2001.
[17] P. Schroeder-Heister and K.

$D\check{o}sen$, “Substructural Logics,” Oxford University Press,

1993.
[18] R. Smullyan, “To Mock a Mockingbird,” Knopf, New York, 1985.
[19] M. Sprenger and M. Wymann-B\"oni, “How to decide the lark,” Theoretical Computer
Science, 110, pp.419-432, 1993.
[20] R. Statman, “The word problem for Smullyan’s lark combinator is decidable,” J.
Symbolic Computation, 7, pp.103-112, 1989.
[21] Terese, “Term Rewriting Systems,” Cambridge University Press, 2003.
[22] J. Waldmann, “The combinator

2000.

$S,$

”

Information and Computation, 159, pp.2-21,