Based on A New Look at Multisets by Norman J Wildberger.
The data structure provided by this library is MSet
. An MSet[M,A]
is a multiset of values of type A with multiplicities in M.
For example, an MSet[Natural,A]
is a multiset where values of type A
can have zero or more occurrences. An MSet[Boolean,A]
is an ordinary set.
To get all the functionality of this library, add the following imports:
import spire.syntax.all._
import mset._
import Realm._
This type differs from most implementations of multisets in that the multiplicities can be integers (for negative occurrences), rational numbers (for fractional occurrences), intervals and probability distributions (for non-deterministic or "fuzzy" occurrences), or any other type of value. The algebra on that type will determine what operations are available on the MSet
. In particular, MSet
provides operations for any type of measure that forms a Realm
, a type this library also provides:
trait Realm[A] {
def meet(x: A, y: A): A
def join(x: A, y: A): A
def sum(x: A, y: A): A
def zero: A
}
Notably, MSet[M,A]
forms a Realm
for any Realm[M]
.
A Realm[A]
is a distributive lattice on A
(through meet
and join
), and a commutative monoid (on sum
and zero
). Realms must obey the following laws (where ∧
is meet
, ∨
is join
, +
is sum
and 0
is zero
):
m + n ≡ n + m
m ∨ n ≡ n ∨ m
m ∧ n ≡ n ∧ m
k + (m + n) ≡ (k + m) + n
k ∨ (m ∨ n) ≡ (k ∨ m) ∨ n
k ∧ (m ∧ n) ≡ (k ∧ m) ∧ n
k + (m ∨ n) ≡ (k + m) ∨ (k + n)
k + (m ∧ n) ≡ (k + m) ∧ (k + n)
k ∧ (m ∨ n) ≡ (k ∧ m) ∨ (k ∧ n)
k ∨ (m ∧ n) ≡ (k ∨ m) ∧ (k ∨ n)
0 + m ≡ m
0 ∨ m ≡ m
0 ∧ m ≡ 0
m ∨ (m ∧ n) ≡ m
m ∧ (m ∨ n) ≡ m
m ∨ m ≡ m
m ∧ m ≡ m
(m ∨ n) + (m ∧ n) ≡ m + n
Realm
extends spire.algebra.Order
because any join semilattice
defines an order:
m ≤ n ≡ m ∨ n = n
Some realms may additionally obey a cancellation law, and we call these cancellative realms:
(k + n = m + n) ⇒ (k = m)
Two Realm
subtypes with products are also provided which are RigRealm
(realms with products) and RingRealm
(realms with products and additive inverses).
A well-behaved realm with products requires products to distribute over the realm operations:
a * (b ∨ c) ≡ (a * b) ∨ (a * c)
a * (b ∧ c) ≡ (a * b) ∧ (a * c)
a * (b + c) ≡ (a * b) + (a * c)
A realm with inverses must obey a De Morgan law:
¬(a ∨ b) ≡ (¬a) ∧ (¬b)
¬(a ∧ b) ≡ (¬a) ∨ (¬b)
An MRealm
is a realm with a partial additive inverse called monus
or ∸
. Every RingRealm
is an MRealm
, where the monus happens to be exact. A monus operation
is a kind of truncated or residuated subtraction.
The monus must be left adjoint to the addition:
a ∸ b ≤ c ≡ a ≤ b + c
In terms of the meet
and join
, that means:
a ∧ (b + (a ∸ b)) ≡ a
((b + c) ∸ b) ∨ c ≡ c
That is, monus(a,b)
is the smallest object which when added to b
is at
least a
.
Examples of monus operations include truncated subtraction on natural numbers, the quotient operation on integers, and the difference operation on sets and multisets.