Design and system development of a programming language based on a temporal linear logic

本课题主要完成了直观时间线性逻辑系统ITLL的设计，基于ITLL的逻辑程序设计语言TLLP的设计，以及TLLP编译系统的开发。除了线性逻辑运算符之外，ITLL还有以下逻辑运算符：用于指定下次只能使用一次的资源的模态运算符〇，用于指定每次只能使用一次的资源的模态运算符□，以及模态运算符！用于指定任意次数和任何时间可用的资源。所有的直觉逻辑、直觉线性逻辑和直觉时间逻辑都可以嵌入到ITLL中。逻辑程序设计语言tlllp是基于该ITLL的，它是Prolog和线性逻辑程序设计语言LLP的超集。在TLLP中，可以表示与时间相关的资源消耗的概念。通过推广Miller的一致证明思想、Hodas的io模型和LLP的分层io模型，给出了LLP的计算模型。TLLP的编译器基于扩展的分层io模型，使TLLP程序能够高效地执行。为了进一步研究TLLP的高效实现，我们还研究了一种线性逻辑编程语言到Java的翻译系统和一种经典线性逻辑编程语言的静态分析方法。

In this research project, the followings are accomplished : the design of Intuitionistic Temporal Linear Logic system ITLL, the design of a logic programming language TLLP which is based on ITLL, and the development of the compiler system of TLLP.In addition to linear logic operators, ITLL has the following logical operators : a modal operator ○ which is used to specify a resource usable only once at the next time, a modal operator □ which is used to specify a resource usable only once at any time, and a modal operator ! which is used to specify a resource usable any number of times and at any time. All of intuitionistic logic, intuitionistic linear logic, and intuitionistic temporal logic can be embedded into ITLL.Logic programming language TLLP is based on this ITLL, and it is a super-set of Prolog and a linear logic programming language LLP.In TLLP, it is possible to represent a concept of time-dependent resource consumption.Computation model of TLLP is given by extending the idea of Miller's uniform proof, Hodas's IO-model, and leveled IO-model of LLP.Compiler of TLLP is based on the extended leveled IO-model which enables the efficient execution of TLLP programs.In order to investigate a further efficient implementation of TLLP, we also studied about a translator system of a linear logic programming language into Java and about a static analysis method of a classical linear logic programming language.