# Quotienting

A term from logic for a type of abstraction which takes a class of objects according to some set of rules, providing new identities for objects that are identical*according to those rules*. This can also be restated to say that it takes one domain and an equivalence relation over it and produces a new domain from the collections of objects unified by the relation.

For example, if you want to describe the Rational numbers while knowing only the Integers, you can take:

"All answers to the equation `a * x = b`

for any Integers `a` and `b`."

as describing *quotients* of Integers. This is, in fact, the origin of the term. The Rationals then are described as a domain of new (derived) objects, each of which is the set of equations which describe some equivalent or isomorphic concept. Specifically, the object we call "5/3" is an equivalence class of equations such as `x * 3 = 5`

, `x * 6 = 10`

, and so forth. So the quotienting is happening on pairs of Integers with this
equation, `(3,5)`

, `(6,10)`

, `(21,35)`

, etc. Note that "5/3" as an object is an *abstraction*, and it is not universal that a quotienting suggests an immediate *implementation* as this one's name suggests a pair of Integers. A name like that for rationals is possible because there is a uniform concept of *normalization*: a single simplest representations with all other representations inductively derivable from it.

This is generally part of the mathematical tradition of forming inductive definitions from primitive axioms to describe higher-level concepts, but **the point with Tunes is that we don't care which parts are core (primitive) and which are derived**: we want to be able to implement some concepts and translate back and forth across an isomorphism as we need to. We deliberately do

*not*want to care about implementation decisions after they are made.

- A formal but concise and informative overview from the NuPrl paper Formalizing Automata Theory I: Finite Automata (.ps). See also Quotient Types in Nuprl.
- A formal paper on quotient algebras of term-manipulation systems.
- A description of quotient structures in Coq.

**This page is linked from: ** Forth is NOT intrinsically slow