|
関数、論理型言語を融合する宣言型言語の計算モデルとして、遅延ナロ-イング計算系と呼ばれる計算系を定義した。この計算系は、条件付き項書換え系に基づくものである。反駁による証明を計算の機構とし、証明の過程で値が必要となった関数項のみをナロ-イングにより簡約するものである。この計算系はナロ-イングをいくつかの基本的な推論規則に分解することで、等式の反駁の高速な実行を可能にしている。この計算系関して行った研究内容を以下に示す。
1.遅延ナロ-イング計算系の完全性の証明
我々が答とみなすすべての項が答として確かに得られることを示した。
2.関数・論理型言語の設計
遅延ナロ-イング感算系に基づく言語を設計し、さらにその処理系を実装した。
3.上記言語の抽象機械の設計
上記言語の処理系は、抽象機械をシミュレ-トすることによって動作している。この抽象機械を、遅延ナロ-イング計算系の推論規則の振舞いを解析することによって、得た。また、プログラムから抽象機械の命令列へと翻訳するコンパイラも作成した。
4.正則項書換え系の正規化手続きの実現への応用
遅延ナロ-イング計算系を応用して、正則項書換え系の正規化簡約系を得る方法を示した。
|
