等式E : d(x)=(x2x2x)+x のとき、
R
2 [ R
+ [ R
s [ R
d
: f(x 2 x2 x) + x ! d(x)g に対して完備化を行なうと、
d>2>+>s の順序付けでのみ7ステップで完備化が成功する。完備化が成功す ると次のような書き換え規則が生成する。
d(0)!02020
d(s(x))!s((s(x)2s(x)2s(x))+x)
等式E : d(x)=(x+x+x)2x のとき、
R
2 [ R
+ [ R
s [ R
d
: f(x + x+ x) 2 x ! d(x)g に対して完備化を行なうと、
d > 2 > + > s の順序付けでのみ7ステップで完備化が成功する。完備化が成 功すると次のような書き換え規則が生成する。
d(0)!0
d(s(x))!((s(x)+s(x)+s(x))2x)+(s(x)+s(x)+s(x))
た。その他のプログラム合成の例に関しても、比較的に同様のことが言える。
例2 リストの長さを表すlength と追加を表す@ 、反転を表すreverse などの関数を用 いて、等式E : h(x;y)=length(reverse(x;y)) を満たす関数h のプログラム合成を試み る。
R
+ :
(
x+0!x
x+s(y)!s(x+y)
R
l ength :
(
l ength[]!0
l ength(x::y)!l ength(y)+s(0)
R
@ :
(
[]@y !y
(x::y)@z !x::(y@z)
R
r ever se :
(
reverse(x::y)!reverse(y@(x ::[]))
reverse(reverse(x))!x
R
+ [R
l eng th [R
@ [R
rev erse [R
h
: flength(reverse(x;y))! h(x)g に対して完備化を 行なうと、length(reverse(x;y))! h(x;y) の書き換え規則しか合成されない。新たな生 成規則が得られないので、この例は失敗だと見なされる。
例3 融合項が非線形項であっても、成功する例を前節で述べたが、完備化できないで失 敗する例も見られる。例えば、5.2.1の例1.1のh(x;y)=l ength(x@y)の等式では8ステッ プで完備化に成功しても、それを非線形にしたd(x)=length(x@x)を満たす関数d(x)の プログラム合成は完備化できない。
R
+ :
x+0!x
0+y!y
R
s :
(
x+(s(y))!s(x+y)
(s(x)+y)!s(x+y)
R
l eng th :
(
length[] !0
length(x ::y)!length(y)+s(0)
R
@ :
(
[]@y !y
(x::y)@z!x::(y@z)
R
+ [R
s [R
length [R
@ [R
h
:flength(x@x)!d(x)gに対して完備化を行なうと、停止 せずにループに陥るか、途中で失敗する場合が多く観察される。完備化に成功した場合、7 ステップでl ength(append(x)) !d(x) の規則が生成されるが、Rh
:l ength(x@x)!d(x)
の形ではないのでプログラム合成ができない。
等式E :d(x)=x@xのプログラム合成の成功例も、まだ観察されていない。R@[
fx@x!d(x)gに対して完備化手続きを行なっても、生成規則が得られるような順
序付けや合成する良い関数の集合が見つかっていない。
等式 E :d(x)=length(x+x) のプログラム合成も、成功した例が観察されていな
い。
例4 map 関数のプログラム合成に関して、5.2.5節で成功した例を示したが、合成でき ない例を示す。等式E :h(x;y;z) =x+map(l ength(y :: z))を合成させる時、次の関数 の集合ではうまくいかないことがわかった。
R
+ :
x+0!x
0+y!y
R
s :
(
x+(s(y))!s(x+y)
(s(x)+y)!s(x+y)
R
l eng th :
(
length[]!0
length(x::y)!length(y)+s(0)
R
map :
(
map(l ength[])![]
map(l ength(x::y))!l ength(x)::map(l ength(y))
R
+ [R
s [R
length [R
map [R
h
:fx+map(l ength(y ::z))!h(x;y;z)gに対して完備化 手続きを行なうと、成功しない。
第
6章 まとめ
6.1
本論文のまとめ
本研究では、主にKnuth-Bendix完備化手続きを用いて再帰的なプログラムの形をし た関数の集合の合成を行ない、切り払いのための融合規則が得られるか否かの実験を繰り 返してきた。これまでの結果を順序付けに着目して考察してみると、線形項の融合項の合 成に関して言えば、新しく導入する関数記号(Fresh symbol)は、一番上に持ってくると 成功しやすいことがわかる。そして、順序付けが異なるが完備化が成功する例を見てみる と、完備化するまでのステップ数が異なることが多い。そして、実際は、順序付けが異な ると同じプログラム合成でも、完備化される途中で失敗して停止したり、発散して停止し なくなったりすることが多い。このようにして、順序付けがプログラム合成の完備化に対 して、大きく左右していることがよくわかる。また、合成を行なう時、その再帰的プログ ラムの形や融合項の構造に着目して、プログラム合成の完備化が可能かどうかが判断でき るように、第3章に触れたような表記を用いて、項書き換え系の計算モデルとして理論的 に解析できると考えられる。