関数型言語の解析・検証・効率的実行のための書換え系理論の研究

2003 Fiscal Year Annual Research Report

• Project/Area Number: 15500007
• Research Institution: Nagoya University
• Principal Investigator: 酒井 正彦 名古屋大学, 大学院・情報科学研究科, 助教授 (50215597)
• Co-Investigator(Kenkyū-buntansha): 粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579) ; 草刈 圭一朗 名古屋大学, 大学院・情報科学研究科, 講師 (90323112) ; 坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
• Keywords: 項書換え系 / 関数型言語

Research Abstract

本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャッブとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
初年度は以下の研究を行った。
1.構成子項書換え系の逆関数を定義する書換え系の生成法を与えた。また、出力の項書換え系に余剰変数が含まれるときの実行方法を明らかにした。
2.コンピュータビリティに基づく、高階項書換え系の停止性の十分条件である高階経路順序を提案した。
3.高階関数が扱える高階書換え系において、頭正規形を得るための必須リデックスを計算する機構について研究した。強逐次近似とNV近似に基づく必須リデックスが、木オートマトン技術とデブロイ記法を用いて決定可能であることが分かった。
4.高階書換え系に実用上問題のない制限をつけて得られるSRSシステムの、代数的なモデルを定め、定理自動証明のための理論的枠組を与えた。
5.非直交な項書換え形の正規化戦略について検討した。その結果、強逐次戦略とNV逐次戦略については、左線形かつ左辺が一致するオーバレイの場合にも正規化戦略として働くことが判明した。

Research Products

• [Publications] 西田直樹, 酒井正彦, 坂部俊樹: "右辺のみに現れる変数を持つ項書換え系の計算モデル"コンピュータソフトウェア. 20・5. 85-89 (2003)
• [Publications] K.Kusakari: "Higher-Order Path Orders based on Computability"IEICE Transactions on Information and Systems. E87-D・2. 352-359 (2004)
• [Publications] M.Sakai, K.Okamoto: "Innermost Reductions Find All Normal Forms on Right-Linear Terminating Overlay TRSs"3rd Int'l Workshop on Reduction Strategies in Rewriting and Programming. WRS'03. 198-211 (2003)
• [Publications] N.Nishida, M.Sakai, T.Sakabe: "Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof"12th Int'l Workshop on Functional and (Constraint) Logic Programming. WFLP'03. 198-211 (2003)
• [Publications] 粕谷英人, 酒井正彦, 阿草清滋: "高階書換え系の決定可能性問題のためのNk木オートマトンとその性質"日本ソフトウェア科学会第20回大会論文集. 5B-2. 1-5 (2003)
• [Publications] 西田直樹, 酒井正彦, 坂部俊樹: "右辺のみに現れる変数を持つ右線形構成子項書換え系の計算の効率化"日本ソフトウェア科学会第20回大会論文集. 5B-3. 1-5 (2003)