[TYPES] What algebra am I thinking of?

[Francesco Gavazzo]

I am not sure whether the following is the correct definition of a monus,
but following Neel (as well as the analogy with natural numbers) one could
look at monus in a monoid as right adjoint to monoid multiplication. In
particular, any quantale has monus, given by 'implication'.
This can indeed be found in Lawvere's 1973 paper, as well as in any
introduction/paper on quantales and/or generalised metric spaces. Another
relevant reference could be Chapter II of  Monoidal Topology, by Hofmann,
Seal, and Tholen. More generally, any paper dealing with V-categories (or
quantale-categories) provides relevant information on such algebraic
structures.

Best,
Francesco

2018-03-28 12:21 GMT+02:00 Neel Krishnaswami <
neelakantan.krishnaswami at gmail.com>:

> [ 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/ma
>> ilman/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.
>>>
>>