[TYPES] What algebra am I thinking of?

[Philip Wadler]

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 <Sanjiva.Prasad at cse.iitd.ac.in>
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
>
>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20180327/4a89718d/attachment.ksh>