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[2] 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[4].  Upto
now, I've mostly been talking about ``linear memory management'' as
``conservation of memory'', mostly in the form of binary tree nodes
(CONS cells).

[1] http://en.wikipedia.org/wiki/Linear_type_system
[2] http://en.wikipedia.org/wiki/Linear_logic
[3] http://en.wikipedia.org/wiki/C*-algebras
[4] http://en.wikipedia.org/wiki/Hamiltonian_mechanics