数理解析研究所講究録
第 1554 巻 2007 年 258-263

$K$

258

-開発閉包な左線形項書換えシステムの合流性*
島根大学総合理工学部 岩見宗弘 (Munehiro Iwami)

Faculty of Scienoe and Engineering, Shimane University
Matsue, Shimane, Japan, 690-8504
e-mail: munehiro@cis.shimane-u.ac.jp

概要

Huet は, 左線形かっ並行閉包な項書換えシステム (T$) は合流性を持つことを示
Toyama は, 並行閉包の条件を拡張し, 左線形かつ緩和並行閉包な TRS は合流性を持つことを示した. Ooetrom は, Huet と Toyama の条件を拡張し, 左線形かつ開発閉包な TRS は合流性を持つことを示した. さらに, Oyamagtlchi らは, Toyama の結果を一般化した $K$-閉包の概念を導入し, 左線形かつ $K$-閉包な TRS は, 合流性を持つことを示している. 本稿では, Oyamaguchi らと同様の手法により, 開発閉包を一般化した $K$ -開発閉包の条件を与え, 左線形かつ $K$-開発閉包な TIE は合流性を持つこ
した.

とを示す.

1

はじめに

項書換えシステム (TRS) は, 等式による柔軟な計算と効率的な推論を与えることができる [8]. TRS は, 関数論理型言語の計算モデルや定理自動証明, 記号処理, 代数的仕様記
述, 検証等に広く応用されている. TRS の合流性は, 与えられた項の最も単純な形 (正規形) が一意であることを保証する. しかしながら, 合流性は一般に決定不能であることが知られており, 合流性を示すために多くの十分条件が与えられている.
Huet は, 左線形かっ並行閉包な TRS は合流性を持つことを示した [2]. Toyama は, 並
行閉包の条件を拡張し, 左線形かつ緩和並行閉包な TRS は合流性を持つことを示した [9].
Oostrom は, Huet と Toyama の結果を, 開発閉包の概念を導入し, 高階項書換えシステム(HRS) へ拡張した [4], すなわち, 左線形かつ開発閉包な HRS は, 合流性を持つことを示した. Oyamaguchi らは, 上側並行閉包の概念を与え, 左線形かつ上側並行閉包な TRS は合流性を持つことを示した [6]. Gramlich は, 並行危険対の概念を与え, 左線形かっ並行危険対条件を満たす TRS は, 合流性を持つことを示した [1]. Okui は, 同時危険対の概念を与え,
左線形かっ強閉包な TRS は, 合流性を持つことを示した [3]. Oyamaguchi らは, Toyamaの結果を一般化した $K$-閉包の概念を導入し, 左線形かつ $K$-閉包な TRS は, 合流性を持つことを示した [7].

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

259
本稿では, Oyamaguchi ら [7] と同様の手法により, 開発閉包を一般化した K-開発閉包の条件を与える. 次に 左線形かつ $K$-開発閉包な TRS は合流性を持つことを示す. さらに,
本結果の有用性を示すために, 例を与える.

2

準備

本節では, 本稿で使用する定義と概念を述べる. 定義と概念は文献 [7], [8] に準ずる.
記号 は空列を表し,は空集合を表す. $V$ は変数の集合, $F$ は関数記号の集合とする.
$T$ は $V$ と $F$ から生成される項の集合とする.
項 $M$ に対して, $P(M)$ は $M$ の出現の集合$\emptyset$$\epsilon$を表す. $P_{F}(M)$ は項 $M$ における関数記号の出現の集合を表し, $M/u$ は出現 の $M$ の部分項を表し, $M[uarrow N]$ は部分項 $M/u$ を項 $N$ により置き換えることにより得られる項を表す. 項 $M$ における任意の変数の出現が 1 より大きくないとき線形であるという.
書換え規則 $l-r$ は, 項上の方向付けられた等式であり, 次の条件を満たす : $l\not\in V$ かつ$V(r)\subseteq V(l)$ . 書換え規則 $l-r$ } こ対して,が線形であるとき, 左線形であるという. 項書
$u$

$l$

換えシステム (TRS) は, 書換え規則の有限集合である. 任意の書換え規則が左線形であるとき, TRS $R$ が左線形であるという. TRS $R$ により, 項 $M$ が出現 において $N$ に書換えられるとは, ある代入 と書換え規則 $l-r\in R$ が存在し, $M=M[uarrow\sigma(l)]$ かつ $N$$=M[uarrow\sigma(r)]$ を満たすときをいい,により表す. TRS $R$ が合流性を持つとは,が成り立っときをいう. TRS $R$ により, それ以上書換えることができない項を $R$ の正規形と呼び, $R$ のすべての正規形の集合を $NF(R)$ により表す.
:
を書換え列とする. このとき, $\mathcal{R}(\gamma)=\{u_{0}, u_{1}, \ldots, u_{n-1}\}$ , すが互いに素ならば, は並行書換えであなわち, のリデックス出現の集合とする.
るとい $A\searrow M-$との書換え規則から得られる危険対のにより表す. TRS
集合 $CP(R_{1}, R_{2})$ を次のように定義する : $CP(R_{1}, R_{2})=\{\langle\theta(l_{1})[uarrow\theta(r_{2})], \theta(r_{1})\rangle_{u}|l_{1}$$arrow r_{1}\in R_{1},$ $l_{2}arrow r_{2}\in R_{2},$ $u\in P_{F}(l_{1}),$ $l_{1}arrow r_{1}\neq J_{2}arrow r_{2},$ $\theta(l_{1}/u)=\theta(l_{2})$}. ここで, $V(l_{1})$$\cap V(l_{2})=\emptyset$ かつ
は $l_{1}/u$ との最汎単一子である. $CP(R)$ は $CP(R, R)$ で定義される危険対の集合である. TRS $R$ に対して, 同時書換え $arrow R$ を次のように帰納的に定義する.
1. を変数とする. $xarrow R^{X}\cdot 2$ . $f$ を項数 の関数記号とする. $s_{i}arrow_{R}t_{t}(1\leq i\leq n)$ な,を満たす代入らば, $f(9_{1}, \ldots, s_{n})arrow_{R}f(t_{1}, \ldots, t_{n})$ . . $larrow r\in R$ とする.
すなわち, 任意の変数 に対して $\sigma(x)-e*R\tau(x)$ に対して, $\sigma(l)arrow_{R}\tau(r)$ .
$u$$\sigma$$M \bigwedge_{R}^{u}N$$arrow^{*}\cdotarrow tRR\subseteqarrow R*arrow_{R}^{*}$$\gamma$$M_{0}$$arrow R^{t)}uM_{1}arrow_{R^{1}}^{u}\ldotsarrow_{R}^{u_{n-1}}M_{n}$$\mathcal{R}(\gamma)$$\gamma$$R(\gamma)RM_{n}$$\theta$$R_{1}$$\gamma$$R_{2}$$l_{2}$

$x$

$n$

$3$

$\sigma-e\nu_{R}\tau$$\sigma,$$\tau$

$x$

3

$K$

-開発閉包な左線形項書換えシステムの合流性-開発閉包の定義を与える. 次に, 左線形かつ $K$-開発閉包な TRS は合流性を持っことを示す.
$K$-開発閉包は,Oostrom による大方開発閉包 [4] を一般化した条件であり, 匹開発閉包$(K=\emptyset)$ は, 大方開発閉包と一致する.
本節では,

$K$

定鵜 3.1 次の条件を満たすとき, 左線形 TRS $R$ は $K$ -開発閉包 (K-development closed)であるという.

1.

$K\subseteq R$

かつ $K$ は合流性を持つ.

260
2. $\forall\langle P, Q\rangle_{u}\in CP(K, R-K)(u\neq\epsilon)$ に対して,$Parrow KQ$ .

3. $\forall\langle P, Q\rangle_{u}\in CP(R-K, R)(u\neq\epsilon)$ に対して,$P-\infty_{R-K}\cdotarrow*K^{\cdot}arrow^{*}KQ$

4.

$\forall(P,$に対して,$Q\rangle_{\epsilon}\in CP(K, R-K)$$Parrow_{K}^{*}$.

$arrow_{K}^{*}$.

$c-\triangleright R-KQ$.

.

5. $\forall\langle P, Q\rangle_{\epsilon}\in CP(R-K, R-K)$ に対して,$Parrow_{K}^{*}$.

$arrow R-K$

$arrow_{K}^{*}$.

$arrow_{R}^{*}Q$.

定理 3.2 左線形かつ $K$ -開発閉包な TRS $R$ は, 合流性を持つ.
定理 3.3 TRS $R$ が, $K$ -閉包ならば,

4$K$-開発閉包である.

例
本節では, 本結果の有用性を示すために, 例を与える.

例 4.1 次の 3 つの TRS$R_{1}$,$R_{2},$$R_{3}$

を考える.

$R_{1},$$R_{2},$$R_{3}$

は, 文献碑で与えられている.

$R_{1}=\{f(g(g(x)))arrow a_{f}f(g(h(x)))arrow b$ ,$f(h(g(x)))arrow b,$ $f(h(h(x)))arrow c,$ ,$g(x)arrow h(x),$ $aarrow b,$ $barrow c$}.

,$f(c, x)arrow f(c, c,),darrow f(a, c),darrow f(c, b)\}$ .

$R_{2}=\{aarrow c_{f}barrow(i,$$f(a, b)arrow d,f(x, c,)arrow f(c,, c)$$R_{3}=\{f(x)arrow x,f(x)arrow f(f(x))\}$.

Okui により, 次のような表が与えられている $[3J$ .
$R_{1}$$R_{2}$$R_{3}$$\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}^{\cross}\ovalbox{\tt\small REJECT}^{\cross}Oyamaguchi- Ohta[6JO\cross Okui[3JToyama- Gmmlich[10J,[JJO\cross xxO$

満たさない)(O. . . 満たす,を与える.
本稿では, 新たに次の TRS$\cross\ldots$$R_{4}$$R_{4}=\{\begin{array}{l}g(x)arrow xf(f(x))arrow g(x)f(x)arrow f(f(f(x)))\end{array}\}$は, 従来までに提案されている合流条件を満たさないので, TRS
に対して, 次のような表が得られる.

TRS$R_{4}$$R_{4}$

Toyama-Grumlich$R_{1}$$R_{2}$$R_{3}$$R_{4}$$O$$\cross$$\cross$$x$$\Re OOOOOOOOOOkkuyyau\iota i\cross\cross Oxamm_{\vee}aguchi- Ohta[61Oaamaguchi- Ohta/7JOOOx\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}^{\cross X}\ovalbox{\tt\small REJECT}^{\cross}\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}\ovalbox{\tt\small REJECT}$$HHuex^{yy}Xfflffl$

究$R_{1},$$R_{2},$$R_{3}$,

261$CP(R_{4})=\{\langle g(x),$$(f(g(x)), g(f(x))\rangle_{1}\}$$\bullet$TRS$f(f(f(f(x)))))_{\epsilon},$$\langle f(f(f(f(x)))), g(x)\rangle_{\epsilon},$$\langle f(f(f(f(x)))), g(x)\rangle_{1;}$である.

は, Toyama-Gramlich の条件 $/10J,$ $/1J$ を満たさない, すなわち, 並行危険対条件 (parallel critical pair condition) (/1], pp.219) を満たさない.
$R_{4}$$\langle f(f(f(f(x)))), g(x)\rangle_{\epsilon}\in CP(R_{4})$に対して, $f(f(f(f(x))))(=P)4_{\ }\cdotarrow R_{4}*$$g(x)(=Q)$ が成立しない.
$\bullet$

TRS 塙は 2 Oyama9uchi-Ohta の条件 [司を満さない 2 すなわち, 上側並行閉包 (upside parallel closed) (/6], pp.190) ではない.
に対して, $f(f(f(f(x))))(=P)(\cdot\#_{R_{4}}\cuparrow_{R_{4=}}^{\epsilon})$. $(\dashv\vdash R_{4}W\cuparrow_{R_{4=}^{\epsilon}})g(x)(=Q)(W\neq\{\epsilon\})$ が成立しない.
$\langle f(f(f(f(x))))_{f}g(x)\rangle_{\epsilon}\in CP(R_{4})$$\bullet$は, Huet-Toyama-Oostrom の条件 $/4J_{f}/5$] を満たさな発閉包ではない.

TRS$R_{4}$$\langle f(f(f(f(x)))), g(x)\rangle_{\epsilon}\in CP(R_{4})$$Aa$すなわち, 大方開に対して, $f(f(f(f(x))))(=P)arrow R_{4}$$arrow^{*}\$$g(x)(=Q)$ が成立しない.
$\bullet$TRS 馬は, Okui の条件岬を満たさない, すなわち, 強閉包 (strongly closed) ([3],pp.10) ではない.
$\langle g(x), f(f(f(f(x)))) \rangle$\epsilon \in CP(五) に対して, $g(x)(=P)arrow^{*}R_{4}_{R_{4}}f(f(f(f(x))))$$(=Q)$ が成立しない.
$\bullet$

TRS($R_{4}$$K\neq\emptyset$

は, Oyamagu chi-Oh 如の条件 [7] を満たさない, すなわち, すべてのかつ $K\neq R_{4}$ ) に対して, $K$ -閉包 (K-closed) $([7J, pp.132)$ ではない.

$K\subseteq R_{4}$1. $K=\{g(x)arrow x\},$ $R_{4}-K=\{f(f(x))arrow g(x), f(x)arrow f(f(f(x)))\}$ のとき ;$\langle f(f(f(f(x)))),g(x)\rangle_{1}\in CP(R_{4}-K, R_{4})$ に対して, $f(f(f(f(x))))(=P)$$*_{R_{4}-K}\cdotarrow_{K}^{*}$. $arrow^{*}Kg(x)(=Q)$ は成立しない.

2. $K=\{g(x)arrow x, f(f(x))arrow g(x)\}$ , I ら一 $K=\{f(x)arrow f(f(f(x)))\}$ のとき ;$\langle f(f(f(f(x)))), g(x)\rangle_{1}\in CP(K, R_{4}-K)$

に対して, $f(f(f(f(x))))(=P)\dashv\vdash K$$g(x)(=Q)$ は成立しない.

3. $K=\{g(x)arrow x, f(x)arrow f(f(f(x)))\}$ , R ら $-K=\{f(f(x))arrow g(x)\}$ のとき ;に対して,は成立しない.

$\langle f(f(f(f(x)))),g(x)\rangle_{1}\in CP(R_{4}-K, R_{4})$$-\vdash R_{4}-K$$arrow^{*}K^{\cdot}arrow^{*}Kg(x)(=Q)$$f(f(f(f(x))))(=P)$

4. $K=\{f(f(x))arrow g(x), f(x)arrow f(f(f(x)))\},$ $R_{4}-K=\{g(x)arrow x\}$ のとき ;TRS $K$ は合流性を持たない.
$NF(K)\ni g(g(x))arrow^{*}Kf(f(f(f(x))))arrow^{1}Kf(f(x))arrow^{\epsilon}Kg(x)\in NF(K)$.

5. $K=\{f(x)arrow f(f(f(x)))\},$ $R_{4}-K=\{g(x)arrow x, f(f(x))arrow g(x)\}$ のとき ;$\langle f(f(f(f(x)))), g(x)\rangle_{1}\in CP(R_{4}-K, R_{4})$ に対して, $f(f(f(f(x))))(=P)$$-*R_{4}-K$$arrow^{*}K^{\cdot}arrow^{*}Kg(x)(=Q)$

は成立しない.

262
6. $K=\{f(f(x))arrow g(x)\},$ $R_{4}-K=\{g(x)arrow x, f(x)arrow f(f(f(x)))\}$ のとき ;TRS $K$ は, 合流性を持たない,$NF(K)\ni f(g(x))arrow_{K}^{1}f(f(f(x)))arrow_{K}^{\epsilon}g(f(x))\in NF(K)$1 から 6 より, TRS
包ではない.
$\bullet$

TRS$R_{4}$$R_{4}$は, すべての$K\subseteq R_{4}$($K\neq\emptyset$.

かつ $K\neq R_{4}$ ) に対して, $K$ -閉の合流性を定理鼠 2 を適用し示す.

$K=\{g(x)arrow x\}$R4-K={ff((鋼談鬼)))}1. TRS $K$ は合流性を持つ.
2. $CP(K, R_{4}-K)=\emptyset$ .
,S. $CP(R_{4}-K, R_{4})=\{(f(f(f(f(x)))), g(x)\rangle_{1_{f}}\langle f(g(x)), g(f(x))\rangle_{1},$$f(f(f(f(x))))\rangle_{\epsilon\prime}\langle f(f(f(f(x)))), g(x)\rangle_{\epsilon}\}$ .
$\langle f(f(f(f(x)))), g(x)\rangle_{1}\in CP(R_{4}-K, R_{4})$ に対して, $f(f(f(f(x))))(=P)$$\langle g(x)$$-arrow_{R_{4}-K}g(g(x))arrow Kg(x)(=Q)$ が成り立っ.

4. $CP(K, R_{4}-K)=\emptyset$ .
5. $CP(R_{4}-K, R_{4}-K)=\{\langle g(x), f(f(f(f(x))))\rangle_{e’}\langle f(f(f(f(x)))), g(x)\rangle$ ,$\langle f(g(x)), g(f(x))\rangle_{1}\}$.

$\forall\langle P, Q\rangle\in CP(R_{4}-K, R_{4}-K)$ に対して,$Q$$Parrow^{*}K^{\cdot}arrow R_{4}-K$$arrow_{K}^{*}$.

$arrow^{*}\$

が成り立っ. 例えば,

$f(f(f(f(x))))(=P)-e_{R_{4}-K}g(g(x))arrow_{K}g(x)(=Q)$ .
よって,$R_{4}$

は左線形かつ $K$ -開発閉包である. 定理 S.2 から,$TRSR_{4}$

は合流性を

持つ.

の合流性を, 本結果を用いしたがって f 従来までの合流条件が適用できない TRSの全ての合流性を本結果を用いて示て示すことができる. さらに, TRSの全てには適用できない.
すことができる. 従来の合流条件は, TRSの全てに適用可能であり,しかしながら, 本研究の合流条件は, TRS$R_{4}$$R_{1},$ $R_{2},$ $R_{3}$$R_{1},$ $R_{2},$ $R_{3},$ $R_{4}$$R_{1},$ $R_{2},$ $R_{3},$ $R_{4}$合流性を示すことができる.

5

むすび

本稿では, Oyarnaguchi らと同様の手法により, 開発閉包を一般化した $K$-開発閉包の条件を与えた. 次に, 左線形かつ $K$-開発閉包な項書換えシステムは合流性を持っことを示した. さらに, 本結果の有用性を示すために, 例を与えた. 今後の課題は, 本結果と Okui の条件を理論的に比較・検討することである.

263
謝辞

本研究に対して有益な助言を頂いた外山芳人先生, 酒井正彦先生に感謝致します.

参考文献[1] B. Gramlich, “Confluence without termination via parallel critical Pairs’ Proc. on
21st International Colloquium on Trees in Algebra and Programming, LNCS, 1059,
pp.211225, 1996.
[2] G. Huet, “Confluence reductions: abstract properties and applications to term rewriting systems,” J. ACM, 27, 4, pp.797821, 1980.
[3] S. Okui, “Simultaneous critical pairs and Church-Rosser property,” Proc. on 9th
Intemational Conf. on Rewriting Techniques and Applications, LNCS, 1379, pp.216, 1998.

[4] V. van Oostrom, “Development closed critical pairs,” Proc. 2nd International Workshop on Higher-Order Algebra, Logic and Term Rewriting, LNCS, 1024, pp.185-200,

1995.
[5] V. van Oostrom, “Developing developments’ TheoreticaJ.Computer Science, 175,
1, pp. 185200, 1997.

[6] M. Oyamaguchi and Y. Ohta, “A new parallel closed condition for Church-Rosser ofleft-linear term rewriting systems,” Proc. on 8th International Conf. on Rewriting
Techniques and Applications, LNCS, 1232, pp.187201, 1997.
[7] M. Oyamaguchi and Y. Ohta, “On the Church-Rosser property of left-linear term
rewriting systems,” IEICE Transactions of Information and Systems, E86-D, 1,
pp.131135, 2003.
[8] Terese, “Term rewriting systems,“ Cambridge University Press, 2003.

[9] Y. Toyama, “On commutativity of term rewriting systems,” IEICE Ttansactions ofInformation and Systems, J66-D, 12, pp.13701375, 1983 (in Japanese).

[10] Y. Toyama, “On the Church-Rosser property of term rewriting systems,” Technical
Report, 17672, NTT ECL , 1981 (in Japanese).