資源と時間の論理に基づいたプログラミング言語の設計と処理系の構築

2000 Fiscal Year Annual Research Report

• Project/Area Number: 11680359
• Research Institution: KOBE UNIVERSITY
• Principal Investigator: 高橋 真 神戸大学, 発達科学部, 助教授 (50154860)
• Co-Investigator(Kenkyū-buntansha): 番原 睦則 奈良工業高等専門学校, 一般教科, 講師 (80290774)
• Keywords: 時相線形論理 / 線形論理 / 時相論理 / 論理型言語 / 直観主義 / コンパイラ

Research Abstract

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

Research Products

• [Publications] 田村直之: "直観主義時相線形論理における論理プログラミングについて"情報処理学会論文誌:プログラミング. 41・SIG4(PRO7). 11-23 (2000)
• [Publications] 姜京順: "古典線形論理型プログラミング言語の静的解析の一手法について"情報処理学会論文誌:プログラミング. 41・SIG4(PRO7). 42-55 (2000)
• [Publications] 姜京順: "線形論理型言語の効率的なリソース管理モデル"コンピュータソフトウェア. 18・0. 138-154 (2001)
• [Publications] 番原睦則: "線形論理型言語のコンパイラ処理系のための抽象機械について"コンピュータソフトウェア. 18・1. 39-60 (2001)