In mathematics, a partial equivalence relation (often abbreviated as PER) R on a set X is a relation which is symmetric and transitive. In other words, it holds for all a, b and c in X that:
- (Symmetry) if a R b then b R a
- (Transitivity) if a R b and b R c then a R c
If R is reflexive, then R is an equivalence relation. On the other hand, R could be taken as the empty relation, so that there are PERs that are not equivalence relations. There is in fact a simple structure to the general PER R on X: it is an equivalence relation on some subset Y of X, such that in the complement of Y no element is related by R to any other. Concretely, let <math>Y = \{ x \in X | x\,R\,x\}</math>. By construction, <math>R</math> is reflexive on <math>Y</math> and therefore an equivalence relation on <math>Y</math>. But if <math>z \notin Y</math>, then there is no <math>w \in X</math> for which z R w; if there were, then by symmetry we would have w R z, which implies z R z by transitivity, contradicting <math>z \notin Y</math>.
Example
For an example of a PER, consider a set <math>A</math> and a partial function <math>f</math> that is defined on some elements of <math>A</math> but not all. Then the relation <math>\approx</math> defined by
- <math>x \approx y</math> if and only if <math>f</math> is defined at both <math>x</math> and <math>y</math>, and <math>f(x) = f(y)</math>
is a partial equivalence relation but not an equivalence relation. It possesses the symmetry and transitivity properties, but it is not reflexive since if <math>f(x)</math> is not defined then <math>x \not\approx x</math> -- in fact, for such an <math>x</math> there is no <math>y \in A</math> such that <math>x \approx y</math>. It follows immediately that the subset of <math>A</math> for which <math>\approx</math> is an equivalence relation is precisely the subset on which <math>f</math> is defined.
Uses
PER's are used mainly in computer science, in type theory. It is also used in constructive mathematics to define setoids, sometimes called partial setoids. The action of forming one from a type and a PER is an analogue to the operations of subset and quotient in classical set-theoretic mathematics.
