[ 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
[ 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
[ 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
[ 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
>
[ 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
[ 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
[ 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 ∸
[ 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,
[ 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
