Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials

摘要

It is known that Girard's linear logics can elegantly represent the concept of "resource consumption". The linear exponential operator ! in linear logics can express a specific infinitely reusable resource (i.e., it is reusable not only for any number, but also many times). It is also known that the propositional intuitionistic linear logic with ! and the first-order intuitionistic linear logic without ! (called here ILL) are undecidable and decidable, respectively. In this paper, a new decidable first-order intuitionistic linear logic, called the resource-indexed linear logic RL[l], is introduced by extending and generalizing ILL. The logic RL[l] has an l-bounded exponential operator !{sub}l, and this operator can express a specific finitely usable resource (i.e., it is usable in any positive number less than l + 1, but only once). The embedding theorem of RL[l] into ILL is proved, and by using this theorem, the cut-elimination and decidability theorems for RL[l] are shown.