数理解析研究所講究録
第 833 巻 1993 年 69-79

69

部分項の評価順が指定できる項書換え系とその性質について
服部 哲, 岡野 浩三, 東野 輝夫, 谷口

健一

Satoshi Hattori, Kozo Okano, Teruo Higashino and Ken’ichi Taniguchi
大阪大学基礎工学部情報工学科

Department of Information and Computer Sciences, Faculty of Engineering Science,

Osaka University, Toyonaka, Osaka 560, JAPAN

1

まえがき

等式によって表現された系を計算モデルとして扱う枠組みである項書換え系が近年活発に研究されて[1, 2, 3, 4].

る.

項を分割することは, 例えば, 停止性の判定の際の 2 項間の順序の判定の容易化にっながる. また, 分割した部分項の評価順を定めることは, 項書換えの経路を限定することになる. これらによって, 古典的な項書換え系では, 等式は向きの付いた
書換え規則とみなされ, 項を書換え規則で簡約するこ

項書換え系による記述では停止性や合流性を満たさとによって計算を行う. また, 項書換え系の拡張とし

がある.

いる

なかった場合でも, それらを満たすようにできる場合て条件付き項書換え系が提案されている $[5, 6]$ . 条件付

本論文では, 部分項の評価順が指定できるクラス

約を行う. 項書換え系や条件付き項書換え系では停nuCTRS に対し, 停止性, 合流性を満たすための1 っの十分条件を与えているが, クラスを制限することで, 正当性の証明は文献 [6] の Kaplan の方法を拡止性と合流性が重要な性質であり, それらを満たすた

張して行えた. また, それらの十分条件を用いた完備めの十分条件と, 十分条件を用いた完備化手続きが知化手続きを提案している (完備化手続きが利用できるられている [1, 2, 3, 4, 5, 6].

ための条件の詳細にっいては現在検討中である). 結果として, 提案するクラスでは, 条件の等式での単一き項書換え系は条件付き書換え規則から成るが, 条件付き書換え規則は条件が成立する場合にのみ項の簡条件付き書換え規則における条件としては, 等式の論理積$(S, 6$ ]や, メンバシップ関係 $[10, 11]$ などが提案さの化代入で部分的な計算結果を保持することによって,れている. さらに, 等式の論理積による条件を用いる

自然な形で部分項の評価順が指定できるようになっが, 等号の意味を項の同一性でなく単一化可能性とすている. また, 与えた停止性, 合流性の十分条件も文る条件付き項書換え系 (例えば AMLOG [8, 9]) も提案されている. そのような条件付き項書換え系では,

PROLOG のような充足可能解の推論や, 手続き型言語的な計算順序の指定が可能である.
本論文では, 条件の等式の等号の意味を単一化可能性とするような条件付き項書換え系の 1 っの部分クラス (正規形単一化可能条件付き項書換え系, nuCTRS)を提案する. ただし, 本論文では, 条件の等式の成立の判定順序を定めたクラスで, さらに, 出現する変数

献 [6] の十分条件を若干変更した程度のもので, 従来の結果の自然な拡張になっている.
以下, 2. で項書換え系と条件付き項書換え系について簡単に述べた後, 3. で正規形単一化可能条件付き

項書換え系と, その部分クラスである

IIIui 型の項書

換え系を定義する. そして, IIIui 型の項書換え系に
対し, 4. で停止性, 5. で合流性を満たすための 1 っの十分条件をそれぞれ与え, 6. で完備化手続きを提案
する.

に制限を加えたク ラスの mICTRS について論じている.

その結果, PROLOG のような充足可能解の推論

2

項書換え系, 条件付き項書換え系

機能はもたず, 手続き型言語的な計算順序の指定に重点をおいたクラスとなっている.
ここでの計算順序の指定とは, 簡約時の部分項の評

2.1

項書換え系

本節の定義, 定理などは, 文献[1, 2, 3] などに基価順の指定という意味である. 条件の等式の右辺の項を変数とすれば, 等式の左辺での計算結果を単一化

づく .

代入で保持することになる. その左辺での計算を簡約時の部分項の評価とすれば, 簡約時に項を分割する

定義 2.1 書換え規則$T=T(F, V)$ を, 関数記号の集合 $F$ の要素と変数記ことや, 分割した部分項の評価順を定めることができ

号の集合

$V$

の要素で表される項の集合 (項集合) と

70
する.

書換え規則

このとき,

$r$

は,

2 っの項

かっ,

$u\not\in v$$r$$Var(u)\supseteq Var(v)$$uarrow v$ と表すを

ここで, $Var(t)$ は項$t$$v\in T$ の組で,$u,$

定義 2.6 項書換え系の局所合流性, 合流性

項書換え系 $\Sigma=<T,$ $R>$ が以下を満たすとき,であるものをいう.

.

.

に含まれる変数記号の集合
口と項の間に, 書換え規則$s$: $uarrow v$ によって$r$

簡約関係 $tarrow s$ が成立するとは, 以下の 2 点が成立

.
.

$t$

の位置

$\omega$における変数でない部分項ちと,の書換え規則部の左辺の項とが単一化代入$u$によって単一化可能 (すなわち, ち$s=t[\omegaarrow v\sigma]$

また, 関係$arrow$$=u\sigma$$\Sigma$$t_{1},$$t_{2}\in T$に対し$t_{1}arrow s,$ $t_{2}arrow rs$$tarrow t_{1},$ $tarrow t$

.

, であ

なる項 $s\in T$ が存在する.
$\Sigma$は合流性を満たすという.

任意の項
るとき,

$t,$

$t_{1},$$t_{2}\in T$$t_{1}arrow\alpha s,$に対し$t_{2}arrow’s$$tarrow^{*}t_{1},$ $tarrow t_{2}$

なる項

であ

$s\in T$ が存在する.

$r$口$\sigma$) である.
定義 2.7 危険対である.

2 つの書換え規則の反射推移閉包を$arrow^{\vee}$

と表す.

口

$u$

$r_{1}$の変数でない部分項: $uarrow v,$$u_{\omega}$と$p$$r_{2}$: $parrow q$ について,とが最汎単一化代入

によって単一化可能であるとする. このとき

$r_{1}$と$\sigma$$r_{2}$の危険対 $<A,$ $B>$ を次のように定義する.

定義 2.3 項書換え系

項書換え系

$t,$

また, 項書換え系 \Sigma が以下を満たすとき,することをいう.

項

任意の項
るとき,

定義 22 書換え規則による簡約関係$t$は局所合流性を満たすという.

を表すとする.

項$\Sigma$は, 以下の 2 字組で定義される.
$<A,$ $B>=<v\sigma,$ $u\sigma[\omegaarrow q\sigma]>$$\Sigma=<T,$ $R>$口

ここに, $T$ は項集合, $R$ は書換え規則の集合である. 口定理 22 項書換え系 $\Sigma=<T,$ $R>$ が以下を満たすと定義 2.4 正規形$tarrow s$ なる項という. 項$s$.

き, \Sigma は局所合流性を満たす.

項書換え系 $\Sigma=<T,$ $R>$ において, 項 $t\in T$ に対しが存在しないとき,$u\in T$ の正規形を,$u\downarrow$$t$は正規形である
口

と記す

$R$

の任意の危険対 $<A,$ $B>$ に対し,

$A\downarrow=B\downarrow$

が

成立する.

定義 2.5 項書換え系の停止性

口

項書換え系 $\Sigma=<T,$ $R>$ の $R$ の規則による簡約に対し, $t_{1}arrow t_{2}arrow\cdots(t_{1}, t_{2}, \cdots\in T)$ なる無限の簡約列が存在しないとき,$\Sigma$は停止性を満たすという.

定理 21 項書換え系 $\Sigma=<T,$ $R$

口>が単純化順序(simplification ordering)\succ によって以下を満たすとき,$\Sigma$.

は停止性を満たす.
$R$$\sigma$

に対し,

すとき,

2.2

口

は合流性を満たす$\Sigma$

条件付き項書換え系

本節の定義, 定理は, 特記しない限り文献 [中の任意の書換え規則$u\sigma\succ$

定理 2.3 項書換え系 \Sigma が停止性と局所合流性を満た$r$: $uarrow v$ と任意の代入

v\mbox{\boldmath $\sigma$}が成立する.

$6|$

に基

づく .

定義 2.8 条件付き書換え規則 [5]口

条件付き書換え規則$r$は, 以下のような構文で表される.
ここで, 単純化順序$\succ$は以下の 2 条件を満たす厳格$u_{1}=v_{1}\wedge\cdots\wedge u_{n}=v_{n}\Rightarrow uarrow v$

半順序 (strict partial order) である.

.
.

(subterm property):$f(\cdots)t,$
)

部分項性
$T,$

$\cdots$

単純化順序は整礎
る$\cdots\in T,$$F,$$\forall t$$\in$

ここで, $u,$ $v,$

$u_{1},$$v_{1},$$\cdots,$$u_{n},$ $v_{n}$は項である.

口

以下特記しない限り, 条件付き書換え規則

単調性 (compatibility): $\forall f\in F,$$t_{1)}t_{2},$$\in$$\succ t$$\forall t,$$t’\in T$(well-founded)$iota\succ t_{2}\succ$,$t\succ$)$t’\Rightarrow f(\cdots, t, \cdots)\succ f(\cdots, t’)$($\forall f$

$r$

といえ

を示すものとする.

[5)
定義 2.9 条件付き書換え規則による簡約関係

であなる無限の項の列が存在しない) ことが知られている.

ば, 上記の

$r$

項

$t$

と項

$s$

の間に, 条件付き書換え規則

$r$

によって

簡約関係 $tarrow s$ が成立するとは, 以下の 3 点が成立することをいう.

71

.
.

項

の位置 \omega における変数でない部分項ちと,$t$の書換え規則部の左辺の項

任意の $i(1\leq i\leq n)$ に対し,

$-$

$r$

とが単一化代入 \mbox{\boldmath $\sigma$}に$u$

よって単一化可能 (すなわち,$t_{\omega}=u\sigma$$c\iota\sigma\succ$) である.
口

すべての$i(1\leq i\leq n)$に対し, 以下のいずれかが成立する.

( 型)

$-$

$I$

$u_{i}$

定理 2.4 安定で単純化性を満たす II 型の項書換え系
から$v_{i}$

へ到達可能である. これは,ある系列
$u;\equiv t_{1,}t_{j},$ $\cdots,$ $t_{m_{i}}\equiv v_{i}$ が存在して意の $j(1\leq j\leq m_{i}-1)$ に対し,

$t_{j}arrow 1_{j}+\iota$である

口

定義 2.13 文脈付き危険対

えられる.

条件付き項書換え系 $\Sigma=<T,$ $R>$ の $R$ 中の 2 っの(III 型) u:から$-$

$v_{i}$

への( 回以上の) 簡約過
$0$

書換え規則

程が存在する.
$r_{1}$(IIIn 型) III 型で,$-$口に対し, ある項の正規形を求める手続きは決定手続き)(II 型) u:と v:とが, 互いに等しい項に書換$-$は停止性を満たす.

定理 2.5 安定で単純化性を満たす II 型の項書換え系, 任または, $t_{j+1}arrow t_{j}$ が成立することである.

.

$u\sigma\succ u_{j}\sigma,$$v_{i}\sigma$$v_{i}$

が変数を含まない正規$r_{2}$$r_{1},$$r_{2}$:: $u_{1}=v_{1}\wedge\cdots\wedge u_{n}=v_{n}\Rightarrow uarrow v$: $p_{1}=q_{1}\wedge\cdots\wedge p_{m}=q_{m}\Rightarrow parrow q$形である.
$s=t[\omegaarrow v\sigma]$について, $u$ の変数でない部分項

である.

一化代入
口

定義 210 条件付き項書換え系

条件付き項書換え系$\Sigma$$\sigma$

$T$

と

$P$

とが最汎単

によって単一化可能であるとする.

このときの$r_{1},$$r_{2}$の文脈付き危険対 (contextual crit-

ical pair) $ccp$ を以下のように定義する.

$[s]$は以下の 2 字組で定義される.

$B>$

$ccp$

$=$

$C\Rightarrow<A,$

$C$

$=$

$u_{1}\sigma=v_{1}\sigma\wedge\cdots\wedge u_{n}\sigma=v_{n}\sigma$

$A$

$=$

$v\sigma$

$B$

$=$

$u\sigma[\omegaarrow q\sigma]$$\Sigma=<T,$ $R>$

ここに,$u_{\omega}$$\wedge p_{1}\sigma=q_{1}\sigma\wedge\cdots\wedge p_{m}\sigma=q_{m}\sigma$

は項集合, $R$ は条件付き書換え規則の集合である. また, 例えば I 型の意味で条件の等式が成立する場合, \Sigma を 1 型の条件付き項書換え系という.

定義 2.14 文脈付き危険対の feasibility

定義 211 安定な条件付き項書換え系

条件付き項書換え系 $\Sigma=<T,$ $R>$ で, すべての
$R$

口

口

文脈付き危険対 $ccp=C\Rightarrow<A,$ $B>$ において,$r\in$が出現する変数にっいて以下の条件を満たすとき,$r$は安定な (steady) 条件付き項書換え系であるという.

ある代入 \mbox{\boldmath $\sigma$}が存在して, 任意の$c\iota_{i}\sigma\downarrow=v;\sigma\cdot\downarrow$$i(1\leq i\leq n)$が成立する (これを$\models_{R}C\sigma$

に対しと表す) とき, $ccp$ は feasible であるという$Var(u)\supseteq$

口$Var(v)$$\cup(\cup^{n}:=\iota(Var(v:)\cup Var(u_{i})))$

定理 26 安定で単純化性を満たす II 型の項書換え系$(1 \leq i\leq n)$$\Sigma=<T,$ $R>$ が以下を満たすとき,

口.

は局所合流性を満たす.

安定な条件付き項書換え系とすることの意義は, 変

$R$

の任意の
$B>,$

数を含まない項を簡約する過程で, 値の代入されてい$A,$ない変数を出現させないことにある.

する.

定義 212 単純化性を満たす条件付き項書換え系

条件付き項書換え系 \Sigma が以下を満たすとき, \Sigma は単$\Sigma$さらに,$\Sigma$満たすので,

feasible な文脈付き危険対$\models_{R}C\sigma$

に対し,$A\sigma\downarrow=B\sigma\downarrow$$C\Rightarrow<$が成立

は安定で単純化性を満たすから停止性を$\Sigma$は合流性を満たす

口

純化性を満たす (simplifying) という.

.

ある単純化順序則$r$$\succ$と任意の代入する.

が存在し, $R$ の任意の書換え規$\sigma$3

1 垣 ui 型の項書換え系に対し, 以下の 2 条件が成立

定義 3.1 正規形単一化可能, 正規形単一化可能条件
付き項書換え系$-u\sigma\succ v\sigma$

正規形単一化可能とは, 次の 2 っの総称である.

72
1. 両正規形単一化可能
項

$s$

と

とは,

$s$

$t$

とが両正規形単一化可能

の正規形と

$t$

$s\sim^{\downarrow}t$であるの正規形とが単一化可能であることをいう.

$s$

と

とは,

$s$

換え規則 $r\in R$ の条件の等式の成立の判定順序を左,第から右へ (第 1 条件, 第 2 条件,$n$条件の順) とし, 計算代入, 簡約代入を以下で定義するものを IIIui

2. 片正規形単一化可能項

3.3 IIIui 型の項書換え系
IIIu 型の項書換え系 $\Sigma=<T,$ $R>$ で, 条件付き書

定義.

型の項書換え系という.
$s\simarrow t$

であるとが片正規形単一化可能とが単一化可能であること
の正規形と

$t$

$t$

第

$i$

条件 $(1 \leq i\leq n)$ の計算代入旺

をいう.

;

$\rho;=\sigma\tau_{1}\cdots\tau$

正規形単一化可能条件付き項書換え系 (nuCTRS).

は, 条件付き書換え規則における条件の等式の等号の意味を正規形単一化可能とする項書換え系の総称である.

ただし, $i=1$ のときは \mbox{\boldmath $\rho$}i=\mbox{\boldmath $\sigma$}である.

簡約代入 \mbox{\boldmath$\rho$}$\rho(\sigma, \tau_{1}, \cdots, \tau_{\mathfrak{n}})=\sigma\tau_{1}\cdots\tau_{n}$口まず, 正規形単一化可能条件付き項書換え系の部分

口

クラスである, 次の IIIu 型の項書換え系を定義する.

定義

3.2 IIIu 型の項書換え系での条件付き書換え規

める手続き

則による簡約関係

IIIu 型の項書換え系 $\Sigma=<T,$ $R>$ で, 項IIIui 型の項書換え系 $\Sigma=<T,$ $R>$ において, 項
と項

$t$

$s$

の

間に, 条件付き書換え規則川こよって簡約関係 $tarrow s$.
.

3.2 IIIui 型の項書換え系における正規形を求

手続きの正規形は表 2 の手続き

$NF_{R}(t)$で求めることができる.

が成立するとは, 以下の 3 条件が成立することをいう.

項$t$の位置 \omega における変数でない部分項ちと,の書換え規則部の左辺の項

$u$

$r$

とが単一化代入 \mbox{\boldmath $\sigma$}によって単一化可能 (すなわち,$t_{\omega}=u\sigma$) である.

すべての $i(1\leq i\leq n)$ に対し以下が満たされる.

一第

$i$

口

定義 3.4 安定な IIIui 型の項書換え系

IIIui 型の項書換え系 $\Sigma=<T,$>で, すべてのとき, \Sigma は安定な IIIui 型の項書換え系であるという.
$Var(u_{i})$$\subseteq$$Var(u) \cup(\bigcup_{k=1}^{:-1}Var(v_{k}))$$(1\leq i\leq n),$った項と, 右辺の項 v:に代入 \mbox{\boldmath $\rho$}:を行った項とが片正規形単一化可能$R$$r\in R$が出現する変数にっいて以下の条件を満たす

条件において, 左辺の項 u:に代入旺を行$(u_{i}\rho_{i}^{arrow}\sim v;\rho;)$$Var(v)$である.

$\subseteq$$B^{a\prime}\supset$)$Var(u) \cup(\bigcup_{k=1}^{n}Var(v_{k}))$

このときの最汎単一化代入 (most generalunifier) を : とし,$\tau$.

$\rho_{j}$は$\sigma,$$\tau_{1},$$\cdots,$

義されているものの合成とする.

$\tau_{n}$

口

のうち定

$\rho$

本論文では, 安定な IIIui 型の項書換え系にっいて; を第峰

件における計算代入という.
$s=t[\omegaarrow v\rho(\sigma, \tau_{1}\tau_{n})]$

論じる.

である.

例

ここで, 代入 \mbox{\boldmath $\rho$}を簡約代入といい, その引数で示される代入の合成とする.

口(注) この定義における℃が一意に定まらないとき,

3.1 IIIui 型の項書換え系の例
以下のような項書換え系 \Sigma を考える.
$\Sigma=<T(F, V),$ $R>$
$F=\{f, s, +, 0, \geq, TRUE\}$.

1 っの部分項ちと 1 っの条件付き書換え規則 に対し$r$

2 っ以上の簡約関係が定義されることになる口$intintint\cross int\cross int$$(TR^{\theta}UE:0+f\geq’...\cdot..\cdot$

手続き$arrow boolarrow boolarrow intarrow intarrow int)$

3.1 IIIu 型の項書換え系における正規形を求める手続き
以上の定義により,$T,$$R>$ において, 項$t$IIIu 型の項書換え系 $\Sigma=<$の正規形は表 1 の手続き $NF_{R}(t)$で求めることができる.

表 1 の手続き中の Unif

$V=\{x, y\}$

(

$x,$

$y$

: int)$R=\{r_{1}, r_{2)}\cdots\}$$(t_{1}, t_{2})$$t$は 2 っの項$t_{1},$ $t_{2}$が単一化可能ならば最汎単一化代入を返し, 単一化不可能ならば fadure を返す決定手続きである.

口$r_{1}$: $x=0\Rightarrow f(x)arrow 0$$r_{2}$:$x\geq 0=TRUE\wedge f(x)=y$$\Rightarrow f(s(x))arrow s(x+y)$

73
procedure $NF_{R}(t)$begin
for each $r\in R$ do$(r:u_{1}=v_{1}\wedge\cdots\wedge u_{n}=v_{\mathfrak{n}}\Rightarrow uarrow v)$

if $((\sigmaarrow Unif(t_{\omega}, u))\neq failure)$ thenbegin
$reduciblearrow true$ ;for each $i\in[1..n]$ do
if $((\tau:arrow Unif(NF_{R}(u:\rho;), v:\rho;))=failure)$ then$reduciblearrow false$ ;if reducible then return$(NF_{R}(t[\omegaarrow v\rho(\sigma, \tau_{1}, \cdots , \tau_{\mathfrak{n}})])$

end;
return $(t)$end;
表1: IIIu 型の項書換え系における手続き $NF_{R}(t)$procedure N
begin
for each $r\in R$ do$F_{R}(t)$$(r : u_{1}=v_{1}\wedge\cdots\wedge u_{n}=v_{\mathfrak{n}}\Rightarrow uarrow v)$

if $((\sigmaarrow Unif(t_{\omega}, u))\neq failure)$ thenbegin
$reduciblearrow true$ ;for $iarrow 1$ to do
if $((\tau_{1}arrow Unif(NF_{R}(u_{i}\sigma\tau_{1}\cdots\tau_{i-1}), v:\sigma\tau_{1}\cdots\tau_{i-1}))=failure)$ then$reduciblearrow false$ ;if reducible then return
end;
return $(t)$
end;
$n$

$(NF_{R}(t[\omegaarrow v\sigma\tau_{1}\cdots\tau_{n}])$

表 2: IIIui 型の項書換え系における手続き

N$F_{R}(t)$74\Sigma で定義される関数 $f(x)$ は, から非負整数 までの和を与えるものである (関数記号 $+,$ に関する書
換え規則は省略している).
をみると, 書換え規則
$0$

および,

$x$

$\succ$の単調性から,$\geq$$t=t[\omegaarrow u\sigma]\succ t[\omegaarrow v\sigma\tau_{1}\cdots\tau_{n}]=s$$r_{2}$

部の右辺の項に左辺の項に含まれない変数 があり,
第 2 条件により, この には $f(x)$ の正規形が代入さ
$y$

$R$

$y$

れる. すなわち

分項のうち, 変数$r_{2}$$y$による簡約において, 簡約後の部に代入される項が先に評価されるの任意の書換え規則が, 定義 4.1 の条件 (A) を満たすから, 任意の簡約関係 $tarrow s$ に対し, $t\succ s$ が成

立する.
さらに,

ことになる. このような計算が可能であることから,$\succ$は整礎だから, \Sigma は停止性を満たす.

IIIui 型の項書換え系は部分項の評価順が指定できる
項書換え系であるとみなせる

口

口

定理

3.2 IIIn 型, II 型の項書換え系と IIIui 型の項書換例

4.2 安定で単純化性を満たす IIIui 型の項書換

え系 $\Sigma=<T,$ $R>$ に対し, $NF_{R}$ は決定手続きである.

え系

口

任意の IIIn 型の項書換え系が, IIIui 型の項書換え系であることは明らかである.
さらに,II 型の項書換え系$=<$
IIIui 型の項書換え系

任意の$\Sigma$$T(F, V),$ $R>$ は, 次のように$\Sigma=<T’(F, V’),$ $R’>$ に変換可能である.

:$r\in R$$u_{1}=v_{1}\wedge\cdots\wedge u_{n}=v_{n}\Rightarrow uarrow v$

に対し,

:

$r’\in R’$[証明] 項 $t\in T$ に対し, 手続き 3.2 の N $F_{R}(t)$ において, 手続き Unif の呼びだしが 2 回, 手続き Nの$F_{R}$

呼びだしが 2 回行われる. 手続き Unif は決定手続きであるので, 2 っの手続きが停止することを示
は停止性を満たす. したがって,に関する Noetherian 帰納法による.

す. 定理 4.1 より,$\succ$項$u_{1}=x_{1}\wedge v_{1}=x_{1}\wedge\cdots\wedge u_{n}=x_{n}\wedge v_{\mathfrak{n}}=x_{n}$き$t$$NF_{R}$$\Sigma$にっいて, $t\succ s$ なる任意の項$NF_{R}(s)$$\Rightarrow uarrow v$$s$

条件付き書換え規則 $r\in R$ に対し,
とする.

ただし,

$\{x_{1}, \cdots, x_{n}\}$$V\cap\{x_{1}, \cdots, x_{n}\}=\phi$)$V’=V\cup$

である

とする.

$\succ$に対し, 手続が停止すると仮定する.
$t_{\omega}=$u\mbox{\boldmath $\sigma$}であるの部分項性により,口$t\succ t_{\omega}=u\sigma$

4

騎 ui 型の項書換え系の停止性

第 $i(1\leq i\leq n)$ 条件について, 定義 4.1 の条件 (B) に

4.1 単純化性を満たす IIIui 型の項書換え系
IIIui 型の項書換え系 \Sigma が以下を満たすとき, は単より, 任意の代入$\sigma,$$\tau_{1},$$\tau:-\iota$$\cdots,$

に対し,

定義

$u\sigma\succ u;\sigma\tau_{1}\cdots\tau;-\iota$$\Sigma$.

純化性を満たすという.
したがって,

ある単純化順序 \succ が存在し,
き書換え規則$\sigma,$$\tau_{1},$$\cdots$

$r$

と,

$R$

の任意の条件付

定義 3.2 における任意の, ちに対し, 以下の 2 条件が成立する.

$-$

任意の

$i$

(1

$\leq$$i$$\leq$n) に対し,また,$\succ$$u\sigma$

手続き$NF_{R}$は停止する.

の単調性, および定義 4.1 の条件

り, 任意の代入$\sigma,$$\tau_{1},$$\cdots,$$\tau_{n}$(A) によに対し,$\succ$(B)$u:\sigma\tau_{1}\cdots\tau_{i-1}$

帰納法の仮定により,

よって,$(u_{j}\sigma\tau_{I}\cdots\tau_{i-1})$(A)$-u\sigma\succ v\sigma\tau_{1}\cdots\tau_{\mathfrak{n}}$$t\succ u_{i}\sigma\tau_{1}\cdots\tau_{i-1}$

口

安定で単純化性を満たす IIIui 型の項書換え系に対しては, Noetherian 帰納法が適用できる.

$t=t[\omegaarrow u\sigma]\succ t[\omegaarrow v\sigma\tau_{1}\cdots\tau_{n}]$よって, 帰納法の仮定により, 手続き$v\sigma\tau_{1}\cdots\tau_{n}])$$NF_{R}(t[\omegaarrow$は停止する.

以上より, 手続き

$NF_{R}(t)$は, 任意の入力 $t1$ こ対して停止する決定手続きである.

口

定理 4.1 安定で単純化性を満たす IIIui 型の項書換

え系 $\Sigma=<T,$ $R>$ は停止性を満たす.

[証明] 条件付き書換え規則$r$

口5IIIui 型の項書換え系の合流性に対し, $t_{\omega}=u\sigma$ であ

5.1

り, $tarrow s$ となるとする.

定義 4.1 の条件 (A) により, 任意の代入
に対し,$u\sigma\succ v\sigma\tau_{1}\cdots\tau_{n}$$\sigma,$$\tau_{1},$$\cdots,$$\tau_{\mathfrak{n}}$IIIui 型の項書換え系における文脈付
き危険対

IIIui 型の項書換え系における文脈付き危険対は, 定
義 2.13 のものと同じである.

75
5.1 IIIui 型の項書換え系における文脈付き危険

定義

簡約関係が成立するから,対の feasibility$u_{1}\sigma\downarrow\tau_{1}=v_{1}\sigma\tau_{1}\wedge\cdots$

IIIui 型の項書換え系における文脈付き危険対 $ccp$ に,$\wedge u_{n}\sigma\tau_{1}\cdots\tau_{n-1}\downarrow\tau_{n}=v_{n}\sigma\tau_{1}\cdots\tau_{n-1}\tau_{n}$対し, 次の式を満たす代入$\sigma,$$\cdots,$ $\sim,$$\tau_{1},$$\nu_{1},$$\cdots,$$\nu_{m}$が$p_{1}\eta\downarrow\nu_{1}=q_{1}\eta\nu_{1}\wedge\cdots$

存在するとき, $ccp$ は feasible であるという.

$\wedge p_{m}\eta\nu_{1}\cdots\nu_{m-1}\downarrow\nu_{m}=q_{m}\eta\nu_{1}\cdots\nu_{m-1}\nu_{m}$$u_{1}\sigma\downarrow\tau_{1}=v_{1}\sigma\tau_{1}$(これを peak [7] という)のは, 以下の 3 っの状況 (disjoint peak, critical peak,variable peak) のいずれかである.
$t$$\wedge$$u_{n}\sigma\tau_{1}\cdots\tau_{n-1}\downarrow\tau_{n}$$\wedge$が, 2 通りに簡約される$1^{7}1$$=v_{n}\sigma\tau_{1}\cdots\tau_{\mathfrak{n}-1^{\mathcal{T}_{\mathfrak{n}}}}$

1. disjoint peak

$p_{1}\sigma\downarrow\nu_{1}=q_{1}\sigma\nu_{1}$$\wedge$$\wedge$$\omega$$p_{m}\sigma\nu_{1}\cdots\nu_{m-1}\downarrow\nu_{m}$$\wedge$, \pi が,において独立した位置である場合であ$t$

る. このとき,$=q_{m}\sigma\nu_{1}\cdots\nu_{m-1}\nu_{m}$$t$

また, このとき, 以下の $ccp’=<A,$ $B>$ を対応する

代入を適用された危険対という.

$t$$<A,$ $B>$となる.

$=<v\sigma\tau_{1}\cdots\tau_{n},$ $u\sigma[\omegaarrow q\sigma\nu_{1}\cdots\nu_{m}]>$口$arrow t[\omegaarrow v\sigma\tau_{1}\cdots\tau_{l}]$$=t_{1}$$arrow t_{1}[\piarrow q\eta\nu_{1}\cdots\nu_{m}]$$=s$$arrow t[\piarrow q\eta\nu_{1}\cdots\nu_{m}]$$=t_{2}$$arrow t_{2}[\omegaarrow v\sigma\tau_{1}\cdots\tau_{n}]$$=s$

したがって,$t_{1}\downarrow t_{2}$となり, 仮定に反する.

2. critical peak

IIIui 型の項書換え系の合流性

5.2

位置 \omega は位置 \pi の上にあるとしても一般性を失わない. いま,補題 5.1 の証明のために次の用語を定義する.

.

$p$について, 任意の項$t$るとき, 項$t$$t_{1)}t_{2}$に対し以下が成立すは局所合流的であるという.

の最汎単一化代入を存在して,$r_{1)}r_{2}$$A,$$tarrow t_{1},$ $tarrow$$s$

ちとなるとき,$t_{1}arrow^{*}s,$ $t_{2}arrow^{*}s$の部分項 $u_{(}(\pi=\omega()$ と一化代入 \mbox{\boldmath $\sigma$}\cup \eta で単一化可能である.

定義 5.2 局所合流的な項項$u$$\sigma\cup\eta=\gamma\delta$$\gamma$

$p$

は, 単

ここで

$u_{\zeta}$となる.

のこの場合の文脈付き危険対 $ccp=C\Rightarrow<$$B>$ は, 以下となる.

なる項
$C$

が存在する.

$=$$u_{1}\gamma=v_{1}\gamma\wedge\cdots\wedge u_{n}\gamma=v_{\mathfrak{n}}\gamma$$\wedge p_{1}\gamma=q_{1}\gamma\wedge\cdots\wedge p_{m}\gamma=q_{\mathfrak{n}}\gamma$

口

5.1 安定で単純化性を満たす IIIui 型の項書換

補題

え系 $\Sigma=<T,$ $R$ >が以下を満たすとき, \Sigma は局所合

$A$

$=$

$v\gamma$

$B$

$=$

$u\gamma[\omegaarrow q\gamma]$

ここで,$\gamma\delta=\sigma\cup\eta\supseteq\sigma,$ $\eta$

流性を満たす.

.

だから,
$R$

の全ての feasible な文脈付き危険対 $ccp$ につい$\gamma\delta\tau_{1}\cdots\tau_{j-1}\supseteq\sigma\tau_{1}\cdots\tau:_{-1},$て, 対応する代入を適用された危険対 $ccp’=<$$\gamma\delta\nu_{1}\cdots\nu_{j-1}\supseteq\eta\nu_{1}\cdots\nu_{j-1},$$A,$$B>$ に対し,$A\downarrow=B\downarrow$$(1\leq i\leq n)$$(1\leq j\leq m)$が成立する.
したがって,
口$u_{1}\gamma\delta\downarrow\tau_{1}=v_{1}\gamma\delta\tau_{1}$[証明] 背理法で証明する. いま, 局所合流的でない
項 $t\in T$ が存在すると仮定する.
$r_{1},$$r_{2}\in R$$\wedge$$\wedge$が以下で示される書換え規則で,$r_{1}$$r_{2}$:: $p_{1}=q_{1}\wedge\cdots\wedge p_{m}=q_{m}\Rightarrow parrow q$$u_{\iota}\gamma\delta\tau_{1}\cdots\tau_{n-1}\downarrow\tau_{n}$$=v_{n}\gamma\delta\tau_{1}\cdots\tau_{n-1}\tau_{n}$$\wedge$$u_{1}=v_{1}\wedge\cdots\wedge\tau\iota_{n}=v_{n}\Rightarrow uarrow v$$p_{1}\gamma\delta\downarrow\nu_{1}=q_{1}\gamma\delta\nu_{1}$$\wedge$$\wedge$$p_{m}\gamma\delta\nu_{1}\cdots\nu_{m-1}\downarrow\nu_{m}$$=q_{m}\gamma\delta\nu_{1}\cdot$

項

$t$

が,

$r_{1}$

によって$t_{1}$に,$r_{2}$

によって$t_{2}$..

$\nu_{m-1}\nu_{m}$に簡約されるとする. また, $t_{\omega}=u\sigma$ , t\pi =p\eta であるとする.

ととすると, ある代入 \delta がとなり, $ccp$ は feasible である.

76となるから, 帰納法の仮定により,補題の条件から,.

$u:\sigma’\tau_{1}\cdots\tau_{\mathfrak{i}-1}\downarrow u’$$t_{1\omega}=$$v\gamma\delta\tau_{1}\cdots\tau_{n}\downarrow u\gamma\delta[\omegaarrow q\gamma\delta\nu_{1}\cdots\nu_{m}]$よって,$=t_{2\omega}$$u_{1}\sigma’\tau_{1}\cdots\tau_{j-1}\downarrow\tau_{i}$が成立し)となり, 仮定に反する.

$t_{1}\downarrow t_{2}$$=v_{i}\sigma\tau_{1}$3. variable peak

また, $v_{j}\sigma\tau_{\iota:-\iota}$$\tau\tau_{i}$\Sigma は単純化性を満たすから定理 4.1 により停止性を満たす. したがって納法により, 項$t$$\succ$$t$$v:\sigma\tau_{1}$Noetherian 帰

に関する

について

\succ \sim ’ なる任意の項

(

$t’$

$\sigma’-\sigma$

が局所合流的であるとできる.

...

$u$

$\tau_{i-1^{\mathcal{T}}:}$$\mathcal{T}j-1^{\mathcal{T}}:=v;\sigma’\tau_{1:-1}$$\tau\tau_{j}$の要素の代入は適用されない). 以上より,$u_{j}\sigma’\tau_{1}\cdots\tau_{*-1}\downarrow\tau_{i:}=v\sigma’\tau_{\iota\cdots:-1}\tau\tau_{1}$

中の変数

$x$

( (1) の証明終わり)の位置で以上より, 任意の項 $t\in T$ は局所合流的であり, 局あったとする.

所合流性が満たされる.

このとき,

口

IIIui 型の項書換

定理 5.1 安定で単純化性を満たす$t_{\omega}$...

は正規形だから,

危険対分岐の場合と同様に, 位置 \omega は位置 \pi の上にあるとし, さらに \pi が$=u\sigma\tau_{1}\cdots\tau\downarrow \mathcal{T}_{1}$$arrow t_{2\omega}=u\sigma[\piarrow q\eta\nu_{1}\cdots\nu_{m}]$え系 $\Sigma=<T,$ $R>$ が以下を満たすとき, \Sigma は合流性

$arrow^{*}u\sigma[xarrow q\eta\nu_{1}\cdots\nu_{m}]$

.

を満たす.

ここで, $\sigma’=\sigma\cup\{xarrow q\eta\nu_{1}\cdots\nu_{m}\}$ とすると,$R$の全ての feasible な文脈付き危険対 $ccp$ にっいて, 対応する代入を適用された$t_{2w}arrow^{*}u\sigma’$に対し,$A\downarrow=B\downarrow$$ccp’=<A,$ $B>$が成立する.

となる. いま,口. .

$u_{j}\sigma’\tau_{1}\cdots\tau_{i-1}\downarrow\tau_{1}=v;\sigma’\tau_{1}$$\mathcal{T}:-1\mathcal{T}_{j}$[証明] 補題 5.1 の局所合流性, 定理 4.1 の停止性に(1)$(^{\forall}i, 1\leq i\leq n)$より示される.

が成立するならば,口

IIIui 型の項書換え系に対する完

6$u\sigma’arrow v\sigma’\tau_{1}\cdots\tau_{n}$備化手続きとなる. 一方,

項書換え系に対する$t_{\omega}arrow t_{1\omega}=v\sigma\tau_{1}\cdots\tau_{n}arrow rv\sigma’\tau_{1}\cdots\tau_{n}$よって,(1) が成立するならば

ちとなり, 仮定に反する.

$t_{1}\downarrow t_{2}$$t_{1\omega}\downarrow t_{2\omega}$

, すなわ

だが,

$r_{2}$...

...

$\tau_{j-1}\downarrow\tau:=v;\sigma\tau_{1}$...

な項書換え系を得る手続きとはせず, 項書換え系から完備な項書換え系を得る手続きとする. また, 完備化$\tau_{i-1^{\mathcal{T}j}}$

手続きが利用できるための条件の詳細と, 手続きの正当性の証明にっいては現在検討中である.

によって,$u_{\mathfrak{i}}\sigma\tau_{1}$る完備化手続きを提案する. ただし, IIIui 型の項書
換え系では, 書換え規則部の右辺が左辺に比べ特別な意味をもっ (例 3.1 など参照) ので, 等式仕様から完備(1) の成立を示す. 任意の $i(1\leq i\leq n)$ に対し,
$u;\sigma\tau_{1}$Knuth-Bendix の完備化手続

2, 3, 4]を基にした, IIIui 型の項書換え系に対す
き [1,$\tau_{j-1}arrow u_{\mathfrak{i}}\sigma’\tau_{1}$

. .

手続き
$\tau_{1-1}$

...

続き

IIIui 型の項書換え系 $\Sigma=<T,$ $R>$ を完備化し,IIIui 型の項書換え系 $\Sigma’=<T,$ $R’>$ とする手続き

他の書換え規則によって,$u_{i}\sigma\tau_{1}$6. 1IIIui 型の項書換え系に対する完備化手$\tau_{i-1}arrow u_{i}’$$CPC(R, \succ)$ を表 3 に示す.

手続き $CPC(R, \succ)$ 中の RulesByCCP $(R’, \succ)$ は,となる場合が生ずる.

R’ 中の全ての文脈付き危険対を求め, それらをしかし, 定義 4.1 の条件 (B) とよって条件付き書換え規則の集合$\succ$の部分項性より,きである$t\succ u\cdot\sigma\tau_{1}\cdots\tau_{1-1}|$$R$$\succ$に’ として返す手続(表 4).
口

77(注) 手続き $CPC$ 中の〆は による簡約関係の意味[8] 富樫 敦:“等式プログラ ミングから融合型プロを保存しない. しかし, 完備化手続きの性質上, 意味

グラ ミングヘ’), 新しいプログラ ミングパラダイを保存した場合の正規形と保存しない場合の正規形は一致する. そして, 完備化手続きの目的が正規形の

ム, 井田哲雄編, 共立出版, pp.187-21S (1988).

$r$

一意性を保証するためのものであるから, 意味を保存

しないことに問題はない

7

口

あとがき
本論文では, 部分項の評価順を指定できるという特徴をもっ IIIui 型の項書換え系に対し, 停止性, 合流性を満たすための 1 っの十分条件を与え, それらを用いた完備化手続きを提案した.
今後の課題としては, 完備化手続きが利用できるための条件を与え, 手続きの正当性を示すこと, IIIui 型の項書換え系の他の応用例などを検討すること, 正規系単一化可能条件付き項書換え系の他のクラス (IIIu型, 両正規系単一化可能条件を用いた IIu 型, IIui 型)について検討すること, などがあげられる.

参考文献[1] 二木厚吉, 外山芳人:“項書き換え型計算モデルとその応用”, 情報処理, Vol.24, No.2, pp. 133-146(1983).
$[)]$

井田哲雄:

$\llcorner_{\frac{=}{Q}+}$

算モデルの基礎理論”, 第 6 章書換えモデル, 岩波書店, pp.223-296 (1991).

[3] 大須賀 昭彦:“項書換えシステムと完備化手続
き , 新しいプログラ ミングパラダイム, 井田哲
雄編, 共立出版, pp. 165-186 (1988).
[4] 坂井公:“Knuth-Bendix の完備化手続きとその応用 )) コンピュータソフトウェア, Vol.4, No. 1,
pp.2-22 (1987).

[5] Bergstra J.A. and Klop J.W.: (Conditional
Rewrite Rules: Confluence and Ternlination’,J. of Computer and System Sciences, Vol.32,
pp.323-362 (1986).
[6] Kaplan S.: “Simplifying Conditional Term
Rewriting Systems: Unification, Termination
and Confluence”, J. of Symbolic Computation,
4, pp.295-334 (1987).
[$\eta$

Dershowitz N., Okada M. and Sivakumar G.:(Confluence of Conditional Rewrite Systems“,
Proc. of 1st International Workshop on Conditional Term Rewriting Systems, Orsay, France,
July 1987, LNCS308, Springer Verlag, Berlin,pp.31-44 (1988).

[9] Mansfield G.,Togashi A. and Noguchi S.: (AMLOG: an Amalgamated Equational Logic Program Language”, J. of Information Processing,Vol.11, No.4, pp.278-287 (1988).
[10] Toyama Y.: (Membership Conditional Term
Rewriting $SystemS^{)}$ , ‘Ilrans. IEICE, E72,
pp.1224-1229 (1989).
[11] 山田順之介:“停止性をもっメンバシップ条件付
き TRS の合流性について’), 信学論, Vol.J74-D-I,
No 9, pp.666-674 (1991).

78

.
.

, 厳格半順序

入力

$R$

出力

$R’$

$\succ$procedure $CPC(R, \succ)$
begin$R’arrow\phi$ ;
do
while
begin
choose a rule $r\in R$ , s.t.
$R\neq\phi$$u_{1}=v_{1}\wedge\cdots\wedge u_{n}=v_{n}\Rightarrow uarrow v$$u\downarrow tmparrow NF_{R’}(u)$for $iarrow 1$ to
begin

$n$

;

;

do

;
if $(\tau_{j}arrow Unif(u_{i}\downarrow_{\ell mp}, v;\tau_{1}\cdots\tau_{i-1}))=failure$ then$u_{j}\downarrow tmparrow NF_{R’}(u\tau_{1}\cdots\tau)$$\tau_{i}arrow\phi$

end;$v\downarrow\ell mparrow NF_{R’}(v\tau_{1}\cdots\tau_{n})$if$u\downarrow tmp=v$;

ltmp then$Rarrow R-\{r\}$

else

begin
if

$u\downarrow\ell mp\succ v\downarrow\ell mp\wedge^{\forall}i(1\leq i\leq n)u\downarrow tmp\succ u_{i}\downarrow tmp$

beginmake a rule

$r’$

then

, s.t.

$u_{1}\downarrow_{mp}=v_{1}\wedge\cdots\wedge u_{n}\downarrow_{tmp}=v_{n}\Rightarrow u\downarrow tmparrow v\iota_{\ell mp}$;

$Rarrow R-\{r\}$ ;$R’arrow R’\cup\{r’\})$$Rarrow R\cup$

RulesByCCP(R’,endelse if
begin
make a rule$\succ$)$v\rfloor_{tmp}\succ u\downarrow tmp\wedge^{\forall}i(1\leq i\leq n)v\downarrow tmp\succ u_{i}$$u_{1}\downarrow$

tmp

$r’$

ltmp then, s.t.

$=v_{1}\wedge\cdots\wedge u_{n}1_{t\mathfrak{n}p}=v_{n}\Rightarrow v\downarrow tmparrow u1_{tmp}$$Rarrow R-\{r\}$ ;$R’arrow R’\cup\{r’\}$;$Rarrow R\cup RulesByCCP(R’, \succ)$

end
else
return(failure)

end
end;
return(R’)
end;
表 3: 手続き $CPC(R, \succ)$

;

79

.
.

, 厳格半順序

入力

$R’$

出力

$R”$

$\succ$procedure RulesByCCP(R’, )begin$R”arrow\phi$ ;$CCParrow all$ Contextual Critical Pairs of $R’$
while $CCP\neq\phi$ do
beginchoose a $ccp\in CCP$ , s.t.
$\succ$$u_{1}=v_{1}\wedge\cdots\wedge u_{n}=v_{n}\Rightarrow<A,$$A\downarrow mparrow NF_{R’}(A)$for $iarrow 1$ to
begin

$n$

$B>$ ;;

do$ltmparrow NF_{R’}(u;\tau_{1}\cdots\tau_{i-1})$ ;if $(\tau_{1}\cdotarrow Unif(, v\tau_{1}\cdots\tau_{\mathfrak{i}-1}))=failure$ then$u_{i}$$\tau_{1}arrow\phi$end;$B\downarrow\ell mparrow NF_{R’}(v\tau_{1}\cdots\tau_{\mathfrak{n}})$if A$ltmp=B\downarrow tmp$

;

then

$CCParrow CCP-\{ccp\}$

else

begin
if

$A\downarrow tmp\succ B\downarrow\ell_{mp}\wedge^{\forall}i(1\leq i\leq n)A[\ell_{mp}\succ u$; ltmpthen

begin
make a rule , s.t.
$r$$u_{1}\downarrow\ell_{mp}=v_{1}\wedge\cdots\wedge u_{n}\downarrow tmp=v_{n}\Rightarrow A\downarrow\ell mparrow BJ_{\ell mp}$;

$CCParrow CCP-\{ccp\}$ ;;endel.se if
begin
make a rule , s.t.
$R”arrow R”\cup\{r\}$$B\downarrow\ell m_{l}’\succ A\downarrow\ell mp\wedge^{\forall}i(1\leq i\leq?l)B\downarrow tmp\succ u$; ltmpthen$r$$u_{1}$$ltmp=v_{1}\wedge\cdots\wedge z\iota_{n}$ $ltmp=v_{n}\Rightarrow B\downarrow\ell mparrow A1_{tmp}$$CCParrow CCP-\{ccp\}$ ;$R”arrow R”\cup\{r\}$

;

end
else
exit procedure $CPC$ with returning(failure)

end
end;
return $(R”)$
end;
表 4: 手続き $Re(lesByCCP(R’, \succ)$;