Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Bag Equivalence via a Pro… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Bag Equivalence via a Proof-Relevant Membership Relation

Paper i proceeding
Författare Nils Anders Danielsson
Publicerad i Interactive Theorem Proving, Third International Conference, ITP 2012
Volym 7406 (LNCS)
Sidor 149-165
ISBN 978-3-642-32347-8
ISSN 0302-9743
Publiceringsår 2012
Publicerad vid Institutionen för data- och informationsteknik (GU)
Sidor 149-165
Språk en
Länkar dx.doi.org/10.1007/978-3-642-32347-...
https://gup.ub.gu.se/file/93810
Ämneskategorier Teoretisk datalogi

Sammanfattning

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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?