Partial equivalence relation

In type theory, constructive mathematics and their applications to computer science, constructing analogues of subsets is often problematic[4]—in these contexts PERs are therefore more commonly used, particularly to define setoids, sometimes called partial setoids. Forming a partial setoid from a type and a PER is analogous to forming subsets and quotients in classical set-theoretic mathematics.

The algebraic notion of congruence can also be generalized to partial equivalences, yielding the notion of subcongruence, i.e. a homomorphic relation that is symmetric and transitive, but not necessarily reflexive.[5]

If ${\displaystyle f}$ is a partial function on a set ${\displaystyle A}$, then the relation ${\displaystyle \approx }$ defined by

${\displaystyle x\approx y}$ if ${\displaystyle f}$ is defined at ${\displaystyle x}$, ${\displaystyle f}$ is defined at ${\displaystyle y}$, and ${\displaystyle f(x)=f(y)}$

is a partial equivalence relation, since it is clearly symmetric and transitive.

If ${\displaystyle f}$ is undefined on some elements, then ${\displaystyle \approx }$ is not an equivalence relation. It is not reflexive since if ${\displaystyle f(x)}$ is not defined then ${\displaystyle x\not \approx x}$ — in fact, for such an ${\displaystyle x}$ there is no ${\displaystyle y\in A}$ such that ${\displaystyle x\approx y}$. It follows immediately that the largest subset of ${\displaystyle A}$ on which ${\displaystyle \approx }$ is an equivalence relation is precisely the subset on which ${\displaystyle f}$ is defined.

Let X and Y be sets equipped with equivalence relations (or PERs) ${\displaystyle \approx _{X},\approx _{Y}}$. For ${\displaystyle f,g:X\to Y}$, define ${\displaystyle f\approx g}$ to mean:

${\displaystyle \forall x_{0}\;x_{1},\quad x_{0}\approx _{X}x_{1}\Rightarrow f(x_{0})\approx _{Y}g(x_{1})}$

then ${\displaystyle f\approx f}$ means that f induces a well-defined function of the quotients ${\displaystyle X/{\approx _{X}}\;\to \;Y/{\approx _{Y}}}$. Thus, the PER ${\displaystyle \approx }$ captures both the idea of definedness on the quotients and of two functions inducing the same function on the quotient.

The IEEE 754:2008 floating point standard defines an "EQ" relation for floating point values. This predicate is symmetrical and transitive, but is not reflexive because of the presence of NaN values that are not EQ to themselves.