修正AC単調意味論経路順序によるAC停止性
スポンサーリンク
概要
- 論文の詳細を見る
AC項書き換え系はAC(結合律・交換律)を法とした簡約関係により項書き換え系を拡張した計算モデルである. AC項書き換え系の停止性(AC停止性)を示すために様々なAC簡約化順序が提案されている. 本論文では, 最近BorrallerasとRubio(2003)により示された, AC単調意味論経路順序がAC簡約化順序であるという結果に対して反例を与える. つまり, 彼らのAC単調意味論経路順序はAC停止性を保証できない. 我々は, この反例の解析をもとに, AC単調意味論経路順序を修正した新しい順序を提案し, その正当性を示す. この修正AC単調意味論経路順序は, 現在知られているAC簡約化順序のうち, 最も強力なAC簡約化順序の1つとなっている.
- 2005-03-11
著者
関連論文
- 帰納的定理の決定可能なクラスについて
- 項書き換えシステムの合流性自動判定
- A-033 S式書き換えシステムの停止性を保証するカリー化について(モデル・アルゴリズム・プログラミング,一般論文)
- 木準同型写像を用いた項パターンマッチング
- 反証機能付き書き換え帰納法のための補題自動生成法
- 新しいソフトウェアの実現 : 科研「情報学」プロジェクトA01柱を振り返って(「情報学を創る」-科研プロジェクトがめざしたもの)
- LA-009 項書き換えシステムの合流性自動判定(モデル・アルゴリズム・プログラミング)
- LA-002 パターンに基づくプログラム変換における列変数の導入(A分野:モデル・アルゴリズム・プログラミング)
- A-032 多重Knuth-Bendix完備化における危険対除去手法の導入(モデル・アルゴリズム・プログラミング,一般論文)
- A-034 基底項書き換え系の合流性自動判定(モデル・アルゴリズム・プログラミング,一般論文)