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

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10139214
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 外山 芳人 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
• Co-Investigator(Kenkyū-buntansha): 酒井 正彦 名古屋大学, 大学院・工学研究科, 助教授 (50215597) ; 鈴木 大郎 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (90272179)
• Keywords: 項書き換えシステム / 停止性 / 決定可能性 / 高階システム

Research Abstract

プログラムの漸増的な発展過程で保存される性質を明らかにするため、書き換えシステムの変形、高階化で保存される性質の理論的解析を中心に研究を進め、以下の成果を得た。
1. 木持ち上げ順序による停止性判定
従来提案されていた削除法による停止性判定手法を発展させ、新しく木持ち上げ順序による停止性の判定手法を提案した。さらに、この手法が複数の項書き換えシステムの組み合せの解析にも有効であることを示した。
2. 高階システムの停止条件
従来提案されていた再帰分解順序を拡張し、高階項書き換えシステムの停止性手法として適用可能であることを明らかにした。さらに、高階システムに対する単純化順序の定式化を行ない、高階システムの停止条件の統一的な枠組みを与えることに成功した。
3. グローイング項書き換えシステムの決定性
左線形なグローイング項書き換えシステムの決定性問題を解析し、到達可能性が決定可能となることを明らかにした。

Research Products

• [Publications] T.Nagaya: "Decidability for left-limear growing term rewriting systems" Lecture Notes in Comput.Sci.(発表予定). (1999)
• [Publications] M.Iwami: "An Improved recursive decomposition ordering for higher-oder rewriting systems" IEICE TRANS.INF.& SYST.E81-D-9. 988-996 (1998)
• [Publications] M.Sakai: "Semantics and strong sequentiality of priority term rewriting systems" Theoretical Comput.Sci.208. 87-110 (1998)
• [Publications] T.Nagaya: "Index reduction of overlapping strongly sequential systems" IEICE TRANS.INF.& SYST.E81-D-5. 419-426 (1998)
• [Publications] T.Aoto: "Termination transformation by tree lifting ordering" Lectur Notes in Comput.Sci.1379. 256-270 (1998)
• [Publications] M.Iwami: "Simplification ordering for higher-order rewrite systems" Trans.of IPS of Japan. (発表予定).