[ 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 - 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 > [email protected] > >
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
