Why quotient and subset on datatype ?

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 R_{uo} as (a, b)~R_{uo}~(b, a) for all a, b \in \mathbf{A}. Then, (\mathbf{A} \times \mathbf{A}) / R_{uo} is the unordered pair.

Another example is (\mathbb{N} \times \mathbb{N}) / R_{Z} where (a, b)~R_{Z}~(c, d) if a + d = b + c. We could define plus, inverse, and products via {[}(a, b){]} + {[}(c, d){]} = {[}(a + c, b + d){]}, -[(a, b)] = [(b, a)], and {[}(a, b){]} * {[}(c, d){]} = {[}(a*c+b*d), (b*c+a*d){]} respectively. It could be shown that it’s isomorphic to (\mathbb{Z}, +, *) .

One more example is \mathbf{Queue(A)}. We could construct a queue by defining a equivalence relation \mathbf{R}_q such that for all xs_{1}, xs_{2}, ys_{1}, ys_{2} \in \mathbf{List(A)}, (xs_{1}, xs_{2})~R_q~(ys_{1}, ys_{2}) if xs_{1} + xs_{2}^{r} = ys_{1} + ys_{2}^{r} where xs^{r} is ther reverse list of xs. Hence, the standard operations on \mathbf{Queue(A)} like pop and push could be defined as {[}(init(xs_{1}), xs_{2}){]} for a is not null list {[} \epsilon, (init(xs_{2}^{r}))^{r}] otherwise, and {[}(xs_{1}, xs_{2}){]} \mapsto {[}(xs_{1}, (x :: xs_{2}) {]} respectively.

Likewise, we could describe many data structure as subsets. For example, the complete binary tree (x, l, r) where x is the root and l, r are binary tree satisfying the complete properties. That is, size(l) = size(r) and l, r 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 \mathbf{A} and we could (almost) directly use it on its quotient and subset via a natural mapping, that is, given f : A \rightarrow B and g : B \rightarrow A , do we have

  • g_q : B \rightarrow (A/\sim) , and
  • f_s : A' \subset A \rightarrow B


  • \pi : A \rightarrow (A / \sim)
  • \mathbf{i} : (A') \rightarrow A

such that f_q = \pi \circ g and f_q = f \circ \mathbf{i} where \pi is surjective and \mathbf{i} is injective (\mathbf{i} is just inclusion).


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s