| 研究概要 |
本研究では,線形論理と時相論理の特徴を融合した直観主義時相線形論理の体系ITLLの設計,この体系に基づいた論理型プログラミング言語TLLPの設計,およびそのコンパイラ処理系の開発を行った.
直観主義時相線形論理の体系ITLLは,直観主義線形論理の演算子に加え,次の時刻に一回だけ利用可能な資源を表す様相演算子○,現在以降の任意の時刻に一回だけ利用可能な資源を表す様相演算子□,現在以降の任意の時刻に任意の回数利用可能な資源を表す様相演算子!を含んでいる点を特徴とする.直観主義論理,直観主義線形論理,直観主義時相論理は,このITLLに埋め込み可能である.
直観主義時相線形論理型言語TLLPは,この直観主義時相線形論理の体系ITLLに基づいており,Prologおよび直観主義線形論理型言語LLPのスーパーセットとなっている.ちょうど一度しか利用できないという線形論理型言語でのリソース概念に加え,どの時刻でリソースを利用できるかという時相性を記述できる点を特徴としている.
TLLPの計算モデルは,Millerのユニフォーム証明,HodasのIOモデル,LLPのレベル付きIOモデルをITLL用に拡張することによって与えられる.
TLLPのコンパイラ処理系は,この拡張したレベル付きIOモデルに基づいており,TLLPプログラムの効率的な実行が可能である.
また,時相線形論理型言語の効率良い実装方式の検討のため,線形論理型言語の静的解析に関する研究も行った.
|
