関数型言語における計算戦略

2002 Fiscal Year Annual Research Report

• Project/Area Number: 11680352
• Research Institution: Nagoya University
• Principal Investigator: 酒井 正彦 名古屋大学, 大学院・工学系研究科, 助教授 (50215597)
• Co-Investigator(Kenkyū-buntansha): 粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579) ; 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968) ; 坂部 俊樹 名古屋大学, 大学院・工学系研究科, 教授 (60111829)
• Keywords: 項書換え系 / 正規化戦略 / 関数型言語

Research Abstract

本研究の目的は、項書換え系における計算戦略の結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。そのため、規則間に優先順序がついた項書換え系、高階関数、モジュールを持つ項書換え系の上での計算戦略を解析・明らかにすることが必要である。
本年度は、昨年度に引続き以下を行った。
1.高階関数が扱える高階書換え系において、頭正規形を得るための必須リデックスを計算する機構について研究した。このための技術として、強逐次近似とNV近似の概念を高階に拡張した。また、Δ-木オートマトンとそれに基づくGTTにより、デブロイ記法の高階項が正規形であること、ならびに、項の到達可能性が決定可能であることの証明のための大まかな道筋を与えることができた。
2.与えられた高階書換え系が停止性をもつことを示す有効な条件について研究した。停止性を持つことが分かれば、いかなる戦略で計算を行っても解が求められるので、これは重要である。具体的な手法としては、項書換え系の依存対に基づく手法を高階の場合に拡張した。この手法は無限計算列を引き起こす引き起こす可能性のある場所に注目して停止性の証明のしやすいシステムに変換する方法である。しかしながら、高階の場合には、注意すべき場所が規則からは予想が難しいため、これらを行うことが可能な書換え系のクラスを明らかにした。
3.以上の研究の他、逆計算を行うプログラムへの変換を与え、それによる逆計算の戦略の研究にも着手した。

Research Products

• [Publications] 西田直樹, 酒井正彦, 坂部俊樹: "右辺のみに現れる変数を持つ項書換え系の計算モデル"コンピュータソフトウェア. (採録決定). (2003)
• [Publications] M.Sakai, K.Kusakari: "On Proving Termination of Higher-Order Rewrite Systems by Depen-dency Pair technique"The First International Workshop on Higher-Order Rewriting. HOR'02. 25-25 (2002)
• [Publications] H.Kasuya, M.Sakai, K.Agusa: "Descendants and Head Normalization of Higher-Order Rewrite Systems"6th International Symposium on Functional and Logic Programming, LNCS 2441. FLOPS2002. 198-211 (2002)
• [Publications] 西田直樹, 酒井正彦, 坂部俊樹: "右辺のみに現われる変数を持つ項書換え系のナローイングに基づく実行的書き換えとその停止性"電子情報通信学会技術報告. COMP03-68. 45-52 (2003)