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

[ 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 <[email protected]>
> 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.