Quotient types

quotient type

The equality relation on a type, written s=t in T or s=_Tt, defines the element's referential nature. The semantic models we use in section  take a type to be a partial equivalence relation (per)partial equivalence relation (per) on a collection of terms.

Given a type T, other types can be defined from it by specifying new equality relations on the elements of T. For example, given the integers ${{\mathbb{Z} }}$, we can define the congruence integers ${{\mathbb{Z} }} /\!/ mod\ n$ to be the type whose elements are those of ${{\mathbb{Z} }}$ related by

$$x=y\ mod\ n\ \mbox{iff}\ n\ divides\ (x-y).$$

More symbolically, let $n\ \vert\ m$ mean that n divides m, i.e., $\exists k\!:\!{{\mathbb{N} }}.\ m=k\star n$. Then $x=y\ mod\ n$ iff $n\ \vert\ (x-y)$. If rm(x, n) is the remainder when x is divided by n, then clearly $x=y\ mod\ n\ \mbox{iff}\ rm(x, n)=rm(y, n)$ in ${{\mathbb{Z} }}$. It is easy to see that $x=y\ mod\ n$ is an equivalence relation on ${{\mathbb{Z} }}$. In general, this is all we require to form a quotient type. If A is a type and E is an equivalence relation on A, then $A/\!/E$quotient type is a new type, the quotient of A by E. The equality rule is x=y in $A/\!/E\ \mbox{iff}\ E(x, y)\ \mbox{for}\ x, y$ in A. Here are the new rules.

$A/\!/E$ is a type iff A is a type and E is an equivalence relation on A

$\bar{H} \vdash a$ in $A/\!/E$ by $quotient\_member$

$\bar{H} \vdash a$ in A

$\bar{H}, x\!:\!A/\!/E, \bar{J} \vdash b[x]$ in B by quotientL

$\ \ \ \ \bar{H}, x\!:\!A, \bar{J} \vdash b[x]$ in B

$\ \ \ \ \bar{H}, x\!:\!A, x'\!:\!A, E(x, x'), \bar{J} \vdash b[x]=b[x']$ in B

For P to be a propositional function on a type A, we require that when a=a' in A then P(a) and P(a') are the same proposition. If we consider atomic propositions P(x) iff x=t in $A/\!/E$, then a=t in $A/\!/E$. The rules for equality of expressions built from elements of $A/\!/E$ will guarantee the functional nature of propositions over $A/\!/E$. We discuss the topic in detail in section  and in the literature on Nuprl [28,3].

The quotient type is very important in many subjects. We have found it especially natural in automata theory ([32]), rational arithmetic and of course, for congruences. For congruence integers we have proved Fermat's little theorem in this form:Fermat's little theorem

Theorem 6   $\forall p\!:\!\left\{x\!:\!{{\mathbb{N} }}\ \vert\ prime(p)\right\}.\ \forall x\!:\!{{\mathbb{Z} }}/\!/mod\ p.\ (x^p=x)$

Here the display mechanism suppresses the type on equality when it can be immediately inferred from the type of the equands.