Calculating Bag Equalities

Calculating Bag Equalities
Talk given at meeting #68 of IFIP WG2.1, Rome, 2012-02-06. (Slightly edited.) [pdf]


Two lists are "bag equal" if they are permutations of each other, i.e. if they contain the same elements, with the same multiplicity, but perhaps not in the same order. I plan to describe how one can define bag equality as the presence of bijections between sets of membership proofs. This definition has some nice properties:

  • Many bag equalities can be proved using a flexible form of equational reasoning.
  • The definition generalises easily to arbitrary unary containers, including types with infinite values, such as streams.
  • By using a small variant of the definition one gets set equality instead, i.e. equality where neither multiplicity nor order matters. Similar variations give the subset and subbag preorders.
  • The definition works well in mechanised proofs.

Nils Anders Danielsson
Last updated Mon Feb 6 21:20:01 UTC 2012.