A static analysis for classical linear logic programming language
Kyoung-Sun Kang, Naoyuki Tamura · 1999
In this thesis, we propose a new static analysis method which is applicable for a classical linear logic programming language. Andreoli et al. proposed a static analysis method for the classical linear logic programming language LO, but their method did not cover the multiplicative conjunction which is the most important connective for a resource-sensitive feature of linear logic. Our method, in contrast, covers the multiplicative conjunction in addition to the multiplicative disjunction and linear implication. In classical linear logic programming language, such as Forum, the execution of a program is sometimes highly non-deterministic. For example, the execution time of a sorting program written in Forum rises hyper-exponentially with list length. The reason is that most of the execution time is spent for trying to prove unprovable sequents. Therefore, it is very important to find unprovable sequents before the execution of programs, and this is realizable by a static analysis performing an abstract proof search on an abstract proof. In order to develop abstract proof search in linear logic, we need to map the sequents into finite sets. we introduce a finite monoid #M,+, 0# homomorphic to N (a set of natural numbers including 0) t...