|
研究目的:(A)関数・論理型融合言語の計算モデルとしてのナローイングカリキュラスの改良および諸性質の解明、(B)PrologからLispへのプログラム変換を生かした論理型、関数型(Lisp)プログラムの融合方法をLisp処理系のレベルで探る。
研究実績:研究テーマを次のサブテーマに分割して研究を進め、次の研究成果を得た。
(1)Lispの翻訳系の正当性の証明とLisp抽象機械の設計、(2)Prologの操作的意味論の再構成、(3)ナローイングに基づく、関数・論理型言語の計算モデルの設計
(1)(2)に関しては、Prologの操作的意味論をSLD反駁から出発して、書換えシステムを経由し、Scheme(Lisp)へとプログラム変換する方法を考案した。これは、次の3つの点で重要な意味を持つ。(i)証明論的意味論が損なわれることなく、より計算機構に近い、操作的モデルでPrologの意味を理解することができた。(ii)PrologとLispの操作的モデルにおける融合が可能になる。(iii)処理系のレベルで見たPrologとLispの計算の複雑度をより厳密に論じられるようになる。(3)に関しては、OI条件付ナローイング(outside-in conditional narrowing)と呼ぶナローイング法を考案し、その反駁手続きとしての完全性を証明した。さらに、このOI条件付ナローイングをより細かな計算ステップに分解し、計算機による実現を目指した計算系を考案した。
研究の評価:目的(A)に関しては、本研究の当初の目的をかなり満足したと思われる。目的(B)に関しては、対象とする条件付書き換え系の性質を様々に変化させることにより、完全性の議論はさらに多様になりうるので、まだ研究は終了したとは言い難く、これからも研究を継続していく予定である。
|
