[TYPES] What algebra am I thinking of?

[Neel Krishnaswami]

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.