単純型付き項書換え系における停止性の自動証明
スポンサーリンク
概要
- 論文の詳細を見る
単純型付き項書換え系は,山田(RTA'01,2001)によって提案された,高階関数を利用できる項書換え系である.通常の高階項書換え系と異なり,この項書換え系は束縛変数を組み込んでいない.本論文では,単純型付き項書換え系の停止性証明法を提案する.まず, 項書換え系の変換法を導入し,単純型付き項書換え系の停止性が,変換により得られる第1階項書換え系の停止性から導かれることを示す.次に,変換で得られた第1階項書換え系の停止性証明を容易にするラベリングを提案する.山田(RTA'01,2001)が与えた意味論的な停止性証明法とは対照的に,本論文で提案する停止性証明法は構文論約なため,停止性証明の自動化が容易である.
- 一般社団法人情報処理学会の論文
- 2003-03-15
著者
関連論文
- The Reachability and Related Decision Problems for Semi-Constructor TRSs (Theoretical Computer Science and its Applications)
- The Joinability and Unification Problems for Confluent Semi-Constructor TRSs (Evolutionary Advancement in Fundamental Theories of Computer Science)
- 単項的TRSにおける単ー化問題について
- 型付けによるファイル間データ非干渉の検証
- 単純型付き項書換え系における停止性の自動証明
- 単純型付き項書換え系における停止性の自動証明
- A-016 DAGの高さを4以下に制限したタスクスケジューリングの近似アルゴリズムについて(A分野:モデル・アルゴリズム・プログラミング)
- DAG の高さを4以下に制限したタスクスケジューリングの近似アルゴリズムについて(計算機科学の理論とその応用)