[ 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 <nk...@cl.cam.ac.uk> 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
nk...@cl.cam.ac.uk
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
