Re: [TYPES] What algebra am I thinking of?

[Valeria de Paiva]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Neel,

Still on the subject of Lawvere's metric spaces and generalized logic, I
think many people knew about it. I, for instance had a paper from 1991,
which you can read in
https://www.slideshare.net/valeria.depaiva/a-dialectica-model-of-the-lambek-calculus,
which has the Lawvere example of the natural numbers N as a model of
multiplicative linear logic LP, as a folklore example that Pino Rosolini
told me about. But yes, I was not looking for traces then.

cheers
Valeria

>
> Neel Krishnaswami 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/
> 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 
> 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.
> >
> >
>
>
>
> --
>
> Message: 2
> Date: Fri, 06 Apr 2018 11:07:19 +
> From: Alejandro D?az-Caro 
> To: types 
> Subject: [TYPES] System F and System T names
> Message-ID:
>  hazre_u1ial...@mail.gmail.com>
> Content-Type: text/plain; charset="UTF-8"
>
> Dear Type-theorists,
>
> Does anyone know where do the names System "F" and System "T" comes from? I
> am not asking who introduced those names (Girard System F, and G?del System
> T), but what the "F" and the "T" means.
>
> Kind regards,
> Alejandro
> --
>
> http://diaz-caro.web.unq.edu.ar
>
>
> --
>
> Message: 3
> Date: Fri, 6 Apr 2018 13:03:17 +0100
> From: Neel Krishnaswami 
> To: Alejandro D?az-Caro , types
> 
> Subject: Re: [TYPES] System F and System T names
> 

Re: [TYPES] What algebra am I thinking of?

[Peter Selinger]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Neel and Phil,

I don't think the connection between the name of the Int construction
and the integers is a joke, but that that was in fact the original
motivation for the name. As far as I know, the name Int V for what we
now call the Int-construction originates in Joyal, Street, and
Verity's original 1996 paper "Traced monoidal categories" (p.453). A
beautiful paper, by the way. In the same paper, they also mention at
the top of p.465 an example where the compact category has objects
that are words in the symbols "-" and "+", whereas the underlying
traced monoidal category only has "+". Also, on p.467, they write "The
objects of Int Rel can be called integer sets in contrast to the
objects of Rel which are natural sets". So while they didn't give the
exact example you mentioned, it is clear from their formulation that
the relationship between the natural numbers and the integers is very
much what they had in mind, and that that is where they took the name
"Int" from (i.e., "Integers" and not "Interaction"). They do also
mention the geometry of interaction, but only in passing in the last
sentence of the introduction.

-- Peter

Neel Krishnaswami 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/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  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.
> 
> 

Re: [TYPES] What algebra am I thinking of?

[Tadeusz Litak]

[ 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 <
neelakantan.krishnasw...@gmail.com> 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  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.




The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Re: [TYPES] What algebra am I thinking of?

[Francesco Gavazzo]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I am not sure whether the following is the correct definition of a monus,
but following Neel (as well as the analogy with natural numbers) one could
look at monus in a monoid as right adjoint to monoid multiplication. In
particular, any quantale has monus, given by 'implication'.
This can indeed be found in Lawvere's 1973 paper, as well as in any
introduction/paper on quantales and/or generalised metric spaces. Another
relevant reference could be Chapter II of  Monoidal Topology, by Hofmann,
Seal, and Tholen. More generally, any paper dealing with V-categories (or
quantale-categories) provides relevant information on such algebraic
structures.

Best,
Francesco

2018-03-28 12:21 GMT+02:00 Neel Krishnaswami <
neelakantan.krishnasw...@gmail.com>:

> [ 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  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.
>>>
>>

Re: [TYPES] What algebra am I thinking of?

[Neel Krishnaswami]

[ 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  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.

Re: [TYPES] What algebra am I thinking of?

[Philip Wadler]

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

Re: [TYPES] What algebra am I thinking of?

[Jacques Carette]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

You are looking for 'multiset difference'.

http://theory.stanford.edu/~arbrad/pivc/sets.pdf

Jacques


On 2018-03-27 10:27 AM, Philip Wadler wrote:

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]



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?

James' suggestion of bags with delete is spot on. I would prefer delete to
be total rather than partial, so that deleting an element not present in
the bag leaves the bag unchanged. If a bag is a free commutative monoid,
then how does (total) delete come into the picture? Does it have an
algebraic characterisation?

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 10:42, Sanjiva Prasad 
wrote:


Eugenio, is there some reason I am missing that a left semimodule to a
semiring won't suffice?

On 27.03.2018 17:08, Eugenio Moggi wrote:


[ The Types Forum, http://lists.seas.upenn.edu/ma
ilman/listinfo/types-list ]

Consider a blockchain managing several different resources. Over time, new

resources may be added or deleted. Each input to or output from a
transaction is associated with a value, where each value consists of
associating zero or more resources with amounts, where the amounts are
natural numbers (that is, integers greater than or equal to zero).

What kind of algebra do values correspond to? It seems similar to vector
spaces, except:
   (a) adding or deleting resources increases or decreases the number of
dimensions in the vector space
   (b) the scalars in the vector space are natural numbers rather than
reals

What algebra am I thinking of? Cheers, -- P


Dear Phil, regarding the issue (b) you want to replace the FIELD of the
real
numbers with the SEMI-RING of natural numbers (N,+,*,0,1).

As suggested by Meola the structure should be a module over a RIG, see
https://ncatlab.org/nlab/show/module
More precisely
- a rig (F,*,+,1,0) for the scalars
- a commutative monoid (V,+,0) for the vectors
- an action *:FxV->V satisfying certain properties, in particular
0*v=0=f*0

When F is a field, one recovers the usual notion of vector space.

A vector space V can be infinite dimensional. In the case of a module
over a
RIG, the definition of base B should be the usual one, namely a subset of
B is a
base for V iff

- every finite subset of B is linearly independent
- every element of V is the linear combination of a finite subset of B

but the definition of LINEARLY INDEPENDENT has to be revised, to avoid
the use
of "negative".  A finite subset {v_i|i:n} of V is lineraly independent <=>
for every a,b:F^n if Sum_i a_i*v_i = Sum_i b_i*v_i, then a=b.

In the module of over N proposed by Meola, ie the maps from the set of
resourses
to the rig N that have finite support, the base is unique, and there is an
obvious definition of inner product, but I doubt you can do much with it.

However, there are modules over N that have no base.  For instance, the
module Z
over N, {1} is too small to be a base, and {1,-1} is too big.

Best Regards
Eugenio Moggi


--
Sanjiva Prasad
Professor, Department of Computer Science & Engineering
Indian Institute of Technology Delhi
Hauz Khas, New Delhi 110016




The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Re: [TYPES] What algebra am I thinking of?

[Neel Krishnaswami]

[ 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

Re: [TYPES] What algebra am I thinking of?

[Philip Wadler]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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?

James' suggestion of bags with delete is spot on. I would prefer delete to
be total rather than partial, so that deleting an element not present in
the bag leaves the bag unchanged. If a bag is a free commutative monoid,
then how does (total) delete come into the picture? Does it have an
algebraic characterisation?

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 10:42, Sanjiva Prasad 
wrote:

> Eugenio, is there some reason I am missing that a left semimodule to a
> semiring won't suffice?
>
> On 27.03.2018 17:08, Eugenio Moggi wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/ma
>> ilman/listinfo/types-list ]
>>
>> Consider a blockchain managing several different resources. Over time, new
>>> resources may be added or deleted. Each input to or output from a
>>> transaction is associated with a value, where each value consists of
>>> associating zero or more resources with amounts, where the amounts are
>>> natural numbers (that is, integers greater than or equal to zero).
>>>
>>> What kind of algebra do values correspond to? It seems similar to vector
>>> spaces, except:
>>>   (a) adding or deleting resources increases or decreases the number of
>>> dimensions in the vector space
>>>   (b) the scalars in the vector space are natural numbers rather than
>>> reals
>>>
>>> What algebra am I thinking of? Cheers, -- P
>>>
>>
>> Dear Phil, regarding the issue (b) you want to replace the FIELD of the
>> real
>> numbers with the SEMI-RING of natural numbers (N,+,*,0,1).
>>
>> As suggested by Meola the structure should be a module over a RIG, see
>> https://ncatlab.org/nlab/show/module
>> More precisely
>> - a rig (F,*,+,1,0) for the scalars
>> - a commutative monoid (V,+,0) for the vectors
>> - an action *:FxV->V satisfying certain properties, in particular
>> 0*v=0=f*0
>>
>> When F is a field, one recovers the usual notion of vector space.
>>
>> A vector space V can be infinite dimensional. In the case of a module
>> over a
>> RIG, the definition of base B should be the usual one, namely a subset of
>> B is a
>> base for V iff
>>
>> - every finite subset of B is linearly independent
>> - every element of V is the linear combination of a finite subset of B
>>
>> but the definition of LINEARLY INDEPENDENT has to be revised, to avoid
>> the use
>> of "negative".  A finite subset {v_i|i:n} of V is lineraly independent <=>
>> for every a,b:F^n if Sum_i a_i*v_i = Sum_i b_i*v_i, then a=b.
>>
>> In the module of over N proposed by Meola, ie the maps from the set of
>> resourses
>> to the rig N that have finite support, the base is unique, and there is an
>> obvious definition of inner product, but I doubt you can do much with it.
>>
>> However, there are modules over N that have no base.  For instance, the
>> module Z
>> over N, {1} is too small to be a base, and {1,-1} is too big.
>>
>> Best Regards
>> Eugenio Moggi
>>
>
> --
> Sanjiva Prasad
> Professor, Department of Computer Science & Engineering
> Indian Institute of Technology Delhi
> Hauz Khas, New Delhi 110016
>
>
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Re: [TYPES] What algebra am I thinking of?

[Jacques Carette]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Correct.  And that (free commutative monoid) is exactly the Bag 
data-structure, with its union and cartesian product operations. [Where 
Bag here is understood to be finitely supported, even though the set of 
resources can be infinite]


Jacques

On 2018-03-27 8:10 AM, Harrison Brown wrote:

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Phil,

I think Meola and Eugenio have it right, and in particular I think you're
describing the free module over N generated by the set of resources. (Free
modules over rings proper behave pretty much like vector spaces; I don't
know much about the theory of free modules over rigs, but the analogy
should hold.) And, analogous to how free abelian groups are free modules
over Z, I believe that this is isomorphic to a free commutative monoid
generated by the set of resources. If you want to forbid the empty
transaction, you have a free commutative semigroup. Of course if the
resources interact in some way you no longer have a free structure, but you
should still have an N-module.

Best,

Harrison

On Tue, Mar 27, 2018 at 7:38 AM, Eugenio Moggi  wrote:


[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
]


Consider a blockchain managing several different resources. Over time,

new

resources may be added or deleted. Each input to or output from a
transaction is associated with a value, where each value consists of
associating zero or more resources with amounts, where the amounts are
natural numbers (that is, integers greater than or equal to zero).

What kind of algebra do values correspond to? It seems similar to vector
spaces, except:
   (a) adding or deleting resources increases or decreases the number of
dimensions in the vector space
   (b) the scalars in the vector space are natural numbers rather than

reals

What algebra am I thinking of? Cheers, -- P

Dear Phil, regarding the issue (b) you want to replace the FIELD of the
real
numbers with the SEMI-RING of natural numbers (N,+,*,0,1).

As suggested by Meola the structure should be a module over a RIG, see
https://ncatlab.org/nlab/show/module
More precisely
- a rig (F,*,+,1,0) for the scalars
- a commutative monoid (V,+,0) for the vectors
- an action *:FxV->V satisfying certain properties, in particular 0*v=0=f*0

When F is a field, one recovers the usual notion of vector space.

A vector space V can be infinite dimensional. In the case of a module over
a
RIG, the definition of base B should be the usual one, namely a subset of
B is a
base for V iff

- every finite subset of B is linearly independent
- every element of V is the linear combination of a finite subset of B

but the definition of LINEARLY INDEPENDENT has to be revised, to avoid the
use
of "negative".  A finite subset {v_i|i:n} of V is lineraly independent <=>
for every a,b:F^n if Sum_i a_i*v_i = Sum_i b_i*v_i, then a=b.

In the module of over N proposed by Meola, ie the maps from the set of
resourses
to the rig N that have finite support, the base is unique, and there is an
obvious definition of inner product, but I doubt you can do much with it.

However, there are modules over N that have no base.  For instance, the
module Z
over N, {1} is too small to be a base, and {1,-1} is too big.

Best Regards
Eugenio Moggi

Re: [TYPES] What algebra am I thinking of?

[Harrison Brown]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Phil,

I think Meola and Eugenio have it right, and in particular I think you're
describing the free module over N generated by the set of resources. (Free
modules over rings proper behave pretty much like vector spaces; I don't
know much about the theory of free modules over rigs, but the analogy
should hold.) And, analogous to how free abelian groups are free modules
over Z, I believe that this is isomorphic to a free commutative monoid
generated by the set of resources. If you want to forbid the empty
transaction, you have a free commutative semigroup. Of course if the
resources interact in some way you no longer have a free structure, but you
should still have an N-module.

Best,

Harrison

On Tue, Mar 27, 2018 at 7:38 AM, Eugenio Moggi  wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> > Consider a blockchain managing several different resources. Over time,
> new
> > resources may be added or deleted. Each input to or output from a
> > transaction is associated with a value, where each value consists of
> > associating zero or more resources with amounts, where the amounts are
> > natural numbers (that is, integers greater than or equal to zero).
> >
> > What kind of algebra do values correspond to? It seems similar to vector
> > spaces, except:
> >   (a) adding or deleting resources increases or decreases the number of
> > dimensions in the vector space
> >   (b) the scalars in the vector space are natural numbers rather than
> reals
> >
> > What algebra am I thinking of? Cheers, -- P
>
> Dear Phil, regarding the issue (b) you want to replace the FIELD of the
> real
> numbers with the SEMI-RING of natural numbers (N,+,*,0,1).
>
> As suggested by Meola the structure should be a module over a RIG, see
> https://ncatlab.org/nlab/show/module
> More precisely
> - a rig (F,*,+,1,0) for the scalars
> - a commutative monoid (V,+,0) for the vectors
> - an action *:FxV->V satisfying certain properties, in particular 0*v=0=f*0
>
> When F is a field, one recovers the usual notion of vector space.
>
> A vector space V can be infinite dimensional. In the case of a module over
> a
> RIG, the definition of base B should be the usual one, namely a subset of
> B is a
> base for V iff
>
> - every finite subset of B is linearly independent
> - every element of V is the linear combination of a finite subset of B
>
> but the definition of LINEARLY INDEPENDENT has to be revised, to avoid the
> use
> of "negative".  A finite subset {v_i|i:n} of V is lineraly independent <=>
> for every a,b:F^n if Sum_i a_i*v_i = Sum_i b_i*v_i, then a=b.
>
> In the module of over N proposed by Meola, ie the maps from the set of
> resourses
> to the rig N that have finite support, the base is unique, and there is an
> obvious definition of inner product, but I doubt you can do much with it.
>
> However, there are modules over N that have no base.  For instance, the
> module Z
> over N, {1} is too small to be a base, and {1,-1} is too big.
>
> Best Regards
> Eugenio Moggi
>

Re: [TYPES] What algebra am I thinking of?

[Eugenio Moggi]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> Consider a blockchain managing several different resources. Over time, new
> resources may be added or deleted. Each input to or output from a
> transaction is associated with a value, where each value consists of
> associating zero or more resources with amounts, where the amounts are
> natural numbers (that is, integers greater than or equal to zero).
> 
> What kind of algebra do values correspond to? It seems similar to vector
> spaces, except:
>   (a) adding or deleting resources increases or decreases the number of
> dimensions in the vector space
>   (b) the scalars in the vector space are natural numbers rather than reals
> 
> What algebra am I thinking of? Cheers, -- P

Dear Phil, regarding the issue (b) you want to replace the FIELD of the real
numbers with the SEMI-RING of natural numbers (N,+,*,0,1).

As suggested by Meola the structure should be a module over a RIG, see
https://ncatlab.org/nlab/show/module
More precisely
- a rig (F,*,+,1,0) for the scalars
- a commutative monoid (V,+,0) for the vectors
- an action *:FxV->V satisfying certain properties, in particular 0*v=0=f*0

When F is a field, one recovers the usual notion of vector space.

A vector space V can be infinite dimensional. In the case of a module over a
RIG, the definition of base B should be the usual one, namely a subset of B is a
base for V iff

- every finite subset of B is linearly independent
- every element of V is the linear combination of a finite subset of B

but the definition of LINEARLY INDEPENDENT has to be revised, to avoid the use
of "negative".  A finite subset {v_i|i:n} of V is lineraly independent <=>
for every a,b:F^n if Sum_i a_i*v_i = Sum_i b_i*v_i, then a=b.

In the module of over N proposed by Meola, ie the maps from the set of resourses
to the rig N that have finite support, the base is unique, and there is an
obvious definition of inner product, but I doubt you can do much with it.

However, there are modules over N that have no base.  For instance, the module Z
over N, {1} is too small to be a base, and {1,-1} is too big.

Best Regards
Eugenio Moggi

Re: [TYPES] What algebra am I thinking of?

[Radu Grigore]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

You might want to look at vector addition systems, aka Petri Nets.
"Displacements" are from Z^d, but current values are from N^d, as in your
case. But, unlike your case, the dimension d is typically finite.

The restriction to nonnegative integers makes all sorts of problems harder
than they'd otherwise be.

On Tue, Mar 27, 2018 at 6:19 AM Philip Wadler  wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Consider a blockchain managing several different resources. Over time, new
> resources may be added or deleted. Each input to or output from a
> transaction is associated with a value, where each value consists of
> associating zero or more resources with amounts, where the amounts are
> natural numbers (that is, integers greater than or equal to zero).
>
> What kind of algebra do values correspond to? It seems similar to vector
> spaces, except:
>   (a) adding or deleting resources increases or decreases the number of
> dimensions in the vector space
>   (b) the scalars in the vector space are natural numbers rather than reals
>
> What algebra am I thinking of? 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/
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>

Re: [TYPES] What algebra am I thinking of?

[Matthew Meola]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I think this might be a module over a semiring. The natural numbers with
+,* form a semiring and then, over resources, would form a module over the
semiring.

For the dimensional issue, you might treat it as infinite dimensional
because there are infinitely many potential resources even if not all are
available at the moment. And then take the set of sequences with finitely
many nonzero terms. This a subspace and is infinite dimensional at least
for the vector space R-infinity. Maybe that holds for this case as well.

On Tue, Mar 27, 2018 at 01:21 Philip Wadler  wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Consider a blockchain managing several different resources. Over time, new
> resources may be added or deleted. Each input to or output from a
> transaction is associated with a value, where each value consists of
> associating zero or more resources with amounts, where the amounts are
> natural numbers (that is, integers greater than or equal to zero).
>
> What kind of algebra do values correspond to? It seems similar to vector
> spaces, except:
>   (a) adding or deleting resources increases or decreases the number of
> dimensions in the vector space
>   (b) the scalars in the vector space are natural numbers rather than reals
>
> What algebra am I thinking of? 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/
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>