[TYPES] What algebra am I thinking of?
Philip Wadler
wadler at inf.ed.ac.uk
Wed Mar 28 14:43:30 EDT 2018
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.
>>>
>>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20180328/c73882b6/attachment.ksh>
More information about the Types-list
mailing list