Interpreting Sorts

Interpreting Sorts: Issues and Designs

Recursive Sorts to Non-Recursive Sorts

A major technique for converting recursive structure to non-recursive structure is to represent the recursive structure via a name/code and a (non-recursive) structural description.
Names (or: codes) to refer to structures
Abstractly, this is what references (pointers) provide: a name or address.
(Non-Recursive) structural description
The substructure slots of the structural description are filled with the names/codes of the (representations of the) substructures. This is similar to the use of pointers to structs in C.
Name-Map
The name-map maps the names to their associated structural descriptions
Example: Lists
<name> --> (<data> <name1>)
Example: Binary Trees
<name> --> (<data> <name1> <name2>)

Abstract Sort as a quotient of a subsort

Used for example to represent sets as equivalence classes of lists without repetitions.
Concrete Sort
Say, for example, lists of integers
Admissible-Rep-Subsort
The admissible reps subsort of the concrete sort. In the example, define an admissible-rep? predicate on lists of integers such that (admissible-rep? L) iff L has no repetitions
Abstract Sort = Quotient
In the example, define an equiv-reps? relation on the Admissible-Rep-Subsort such that (equiv-reps? L1 L2) iff L1 and L2 have the same elts. The abstract sort is the resulting quotient.
Template
sort-as-quotient-of-subsort.re
Examples
See the interpretation of sets as bounded maps etc.
Subsort of product vs product of subsorts
Should the subsorting be done on the product or on the coordinates of the product? For example, rationals as pairs of Integer and Nonzero-Integer.
Subsort the product:
Development then follows the standard quotient of a subsort template. In the example, subsort of Integer, Integer
Subsort the coordinate: (distribute the subsort)
  • Concrete sort: product with distributed subsorts.
    (Example: Integer, Nonzero-Integer)
  • Reps: same as the concrete sort because the subsort predicate is always true. (Example: Rat-Rep (= Integer, Nonzero-Integer))
  • Abstract sort. In the example, quotient of equiv-rat-reps?
Distributing the subsorting (pushing it down) seems superior on two counts:
  • it puts the subsort info at the point it is actually used
  • it eliminates a layer of definition/representation