宣言型プログラムを対象とする高階項書換え系の計算理論

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12878047
• Research Institution: University of Tsukuba
• Principal Investigator: 井田 哲雄 筑波大学, 電子・情報工学系, 教授 (70100047)
• Co-Investigator(Kenkyū-buntansha): 鈴木 大郎 東北大学, 電気通信電気通信研究所, 助手 (90272179) ; ミデルドープ アート 筑波大学, 電子・情報工学系, 助教授 (30251044)
• Keywords: 宣言型プログラム / 計算モデル / ナローイング計算系 / 選択関数 / 求解完全性 / 高階遅延ナローイング

Research Abstract

本研究では,高階項書換え系を宣言型プログラミングの計算モデルとして用い,計算理論の構築を図り,宣言型プログラムのプログラム変換や自動導出研究の基礎確立に貢献する.新しく得られた研究成果は次の通りである.
1.ナローイング計算系の戦略に関する研究
宣言型プログラミングの計算モデルとして利用される条件付きナローイング計算系LCNC(Lazy Conditional Narrowing Calclus)は,求解完全性をもつことが,Hamada,Middeldorp,Suzukiによりすでに証明されている.しかし,この完全性の証明の中では,次に解く等式を選択するための関数が与えられていないため,LCNCをそのまま計算モデルとして採用すると,等式選択のためにバックトラックを必要とし,求解の効率が悪かった.本研究では,等式選択のためのバックトラックを必要としない求解法について考察し,等式の選択関数を導入した.さらに,新しく導入した選択関数のもとでの求解完全性の証明を行なった.選択関数の導入は,LCNCを計算モデルとする宣言型プログラミング言語の実装の指針を与えるという点で重要である.
2.高階遅延ナローイング計算系に関する研究
本研究に先立ち我々が考案した高階遅延ナローイング計算系LNffでは,高階変数を含む等式を解くための推論規則を適用する場合の非決定性が高い.本研究では,LNffに内在する非決定性を除去するための改良を加えた.段階的に非決定性の除去を行なうことにより,LN1〜LN4と呼ぶ4つの新たな計算系を得た.また,提案した各計算系についてそれぞれ,計算モデルとして重要な性質である求解完全性の結果を証明した.

Research Products

• [Publications] M.Marin,T.Ida,T.Suzuki: "Higher-order Lazy Narrowing Calculi in Perspective"Proc.9th International Workshop on Functional and Logic Programming. 238-253 (2000)
• [Publications] M.Marin,T.suzuki,T.Ida: "Cooperative Constraint Functional Logic Programming"International Symposium on Principles of Software Evolution. 223-230 (2000)
• [Publications] M.Marin,T.Suzuki: "Cooperative Constraint Functional Logic Programming"Proc.9th International Workshop on Functional and Logic Programming. 382-390 (2000)
• [Publications] T.Suzuki,A.Middeldorp: "A Complete Selection Function for Lazy Conditional Narrowing"Proc.5th International Symposium on Functional and Logic Programming, LNCS. (印刷中). (2001)