[TYPES] What algebra am I thinking of?

[Peter Selinger]

Hi Neel and Phil,

I don't think the connection between the name of the Int construction
and the integers is a joke, but that that was in fact the original
motivation for the name. As far as I know, the name Int V for what we
now call the Int-construction originates in Joyal, Street, and
Verity's original 1996 paper "Traced monoidal categories" (p.453). A
beautiful paper, by the way. In the same paper, they also mention at
the top of p.465 an example where the compact category has objects
that are words in the symbols "-" and "+", whereas the underlying
traced monoidal category only has "+". Also, on p.467, they write "The
objects of Int Rel can be called integer sets in contrast to the
objects of Rel which are natural sets". So while they didn't give the
exact example you mentioned, it is clear from their formulation that
the relationship between the natural numbers and the integers is very
much what they had in mind, and that that is where they took the name
"Int" from (i.e., "Integers" and not "Interaction"). They do also
mention the geometry of interaction, but only in passing in the last
sentence of the introduction.

-- Peter

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 <nk480 at cl.cam.ac.uk> 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
> >> nk480 at cl.cam.ac.uk
> >>
> >>
> >>
> >>
> >> The University of Edinburgh is a charitable body, registered in
> >> Scotland, with registration number SC005336.
> 
>