Re: [TYPES] What algebra am I thinking of?
Tadeusz Litak <[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] 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 < > [email protected]> 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 <[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. >>>> >>> >>> >>> The University of Edinburgh is a charitable body, registered in >>> Scotland, with registration number SC005336.