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