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

[ 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

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

[ 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

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

[ 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

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

[ 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

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

[ 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

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

[ 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

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,

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

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

Re: [TYPES] What algebra am I thinking 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

Re: [TYPES] What algebra am I thinking 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

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

[ 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

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

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

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

[ 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

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

[ 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