Partial equivalence relation
In mathematics, a partial equivalence relation is a homogeneous binary relation that is symmetric and transitive. If the relation is also reflexive, then the relation is an equivalence relation.
Definition
Formally, a relation on a set is a PER if it holds for all that:- if, then
- if and, then
Properties and applications
The following properties hold for a partial equivalence relation on a set :- is an equivalence relation on the subset.
- is difunctional: the relation is the set for two partial functions and some indicator set
- is right and left Euclidean: For, and implies and similarly for left Euclideanness and imply
- is quasi-reflexive: If and, then and.
In non-set-theory settings
In type theory, constructive mathematics and their applications to computer science, constructing analogues of subsets is often problematic—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.
Examples
A simple example of a PER that is not an equivalence relation is the empty relation, if is not empty.Kernels of partial functions
If is a partial function on a set, then the relation defined byis a partial equivalence relation, since it is clearly symmetric and transitive.
If is undefined on some elements, then is not an equivalence relation. It is not reflexive since if is not defined then — in fact, for such an there is no such that. It follows immediately that the largest subset of on which is an equivalence relation is precisely the subset on which is defined.
Functions respecting equivalence relations
Let X and Y be sets equipped with equivalence relations . For, define to mean:then means that f induces a well-defined function of the quotients. Thus, the PER captures both the idea of definedness on the quotients and of two functions inducing the same function on the quotient.