|
|
|---|
|
|
|
|---|
A library of obags (ordered bags), i.e. finite bags (a.k.a. multisets) represented as non-strictly ordered lists.
This is related to the library of osets (ordered sets), i.e. finite sets represented as strictly ordered lists. The lists that represent obags are non-strictly ordered, i.e. they may have (contiguous) duplicate elements. Like osets capture (up to isomorphism) the mathematical notion of finite sets (over ACL2 objects), obags capture (up to isomorphism) the mathematical notion of finite bags (over ACL2 objects). In particular, obag equality is equal.
Since obags are lists, in principle some list operations could be used on obags. However, this library provides versions of those list operations that have stronger guards (i.e. requiring obags instead of just lists) and that treat non-obags as the empty obag. That is, the obag operations respect a `non-bag convention' analogous to the non-set convention respected by the oset operations; some of the latter are, analogously, versions of list operations (e.g. head for car), motivated by the fact that the list operations do not respect the non-set convention.
The obag operations bagp, bfix, emptyp, head, tail, and insert are ``primitive'' in the same sense as the oset primitives: their logical definitions depend on the underlying representation as lists, and provide replacements of list operations that respect the `non-bag convention'. The logical definitions of the other obag operations are in terms of the primitive operations, without reference to the underlying list representation.
There are different logically equivalent ways to define obag operations.
The current definitions (as well as their names) are preliminary
and could be improved if needed;
these definitions favor ease of reasoning over efficiency of execution,
but, as done in osets, mbe could be used to provide
equivalent efficient definitions for execution.
As it is often possible to reason about osets abstractly
(i.e. without regard to their underlying list representation),
it should be often possible to reason about obags abstractly
(i.e. without regard to their underlying list representation),
using the theorems provided by this library.
The current theorems are preliminary
and could be improved and extended if needed.
The empty obag is
Since osets are in the
This obag library is in the same
This obag library could become a new
Compared to using the built-in ACL2::lists to represent bags,
obags are closer to the mathematical notion of bags,
at the cost of maintaining their non-strict order.
These tradeoffs are analogous to the ones between using osets
and using the built-in ACL2::lists to represent sets.
The bag library in