[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
nk...@cl.cam.ac.uk
