Why we need quotients and subsets of datatypes ?
One of the reaons is we could derive operations naturally. A simple example is the unordered pair. Define as for all . Then, is the unordered pair.
Another example is where if . We could define plus, inverse, and products via , , and respectively. It could be shown that it’s isomorphic to .
One more example is . We could construct a queue by defining a equivalence relation such that for all , if where is ther reverse list of . Hence, the standard operations on like pop and push could be defined as for is not null list otherwise, and respectively.
Likewise, we could describe many data structure as subsets. For example, the complete binary tree where is the root and are binary tree satisfying the complete properties. That is, and are complete. We could define the balenced tree similiarly.
In programming, we want to aviod some unsuitable case of the input like the input is outside of the English letters within ASCII code. We usually just check the input in the function or define a type (class, in OOP) which maps the type to the sub-type. In the later method, we have to define functions in the sub-type whether we have one in the super-type or not (thought, inheritance is a possible solution). In the former method, it looks irrelevant to the behavior(algorithm) of the function itself but we glue them together inside the same place.
Can we devise an algorithmtic method on type and we could (almost) directly use it on its quotient and subset via a natural mapping, that is, given and , do we have
- , and
such that and where is surjective and is injective ( is just inclusion).