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

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14580357
• Research Institution: Tohoku University
• Principal Investigator: 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• Co-Investigator(Kenkyū-buntansha): 青戸 等人 東北大学, 電気通信研究所, 助教授 (00293390)
• Keywords: 書き換えシステム / 優先順位付き書き換え / リダクションの近似 / 条件付き書き換え / 構成子システム

Research Abstract

関数型プログラムでは優先順序をもつパターンマッチングによって関数を定義することができる.しかし,定義のパターンに重なりが生じた場合,通常の項書き換えシステムによるリダクションでは,プログラムの意味を直接表現することができない.そのため,優先順序付き項書き換えシステムによるリダクションに基づいてプログラムの意味を与える必要がある
優先順序付き項書き換えシステムの意味は,リダクションの近似に基づく条件付き項書き換えシステムとして与えることができる.一方,多くの関数型プログラムは優先順序付き構成子システムとして形式化可能である.優先順序付き構成子システムの意味を与える方法としては,上記のリダクションの近似に基づく方法以外に,構成子項の補パターンから生成される項書き換えシステムのリダクションに基づく方法がある.
研究では,補パターンに基づく方法を発展させ,補代入の概念を用いて項書き換えシステムを構成する手法を提案した.我々の提案した手法は,リダクションの近似を使わずに優先順位付き書き換えの意味を与えることができ,計算機上の実装が容易である.さらに,リダクションの近似による意味付けでは取り扱うことができない非線形パターンに対しても適用可能な場合がある.さらに,本研究では,リダクションの近似に基づく意味付けと補代入に基づく意味付けを理論的に解析し,左線形で十分完全な順序付き構成子システムでは,両者の意味付けが計算モデルとしては等価となることを明らかにした.

Research Products

• [Publications] T.Aoto: "Termination of simply typed term rewriting systems by translation and labelling"Lecture Notes in Computer Science. Vol.2706. 380-394 (2003)
• [Publications] 青戸等人: "単純型付き項書き換え系における停止性の自動証明"情報処理学会論文誌:プログラミング. Vol.44, No.SIG 4. 67-77 (2003)
• [Publications] 青戸等人: "高階関数型プログラムにおける帰納的定理証明"情報技術レターズ. Vol.2. 21-22 (2003)
• [Publications] 本多洋平: "完備化手続きにおける関数記号の自動導入機構"電気関係学会東北支部連合大会予稿集. 1G-4. 228 (2003)
• [Publications] 落合秀幸: "AC-完備化手続きに基づくプログラム融合変換"電気関係学会東北支部連合大会予稿集. 1G-5. 229 (2003)
• [Publications] 秋谷 賢司: "優先順位付き書き換えの計算モデル"信学技報. (発表予定). (2004)