Partial equivalence relation explained

In mathematics, a partial equivalence relation (often abbreviated as PER, in older literature also called restricted equivalence relation[1]) 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

R

on a set

X

is a PER if it holds for all

a,b,c\inX

that:
  1. if

aRb

, then

bRa

(symmetry)
  1. if

aRb

and

bRc

, then

aRc

(transitivity)

Another more intuitive definition is that

R

on a set

X

is a PER if there is some subset

Y

of

X

such that

R\subseteqY x Y

and

R

is an equivalence relation on

Y

. The two definitions are seen to be equivalent by taking

Y=\{x\inX\midxRx\}

.[2]

Properties and applications

The following properties hold for a partial equivalence relation

R

on a set

X

:

R

is an equivalence relation on the subset

Y=\{x\inX\midxRx\}\subseteqX

.[3]

\{(a,b)\midfa=gb\}

for two partial functions

f,g:X\rightharpoonupY

and some indicator set

Y

a,b,c\inX

,

aRb

and

aRc

implies

bRc

and similarly for left Euclideanness

bRa

and

cRa

imply

bRc

x,y\inX

and

xRy

, then

xRx

and

yRy

.[4] [5]

None of these properties is sufficient to imply that the relation is a PER.[6]

In non-set-theory settings

In type theory, constructive mathematics and their applications to computer science, constructing analogues of subsets is often problematic[7] —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.[8]

Examples

R=\emptyset

, if

X

is not empty.

Kernels of partial functions

If

f

is a partial function on a set

A

, then the relation

defined by

xy

if

f

is defined at

x

,

f

is defined at

y

, and

f(x)=f(y)

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

If

f

is undefined on some elements, then

is not an equivalence relation. It is not reflexive since if

f(x)

is not defined then

x\notx

- in fact, for such an

x

there is no

y\inA

such that

xy

. It follows immediately that the largest subset of

A

on 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\toY

, define

fg

to mean:

\forallx0x1,x0Xx1f(x0)Yg(x1)

then

ff

means that f induces a well-defined function of the quotients

X/{X}\toY/{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

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

Notes and References

  1. Scott . Dana . Data Types as Lattices . SIAM Journal on Computing . September 1976 . 5 . 3 . 560 . 10.1137/0205037.
  2. Book: Mitchell . John C. . Foundations for programming languages . 1996 . MIT Press . Cambridge, Mass. . 0585037892 . 364–365.
  3. By construction,

    R

    is reflexive on

    Y

    and therefore an equivalence relation on

    Y

    .
  4. https://www.britannica.com/topic/formal-logic/Logical-manipulations-in-LPC#ref534730 Encyclopaedia Britannica
  5. This follows since if

    xRy

    , then

    yRx

    by symmetry, so

    xRx

    and

    yRy

    by transitivity. It is also a consequence of the Euclidean properties.
  6. For the equivalence relation, consider the set

    E=\{a,b,c,d\}

    and the relation

    R=\{a,b,c\}2\cup\{(d,a)\}

    .

    R

    is an equivalence relation on

    \{a,b,c\}

    but not a PER on

    E

    since it is neither symmetric (

    dRa

    , but not

    aRd

    ) nor transitive (

    dRa

    and

    aRb

    , but not

    dRb

    ). For Euclideanness, xRy on natural numbers, defined by 0 ≤ xy+1 ≤ 2, is right Euclidean, but neither symmetric (since e.g. 2R1, but not 1R2) nor transitive (since e.g. 2R1 and 1R0, but not 2R0).
  7. Book: https://ieeexplore.ieee.org/document/5135. 10.1109/LICS.1988.5135. The strength of the subset type in Martin-Lof's type theory. [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science. 1988. Salveson. A.. Smith. J.M.. 384–391. 0-8186-0853-6. 15822016.
  8. Book: Aldo Ursini . Paulo Agliano. Logic and Algebra. 1996. CRC Press. 978-0-8247-9606-8. 161–180. J. Lambek. The Butterfly and the Serpent.
  9. Goldberg . David . 10.1145/103162.103163 . 1 . ACM Computing Surveys . 5–48 . What Every Computer Scientist Should Know About Floating-Point Arithmetic . 23 . 1991. See page 33.