Re: [TYPES] What algebra am I thinking of?
Neel Krishnaswami <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ 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/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 <[email protected]> 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 >> [email protected] >> >> >> >> >> The University of Edinburgh is a charitable body, registered in >> Scotland, with registration number SC005336.