正規化戦略に基づく関数型プログラムの効率的実行に関する研究

本研究は,関数型プログラミング言語を高階書換え系としてモデル化し,高階書換え系の正規化戦略を用いることによって,関数型プログラミング言語プログラム(以下,関数型プログラム)の効率的な実行を動的に実現することを目的とする。これまで書換え型計算モデルの書換え戦略に関する研究の多くは,項書換え系の上で行われてきた。しかし,項書換え系には関数型言語の重要な機能である高階関数の概念がないため,これまでの項書換え系での成果をそのまま関数型言語に応用することができない。そこで,関数型言語の高階関数を扱うことのできる書換え型計算モデルである高階書換え系に着目し,次の3点の目標について研究をおこなった。(1)項書換え系の書換え戦略に関する性質を高階書換え系へ拡張する。そのために必須リデックス,高階書換え系の近似書換え計算,必須リデックスの決定可能性の性質を順次証明する。(2)高階書換え系とその上での必須書換え戦略を行う実行系を実現し,関数型プログラムの効率的な実行を行う。(3)本手法は近似計算を用いて計算戦略を実現するため,関数型言語の実行系として適用できる範囲を明らかにする。その結果(1)に関して,高階書換え系の頭必須書換えについての性質を明らかにし,その計算手法が正しい計算結果を導くことができるという正規化戦略となっていることを示すことができた。また,実際にこの戦略を用いて計算を実行するため,具体的な計算手順である必須リデックスの決定方法を示し,これらに関して論文発表の準備を行った。

本研究は,関数型プログラミング言語を高階書換え系としてモデル化し,高階書換え系の正規化戦略を用いることによって,関数型プログラミング言語プログラム(以下,関数型プログラム)の効率的な実行を動的に実現することを目的とする。これまで書換え型計算モデルの書換え戦略に関する研究の多くは,項書換え系の上で行われてきた。しかし,項書換え系には関数型言語の重要な機能である高階関数の概念がないため,これまでの項書換え系での成果をそのまま関数型言語に応用することができない。そこで,関数型言語の高階関数を扱うことのできる書換え型計算モデルである高階書換え系に着目し,次の3点の目標について研究をおこなった。(1)項書換え系の書換え戦略に関する性質を高階書換え系へ拡張する。そのために必須リデックス,高階書換え系の近似書換え計算,必須リデックスの決定可能性の性質を順次証明する。(2)高階書換え系とその上での必須書換え戦略を行う実行系を実現し,関数型プログラムの効率的な実行を行う。(3)本手法は近似計算を用いて計算戦略を実現するため,関数型言語の実行系として適用できる範囲を明らかにする。その結果(1)に関して,高階書換え系の頭必須書換えについての性質を明らかにし,その計算手法が正しい計算結果を導くことができるという正規化戦略となっていることを示すことができた。また,実際にこの戦略を用いて計算を実行するため,具体的な計算手順である必須リデックスの決定方法を示し,これらに関して論文発表の準備を行った。