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.

This page is linked from: Forth is NOT intrinsically slow