[Prev][Next][Index][Thread]
Affine
What is affine in "affine logic" ? Take the viewpoint of denotational
semantics and consider the intuitionistic version of linear logic, in
terms of coherent spaces or Banach spaces. Then the weakening rule
introduces fake dependencies, eg constant functions, and when we
combine it with additive features, we get more generally affine
functions. That's it.
However, this is slightly problematic :
i) we need to modify the interpretation of the tensor, ie define
E @ F by 1 & (E @ F) = (1&E) \otimes (1&F) ; however this connective
will hardly distribute over \oplus
ii) in presence of the classical symmetry, we need to consider
weakening on both sides, and the situation is rather complex.
So, to sum up, "affine" means that, if we define a denotational
semantics, then it has to be done with affine functions ; but
unfortunately, "affine logic" does not quite live at the level of
denotational semantics... what is loosened up is denotational
semantics, which is rather unpleasant.