| 研究概要 |
線形論理は,環境が動的に変化するソフトウェアを表現するための論理として非常に有望である.しかしながら,線形論理では「動的に変化する環境」を表現することはできるが,「時間経過とともに動的に変化する環境」を表現しきれているとは言えない.これは線形論理には時間の概念が直接的には入っていないからである.
そこで本研究では,線形論理と時相論理の特徴を融合した直観主義時相線形論理の体系,およびこの体系に基づいた論理型プログラミング言語についての研究を行った.
この直観主義時相線形論理の体系ITLLは,著者らのグループによって考えられたものであり,直観主義線形論理の演算子に加え,次の時刻に一回だけ利用可能な資源を表す様相演算子○,現在以降の任意の時刻に一回だけ利用可能な資源を表す様相演算子□,現在以降の任意の時刻に任意の回数利用可能な資源を表す様相演算子!を含んでいる.
この直観主義時相線形論理の体系ITLLに対して,Millerのユ二フォーム証明の考えを適用することによって,直観主義時相線形論理型言語TLLPを設計し,HodasのIOモデルの考えを適用することによって,効率的な計算モデルを与えた.
TLLPでは,ちょうど一度しか利用できないという線形論理型言語でのリソース概念に加え,どの時刻でリソースを利用できるかという時相性を記述できる点を特徴としている.
また,時相線形論理型言語の効率良い実装方式の検討のため,直観主義線形論理型言語のJavaへのトランスレート方式に関する研究,古典線形論理型言語の静的解析に関する研究を行った.
|
