[TYPES] What algebra am I thinking of?
Neel Krishnaswami
neelakantan.krishnaswami at gmail.com
Tue Mar 27 12:41:20 EDT 2018
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
More information about the Types-list
mailing list