書き換えシステムに基づく発展的プログラミングの研究

1997 Fiscal Year Annual Research Report

• Project/Area Number: 09245212
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
• Co-Investigator(Kenkyū-buntansha): 酒井 正彦 名古屋大学, 大学院・工学研究科, 助教授 (50215597)
• Keywords: 項書き換えシステム / 合流性 / 停止性 / 優先順位付き書き換えシステム / 正規化戦略

Research Abstract

プログラムの漸増的な発展過程で保存される性質を明らかにするため,書き換えシステムの変形・組合せで保存される性質の解析を中心に研究を進め,以下の成果を得た。
1。書き換えシステムの分解・合成
書き換えシステムの発展過程における不変な性質を明らかにするため,型情報の変更が書き換えシステムの停止性や合流性に及ぼす影響を理論的に解析した。さらに、自然なソ-ト付けによるシステムの分解可能性という概念を導入することで,直和システムのモジュラ性と同様な性質が成り立つことを明らかにした。
2。木持ち上げ順序による停止性
2つの項書き換えシステムの合併の停止性を導く手法として木持ち上げ順序を提案した。これは,従来知られていたダミ-削除による停止性判定手法を発展させたものであり,階層構造をもつシステムの解析にも有効な手法である。
3。優先順位付き書き換えシステムの意味論
関数型言語の計算モデルである優先順位付き書き換えシステムの操作的意味論を与えた。さらに,優先順位付き書き換えシステムの効率的な計算方法について解析を行い,強逐次性のクラスが決定可能であること,及び,そのクラスにおいては,インデックス書き換えが正規化戦略であることを示した。

Research Products

• [Publications] T.Aoto: "On Composakle properties of term rewriting systems" Lecture Notes in Compnto Sci.1298. 114-128 (1997)
• [Publications] T.Aoto: "Persistency of confluence" Journal of universal comput.Sci.3・11. 1134-1148 (1997)
• [Publications] T.Aoto: "Tree lifting orderings for termination transformation of term rewriting systems" Proc.of LA symposium(1997-07). 109-114 (1997)
• [Publications] T.Nagaya: "Index reduction of overlapping strongly sequential systems" IEICE TRANS.INF. & SYST.(発表予定).
• [Publications] T.Aoto: "Termination transformation by tree lifting ordering" Lecture Notes in Comput.Sci.(発表予定). (1998)
• [Publications] M.Sasai: "Semantics and strong sequentiality of priority term rewriting systams" Theoretical Comput.Sci.(発表予定).