[TYPES] What algebra am I thinking of?

[Tadeusz Litak]

You're welcome! I realized now that this is explicitly stated in the opening paragraph of the 1996 Joyal, Street and 
Verity paper:

> Naively speaking, the construction is a glorification of the construction of the
> integers from the natural numbers.

O ye classical papers that we quote so oft and so rarely read...


t.



On 28/03/18 20:43, Philip Wadler wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
>
> Thanks to Neel, Tadeusz, and Francesco for additional replies & citation. I
> love the "Int" joke! -- 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 28 March 2018 at 07:21, Neel Krishnaswami <
> neelakantan.krishnaswami at gmail.com> 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/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.
>>>>
>>>
>>>
>>> The University of Edinburgh is a charitable body, registered in
>>> Scotland, with registration number SC005336.