Re: [TYPES] What algebra am I thinking of?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Neel,

Still on the subject of Lawvere's metric spaces and generalized logic, I
think many people knew about it. I, for instance had a paper from 1991,
which you can read in
https://www.slideshare.net/valeria.depaiva/a-dialectica-model-of-the-lambek-calculus,
which has the Lawvere example of the natural numbers N as a model of
multiplicative linear logic LP, as a folklore example that Pino Rosolini
told me about. But yes, I was not looking for traces then.

cheers
Valeria

>
> Neel Krishnaswami wrote:
> >
> >
> > [ The Types Forum, http://lists.seas.upenn.edu/
> mailman/listinfo/types-list ]
> >
> > Hi Phil,
> >
> > I learned about this from Martin Escardo, and he told me the observation
> > about monoidal closure is in Lawvere's paper "Metric Spaces, Generalized
> > Logic, and Closed Categories".
> >
> > One further observation I have not seen written down anywhere is that
> > the natural numbers also support a trace (ie, feedback) operator, since
> > it is also the case that x + y ? z + y if and only if x ? z.
> >
> > This means that the Geometry of Interaction construction can be applied
> > to the natural numbers, which yields a preorder of pairs of natural
> > numbers (n,m). In this case, two objects have a map between them if
> > one object is greater than the other, viewing each object (n, m) as the
> > signed integer n - m.
> >
> > As a result, I've sometimes wondered if the Int construction got its
> > name as a bit of a joke!
> >
> > Best,
> > Neel
> >
> >
> > On 27/03/18 21:02, Philip Wadler wrote:
> > > [ The Types Forum, http://lists.seas.upenn.edu/
> mailman/listinfo/types-list ]
> > >
> > >
> > >
> > > Thanks to all for further replies, and especially to Neel for his
> > > observation about monus and monoidal closure. Neel, is this written
> down
> > > anywhere? Cheers, -- P
> > >
> > > .   \ Philip Wadler, Professor of Theoretical Computer Science,
> > > .   /\ School of Informatics, University of Edinburgh
> > > .  /  \ and Senior Research Fellow, IOHK
> > > . http://homepages.inf.ed.ac.uk/wadler/
> > >
> > > On 27 March 2018 at 13:39, Neel Krishnaswami <[email protected]>
> wrote:
> > >
> > >> On 27/03/18 15:27, Philip Wadler wrote:
> > >>
> > >> Thank you for all the replies, and for reminding me of bags,
> > >>> rigs/semirings, and modules.
> > >>>
> > >>> In a rig, what corresponds to the notion of monus?
> > >>>     _?_ : ? ? ? ? ?
> > >>>     m          ? zero      =  m
> > >>>     zero      ? (suc n)  =  zero
> > >>>     (suc m) ? (suc n)  =  m ? n
> > >>> Is monus defined for every rig? (While zero and suc are defined in
> every
> > >>> rig, it's not immediately obvious to me that definition by pattern
> > >>> matching
> > >>> as above makes sense in an arbitrary rig.) What are the algebraic
> > >>> properties of monus?
> > >>>
> > >>
> > >> The natural numbers Nat, ordered by , form a posetal symmetric
> > >> monoidal closed category. Here, the objects are the natural
> > >> numbers, and Hom(n, m) = { ? | n ? m }
> > >>
> > >> The tensor product is given by:
> > >>
> > >>    x ? y ? x + y
> > >>
> > >> The monoidal closed structure arises from saturating subtraction:
> > >>
> > >>    y ? z ? z - y
> > >>
> > >> It's easy to show that Hom(x ? y, z) = Hom(x, y ? z) since
> > >> x + y ? z if and only if x ? z - y.
> > >>
> > >> (This is all given in Lawvere's paper "Metric Spaces, Generalized
> > >> Logic, and Closed Categories".)
> > >>
> > >> So it seems like the natural thing to do would be to say that a rig
> > >> has a monus when it is monoidal closed with respect to its addition,
> > >> defining x ? z to hold when there exists a y such that x = y + z.
> > >>
> > >> Best,
> > >> Neel
> > >>
> > >>
> > >>
> > >> --
> > >> Neel Krishnaswami
> > >> [email protected]
> > >>
> > >>
> > >>
> > >>
> > >> The University of Edinburgh is a charitable body, registered in
> > >> Scotland, with registration number SC005336.
> >
> >
>
>
>
> ------------------------------
>
> Message: 2
> Date: Fri, 06 Apr 2018 11:07:19 +0000
> From: Alejandro D?az-Caro <alejandro-bV/[email protected]>
> To: types <types-list-nHFbR+4dATOoZA3Q9b/[email protected]>
> Subject: [TYPES] System F and System T names
> Message-ID:
>         <CAGvJX+y9dYNxp6Hii8krNNhb5ip4GM2QniQY
> [email protected]>
> Content-Type: text/plain; charset="UTF-8"
>
> Dear Type-theorists,
>
> Does anyone know where do the names System "F" and System "T" comes from? I
> am not asking who introduced those names (Girard System F, and G?del System
> T), but what the "F" and the "T" means.
>
> Kind regards,
> Alejandro
> --
>
> http://diaz-caro.web.unq.edu.ar
>
>
> ------------------------------
>
> Message: 3
> Date: Fri, 6 Apr 2018 13:03:17 +0100
> From: Neel Krishnaswami <[email protected]>
> To: Alejandro D?az-Caro <alejandro-bV/[email protected]>, types
>         <types-list-nHFbR+4dATOoZA3Q9b/[email protected]>
> Subject: Re: [TYPES] System F and System T names
> Message-ID: <4d2abfd0-b31c-6280-3fb7-5082448c0c1c-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org>
> Content-Type: text/plain; charset=utf-8; format=flowed
>
> Hello,
>
> 1. In "The system F of variable types, fifteen years later", Girard
> remarks  that there was no particular reason for the name F:
>
>     However, in [3] it was shown that the obvious rules of conversion for
>     this system, called F by chance, were converging.
>
> There may be another explanation in his thesis, but I haven't read it
> since unfortunately I am not fluent in French.
>
> 2. However, since I am semiliterate in German, I did take a look at
> G?del's paper "?ber eine noch nicht ben?zte Erweiterung des finiten
> Standpunktes", where System T (and the Dialectia interpretation for it)
> was introduced. He names this system in a parenthetical aside:
>
>    Das heisst die Axiome dieses Systems (es werde T genannt) sind formal
>    fast dieselben wie die der primitiv rekursiven Zahlentheorie [...][1]
>
> However, the previous page and a half were spent talking about the type
> structure of system T, so it is reasonable to guess that T stands for
> "types". But, no explicit reason is given in print.
>
> Best,
> Neel
>
>
> [1] "This means the axioms of this system (dubbed T) are nearly
> the same as those of primitive recursive number theory [...]"
>
> On 06/04/18 12:07, Alejandro D?az-Caro wrote:
> > [ The Types Forum, http://lists.seas.upenn.edu/
> mailman/listinfo/types-list ]
> >
> > Dear Type-theorists,
> >
> > Does anyone know where do the names System "F" and System "T" comes
> from? I
> > am not asking who introduced those names (Girard System F, and G?del
> System
> > T), but what the "F" and the "T" means.
> >
> > Kind regards,
> > Alejandro
> >
>
>
> ------------------------------
>
> Message: 4
> Date: Fri, 06 Apr 2018 14:10:04 +0000
> From: Alejandro D?az-Caro <alejandro-bV/[email protected]>
> To: Neel Krishnaswami <[email protected]>
> Cc: types <types-list-nHFbR+4dATOoZA3Q9b/[email protected]>
> Subject: Re: [TYPES] System F and System T names
> Message-ID:
>         <CAGvJX+yXjqRTfqGruBu3CV2pYL+bdO-oz+aYv+j10un1XX8hkw@mail.
> gmail.com>
> Content-Type: text/plain; charset="UTF-8"
>
> Dear Neel,
>
> Thank you for the info. That is exactly what I was looking for.
>
> Kind regards,
> Alejandro
>
> On Fri, 6 Apr 2018 at 14:03 Neel Krishnaswami <
> [email protected]> wrote:
>
> > Hello,
> >
> > 1. In "The system F of variable types, fifteen years later", Girard
> > remarks  that there was no particular reason for the name F:
> >
> >     However, in [3] it was shown that the obvious rules of conversion for
> >     this system, called F by chance, were converging.
> >
> > There may be another explanation in his thesis, but I haven't read it
> > since unfortunately I am not fluent in French.
> >
> > 2. However, since I am semiliterate in German, I did take a look at
> > G?del's paper "?ber eine noch nicht ben?zte Erweiterung des finiten
> > Standpunktes", where System T (and the Dialectia interpretation for it)
> > was introduced. He names this system in a parenthetical aside:
> >
> >    Das heisst die Axiome dieses Systems (es werde T genannt) sind formal
> >    fast dieselben wie die der primitiv rekursiven Zahlentheorie [...][1]
> >
> > However, the previous page and a half were spent talking about the type
> > structure of system T, so it is reasonable to guess that T stands for
> > "types". But, no explicit reason is given in print.
> >
> > Best,
> > Neel
> >
> >
> > [1] "This means the axioms of this system (dubbed T) are nearly
> > the same as those of primitive recursive number theory [...]"
> >
> > On 06/04/18 12:07, Alejandro D?az-Caro wrote:
> > > [ The Types Forum,
> > http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> > >
> > > Dear Type-theorists,
> > >
> > > Does anyone know where do the names System "F" and System "T" comes
> > from? I
> > > am not asking who introduced those names (Girard System F, and G?del
> > System
> > > T), but what the "F" and the "T" means.
> > >
> > > Kind regards,
> > > Alejandro
> > >
> >
> --
>
> http://diaz-caro.web.unq.edu.ar
>
>
> ------------------------------
>
> Message: 5
> Date: Sun, 20 May 2018 17:05:20 +0100
> From: Aaron Gray <[email protected]>
> To: Types list <types-list-nHFbR+4dATOoZA3Q9b/[email protected]>
> Subject: [TYPES] Generalised Covariant and Contravariant inference
>         rules
> Message-ID:
>         <CANkmNDeMA11QK98f0DszGD_BzStfg7++-m3ny9BiuEXKX0cT5w@
> mail.gmail.com>
> Content-Type: text/plain; charset="UTF-8"
>
> I am looking for a paper I cannot seem to find anymore that if I remember
> correctly gives or hints at a generalised scheme for describing covariant
> and contravariant type inference rules.
>
> Many thanks in advance,
>
> Aaron
> --
> Aaron Gray
>
> Independent Open Source Software Engineer, Computer Language Researcher,
> Information Theorist, and amateur computer scientist.
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Types-list mailing list
> [email protected]
> https://LISTS.SEAS.UPENN.EDU/mailman/listinfo/types-list
>
>
> ------------------------------
>
> End of Types-list Digest, Vol 107, Issue 1
> ******************************************
>



-- 
Valeria de Paiva
http://vcvpaiva.github.io/
http://research.nuance.com/author/valeria-de-paiva/
http://www.cs.bham.ac.uk/~vdp/