Normal-form Computation by Left-most Innermost Narrowing on Right-linear Overlay Term Rewriting Systems with Extra Variables
Normal-form Computation by Left-most Innermost Narrowing on Right-linear Overlay Term Rewriting Systems with Extra Variables
复制标题
带有额外变量的右线性覆盖项重写系统上最左最内缩小的范式计算
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Toshiki Sakabe
中科院分区：
文献类型：
--
作者：
Naoki Nishida;Masahiko Sakai;Toshiki Sakabe
項書換え系 (TRS)の逆計算への取り組みとして, 逆計算 TRSを生成する手法がある [5].関数 f の 逆計算とは,与えられた vから f(v1, ..., vn) = vを 満たす v1, ..., vn を求めることであり,その逆演算 f−1 は f−1(v) = (v1, ..., vn)を満たす写像である. 提案されたアルゴリズムは,与えられた構成子TRS から,その逆計算をする余剰変数付き TRS(EVTRS)を生成する.ここで,EV-TRSとは,書換え 規則の右辺のみに現れる余剰変数と呼ばれる変数の 出現を許す TRSである.EV-TRSは書換え関係が 無限分岐であるが,EV-TRS 上に自然に拡張した ナローイングで EV-TRSの書換えを模倣すること により計算できる [6].この模倣では基礎項から始 まるナローイング系列のみを扱う.ナローイングは ほとんどの場合に停止性を持たないにも関わらず, 基礎項から始まる無限の系列を持たないことが多 い.そこで,著者らはこのような性質,すなわち, ナローイングの基礎項停止性を判定する手法を提案 している [3, 6].2つの自然数の加算の逆計算から 想像がつくように,逆計算は複数個の解を持つこと が多い.そのため,生成される逆計算 EV-TRSは 一般に合流性を持たない.よって,逆計算のすべて の解を求めるためには全探索が必要であり,その計 算量が膨大になる可能性がある. 一方,TRSが合流性を持たなくとも,停止性を 持つ右線形オーバーレイ TRSでは,与えられた項 のすべての正規形は(最左,最右)最内書換えによ り求めることができる [4]. 文献 [5]の手法により生成された逆計算 EV-TRS は構成子システムである.また,入力の TRSが消 滅的でないときには,出力は TRSになる.入力が 左線形ならば,生成された EV-TRSは右線形であ