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

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

宣言型プログラミングの計算のモデルとしての高階項書換え系の諸性質の解明を行った.特に,高階の単一化に関わる機能や一階の項を操作する機構など,高階性に由来する強力な計算能力を活かした計算の理論の構築をはかり,宣言型プログラムのプログラム変換や自動導出研究の基礎の確立に貢献することを目指した.以下に得られた研究成果をまとめる.1.高階書換え系における簡約の戦略について,一階の場合と同様な標準化定理が成立することを確認した.高階簡約の標準化定理はLeft-linear Fully-extendedであるパターン書換え系について成立する.2.標準簡約の概念を組み込んだ高階の計算系HOLN(Higher-order Lazy Narrowing Calculi)を設計し,健全性・完全性の証明を得た.さらに,HOLNを関数・論理型言語の計算モデルとしたときに考えられるいくつかの最適化について考察した.最適化によっても,完全性が失われないことを示した.3.HOLNは高階単一化,遅延ナローイングを組み込んだ計算系であり,本研究の成果をシステムとして実現するものである.さらにHOLNを実装し,関数・論理型言語のモデルとしての適切性について評価を行った.条件付きナローイング計算系が,外変数のない合流性をもつ条件付き書換え系について,正規化可能解に関して完全であることを以前に示していたが,さらにゴールの中の等式選択の戦略として,最左戦略をとっても完全であることを新たに明らかにした.ここで得られた照明技法は上記2.において高階計算系HOLNの完全性を証明する上でも活用された.