`[<<][compsci][>>][..]`
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
(CONS cells).

 http://en.wikipedia.org/wiki/Linear_type_system
 http://en.wikipedia.org/wiki/Linear_logic
 http://en.wikipedia.org/wiki/C*-algebras
 http://en.wikipedia.org/wiki/Hamiltonian_mechanics

```
`[Reply][About]`
`[<<][compsci][>>][..]`