[<<][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[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

[Reply][About]

[<<][compsci][>>][..]