[TYPES] What algebra am I thinking of?
Philip Wadler
wadler at inf.ed.ac.uk
Tue Mar 27 16:02:05 EDT 2018
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 - x
>
> 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
>
>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20180327/24f2be59/attachment.ksh>
More information about the Types-list
mailing list