2003 Fiscal Year Annual Research Report
| Project/Area Number |
15017203
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青戸 等人 東北大学, 電気通信研究所, 助教授 (00293390)
|
|---|
| Keywords | 情報基礎 / ソフトウェア検証 / プログラム変換 / 定理自動証明 / 項書き換えシステム |
|---|
| Research Abstract |
完備化に基づくプログラム融合変換のアイデアを,高階プログラムに適用するためには,高階書き換えシステムの完備化を実現する必要がある。しかし,高階書き換えシステムの完備化手続きの多くは机上の提案にとどまっており,実装にはいたっていない。これは,完備化手続きを実装するために不可欠な高階書き換えシステムの停止性が,簡単に判定できなかったからである。
本研究では,項の幅の上界を設定することで,固定次数の関数記号に対する単純化順序の定義が,可変次数の関数記号に対してもそのまま有効に働くことに注目し,S式書き換えシステムの停止性が辞書式経路順序で簡単に判定できることを示した。実際に利用される高階書き換えシステムの多くは,S式書き換えシステムで表現できるため,ここで提案された停止性判定法をもちいて完備化可能である。我々は,S式書き換えシステムの完備化手続きを計算機上に実装し,高階書き換えシステムの完備化と融合変換が容易に実現できることを実験によって明らかにした。
さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,高階関数を含む帰納的定理の自動証明法を検討し,高階書き換えシステムにおける潜在帰納法の枠組みを提案するとともに,潜在帰納法の適用に不可欠な十分完全性の判定が決定可能であることを明らかにした。
また,書き換え代入に基づく2階のパターンマッチングを提案し,パターマッチングをもちいたプログラム変換手続きを改良するとともに,書き換え帰納法に基づく高階プログラムの融合変換の実験を行った。
|
Research Products
(6 results)
-
[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.SIG4(PRO 17). Vol.44,No.SIG4. 67-77 (2003)
-
[Publications] 青戸等人: "高階関数型プログラムにおける帰納的定理証明"情報技術レターズ. Vol.2. 21-22 (2003)
-
[Publications] 秋谷 賢司: "補代入を用いた書き換えシステムの等価変換"電気関係学会東北支部連合大会予稿集. 1G-3. 227 (2003)
-
[Publications] 千葉勇輝: "高階書き換え系に基づく完備化手続き"電気関係学会東北支部連合大会予稿集. 1G-2. 226 (2003)
-
[Publications] 外山 芳人: "S式書き換えシステムの停止性"LAシンポジウム予稿集. 22.1-22.2 (2003)
