The set-to-list interpretation is
based on SET-AS-LIST in which sets are represented as equivalence classes of
nonduplicating lists.
The interpretation and mediator are in set-to-list.re
SET-AS-LIST uses the standard SORT-AS-QUOTIENT-OF-SUBSORT template.
The interpretation of sorts is:
-
Concrete-Sort
- The Concrete-Sort is List.
- Admissible-Rep-Subsort
- The admissible-rep? predicate is: no-dups?.
A list has no duplicates iff no element occurs more than once.
- Abstract-Sort
- The Abstract-Sort is obtained by factoring the
no-dups Lists via the equivalence relation set-equiv?.
Two sets are set-equiv? iff each is a (List) subset of the other:
i.e., iff they have the same elements.
SpecWeb Index
Interpretations