木準同型写像を用いた項パターンマッチング
スポンサーリンク
概要
- 論文の詳細を見る
ラムダ計算のパターンマッチングに基づくプログラム自動変換法の枠組みがHuet-Lang(1978)によって提案されている.本発表では,項書き換えシステムに基づくパターンマッチングを実現するために木準同形写像の概念を導入する.はじめに,項パターンマッチングを実現するためのアルゴリズムを提案し,アルゴリズムの正当性を示す.さらに,項パターンマッチングアルゴリズムを項書き換えシステムに適用し,木準同形写像がリダクション関係を保存することを証明する.また,正規形が保存されるべきクラスを示し,木準同形写像によってそのクラスの正規形が保存されるための十分条件を示す.本発表におけるパターンマッチングアルゴリズムは,操作的意味論に基づくプログラム変換の正当性を示す第一歩となると期待される.
- 2005-01-15
著者
関連論文
- 帰納的定理の決定可能なクラスについて
- 項書き換えシステムの合流性自動判定
- A-033 S式書き換えシステムの停止性を保証するカリー化について(モデル・アルゴリズム・プログラミング,一般論文)
- 木準同型写像を用いた項パターンマッチング
- 反証機能付き書き換え帰納法のための補題自動生成法
- 新しいソフトウェアの実現 : 科研「情報学」プロジェクトA01柱を振り返って(「情報学を創る」-科研プロジェクトがめざしたもの)
- LA-009 項書き換えシステムの合流性自動判定(モデル・アルゴリズム・プログラミング)
- LA-002 パターンに基づくプログラム変換における列変数の導入(A分野:モデル・アルゴリズム・プログラミング)
- A-032 多重Knuth-Bendix完備化における危険対除去手法の導入(モデル・アルゴリズム・プログラミング,一般論文)
- A-034 基底項書き換え系の合流性自動判定(モデル・アルゴリズム・プログラミング,一般論文)
- 修正AC単調意味論経路順序によるAC停止性
- 修正AC単調意味論経路順序によるAC停止性
- 優先順序付き書き換えの計算モデル
- 項書き換え系のパーシステント性の順序付きソートによる拡張
- Extending persistency of confluence with ordered sorts
- Top-down labelling and modularity of term rewriting systems
- Persistency of confluence
- Persistency of confluence
- 無限項書き換えシステムにおける性質に関する考察 (代数と言語のアルゴリズムと計算理論)