Sun Aug 30 11:24:57 CEST 2009
Linear Type Systems
Main idea: variables disappear from scope once referenced.
From the logic pov.: the linear logic is concerned with
_transformation_ of resources as opposed to an ever growing
accumulation of facts (classical logic).
In a nutshell, a logic is built of a set of axioms and a set of
combination rules. In classical logic, you can start from a set of
propositions and construct larger sets of propositions by chaining
combination rules (inference rules). In linear logic, to add a new
proposition to a ``context'' (multiset), you need to _consume_ one you
already have, preventing you to ever use it again.
It is mentioned in the wikipedia article that that linear logic can
be seen as ``the interpretation of classical logic by replacing
boolean algebras by C*-algebras''. This vaguely rings a bell,
conforming to my intuition of computation as an endomap of a
constant-size space instead of an ``explosion'' of an initial seed.
Conservation of resources in linear logic works a bit like
conservation of energy in a classical hamiltonian system. Upto
now, I've mostly been talking about ``linear memory management'' as
``conservation of memory'', mostly in the form of binary tree nodes