Abstract
Two lists are bag equivalent 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. This paper describes how one can define bag equivalence as the presence of bijections between sets of membership proofs. This definition has some desirable properties:
-
Many bag equivalences 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 slight variation of the definition one gets set equivalence instead, i.e. equality up to order and multiplicity. Other variations give the subset and subbag preorders.
-
The definition works well in mechanised proofs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abbott, M., Altenkirch, T., Ghani, N.: Containers: Constructing strictly positive types. Theoretical Computer Science 342, 3–27 (2005)
Abbott, M., Altenkirch, T., Ghani, N., McBride, C.: Constructing Polymorphic Programs with Quotient Types. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 2–15. Springer, Heidelberg (2004)
Altenkirch, T., Levy, P., Staton, S.: Higher-Order Containers. In: Ferreira, F., Löwe, B., Mayordomo, E., Mendes Gomes, L. (eds.) CiE 2010. LNCS, vol. 6158, pp. 11–20. Springer, Heidelberg (2010)
Altenkirch, T., Morris, P.: Indexed containers. In: LICS 2009, pp. 277–285 (2009)
Contejean, E.: Modeling Permutations in Coq for Coccinelle. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Rewriting, Computation and Proof. LNCS, vol. 4600, pp. 259–269. Springer, Heidelberg (2007)
Danielsson, N.A.: Total parser combinators. In: ICFP 2010, pp. 285–296 (2010)
Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Tech. Rep. inria-00258384, version 10, INRIA (2011)
Hermida, C., Jacobs, B.: An Algebraic View of Structural Induction. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 412–426. Springer, Heidelberg (1995)
Hofmann, M., Streicher, T.: The groupoid model refutes uniqueness of identity proofs. In: LICS 1994, pp. 208–212 (1994)
Hoogendijk, P., de Moor, O.: Container types categorically. Journal of Functional Programming 10(2), 191–225 (2000)
Hoogendijk, P.F.: (Relational) Programming Laws in the Boom Hierarchy of Types. In: Bird, R.S., Morgan, C.C., Woodcock, J.C.P. (eds.) MPC 1992. LNCS, vol. 669, pp. 163–190. Springer, Heidelberg (1993)
Hoogendijk, P.F., Backhouse, R.C.: Relational programming laws in the tree, list, bag, set hierarchy. Science of Computer Programming 22(1-2), 67–105 (1994)
Joyal, A.: Une théorie combinatoire des séries formelles. Advances in Mathematics 42(1), 1–82 (1981)
Meertens, L.: Algorithmics: Towards programming as a mathematical activity. In: Mathematics and Computer Science, CWI Monographs, vol. 1, pp. 289–334. North-Holland (1986)
Morris, P.W.J.: Constructing Universes for Generic Programming. Ph.D. thesis, The University of Nottingham (2007)
Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology and Göteborg University (2007)
Streicher, T.: Investigations Into Intensional Type Theory. Habilitationsschrift, Ludwig-Maximilians-Universität München (1993)
The Agda Team: The Agda Wiki (2012), http://wiki.portal.chalmers.se/agda/
The Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.3pl3 (2011)
Voevodsky, V.: Univalent foundations project - a modified version of an NSF grant application (2010) (unpublished)
Yorgey, B.A.: Species and functors and types, oh my! In: Haskell 2010, pp. 147–158 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danielsson, N.A. (2012). Bag Equivalence via a Proof-Relevant Membership Relation. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-32347-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32346-1
Online ISBN: 978-3-642-32347-8
eBook Packages: Computer ScienceComputer Science (R0)