数理解析研究所講究録
第 1562 巻 2007 年 56-60

56

組合せ子 $L$ の非循環性とその応用 *島根大学総合理工学部 岩見宗弘 (Munehiro Iwami)
Faculty of Science and Engineering, Shimane University

Matsue, Shimane, Japan, 690-8504
e-mail: munehiro@cis.shimane-u.ac.jp

概要

本稿では, Bergstra らと同様の手法により, 書換え規則 $Lxyarrow x(yy)$ を持っ組合
さらに, 本結果の有用性を示すために, 次の 2 つの関係がせ子 $L$ の非循環性を示す.

決定可能であることを示す.
(1) 書換え規則 $Lxyarrow x(yy)$ による書換え関係の反射推移的閉包$arrow*$は決定可能である.

(2) $R=M_{0}arrow M_{1}arrow\cdots$ を組合せ子$L$のみから成る項上の無限書換え列とする. このとき, 関係 $M\in R$ は決定可能である.

1

はじめにSumllyan は, 書換え規則 $Lxyarrow x(yy)$ を持っ組合せ子 (combinator) を提案した [3].
Statman は, 組合せ子 の語の問題 (word problem) が決定可能であることを示した [5].
さらに, Sprenger らは, 組合せ子の語の問題に対する効率的な決定可能アルゴリズムを与えた [4].
$L$

$L$

$L$

組合せ子 $L$ のみから成る項 $LL(LL)$ を書換え規則 $Lxyarrow x(yy)$ で書換えると次のような無限書換え列が得られる [4].
$LL(LL)$$arrow L(LL(LL))$$arrow L(L(LL(LL)))$$arrow L(L(L(LL(LL))$$arrow\cdots$$arrow L^{n}(LL(LL))$$arrow\cdots$

したがって, 組合せ子 $L$ は停止性 (強正規性) を持たない.

Barendregt は, 書換え規則 $Sxyzarrow xz(yz)$ を持っ組合せ子 は停止性を持たないことを示している [1]. Bergstra らは, 組合せ子の非循環性 (acyclicity) を示し, 次の 2 つの関係が決定可能であることを示している [2]. (1) 書換え規則 $Sxyzarrow xz(yz)$ による書換え$S$$S$’This paper is an extended abstract and the detailed version will be published elsewhere.

57

関係の反射推移的閉包は決定可能である. (2) $R=M_{0}arrow M_{1}arrow\cdots$ を組合せ子 $S$ のみから成る項上の無限書換え列とする. このとき, 関係 $M\in R$ は決定可能である. さらに,
Waldmann は, その結果を拡張し, 組合せ子 $S$ の非基底ループ性 (non-ground loopingness)を示し, 組合せ子 のみから成る項が正規形を持っかどうかを決定する手続きを与えてい$arrow^{*}$$S$る [6].

本稿では, Bergstra ら [2] と同様の手法により, 書換え規則 $Lxyarrow x(yy)$ を持っ組合せ子の非循環性を示す. さらに, 本結果の有用性を示すために, 次の 2 つの関係が決定可能であることを示す.
(1) 書換え規則 $Lxyarrow x(yy)$ による書換え関係の反射推移的閉包は決定可能である.
$L$(2) $R=M_{0}arrow M_{1}arrow\cdots$ を組合せ子 のみから成る項上の無限書換え列とする. このとき, 関係 $M\in R$ は決定可能である.

$L$$arrow*$2準備

本稿の定義は, 文献 [2] に準ずる. 組合せ子論理 (combinatory logic) ついては, 文献[1] の弟 7 章を参照して頂きたい.
抽象書換えシステム (ARS)とその集合上の 2 項関係 $arrow\subseteq AxA$ かは, 集合ら成る. 関係の推移的閉包をで表す.
で表し, 反射推移的閉包をは,を表す.
より生成される集合 $A$ 上の等式であり,は,は集合 $A$ 上の構文的等式で$\langle A, arrow\rangle$$arrow+$$arrow$$=$$A$$arrow r$$arrow$$rightarrow$$arrow\cuparrow$$\equiv$ある.

定義 2.1 $xarrow^{+}x$ を満たす $x\in A$ が存在するとき, ARS ( $A,$いう.

$arrow\rangle$は, 循環 (cyclic) であると

定義 22 か項の集合 $CL(L)$ を次のように定義する.

1. $L\in CL(L)$ ,2. $s,t\in CL(L)$ ならば,$(st)\in CL(L)$以下では, $A=CL(L),$項関係

3$2$$arrow$を書換え規則 $Lxyarrow x(yy)$ に関する書換えとする.

組合せ子 $L$ の非循環性

本節では, Bergstra ら [2] と同様の手法により, 組合せ子 $L$ の非循環性を証明する.
ル項の長さと重みを次のように定義する. これらは, 文献 [2] の $S$-項の長さと重みの定
義中の組合せ子 $S$ を $L$ に置き換えたものである.
定義 3.1 $s\in CL(L)$ とする.の長さ $|s|$ を次のように定義する.
$s$(1) $|L|=1$ ,58(2) $|(st)|=|s|+|t|$ .
$s$の重み(1)$\Vert s\Vert$$\cdot\Vert L\Vert=1$を次のように定義する.

,(2) $\Vert(st)\Vert=2||s\Vert+\Vert t\Vert$ .
補題 3.2 $s,t\in CL(L)$ とする.

.

(1)

$sarrow t$ならば,(2)$sarrow t$

かっ $|s|=|t|$ ならば,$|s|\leq|t|$

中の L- リデックス Lxy が簡約され, このとき, $y=L$$s$である.

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

自明

補題 33 $C[]$ を $L$ -文脈, すなわち, 1 つのホールを含むならば, $\Vert C[s]\Vert>||C[t]\Vert$ .

$L$

口項とする.

このとき,$\Vert s\Vert>\Vert t\Vert$(証明)$\bullet$$||s\Vert>\Vert t\Vert$と仮定し,-文脈 $C[]$ の構造に関する帰納法により示す.

$L$$C[]=$ 口のとき ; 自明.

$\bullet C[]=(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$

帰納法の仮定より,.

$\Vert C’[s]\Vert>\Vert C’[t]\Vert$. したがって,$\Vert C[s]\Vert>\Vert C[t]\Vert$.

$C[]=(C’[]M)$ のとき ;$\Vert C[s]\Vert=2\Vert C’[s]\Vert+||M\Vert$$\Vert C[t]\Vert=2||C’[t]||+\Vert M||$

帰納法の仮定より,,.

$\Vert C’[s]\Vert>\Vert C’[t]\Vert$. したがって,$\Vert C[s]\Vert>\Vert C[t]\Vert$.

口

次に本稿の主定理を証明する.

定理 3.4 $L$ -項において, 循環書換えが存在しない.

(証明) 循環書換え $M_{0}arrow M_{1}arrow M_{2}arrow\cdotsarrow M_{n}=M_{0}(n\geq 1)$ が存在すると仮定する.
このとき, $|M_{0}|=|M_{n}|$ . 補題 32(1) より, $|M_{0}|=|M_{1}|=|M_{2}|=\cdots=|M_{n}|$ . 補
題 3.2 (2) より, 循環書換え中で簡約されるすべての L- リデックスは, LxL の形をしている.

しかしながら,$||LxL||=5+2||x||$ ,$\Vert x(LL)||=3+2||x||$

よって,$\Vert$.

LxL $||>\Vert x(LL)\Vert$ が成り立っ. 補題 3.3 より,$\Vert M_{0}\Vert>\Vert M_{1}\Vert>\Vert M_{2}||>\cdots>\Vert M_{\mathfrak{n}}\Vert=||M_{0}\Vert$

よって, 矛盾する.

.

口

59

補題 35 $R=M_{0}arrow M_{1}arrow\cdots$ を $CL(L)$ 上の無限書換え列とする. このとき, $\forall n\in N,$$\exists m\in$$N[|M_{m}|>n]$ .

(証明) $no\in N$ に対して, $\forall m\in N[|M_{m}|\leq no]$ と仮定する. このとき, $R$ の無限部
分書換え列 $R’=M_{m_{0}}arrow M_{mo+1}arrow\cdots$ が存在し, $|M_{m_{0}}|\leq|M_{mo+1}|\cdots\leq|M_{m_{0}+m_{1}}|\leq|$$M_{mo+m_{1}+1}|\leq\cdots(\forall m\in N, |M_{mo+m}|\leq n_{0})$ を満たす. 長さの -項は有限個であるから, は循環書換えを含む. これは, 定理 3.4 こ矛盾する.
口
本稿の主定理の有用性を示すために, 次の定理を証明する.
$n_{0}$$L$$R$定理 36 (1) 書換え規則 $Lxyarrow x(yy)$ による書換え関係の反射推移的閉包
能である.

$arrow*$は決定可(2) $R=M_{0}arrow M_{1}arrow\cdots$ を $CL(L)$ 上の無限書換え列とする. このとき, 関係 $M\in R$ は決定可能である.

(証明)(1) $M,$ $N\in CL(L)$ とする. $Marrow^{*}N$ が成立するかどうかが決定可能であることを示す.
補題 3.5 より, $M$ から始まる $N$ の長さを超えるまでのすべての書換え列を考える.
このとき, $M$ から始まるすべての有限書換え列に $N$ が属するかを確認することが可能である.

(2)no $=|M|$ とする. 補題 35 より, $n_{0}\in N$ に対して, $\exists m_{0}\in N[|M_{m_{O}}|>no].$衡から, $R$ の無限部分書換え列 $R’=M_{m_{0}}arrow M_{m\text{ }+1}arrow\cdots$ に対して, $M\not\in R’$ .
$R$ の有限部分書換え列 $R”=M_{0}arrow M_{1}arrow\cdotsarrow M_{m\text{。}-1}$に対して, $M\in R$ は決定可能$|M_{m_{\text{。}}}|>$。

である.

口次の定義は, 文献 [2] の定義中の A を $CL(L)$ に置き換えたものである.
定義 3.7(J) $CL(L)$ 上の書換え戦略は、 $Marrow^{*}F(M)$ を満たす写像 $F:CL(L)arrow CL(L)$である. よって, $M$ が正規形ならば, $M\equiv F(M)$ .

$CL(L)$ 上の 1 ステップ書換え戦略とは, 次の条件を満たす写像 $F:CL(L)arrow CL(L)$である :$\bullet$$\bullet$$M$が正規形ならば, $F(M)\equiv M$ ,$M$が正規形でないならば, $Marrow F(M)$ .

(2) 戦略 $F$ が, 次の条件を満たすとき Church-Rosser (CR)-戦略であるという :$\forall M,$$N\in CL(L)$ に対して, $M=N$ ならば,$\exists n,$$m\in N[F^{n}(M)\equiv F^{m}(N)]$

予想 3.8 $CL(L)$ 上に再帰的な 1 ステップ $CR$ -戦略が存在する.

.

60

4

むすび

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

$L$$arrow^{*}$

$L$

参考文献
[1] H. P. Barendregt, “The Lambda Calculus, Its Syntax and Semantics,” Elsevier,$Amsterdam/New$ York, 1984.

[2] J. Bergstra and J. W. Klop, “Church-Rosser strategies in the lambda calculus,”$Th\infty retical$ Computer Science, 9, pp.27-38,
1979.
[3] R. Smullyan, “To Mock A Mockingbird, Knopf, New York, 1985.
)[4] M. Sprenger and M. Wymann-Boni, “How to decide the lark,” $Th\infty retical$ Computer
Science, 110, pp.419-432, 1993.
[5] R. Statman, “The word problem for Smullyan’s lark combinator is decidable,” J.

Symbolic Computation, 7, pp.103-112, 1989.
[6] J. Waldmann, “The combinator ,$S$2000.

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