Linear Logic
Linear Logic, which started as a theoretical endeavor in proof theory, is now a theme of study of its own. It is the term for the study of generalized linear algebras over computational term algebras. It has ubiquitous applications in computer science: in proof theory, rewrite logic, compiler optimization, memory management, concurrency control, security assessment, etc.Expressing computations with linear terms (with logical disjunction as the sum operator, and computational constructors as the product operators) is a very convenient and elegant way to cleanly express the semantics of objects taking into account resources (such as memory, time, etc) whose physical unicity prevents multiple instances of the objects from existing at the same time: the state of the system will be represented by terms that are linear in each of the (states of) the unique objects. The sums indicate that several possibilities are open as to the state of the system, upon which a choice may be made, depending on the place in space, the moment in time, and the fulfillment of various logical hypotheses; the products indicate combination of simpler resources into more elaborate states. Linear transformations are then computational operations that preserve the fact that at any time, each unique object has just one state, even though it may still be to decide which state this is among many. Stateful programming is precisely modeled by considering state transitions as pure linear transformers of the state, with linear variables corresponding to state and resources; in such context, immediate recycling optimization for the new value of a "same" variable corresponds to the physical address of the variable not moving with time.
Linearity is a very useful tool in a wide range of situations, for a linear resource, one referenced at precisely one place and used just once, can be recycled immediately after its first and unique use, in real-time. It can be used in concurrent and distributed systems, to manage coherent access to a resource without expensive locking. It can be used in memory management to avoid costly garbage collection algorithms. It can be used in modular programming to assert security properties and negotiate resource responsibility. It can be used in real-time programming to assert real-time response of the system. It can be used in all cases for various compiler optimizations.
Since linearity is a initially a syntactic property of programs, it can be easily checked by compilers as part of type-checking. It can be made user-visible as in Clean, or in Haskell with monads; or it can be handled behind the scenes by the compiler, in a way that can take advantage of automatic optimizations independent from the user. But although user-invisibility may save the user from unnecessary choices (or protect him from harmful ones), it also prevents him from communicating deliberate choices, and thus the compiler might not be able to optimize out of inferred information for objects exported to separate compilation, dynamic linking, or dynamic code modification.
In Tunes, we believe that linear constraints should be explicitly visible to users who care, because of their importance in distributed, concurrent and modular systems.
See: user-visible typing of programs with linear types: the programming languages Clean, Haskell, and Mercury; linearity in resource management and compiler optimization: articles by Henry Baker; linearity in distributed programming: the PhD thesis of Alan Bawden, works by A. Yonezawa's team; linearity in compiler theory: articles by Philip Wadler, lots of interpretation-based analyses done in optimizing compilers; the concept of linearity in rewrite systems: any basic course on rewrite logic; etc.
This page is linked from: Aardappel Clean Constructor and Destructor Continuation Forth Linear Graph Reduction Linear Logic Comments Linearity 101 Referential Transparency and State Sheep Vault