数理解析研究所講究録1093 巻 1999 年 136-141136

順序ソートの自動推論とラベル付けに基づく合流性判定への応用
宮下大

坂部俊樹

酒井正彦

Masahiko Sakai Toshiki Sakabe
名古屋大学大学院工学研究科情報工学専攻

Dai Miyashita

dai@sakabe.nuie.nagoya-u.ac.jp. nagoya-u. .jp{sakai,}$\mathrm{s}\mathrm{a}\mathrm{k}\mathrm{a}\mathrm{b}e$$\copyright \mathrm{n}\mathrm{u}\mathrm{i}\mathrm{e}$$\mathrm{a}\mathrm{c}$本論文は、 項書換え系の合流性を証明するシステムについて述べる。 証明手法としては、 従来の手法の他に外山によって提案されたラベル付けによる方法を用いる。 これは、 関数記号にラベル付けして得られる関数記号を導入することによりラベル付き項上の項書換え系 $R$ を項書換え系 $R’$ に変換する方法である。 新しく得られたの導出関係は、 ラベルを取り除いた項上の $R$ の導出関係と等しいため、 $R’$ の合流性を示すことによって従来の手法が適用できなかった項書換え系 $R$ の合流性を証明できる場合がある。 本研究では、 与えられた項書換$R’$

え系に対してそれと矛盾しない順序付型情報を自動的に付加し、 その型情報に基づいて関数記号にラベルを割り当てることにより自動的に $R’$ を求める方法を提案する。 また、 この方法に基づいて試作した合流性判定システ
ムについて述べる。

1

こでの順序ソート付きシグニチャ推論とは、 型の情報を持たない TRS から、 それと矛盾しない順序つき

はじめには書き換えのみで計算が進む
項書換え系
関数型言語モデルであり、 定理自動証明や代数的仕様記述などに利用され、 そのさまざまな性質についのシグニチャのうちで最も情報量の多いシグニチャを自動的に推論する手法で、 書換え規則によって定まるソートの順序に関する制約条件に基づいて行わて研究されている [2]。

れる。 ラベル割当ては、 推論したシグニチャにおい合流性は TRS の性質の–つで、 書換えの順序によらず計算結果が –意になるという意味を持つ。 しかて、 極大なソートを持つ関数記号にそれぞれラベル$(\mathrm{T}\mathrm{R}\mathrm{S})-$し、 TRS が合流性を持つかどうかは–般的には決定不能であるため、 TRS が合流性を満たす十分条件についてさまざまな条件が提案さてきた。 特に停止性を持つことが判明すれば危険対補題 [3] により合流性の判定は決定可能である。 しかし、 停止性がない
TRS の場合にはいくつかの十分条件 [4, 5, 6, 7] が存在するものの十分ではない。
方、 TRS が関数記号の重複がなく 2 つの TRSの和に分解 (直和分解) できるとき、 それぞれの
TRS の合流性を証明できれば元の TRS の合流性が$-$証明されるというモジ$=\mathrm{L}$

ラー性 [8] も有効である。 すなわち、 停止性を壊す要因となる規則を直和分解により分離することによって、 既存の手法が適用可能になる。

さらに、 直和分解不可能な TRS については、 ラベ

この手続を付けることによって行われる。 最後に、.
きの計算機上への実装について述べる。

2

準備

ここでは項書換え系の基本的な定義について述べる。 詳細については文献 [2] を参照されたい。
定義 1 項書換え系 (Term Rewriting System: $TRS$)
関数記号の集合を

変数の集合を $V$ とする。

$F_{\text{、}}$

項の集合 $T(F, V)$ は $F$ と $V$ から再帰的に定義される。 以下では項を $s,$
$t$

$t$

などで表す。 また $Var(t)$ は、中に出現する変数の集合を返す関数とする。 文脈

$C[$

$]$

は特別な定数口を$C[]$ 中の口を項$t$–つだけ持つ項であり、で置き換えて得られる項を $C[t]$ とは写像 $V$$T(F, V)$ である。 以下

ル付け [1] により各々の関数記号をその働きにより複数の関数記号に分離し、 導出関係が等価な TRS に変表す。 代入換することができる。 それにより、 直和分解の手法が適用可能となる。

$T(F, V)$ に自然に拡張される。

本論文では、 TRS の順序ソート付きシグニチャの推論の結果を用い、 関数記号に対する有効なラベルの割当てを自動的に行う方法について議論する。 こでは$\theta(x)$$\theta$を$x\theta$と表す$arrow$$\vee$とにする。 代入は定義域を項書換え系 $R$ は、 書換え規則と呼ばれる $T(F, V)$の二項組の集合である。 ただし、 どの規貝 U\rightarrow r も
かっ $Var(l)\supseteq Va\prime r(r)$ を満たすものとする。

$l\not\in V$$R$による書換え関係 $arrow_{R}:T(F, V)\cross T(F, V)$ は以下

137のように帰納的に定義される。

, $s=l\sigma,t=r\sigma$$S=f($ .. . , $s’,$, $t=f($ . . . ,$S’arrow Rt^{/},$

またよ.

$\cdots\cdots$.

$\varphi_{0(^{\mathrm{S}_{1}}}arrow \mathrm{S}_{2}\varphi_{0}(\mathrm{R}arrow \mathrm{s}\varphi_{0}(\mathrm{R}3arrow \mathrm{R}$$\exists larrow r\in R,$ $\sigma\in Sub$$sarrow_{R}t\Leftrightarrow\{$$\ldots\ldots$$\ldots)$$t^{l},$$\ldots)$$\mathrm{t}1arrow \mathrm{t}2arrow \mathrm{t}3arrow$$\varphi(\mathrm{R})$$\varphi(\mathrm{R})$$\varphi(\mathrm{R})$

項書換え系 $R$ に対して、 $t_{1}arrow Rt_{2}arrow R\cdots$ なる

図 31: 安定性

無限の書換え系列が存在しないとき、 $R$ は停止性を持つという。 また、 $arrow*0arrow\subseteqarrow**0arrow*$ を満たすとすなわち安定性とは、 図 31 のように、 ラベル付き
規則

き、 $R$ は合流性を持つという。 ここで、書き換えたあとに

$0$

は関係の

合成を表す。

で書き換えた項と、 ラベルなし規則 $R$ で$\varphi_{0}$によりラベル付けしたものが同じになることである。

書換え規則$l_{1}$$arrow r_{1},$ $l_{2}arrow r_{2}$$l_{1}=C[l’]$ なる文脈
$l’\theta_{1}=l_{2}\theta_{2}$$\varphi(R)$$C[]_{\text{、}}$

代入となるとき、 二項組について、 ある$\theta_{1},$$\theta_{2}$が存在し、$\langle r_{1}\theta, (C\theta_{1})[r_{2}\theta]\rangle$

32

を危険対と呼ぶ。 各左辺に出現する変数は 1 度ずつしか現れないとき $R$ は左線形という。 危険対がなく左線形であるとき、 $R$ は直交であると呼ぶ。

トップダウンラベル付け

ラベル割当て関数 $.\rho:\cdot Farrow L$ により、 各関数記
号に対して

付け関数

$\mathrm{L}$の要素の自然数を割り当てる。 ラベル: $T(F, V)arrow T(F\cup F^{L}, V)$ は、$\varphi_{i}$(t=x\in V のとき)

$x^{i}$$f^{i}(\varphi_{i}(t_{1}), \varphi i(t_{2}),$

3$\ldots,$

ラベル付けによる合流性の解析( $t=f(t_{1},$$\varphi_{i}(t)=\{$$t_{n})$$\ldots,$$f^{j}(\varphi_{j(}t_{1}),$ $\varphi j(t_{2}),$

本節では合流性解析のために用いるラベル付けに( $t=f(t1,$ついて述べる。

$\ldots,$$\varphi_{i}(tn))$, P(f)=0 のとき)$\ldots,$$\varphi_{j}(tn))$$tn),$ $\rho(f)=j(j\neq 0)$のとき)と定義される。 ラベル付き項 $t\in T(F^{L}, V^{L})$ に対して、 7 は、

3.1 ラベル付けに基づく項書換え系の変換$t$中の変数のラベルを取り除いて得られる項を表す。

関数記号の重複のない TRS の和からなる TRSは、 モジ ラー性 [8] により、 直和分解で得られたそ

テベル付け関数を書換え規則にも拡張し、$\varphi(R)=\{\overline{\varphi_{i}(l)}arrow\overline{\varphi_{i}(r)}|\forall larrow r\in R, i\in L\}$$=$

れぞれの TRS に分けて合流性を証明することができる。 本手法では与えられた TRS に対して、 ラベル付

け関数によってそれと導出関係が等価な TRS に変形とする。 このようにラベルを付ける手法を、 トップ

ダウンラベル付けと呼ぶ。
$ffl\rfloor 3$するものである [1]。
$0$

$f$

を含む自然数の集合 $L$ をラベルと呼ぶ。 ラベル$\{$付き関数記号の集合ならびにラベル付き変数の集合$\lambda\backslash \}$はは $F^{L}=\{f^{i}|f\in F, i\in L\},$ $V^{L}=\{x^{i}|x\in V,$ $i\in$(ラベル付けの例)
1$g$$arrow\rangle$

2$h,$ $a$

ト\rightarrow

$0$

である。

,

:
$T(F, V)\cross Larrow T$ (, V)、規則に対するラベル付
け関数 : $Rarrow R$ が与えられるとき、 TRSR が定義 2(安定性)項に対するラベル付け関数$t-R^{S}\Leftrightarrow\varphi_{0}(t)\sim_{\varphi(R)}$が成り立つことである。

TRS
関係と

$R$

$\varphi_{1}(g(f(X)))$$=$,$\varphi_{0}(g(x)))$$g^{2}(f^{1}(X^{1}))$$=$$g^{2}(x^{2})$となる。 また、$TRSR=\{h(x)arrow a.\}$ に対してトップダウンラベ

ノレ付けを行うと、 $\varphi(R)=\{h^{0}(x)arrow a^{0},$ $h^{1}(x)arrow$$a^{1},$$h^{2}(x)arrow a^{2}\}$となる。

$\varphi$に対して安定であるとは、$\varphi_{0}(s)$$h^{2}(a^{2})$$=$$\varphi_{0}$$F^{L}$$\varphi$とする。 項 $h(a),$ $g(x),$ $g(f(x))$ にしてそれぞれトップダウンラベル付けを行うと、$\varphi_{2}(h(a))$$L\}$

ラベル割当て関数を $\rho=$$\mapsto$がに対して安定であるとき、 $R$ の導出を行うと、 $\varphi(R)=\{g^{2}(x)arrow g^{2}(\dot{f}^{1}(X))\}$ となる。

の導出関係は–対一対応になり、 $R$ がこのとき $R$ は$\varphi$$\varphi(R)$例 4(トップダウンラベル付けでは安定性を満たさ.
ない例)$R=\{g(x)arrow g(f(x)).\}$ とする。 $R$に対して例 3 の $\rho.\text{を用いてトップダウンラベル付け}$

合流性を満たすこととは等価になる。

$\varphi(R)$.

が合流性を満たすこと$\varphi$に対して安定ではない。 なぜなら、$g(a)arrow Rg(f(a))$ という書換えが行われたとき、

図 4 のように、 ラベル付き規則$\varphi(R)$で書き換えた138

項と、 ラベルなし規則 $R$ で書き換えたあとに$\varphi$

よって $f^{*}.(\varphi i(t_{1}\sigma).,\ldots, \varphi i(tn\sigma))$によ’りラベル付けしたものが同じならないからである。

$=f^{i}(\overline{\varphi_{i}(t_{1})}\sigma..\varphi’,.,\overline{i(tn)}\sigma)$$=f^{i}(\varphi_{i}(t_{1}), \ldots, \varphi_{i}(tn))\sigma’$$=\overline{\varphi^{i}(f(t_{1},\ldots,t_{n}))}\sigma’$.

$\mathrm{f}^{1}\gamma_{\mathrm{a}}^{\mathrm{f}}\varphi|-_{\mathrm{R}}\mathrm{f}\mathrm{g}.\backslash _{\mathrm{f}^{\not\in}}^{\varphi}|\mathrm{a}||$$=\overline{\varphi_{i}(s)}\sigma’$のときも同様に示される。

$\rho(f)\neq 0$

口$\mathrm{g}^{2}$$|_{1}$

a$*$$\backslash ^{\backslash }\backslash$(定理 5 の証明)

証明$\mathrm{a}^{2}|$

.

$s$

$t$

$arrow R$とし、$\mathrm{f}^{1}$$\mathrm{f}^{1}$$\varphi i(s)arrow_{\varphi}(\dot{R})\varphi i(t)\text{であることを_{、}書換え関係の}\dot{\text{定}義}$$\mathrm{a}^{1}|arrow|\varphi\{\mathrm{R})\mathrm{g}^{2}\mathrm{a}|_{1}$$.$に関する帰納法を用いて証明する。

.

が

$t$

$s.arrow R$$l\sigma_{\}}t=r\sigma$

例 4 からわかるように、 トップダウンラベル付けにおける安定条件は、 次の定理が示すように同–規$\sigma$る。 よって$\overline{\varphi_{i}(\iota)}\sigma’$,であるので、ことである。

$\varphi_{i}(r\sigma)=\varphi_{i}(t)$次に.

.

$s’arrow t’$

Sub,

$=$

$s$

$Var(\varphi i(\iota))\supseteq$

とおくと補題 6 より$\varphi_{i}(r\sigma)=\overline{\varphi_{i}(r)}\sigma’$

則に出現する変数はすべて同じラベルがつけられる定理 5(トップダウンラベル付けに対する安定性)$\in$であるので、 $Var(\varphi_{i}(l))$ も無矛盾であ$\sigma’=\delta(\sigma)$$\overline{\varphi_{i}(r)}\in\varphi(R)$$\forall k\forall x^{i},$

$R,$

$\in$

であるとき、 $Var(\varphi_{i}(l)\cup\varphi_{i}(r))$ は無矛盾

$Var(\varphi_{i}(r))$$arrow r$$r$$arrow$であり、 また $Var(l)\supseteq Var(r)$ より

図 32: 安定性を満たさない例

項書換え系 $R$ の任意の規貝 U$\exists l$が成り立つ。

$\varphi_{i}(l\sigma)=$$\overline{\varphi i(l)}arrow$$\varphi_{i}(s)=\varphi_{i}(\iota\sigma)arrow_{\varphi}(R)$が示された。

$s=f(\ldots, s’, \ldots.),$ $t=f(\ldots, t’, \ldots)$

かつ

を考える。

について、

$x^{j}\in(Var(\varphi_{k}(l)\cup Var(\varphi k(r))))[i=j]$$\bullet\rho(f)=0$が成り立つとする。 このとき、 $R$ はトップダウンラベ
ル付け関数 に対して安定である。

$=$$\varphi_{i}(s)$$f^{i}(.

.

のとき、

.

$f^{i}(\ldots, \varphi_{i}(S’),$ $\ldots)$, \varphi_{i}(tl), \ldots)$$\varphi$によりこの定理を証面するために補題を用意する。
$V^{L})$ は$W[i = j]$ を満たすとき無$\varphi_{*}.(S^{J})$

かつ

$=$

$\varphi_{i}(t)$である。 帰納法の仮定であるから$arrow_{\varphi}(R)$$\varphi_{i}(t’)$$W(\subseteq$$\forall x^{i},$ $x^{j}$$\varphi j(s)arrow(R)\varphi j(\varphi t)$

矛盾であるという。 $W$ が無矛盾であるとき、 代入$T(F, V)$ を代入
: $V$
: $V$

$x\sigma’=x$$x^{j}$$S$$\varphi_{i}(_{S)} = f^{k}(\ldots, \varphi_{k}(s’),$ $\ldots),$ $\varphi i(t)$を用意する。 ここで、\in W のとき

その他のとき$f^{k}(\ldots, \varphi k(t^{t}),$

と同様に

とする。

$\ldots)$$=$.

である。 $\rho(f)=0$ の場合$\varphi_{i}(S)arrow\varphi(R)\varphi i(t)$が導かれる。
$\square$

補題 6 $W(\subseteq V^{L})$ を無矛盾なうベル付き変数の集とする。
合、: $V\mapsto T(F, V)$ を代入、

4

ラベル付けの自動化$\sigma’=\delta(\sigma)$$\sigma$

本節では、 TRS の順序ソート付きシグニチャ推論

このとき任意の $i\in L$ について $Var(\varphi_{i(}s))\subseteq W$ な
らば、$\varphi_{i}(s\sigma)=\overline{\varphi_{i}(s)}\sigma’$を用いて、 . ラベル割当てを自動的に行う方法についが成り立つ。

て述べる。

証明 項の構造に関する帰納法で証明する。

$s=x$ のときは明らかであるので、 $t=$.

...,

のとき、

$\ovalbox{\tt\small REJECT}arrow$に変換する関数$x\sigma’=\varphij(X\sigma)$$T(F^{L},V)\{$$\bullet\rho(f)=k\neq 0$$\sigma’$$rightarrow$$\sigma$が導かれる。

$\in$$t_{n}$$f(t_{1}$,) のときを考える。

4.1

順序ソート付きシグニチャ推論

まず、 順序付きシグニチャの定義について述べ$\varphi_{i}(s\sigma)$$=\varphi\dot{*}(f(t_{1}, \ldots, t_{n})\sigma)$.

る。 詳細については文献 [10] などを参照されたい。
ド$=\varphi:(f(t_{1}\sigma, \ldots, tn\sigma))$$f^{i}(\varphi:(t1\sigma), \ldots , \varphi_{i}(t_{n}\sigma))$$\backslash$$\rho(f)=0$ のとき、 明らかに $k=1,$ $\ldots,$ $n$ につ

上の半順序、 $F$ を関
数記号の集合、 $V$ を変数の集合、 $rs\sigma rt:F\cup Varrow$を関数寵号の返り値のソートあるいは変数のソー

いて $Var(\varphi_{i}(t_{k}))\subseteq W$ であるので帰納法の仮トを表す関数。

$=\{$$f^{j}(\varphi j(t1\sigma), \ldots, \varphi j(tn\sigma))$$\bullet$(\rho (f)=0 のとき)(\rho (f)=i\neq 0 のとき)

定義 7 順序ソート付きシグニチャ

定より$\varphi_{*}.\cdot(t_{k}\sigma)=\overline{\varphi i(t_{k})}\sigma l$

である。

$S$

をソートの集合、 $<$ を

$S$

$S$

$as\sigma rt$: $F\cross Narrow S$ を関数記号の引数のソートを表す関数とする。

139

このとき、 6 こ組 $\Sigma=$ ( $S,$ $<,$ $F.’ V$, rsort, asort)

例 10 推論の例

を順序ソート付きシグニチャと呼ぶ。 以下では
$f$$rsort(f)$

$F,$

$\in$

$=$

$asort(f, 1)$$s,$. . . , $aSort$ ( , n)=s、のときに :
$f$

$f$

$=$

$s_{1}$,.

$f(x, g(X))arrow x$$\cdot$$R=\{$$S_{1}\mathrm{X}\ldots \mathrm{X}s_{n}arrow s$$f(y, y)arrow a$と表記する。

定義 8 順序ソート付き項を順序ソート付きシグニヂャとする。 すべての
$s\in S$ について順序ソート付き項の集合$T(F, V)$ を以下のように定義する。

を考える。 推論規則により推論した結果、$\Sigma$rsort $(f)\leq rs\sigma rt(X),rS\sigma\Gamma t(f)\geq rsort(x)$ ,rsort $(f)\geq rsort(a)$(推論規則 (1) による)$\tau_{s}.(F, V)\subseteq$

1. : ならば $x\in T_{s}(F, V)$
ならば $f\in T_{s}(F, V)$
2. $f:arrow S_{0}$ かつ
$x$

$s$

”’

$s_{0}\leq s$

3.
.

$\cdot$$f$:$s_{1}\cross..=\cross s_{n}$つ、 すべての$i$$arrow$$s_{0},$

so$\leq$$s$かに対して $t_{i}\in T_{s:}(F, V)$ ならば$Q=|$$asaSoraSoasoraSoortrrtt(tt((f,2)\geq rsort(y(g,1(f,1)\leq rsort(x),’ a_{S}s)\geq r_{So}sorf,1)\geq rrt(y)f,2)\geq rs\sigma rt(g),aSort(_{X),a})aS\sigma\Gamma t(orortt(t(f(fg,,’ 1)\leq rsort(f,21)\leq rs\sigma rt(y)1))\leq r\Gamma t(y)\geq r_{S\sigma}sort(_{X}x)),$$f(t_{1}, \ldots, t_{n})\in T_{s}(F, V)$

このとき、 順序ソート付き項の集合は $T(F, V)$$\bigcup_{\ell\in s}\tau \mathit{8}(F, V)$$=$(推論規則 (2) による)と定義される。

定義 9 順序ソート付き項書換え系
次の条件をみたすとき項書換え系 $R$ は順序ソート付きシグニチャに整合するという。 $R$ 中の任意の書換え規則 $larrow r$ について、となる。 シグニチャ

なるソート

$s$

ソート付き項書換え系ともいう。

グニチャの推論の手法を述べる。 それぞれの関数について、 項 $t=f(t_{1}, t_{2}, \ldots, t_{n})$ に対して rsort $(t)=$’.

と拡張する。

( が変数めとき)(その他のとき)$\{s\geq rs\sigma rt(t), S\leq rsort(t)\}$$\{s\geq rs\sigma rt(t)\}$

ラベルの割り当て

次に、 推論の結果を、 関数記号へのラベル割り当

順序ソート付きシグニチャ

まず、 与えられた TRS の各々の変数と関数のソートにすべて異なる名前をつける。 次に$\mathrm{T}\mathrm{R}\mathrm{S}(F, R)$

ラベル割当て関数. . . (1)$(\phi;\{f(t1,t2, \ldots, tm)\}\cup T;Q)$$\ldots,$$asort(f, i-1)\not\in S_{maae}$

かつ asort(f, ) $\in S_{\max}$ のとき)$i$

(その他のとき)例 11 (ラベル付けその 1 の例)$t_{1})\cup$$t_{m})\cup Q)$

を次のように定義する。

(asort $(f, 1),$$0$$\Rightarrow(R;\{l, r\}\cup T;compat(rsort(\iota), r)\cup Q)$$\rho$$\tau(as\sigma rt(f, i))$$((\{larrow r\}\cup R);\tau;Q)$. . . (2)る。

$S_{\max}=\{s_{1}\},$ $\tau(s_{1})=1$$f,$ $g$

推論によって得られたソート上の擬順序 $Q$ より定を求めることができる。

ト\rightarrow 1$a\vdasharrow 0$

をソート間の大小関係 $<$ とみなすことによって、 順となる。

例 10 の $R$ を考えより、$\rho=\{$まる同偉類を新たにソートとし、 同値類間の半順序$\Sigma$: $S_{\max}arrow N$ をに$\rho(f)=\{$

序ソート付きシグニチャ

において、 極大なラベル付けその 1

により $(\phi;\phi;Q)$ となるまで推論する。

. . . . $\cup Compat(aSort(f, m),$$\tau$

ソートに対して 1 から順に番号を割り当てる関数とを初期値として、 . 以下の推論規則$\Rightarrow(\phi;T;c\sigma mpat(aS\sigma rt(f, 1),$$\Sigma$ソートの集合を $S_{\max}$ とする。

421

で表される関数である。

$\{$$S_{1}\mathrm{x}s_{1}arrow s_{1},$ $g:s_{1}arrow$$a:-s_{3}\}V=\{x:s_{1}, y:S_{1}\}$ となる。

$\mathrm{t}$

$\{$

対して、

:

$=$

する。

また、 cmpat $(s, t)$ は$(R;\phi;\phi)$$\{S_{1}, S_{2,3}S\}<$$=$てに適用する 2 種類の方法について述べる。

本研究における、 項書換え系の順序ソート付きシ$rs\sigma rt(f)$$s_{2},$

4.2と $s’$ が存在する。 このとき $R$ を順序

は $S$$\{(s_{2,1}S), (_{S_{3}}, S_{1})\}F=\{f$$\Sigma$$l\in T_{s}(F.’ V),r\in T_{s’}(F, V),$ $S\geq s^{t}$$\Sigma$

140

422

ラベル付けその 2conf(R)
switchcase yes: return(yes)case no: return(no)otherwise : if$(\exists\rho\in assign(R)$$=$ラベル割当て関数$\rho’$は、$(\mathrm{s}\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{f}(\mathrm{R}))\{$$\tau(rsort(f))$$\rho’(f)=\{$$0$... rsort. .. その他のとき$(f)\in S_{\max}$ のとき

再び例 10 の $R$ を$[[divide(R,\rho)\neq fail]$

考える。 $s_{1}\in S_{\max},$ $\tau(s_{1})=1$ であるため、 ラベル$\wedge[\forall R’\in divide(R, \rho)$

例 12 (ラベル付けその 2 の例)$conf(R’)=yes]])$付け関数は以下のようになる。

return$f\mapsto 1$$(\mathrm{y}e\mathrm{s})$$\}$$\rho’=\{$$g,$$a-\rangle 0$5

合流性証明システム

5.1

システムの概要

前節のアルゴリズムと、 2 で述べた従来から広く知られている合流性判定手法を計算機上に実装しであり、 ソースは約 5000 行程
た。使用言語は$\mathrm{C}++$

度になった。 本システムは、$\bullet$.

.

$\bullet$

従来の方法による合流性の証明 (sconf)

ラベル付けによる直和分解 (divide)

順序ソート付きシグニチャ推論によるラベル
割当て (assign)の 3 つのモジュールからなる (図 5.1)。

図 52: 合流性判定アルゴリズム

52

証明例 1

まず以下の TRS を考える。
$(f(xf(x,’ ga((x)g(x)arrow g()))arrow fg(f(_{X,x}))(x,x))$$R=\{$ $a(x)arrow x$$h(x)arrow h(a(h(x)))$
この TRS は 4 番目の規則により停止性がなく、 1
番目と 2 番目の規則のため直交性をもたない。 また、 直和分解も不可能である。 よって従来の–般的な方法では合流性の判定が困難である。
本システムでは、 まず順序ソート付きシグニチャ

推論を行う。

図 51: 合流性判定ツール

本システムの実行の流れは以下のようになる。 (図5.2).

罷 $0.\delta$ :11 園片 . ノ $-$ 「丹 8‘\nearrow ’ ノ $–\tau$ 丁す旧隔

1. 従来の方法で合流性が証明できれば、 終了す

ここで、$SO\Gamma t1$, sort2. . . は各ソートを表す。

$rs\sigma rt(g),$ $s_{2}=as\sigma

る。
.

2. できなければ、 順序ソート付きシグニチャ推論を行い、 ラベルの割当てを求める。

3. 2 の結果直和分解できるラベル割当てに対して、 再帰的にメイン関数を呼び出す。

$s_{1}$$=$

rt(a, 1)=rsort(a),s_{3}=$$rs\sigma rt(f),$ $s_{4}=as\sigma\Gamma t(h, 1)$, $s_{5}=rsort(h)$ , $s_{6}=$$as\sigma rt(.g, 1)=as\sigma rt(f, 1)=asort(f, 2)$ である。 各

関数名の右に引数のソートが、$arrow$の右には返り値のソートが表されている。 その後に、 ソートの大小関係が表されている。

141

次に、 推論結果をラベル付けに適用する。 図 53で求めたシグニチャより、 極大なソートは $S_{\max}=$である。 ラベル割り当て関数は、$\rho$て、 関数記号に対するラベルの割り当ての自動化を提案した。 また、 そのアルゴリズムを計算機上に実装し、 合流性判定システムを試作した。

$=$

文献 [1] では、 本論文で用いたラベル付け関数の他$f,$ $g\mathrm{F}arrow 1$$\{\}\{^{s_{4},s_{6}}$となる。

$h\vdasharrow \mathit{2}$$a\mapsto 0$

1$\ovalbox{\tt\small REJECT}_{\mathrm{a}}\mathrm{h}.T^{-1}2\exists^{\aleph,r}\mathrm{x};^{\mathrm{J}1\mathrm{t}\rangle}-->\aleph::r^{-}- 2\aleph->\vdash \mathrm{i}r\overline{\omega}>:1\aleph l^{- 1}\mathfrak{t}_{\mathrm{x}}1\mathrm{g}-\text{響^{}\ovalbox{\tt\small REJECT}}1<\mathrm{r}\mathfrak{B}\aleph\aleph|->\aleph\aleph\rangle$

図 54: ラベル付けに対する適用

その結果$\varphi(R)$$\mathrm{f}$る。 この場合$\varphi(R)$$0$であることを示してい[1] 外山芳人、 ラベル付けによる項書き換えシステムの解析、 LA シンポジ
ム論文集,46-49,1998.

は図 55 のように 3 つに直和分$=\mathrm{L}^{-}$

解される。
$\mathrm{x})\rangle$$\ovalbox{\tt\small REJECT} \mathrm{a}42\overline{\approx}1\mathrm{f}\mathrm{f}-3\vdash 2*1211\iota\aleph;(\aleph)\zeta_{\aleph}\cross)-|,$$\mathrm{g}-\neq_{1}->->-\rangle->1\mathrm{f}_{\aleph}\aleph\overline{)})>8-\overline{1}^{>}(\mathrm{f}\overline{1}(\aleph r\aleph \mathrm{g}\vdash 2(\aleph 1()\mathrm{t}r2()))\vdash 2\mathrm{t}*\underline{\mathrm{g}}1()7)\{1\overline{\mathrm{x}}))^{(\aleph_{l}}$

.

.

.

$\text{図^{、}}\backslash$

$5.5$

.

:

. .

$\text{直和}J\text{ノ}\Re\not\in$$-$

次に、 本システムは直和分解したそれぞれの TRS

後の課題である。

参考文献

は図 54 のようになる。 このとき、図中の f-O は のラベルがにもボトムアップラベル付け関数なども提案されているので、 これらのラベル付け関数に有効なラベル付けについても同様な自動化を行っていきたい。 また、 本手法が適用可能な TRS のクラスについても今

1[2] F.Baader,T.Nipkow: “Term Rewriting and All
That”, Cambridge Univ. Press,1998.
[3]

word problems in Universal algebra”, In J. Leech editor,
Computational Problems in Abstrct Algebra,
263-297,1970.

[4]

the Church-Rosser propertyof term rewriting systems”, Technicalport, NTT,December 1981.
NTT ECL TR.

$\text{ヨ}1--$$\mathrm{Y}.\mathrm{T}\mathrm{o}\mathrm{y}\mathrm{a}\mathrm{m}\mathrm{a}:$””$\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{e}$$0_{\mathrm{n}}$$\mathrm{R}e$の合流性を従来の手法によって示すことによって$\varphi(R)^{\text{の}合流性を示す}-$ 。

$\mathrm{D}.\mathrm{E}.\mathrm{K}\mathrm{n}\mathrm{u}\mathrm{t}\mathrm{h},\mathrm{P}.\mathrm{B}.\mathrm{B}\mathrm{e}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{x}:$$17\dot{6}7\mathit{2}$

その様子を図 56 に示す。

[5]$\mathrm{x})\rangle$$\overline{r}1\mathrm{f}1\mathrm{f}\mathrm{f}-1\aleph\aleph l\mathrm{g}-1\mathfrak{t}^{\epsilon_{\overline{)}}1(\underline{\aleph}}\aleph,\yen 1)->\mathrm{X}\mathrm{x}))\rangle>\mathrm{g}-\overline{1}(\mathrm{f}\overline{\iota}(\rangle>\underline{8}1(\mathrm{f}1\aleph|\overline{\mathrm{x}}))^{(}\aleph$of term rewriting
systems”, Programming of Future Generation
Computers,2:393-407,1988.
$\mathrm{Y}.\mathrm{T}\mathrm{o}\mathrm{y}\mathrm{a}\mathrm{m}\mathrm{a}:$”$\mathrm{C}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{u}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{i}\mathrm{t}\mathrm{y}$$\mathrm{t}_{\Phi 1}1\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{e}$CrltlCal palp$(_{8^{-}}1(\{-1(\mathrm{x},\aleph)),\mathrm{f}- 1(\mathrm{x}.\epsilon- 1(_{\aleph})))$

lolrula[6] V.
developments,TheoreticalComputer Science, 175159-181,1997$\mathrm{o}_{\mathrm{o}\mathrm{S}\mathrm{t}\mathrm{r}}\mathrm{o}\mathrm{m}:\mathrm{D}\mathrm{e}\mathrm{V}\mathrm{e}\mathrm{l}\mathrm{o}\mathrm{P}\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{c}\mathrm{m}\mathrm{f}\mathrm{h}H[] \mathrm{t}$$–2–$$\mathrm{r}0(\theta->\aleph$[7]”$\mathrm{B}.\mathrm{G}\mathrm{r}\mathrm{a}\mathrm{m}\mathrm{l}\mathrm{i}\mathrm{C}\mathrm{h}:$$\mathrm{c}_{0}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{u}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}$$\mathrm{c}\alpha \mathrm{t}i\mathrm{l}\mathrm{t}\mathrm{K}\mathrm{t}$-$\mathrm{h}- 2\yen\Gamma 2(^{\mathrm{x}}\aleph\}_{->\mathrm{h}-}^{-}\rangle \mathrm{x}_{2(\mathrm{a}-2\langle\vdash 2(_{\aleph})\rangle)}$$|\mathrm{D}\mathrm{t}\mathrm{b}q\mathrm{i}\iota_{8\mathrm{f}}l1^{*}1\mathrm{r}\mathrm{H}\alpha\backslash |\mathrm{w}\mathrm{t}\mathrm{i}\infty$

Crltbl Palr doem’tr廿$\Re \mathrm{i}\mathrm{s}\mathrm{t}$$\mathrm{C}\mathrm{A}\mathrm{A}\mathrm{p}’ 96$[8]

the Church-Ros8er property
for the direct sum of term rewriting system”,
Jounal of ACM, 42:128-143,1987.

[9]

and
Church-Rosser theorems”., Jounal of ACM,20:160187,1973.

$\mathrm{m}\mathrm{a}\mathrm{l}$$\mathrm{c}\alpha[] \mathrm{f}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{t}$$[] \mathrm{m}’\iota\epsilon \mathrm{a}1R$

without termination

via parffiel critical pairs”, Trees in Algebra and, ,LNCS,1059,211Programming
225,1996.

$\mathrm{c}\mathrm{p}\mathrm{i}\dot{\iota}_{1\mathrm{c}\mathrm{a}}1\mathrm{t}\varpi 1\mathrm{r}\mathrm{n}\mathrm{t}1\mathrm{o}\mathrm{e}\mathrm{p}_{\mathrm{a}}\mathrm{i}\Gamma \mathrm{m}[]’ \mathrm{t}\Re \mathrm{J}S\mathrm{t}$$1$$\mathrm{Y}.\mathrm{T}\mathrm{o}\mathrm{y}\mathrm{a}\mathrm{m}\mathrm{a}:$”$0_{\mathrm{n}}$.

図 56: 分割証明

その様子を図 56 に示す。

6

おわりに
本研究では、 トップダウンラベル付けを用いてTRS の順序ソート推論の結果を適用することによっ$\mathrm{B}.\mathrm{K}.\mathrm{R}\mathrm{o}\mathrm{S}\mathrm{e}\mathrm{n}:$”$\mathrm{T}\mathrm{r}\mathrm{e}rightarrow \mathrm{m}\mathrm{a}\mathrm{n}\mathrm{i}_{\mathrm{P}^{\mathrm{u}}}1\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{s}\mathrm{y}_{\mathrm{S}\mathrm{t}\mathrm{e}}\mathrm{m}8$[10] U.Waldmann:”Semantics in Order-Sorted Specifications”, Theoretical Computer Science,94:133,1992.