[Prev][Next][Index][Thread]

EXPONENTIALS (PS)


[I've lumped together three related messages on linear logic,
from Ursini, Arnon, and Girard.  -- Philip Wadler, moderator,
Types Forum.]

>From lincoln@Theory.Stanford.EDU Sat Oct  7 02:19:49 1995
>Date: Thu, 5 Oct 1995 9:56:09 +0100 (WET)
>From: URSINI@unisi.it
>To: LINEAR@CS.STANFORD.EDU
>Subject: PAGE 24 



       A final word on page 24 of "Advances in Linear Logic"

      Girard is right ( of course ! ). His canonical way for introducing
the ! on any phase space  works fine and gives completeness.

      I was misled, because I was not aware of the delightful  idea
of putting a turbo on the phase space of contexts, as he explained in
his answer to my question on this same media.So , I read "the monoid
of contexts" in the proof on the same page, to mean the usual lazy
free commutative monoid... with its lonely idempotent.... 
     Now we know that the real thing is this turbo monoid.
     
     Of course I have now to find a motto applicable to myself :

    "Think twice, stupid !, Think twice, stupid ! NAMELY :
                 Think twice, stupid!  "

     Aldo Ursini
 Aldo Ursini,
      Universita' di Siena
      Dipartimento di Matematica
      Via del Capitano 15
53100 Siena - Italy

   ph: OPERATOR : 577-263111 ;  DIRECT : 577-263754
  fax: 577-263730
email: ursini@unisi.it


>From lincoln@Theory.Stanford.EDU Sat Oct  7 02:20:25 1995
>From: Avron Arnon <aa@math.tau.ac.il>
>Subject: Re: EXPONENTIAL
>To: LINEAR@CS.STANFORD.EDU
>Date: Thu, 5 Oct 1995 09:00:17 +0200 (GMT+0200)


I want to add a small piece of information concerning the message
below: The interpretation of ! which is mentioned below is exactly the
one I gave in my paper: "The semantics and Proof theory of Linear
Logic" (TCS 57 (1988), pp. 161-184). Only I have defined it in the
framework of the general algebraic structures which I called "Girard
structures" (now known also as Girard quantales).  which I show to be
equivalent to Girard's phase spaces (personally, I believe that it is
easier to work here in terms of the general algebraic structures,
using some general properties, than in terms of their implementation
as phase spaces).

Arnon Avron

+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

>             On a possible errata corrige ??
> 
> In his survey paper , in "Advances in Linear Logic" (Ed.Girard-Lafont-
> Regnier), page 24, Girard semplifies the phase semantic for ! as follows:
> 
>        !X is the double linear negation of (X intersection I),
>        where  "I is the set of idempotents of M which belong to 1".
> 
>        This would force uniqueness of !,does it ?
>        So one should say that " I is a set of idempotents belonging to 1 and
>        closed under product."
>        
>        If I am right, then this may remind the latin motto
>             Aliquando dormitat et bonus Homerus
>        
>  Aldo Ursini,
>       Universita' di Siena
>       Dipartimento di Matematica
>       Via del Capitano 15
> 53100 Siena - Italy
> 
>    ph: OPERATOR : 577-263111 ;  DIRECT : 577-263754
>   fax: 577-263730
> email: ursini@unisi.it
> 
> 



>From lincoln@Theory.Stanford.EDU Sat Oct  7 02:22:18 1995
>From: girard@lmd.univ-mrs.fr (Jean-Yves GIRARD)
>Date: Fri, 6 Oct 95 10:35:39 +0100
>Subject: EXPONENTIALS (PS)
>To: LINEAR@CS.STANFORD.EDU


A few remarks after (private) reactions to my last mail on LINEAR

i) I was surprised to discover that the version of the paper <<Linear  
Logic : its syntax and semantics>> which is printed in the book  
Advances in Linear Logic is not quite the same as the file Synsem.ps  
available on ftp. In the book the footnote 9, page 24, is missing
...the monoids of contexts (i.e. multisets of formulas^footnote9)
footnote 9 : We ignore the multiplicity of formulas ?\Gamma (I should  
have said ?A), so that I is the set of contexts ?\Gamma.

ii) the congruence p~q is a way to speak of equivalence ; the failure  
of completeness when equality is replaced with ~ comes from the -now  
familiar- fact that
from p -o 1 and p -o p\Tensor p, there is no way to conclude
p -o !p.

iii) although the definition in terms of equality is correct and is  
clearly the simplest one, it is misleading, since many pits are  
hidden under the carpet. I therefore indicata an alternative  
definition, which is not so immediate, but which is more transparent:
- a congruence is defined to be an equivalence compatible with the  
phase space structure, i.e. the monoid operation and the absurd fact.  
All congruences sit in between two extremes, ~ and =.
- an exponential is given by specifying a congruence C; one  
introduces the I = {p;p \in [1] and p C p^2} and one defines 

[!A] = (I \inter A)^{\perp\perp}.

jyg
---

Jean-Yves GIRARD
Directeur de Recherche

CNRS, Laboratoire de Mathematiques Discretes
163 Avenue de Luminy, case 930
13288 Marseille cedex 9

<girard@lmd.univ-mrs.fr>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)