Map Interpretations

Map Interpretations: Issues, and Designs

Interpreting Partial Maps: The Maps are partial in that they do not necessarily have a value at each point in their Dom.
Partial Maps as Alists: The interpretation of partial MAPs as alists is via the SORT-AS-QUOTIENT-OF-SUBSORT template: maps are represented as equivalence classes of No-Dup-Associations Alists. An Alist L has no no-dup-associations? iff there are no two associations in L with the same first coordinate. See below for a discussion of interpretation. The interpretation and mediator are in partial-map-to-alist.re

Concrete-Sort: The Concrete-Sort is Alist.
Admissible-Rep-Subsort: The admissible-rep? predicate is: no-dup-associations?. An Alist L has no duplicate associations iff there are no two associations (pairs) A1, A2 in L such that ((project 1) A1) = ((project 1) A2). Clearly, if an Alist L has no duplicate associations, it is functional.
Abstract-Sort: The Abstract-Sort is obtained by factoring the no-dup-associations? Alists via the equivalence relation map-equiv?. M1 is map-equiv? to M2 iff they are the same size and M1 is a list-subset? of M2.