|
|
|---|
|
|
|
|---|
A library of omaps (ordered maps), i.e. finite maps represented as strictly ordered alists.
This is related to the library of osets (ordered sets), i.e. finite sets represented as strictly ordered lists. Like osets capture (up to isomorphism) the mathematical notion of finite sets (over ACL2 objects), omaps capture (up to isomorphism) the mathematical notion of finite maps (over ACL2 objects). In particular, omap equality is equal.
Since the total order on ACL2 values is lexicographic on cons pairs, an omap is an oset of cons pairs; furthermore, an omap is an alist. While then, in principle, some oset and alist operations could be used on omaps, this library provides versions of those oset and alist operations that have stronger guards (i.e. requiring omaps instead of just osets or alists) and that treat non-omaps as the empty omap. That is, the omap operations respect a `non-map convention' analogous to the non-set convention respected by the oset operations; some of the latter are, analogously, versions of list operations (e.g. set::head for car), motivated by the fact that the list operations do not respect the non-set convention.
The omap operations mapp, mfix, emptyp, head, tail, and update are ``primitive'' in the same sense as the oset primitives: their logical definitions depend on the underlying representation as alists, and provide replacements of alist operations that respect the `non-map convention'. The logical definitions of the other omap operations are in terms of the primitive operations, without reference to the underlying alist representation.
There are different logically equivalent ways to define omap 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
provably 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 omaps abstractly
(i.e. without regard to their underlying alist representation),
using the theorems provided by this library.
The current theorems are preliminary
and could be improved and extended if needed.
The empty omap is
Since osets are in the
This omap library could become a new
Compared to using the built-in ACL2::alists to represent maps,
omaps are closer to the mathematical notion of maps,
at the cost of maintaining their strict order.
These tradeoffs are analogous to the ones between using osets
and using the built-in ACL2::lists to represent sets.
The map library in
Compared to the records in