リダクションの近似に基づくプログラム検証手法の研究

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14580357
• Research Institution: Tohoku University
• Principal Investigator: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• Co-Investigator(Kenkyū-buntansha): 草刈 圭一郎 東北大学, 電気通信研究所, 助手 (90323112)
• Keywords: 書き換えシステム / リダクションの近以 / 到達可能性 / 停止性 / 逐次性 / 木オートマン

Research Abstract

リダクションの近似の概念をもちいることによって,従来よりもより広いクラスの項書き換えシステムに対して決定可能な必須呼び戦略を明らかにした.決定可能な必須戦略の解析には,これまでも項書き換えシステムのさまざまな近似がもちいられていたが,本研究では従来必要とされていた右線形性の制限を取り除いても,グローイング近似が決定可能な近似であることを示した.ここで提案した左線形グローイング近似をもちいると,弾逐次系,NVNF逐次系,シャロー逐次系,さらに従来の線形グローイング逐次系を含むより広いクラスの項書換え系に対して,決定可能な必須呼び戦略の存在を示すことが可能である.
さらに,ここで得られた左線形グローイング近似に基づいて,項書き換えシステムの計算過程の解析を行った.右基底項書き換えシステムの計算の到達可能性および合流性が決定であることは従来知られていたが,左線形グローイング近似の書き換え規則を逆向きに適用することで,従来の結果が拡張できることを示した.
リダクションの近似に基づく計算の停止性の解析はこれまでほとんど知られていなかった.本研究では,左線形グローイング近似の解析手法を適用することで,準直交項書き換えシステムの停止性の解析を行った.Gramlich(1995)は準直交項書き換えシステムの停止性と弱停止性が等価であることを明らかにしている.この結果を我々が示した左線形グローイング近似の到達可能性の決定性と組み合わせることにより,準直交項書き換えシステムの停止性の判定が決定可能となる十分条件を得ることができた.

Research Products

• [Publications] Yohihito Toyama: "Decidability for Left-Linear Growing Term Rewriting Systems"Information and Camputation. 178. 499-514 (2002)
• [Publications] Keiichirou Kusakari: "On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique, The First International Workshop on Higher-Order Rewriting"The First International Workshop on Higher-Order Reivriting. HOR'02. 25 (2002)
• [Publications] Yoshihito Toyama: "Decidability for Left-Linear Growing Term Rewriting Systems"Information and Camputation. 178. 499-514 (2002)
• [Publications] Yoshihito Toyama: "Decision procedure for inductire theorems by rewrting induction"Technical Report of IEICE COMP. 2002-45. 41-45 (2002)
• [Publications] 外山 芳人: "書き換え帰納法による帰納的定理の決定手続き"日本ソフトウェア科学会第19回大会論文集. 2002-9. 3A-2 (2002)
• [Publications] 鶴川敏孝: "変換パターンに基づく高速プログラム変換"信学技法COMP. 2002-83. 61-68 (2002)
• [Publications] 伊藤芳浩: "完備化手続によるプログラム融合変換の停止条件"信学技法COMP. 2002-84. 69-76 (2002)