Partial equivalence relation

Properties and applications

In a set-theoretic context, there is a simple structure to the general PER R on X : it is an equivalence relation on the subset Y = { x ∈ X | x R x } ⊆ X . ( Y is the subset of X such that in the complement of Y ( X ∖ Y ) no element is related by R to any other.) By construction, R is reflexive on Y and therefore an equivalence relation on Y . Notice that R is actually only true on elements of Y : if x R y , then y R x by symmetry, so x R x and y R y by transitivity. Conversely, given a subset Y of X, any equivalence relation on Y is automatically a PER on X.

PERs are therefore used mainly in computer science, type theory and constructive mathematics, particularly to define setoids, sometimes called partial setoids. The action of forming one from a type and a PER is analogous to the operations of subset and quotient in classical set-theoretic mathematics.

Every partial equivalence relation is a difunctional relation, but the converse does not hold.

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 R = ∅ (unless X = ∅ , in which case the empty relation is an equivalence relation (and is the only relation on X )).

Kernels of partial functions

For another example of a PER, consider a set A and a partial function f that is defined on some elements of A but not all. Then the relation ≈ defined by

is a partial equivalence relation but not an equivalence relation. It possesses the symmetry and transitivity properties, but it is not reflexive since if f ( x ) is not defined then x ≉ x — in fact, for such an x there is no y ∈ A such that x ≈ y . (It follows immediately that the subset of A for which ≈ is an equivalence relation is precisely the subset on which f is defined.)

Functions respecting equivalence relations

Let X and Y be sets equipped with equivalence relations (or PERs) ≈ X , ≈ Y . For f , g : X → Y , define f ≈ g to mean:

then f ≈ f means that f induces a well-defined function of the quotients X / ≈ X → Y / ≈ Y . Thus, the PER ≈ captures both the idea of definedness on the quotients and of two functions inducing the same function on the quotient.

Equality of [IEEE floating point] values

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.