項書換え系における必須呼び計算機構に関する研究

点击翻译按钮获取中文摘要

項書換え系のルート正規化簡約と正規化可能性HuetとLevyにより提唱された必須簡約は,正交な項書換え系で次の性質が成り立つ.1.簡約可能な項には,必須可約項が存在する.2.正規形をもつ項の必須可約項を簡約し続けると,正規形に到達する.必須簡可約項とは,計算の順序によらず,必ず評価される可簡約項のことである.必須簡約を用いると,不要な計算を避け,正規形に到達するために書き換える必要のある可約項だけを簡約することができる.効率の良い関数型プログラミング言語処理系を構築するには,必須簡約の理論が不可欠である.本研究では,無限正規形を計算する遅延評価機構に適するように,Huetらの研究成果の理論的拡張を行なった.本研究の成果により,これまでに指摘されていた簡約戦略の理論と実際の遅延型関数プログラミング言語処理系との間隙を埋めることができた.本研究で新たに得られた成果は,パリで開催されたPOPL′97で発表した.項書換え系の決定可能な遅延評価機構簡約項の必須性,およびルート必須性は一般に決定不可能であるため,実用的な評価機構を得るための十分条件を考察する必要がある.これを決定可能性の近似という.これまでに,決定可能性の近似について,多くの論文が発表されており,そのすべてはHuetらの導入した複雑な概念(インデックス,ω-簡約,逐次性)の上で議論が展開されている.申請者は,Irene Durand(ボルド-大学,フランス)との協同研究により,従来の手法を踏襲しないきわめて明解な理論を構築した.この研究成果により,これまで知られていた決定可能性の近似に関するすべての結果は,我々の提案した手法で簡潔に議論できることが分かった.さらに,それらの結果を容易に拡張できることも明らかになった.本研究の結果をまとめた論文は,オーストラリアで開催される予定のCADE′97に受理されている.