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

2001 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.昨年度より検討を続けていた、優先順序つき書換え系について、次に計算すべき場所を示すインデックスを効率良く求めるシステムを試作・評価した。インデックス書換えは、計算の解である正規形が存在するときに、これを求める計算戦略である。これに対して、解が無限の大きさになるために正規形が存在は存在しないが解の内で確定した部分を表す頭正規形が存在する場合に、これを求めるために項書換え系の根インデックスの概念を優先順序つき書換え系への拡張を検討した。詳しい証明はまだ完成していないが、拡張は可能であるとの予測がついた。
2.高階関数が扱える書換え系である高階書換え系において、必須呼びが頭正規化戦略であること、すなわち、部分解とみなせる頭正規形に到達するために将来必ず計算を必要とする部分を計算することにより必ず頭正規形に到達することの証明を与えた。これは主に、高階書換え系でのディセンダントの定義とその性質を示しこれを従来の結果に適用することによって得られた。

Research Products

• [Publications] M.Sakai, Y.Watanabe, T.Sakabe: "An Extension of Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems"IEICE Trans. on Information and Systems. E84-D・8. 1025-1032 (2001)
• [Publications] 西田直樹, 酒井正彦, 坂部俊樹: "PT関数の逆関数を定義するTRSの生成"コンピュータソフトウェア. 19・1. 29-33 (2002)
• [Publications] M.Sakai, K.Kusakari: "On New Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems"The International Workshop on Rewriting in Proof and Computation, Sendai, Japan, RIEC Tohoku University. RPC'01. 176-187 (2001)
• [Publications] 粕谷英人, 酒井正彦, 阿草清滋: "項書換え系におけるディセンダントと頭必須書換えの頭正規化性"電子情報通信学会技術報告. COMP2002. 65-72 (2001)