Linear Logic as a good logical foundation for computer science.

Linear Logic as a good logical foundation for computer

A specification language for a computational system is supposed to be capable of handling both resource-sensitive and time-dependent properties of computational processes. Covering both of the two aspects is necessitated by the fact that computational processes (in particular, concurrent processes) consume their resources and develop in time, so that the state of the resources consumed by the processes and the order of their actions are time-dependent. In consequence, such formal systems should be based on the concept of dynamical state and provide updating, inheritance,and parallelism. Traditional logics like intuitionistic logic (whose proofs are represented with the means of the lambda calculus), have not been very successful at the task of modelling states and changes of states; researchers have had to invent formal systems, like Milner's CCS and pi-calculus, for which it is hard to establish a connection with logic in the traditional sense.

Linear logic has been introduced by Girard as resource-sensitive refinement of classical logic. Research in linear logic has been the thrust behind the development of a closer relationship between logic and computer science, as evid enced for example by natural characterizations of major complexity classes in terms of natural fragments of linear logic (Lincoln, Mitchell, Scedrov, Shankar, Kanovich, Lafont). Direct connections have been established between linear logic and various models of concurrency like Petri nets (Asperti, Brown, Meseguer, Gunter), games (Blass, Abramsky, Lamarche), stochastic Petri nets, Dijkstra's guarded commands (Kanovich); all this shows linear logic to be a good logical foundation for the theory of computational processes that may consume resources.

A number of concurrent programming languages based on linear logic have been designed and implemented (Kobayashi-Yonezawa, Saraswat-Lincoln, Miller-Hodas, Perrier) that, in particular, can simulate CCS and the pi-calculus.

Although these approaches have been shown to incorporate resource-sensitive aspects of computational processes, they run into difficulties with time-depende nt properties of concurrent processes, in particular, when we have to describe more or less precisely the order of the moments when some actions are taken or choices made. Here, we can take the advantage of linear logic flexibility that allows to introduce new connectors like modal operators and n on-commutative product.

Another important aspect is that linear logic provides not only basic input/output specifications (types, or formulas), but also a setting for well-typed programs (terms, or formal proofs), as well as a means of executing well-typed programs by means of term reduction or normalization (Girard, Regnier, Danos).

This computation as term reduction paradigm can be further refined to feasible computations, and two systems, light linear logic (LLL) and elementary linear logic (ELL), have been introduced by Girard, both based on the idea that normalization should respect the depth of formulas. Poly-time and elementary functions have been proved to be the exact classes represented in LLL and ELL, resp. (Girard). Although the syntax of LLL, as well as the self-controlled normalization for this system, is well-understood due to Girard's careful analysis in terms of proof nets, still semantics for LLL had remained an open problem. Recently, this problem has been sorted out by Kanovich, where a semantic setting for the underlying logical system is established in terms of time-state models, an extension of linear logic with certain features of temporal logic.

All these results show linear logic to be a good logical foundation for computer science.

Maxime Kanovich