Affine

• To: lineaire <linear@CS.Stanford.EDU>
• Subject: Affine
• From: Jean-Yves GIRARD <girard@iml.univ-mrs.fr>
• Date: Tue, 1 Jul 97 14:27:03 +0100
• Delivery-Date: Fri, 04 Jul 1997 10:40:26 -0500
• Sender: lincoln@CS.Stanford.EDU

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.

• Prev: WoLLIC'97 - Call for Participation
• Next: Re: Affine
• Index(es):
  • Main
  • Thread