# What is a quotient structure?

I was reading a paper here, and it mentioned "quotient structure" in the following sentence (third page, second paragraph of the paper)

In order to obtain a representation of terms truly isomorphic to λ-terms, we need to build a quotient structure, quotient the set of raw terms with respect to alpha-equivalence. This construction based on a quotient corresponds very closely to the of presentation from standard textbooks on λ-calculus.

I am hoping that someone could point me a good tutorial on quotient structures.

• I wrote a blog post about quotients recently that you may find useful: hedonisticlearning.com/posts/… – Derek Elkins Feb 26 '17 at 19:28
• In mathematics this is called a congruence (an equivalence relation which is compatible with the algebraic or other structure). The author is probably using the term "quotient structure" because he's a computer scientists. They see structures everywhere, and are not necessarily aware of traditional mathematical terminology. – Andrej Bauer Feb 26 '17 at 20:11

The idea is that two expressions which are α-equivalent are not meaningfully different. λx.λy.x and λz.λy.z are technically different expressions. They are α-equivalent, though, they intuitively represent the same thing. In most circumstances, differentiating between them is useless at best, counter-productive at most.

The quotient set is a formal definition that allows to say “we consider α-equivalent expressions to actually be the same”. So what is this formal definition?

### Equivalence relation

First of all, an equivalence relation ~ on a set S is a binary relation that is:

• reflexive: for every x in S, x ~ x.
• symmetric: for x, y in S, if x ~ y, then y ~ x.
• transitive: for x, y, z in S, if x ~ y and y ~ z, then x ~ z.

Examples:

• For any set, = is an equivalence relation.
• a = b (mod n) is an equivalence relation.
• α-equivalence is an equivalence relation.

### Equivalence class and quotient set

Now, given S and ~, and a in S, the equivalence class of a for ~ is the set [a] of all x in S such that x ~ a.

By reflexivity, it is clear that each x in S is in [x]. Moreover, using symmetry and transitivity, you can show that if x in [y], then [y] = [x]. So each x is in a single equivalence class, two distinct equivalence classes do not intersect.

Given S and ~, the set {[x] | x in S} of every equivalent class is a partition of S. This partition is called quotient set of S by ~ (usually noted S/~).

Example: For the relation = (mod 5) on Z, the equivalence classes are [0], [1], [2], [3], [4]. Each integer is equal to a single 0 ≤ n ≤ 4 modulo 5.

Usually, one doesn’t bother writing the [ ] when it’s not necessary.

• So basically, every equivalent class is a quotient set. I know equivalence relations but did not know quotient set. Your description made it clear to me. Thx :) – alim Feb 27 '17 at 15:36
• @alim No, every element of a quotient set is an equivalence class. A quotient set is a collection of equivalence classes (that all together partition the original set). – Derek Elkins Feb 28 '17 at 0:03

It's a term coming from abstract algebra. When you quotient a set $S$ with respect to some equivalence relation $\sim$, you are replacing the set $S$ with its equivalence classes under $\sim$. Often the set $S$ has operations defined on it, and in that case we want these operations to be well defined for the quotient $S/\sim$, in the sense that if $x_i \sim y_i$ then $x_1 \circ x_2 \sim y_1 \circ y_2$. This allows us to define $\circ$ on the quotient.

An example in real analysis is $L^p$ spaces, in which functions are defined "up to measure zero".

• If someone doesn’t know what a quotient set is, I wouldn’t expect them to be familiar with equivalence classes. I would add a definition of the term to make the answer more accessible. – Édouard Feb 26 '17 at 20:08