Fact-checked by Grok 2 weeks ago

Partial equivalence relation

A partial equivalence relation on a set is a binary relation that is symmetric (if x is related to y, then y is related to x) and transitive (if x is related to y and y is related to z, then x is related to z), but not necessarily reflexive (some elements may not be related to themselves).^[1]^[2] The domain of the relation can be partitioned into the subset where it is reflexive, on which it behaves exactly like a full equivalence relation, and the remaining elements that are unrelated to anything, including themselves.^[1]^[3] Partial equivalence relations, often abbreviated as PERs, arise naturally in mathematical logic and computer science, particularly in the semantics of type theories.^[2] In the PER model of intensional Martin-Löf type theory, types are interpreted as partial equivalence relations on the set of closed terms, where two terms are related if they are computationally equivalent up to a certain extent, allowing for partial definitions and undefined computations.^[4]^[5] This framework, pioneered in works like Allen's semantics for Constructive Type Theory, connects to Russell-style type definitions and supports extensional reasoning in otherwise intensional systems.^[5] Beyond type theory, PERs appear in categorical constructions, such as localizations of categories and PROPs for algebraic structures, where they model partial symmetries or equivalences in relational settings.^[6]^[7] They also relate to difunctional relations, though not all difunctional relations are partial equivalences, and find applications in formal verification and programming language semantics for handling polymorphism and computability.^[8]^[9]

Definition and Properties

Formal Definition

A partial equivalence relation on a set X is a binary relation R \subseteq X \times X that satisfies the properties of symmetry and transitivity, but is not required to be reflexive.^[10]^[11] Specifically, symmetry means that for all x, y \in X, if x \, R \, y, then y \, R \, x; transitivity means that for all x, y, z \in X, if x \, R \, y and y \, R \, z, then x \, R \, z.^[10]^[11] In logical notation, these axioms are expressed as \forall x \forall y \, (x \, [R](/page/R) \, y \to y \, [R](/page/R) \, x) and \forall x \forall y \forall z \, ((x \, [R](/page/R) \, y \land y \, [R](/page/R) \, z) \to x \, [R](/page/R) \, z).^[10] The domain of R, denoted \dom(R) = \{ x \in X \mid x \, R \, x \}, is the subset of X on which R is reflexive, and R restricted to \dom(R) forms a full equivalence relation that partitions \dom(R) into equivalence classes.^[10]^[11] Partial equivalence relations are often denoted using symbols such as \sim or \equiv.^[10] This contrasts with standard equivalence relations, which additionally require reflexivity on the entire set X.^[10]

Key Properties

A partial equivalence relation R on a set X is reflexive precisely on its domain D = \{ x \in X \mid x \, R \, x \}. For every x \in D, x \, R \, x holds by definition, while for x \notin D, no self-relation exists. This reflexivity on the domain arises from the symmetry and transitivity axioms: if x \, R \, y for some y \in X, then symmetry yields y \, R \, x, and transitivity implies x \, R \, x, placing x in D.^[12]^[13] The restriction of R to its domain D forms a full equivalence relation on D, as it satisfies reflexivity (on D), symmetry, and transitivity by construction. This equivalence relation partitions D into disjoint equivalence classes _R = \{ y \in D \mid x \, R \, y \} for x \in D, where each class groups elements indistinguishable under R.^[12]^[7] Under relational composition \circ, a partial equivalence relation R is idempotent, satisfying R \circ R = R. Transitivity ensures R \circ R \subseteq R, as x \, R \, y and y \, R \, z imply x \, R \, z. For the reverse inclusion, if x \, R \, z, then x \in D implies x \, R \, x (reflexivity on domain), so there exists y = x with x \, R \, y and y \, R \, z, yielding x \, (R \circ R) \, z; symmetry similarly supports this on the domain.^[7] The quotient set D / \sim_R, consisting of the equivalence classes _R, captures the structure induced by R on its domain. If the ambient set X carries additional operations or structure compatible with R, these may induce well-defined operations on the quotient, such as in algebraic or categorical contexts.^[12]^[7]

Relation to Other Relations

Comparison with Equivalence Relations

A partial equivalence relation on a set X is symmetric and transitive, but reflexive only on its domain, the subset of X where elements are related to themselves. In contrast, an equivalence relation on X is a partial equivalence relation that is total, meaning its domain equals X and it is reflexive everywhere on the set. This totality ensures that every element is partitioned into equivalence classes, whereas a partial equivalence relation induces equivalence classes only on its domain, leaving elements outside unrelated and effectively "undefined" with respect to the relation.^[14] The partial nature of such relations allows for flexible generalizations of equivalence relations, particularly useful in scenarios involving incomplete or restricted definitions, such as when modeling partial functions or domains in logic where not all elements require classification. For instance, elements outside the domain need not participate in the symmetry or transitivity properties, enabling applications where the full set X includes irrelevant or exceptional cases.^[1] The concept of partial equivalence relations emerged in the 1970s within the literature of logic and set theory, notably in the development of intuitionistic type theory by Per Martin-Löf, as a means to generalize equivalences in constructive mathematics and domain theory. This terminology facilitated models where types are interpreted as partial equivalence relations on terms, bridging set-theoretic and computational perspectives.^[15] One key implication of this partiality is that partial equivalence relations do not necessarily extend to a total preorder without imposing additional structure, such as choices for relating undefined elements, unlike the canonical compatibility of full equivalence relations with preorder extensions via quotient constructions. Furthermore, partial equivalences are not inherently compatible with orders, as their restricted domain may conflict with the reflexivity required for preorders or partial orders on the entire set, necessitating supplementary conditions for such integrations.^[16]

Connection to Preorders and Partial Orders

A partial equivalence relation (PER) on a set can be derived from a preorder by extracting its symmetric component. Specifically, given a preorder \leq on a set X, define the relation \sim by x \sim y if and only if x \leq y and y \leq x; this \sim is symmetric and transitive, and due to the reflexivity of the preorder, x \sim x holds for all x \in X, making \sim an equivalence relation on the entire set. This construction highlights how equivalence relations capture the "equivalence-like" behavior inherent in the mutual comparability within preorders, while the preorder itself may exhibit asymmetry outside these pairs. The connection extends to partial orders by considering the relaxation of antisymmetry. A partial order is an antisymmetric preorder, so its symmetric closure—defined analogously as above—yields the equality relation on the entire set, which is a total equivalence relation rather than a proper PER. However, if antisymmetry is relaxed to form a general preorder, the resulting symmetric part becomes a non-trivial equivalence relation on the entire set. Furthermore, given such a preorder \leq and its induced equivalence relation \sim, the quotient set X / \sim inherits a well-defined partial order via \leq if and only if x \leq y for representatives x, y; this induced relation is antisymmetric because any symmetry in the quotient would contradict the preorder's structure modulo \sim.^[17] In category theory, PERs arise as certain symmetric relations or profunctors in relational categories like Rel, where a morphism from A to B is a subset of A \times B satisfying symmetry and transitivity when A = B. More abstractly, in bicategories such as the bicategory of relations PERel, objects are sets and morphisms are PERs on disjoint unions, with composition defined by the minimal PER extending the relational composition; this structure models partial maps and equivalences in a way that aligns with realizability and domain-theoretic semantics. Unlike full preorders, which permit asymmetric relations and thus directedness without reciprocity, PERs enforce symmetry, restricting them to undirected equivalence clusters within potentially larger ordered structures.

Examples

Kernels of Partial Functions

A partial equivalence relation can arise as the kernel of a partial function f: X \rightrightarrows Y between sets, defined by the relation \sim_f on X where x \sim_f y if and only if both x and y are in the domain of f (denoted f(x) \downarrow and f(y) \downarrow) and f(x) = f(y). Formally,

x \sim_f y \iff f(x) \downarrow \land f(y) \downarrow \land f(x) = f(y).

This relation holds only on the domain \operatorname{dom}(f) = \{x \in X \mid f(x) \downarrow\}, making \sim_f partial in the sense that it is undefined or non-reflexive outside this subset.^[18] The kernel \sim_f is a partial equivalence relation because it satisfies symmetry and transitivity on \operatorname{dom}(f). For symmetry, if x \sim_f y, then f(x) = f(y) with both defined, so y \sim_f x follows from the symmetry of equality. For transitivity, if x \sim_f y and y \sim_f z, then f(x) = f(y) = f(z) with all defined, so x \sim_f z by transitivity of equality. Reflexivity holds on \operatorname{dom}(f) since f(x) = f(x) whenever f(x) \downarrow. Thus, \sim_f restricts to an equivalence relation on \operatorname{dom}(f).^[18] Consider a partial function f: \mathbb{N} \rightrightarrows \mathbb{R} defined only on odd natural numbers, where f(2k+1) = \sqrt{2k+1} for k \in \mathbb{N}. The kernel \sim_f equates distinct odds $2k+1 \sim_f 2m+1 if \sqrt{2k+1} = \sqrt{2m+1}, which occurs only if k = m, so each odd is in its own class; evens are unrelated to anything, including themselves. This illustrates how the kernel partitions the domain into singleton classes based on distinct images, while leaving the complement unrelated.^[19] In general, every partial equivalence relation \sim on X is the kernel of its quotient map q: X \rightrightarrows X/{\sim}, where the codomain is the set of equivalence classes on \operatorname{dom}(\sim) = \{x \in X \mid x \sim x\}, and q(x) = (the class of x) if x \in \operatorname{dom}(\sim), undefined otherwise. Then x \sim y if and only if both are defined under q and q(x) = q(y). This construction shows that partial equivalence relations are precisely the kernels of partial functions to quotient sets.^[19]

Functions Respecting Equivalence Relations

A partial equivalence relation can be constructed from an existing equivalence relation on a set by incorporating the kernel of a partial function. Specifically, let X be a set equipped with an equivalence relation \sim, and let g: X \rightharpoonup Z be a partial function to another set Z. Define the relation \sim' on X by x \sim' y if and only if x \sim y, both x and y are in the domain of g, and g(x) = g(y).^[20] This relation \sim' is the intersection of \sim with the kernel of g, where the kernel \ker g consists of pairs (x, y) such that g is defined at both and g(x) = g(y).^[20] Since the intersection of an equivalence relation with another equivalence relation (or partial equivalence relation in the case of \ker g) yields a partial equivalence relation, \sim' satisfies symmetry and transitivity, with reflexivity holding on its domain (the intersection of X with \dom g \times \dom g). The partial equivalence relation \sim' refines the original equivalence \sim restricted to the domain of g, meaning \sim' \subseteq \sim \cap (\dom g \times \dom g), resulting in a finer partition of that subdomain. If g respects \sim—that is, x \sim y implies g(x) = g(y) whenever both are defined—then \ker g \supseteq \sim, so \sim' coincides with the restriction of \sim to \dom g. Otherwise, \sim' properly refines \sim by imposing the additional condition from g, splitting some equivalence classes of \sim. This construction allows for modular refinement of partitions while preserving compatibility with the underlying structure of \sim. In group theory, consider the coset equivalence \sim on a group G induced by a subgroup H \leq G, where x \sim y if and only if x^{-1}y \in H (i.e., y \in xH). A group homomorphism g: G \to Z (possibly partial) can be used to define a finer partial equivalence relation \sim' via the above construction, intersecting \sim with \ker g. Homomorphisms that respect \sim—meaning g is constant on cosets of H and thus factors through the quotient G/H—yield \sim' equivalent to the coset relation restricted to \dom g. This approach refines the coset partition, for instance, when g identifies elements within cosets based on additional homomorphic images, useful in studying quotient structures and normal subgroups. Unlike the standalone kernel of a partial function, which induces a partial equivalence relation solely from equality in the codomain (effectively refining the equality relation on the domain), this construction builds upon a pre-existing equivalence \sim rather than starting from equality alone.^[20]

Equality of IEEE Floating Point Values

In IEEE 754 floating-point arithmetic, the equality operator (=) defines a partial equivalence relation on the set of representable floating-point values, where Not a Number (NaN) values introduce partiality by failing to satisfy reflexivity.^[21] Specifically, every NaN compares as unordered (and thus unequal) to every value, including itself, such that NaN = NaN evaluates to false, while comparisons involving NaNs and other values also yield false for equality.^[21] The domain of this partial equivalence relation excludes NaNs and consists of all finite floating-point numbers along with positive and negative infinity (±∞), on which the equality operator behaves as a standard equivalence relation.^[21] Within this domain, equality is reflexive (x = x holds for all x), symmetric (if x = y then y = x), and transitive (if x = y and y = z then x = z), mirroring the properties of equality in the real numbers but adapted to the discrete floating-point representation.^[21] However, the presence of NaNs outside the domain renders the relation partial overall, as not every pair of floating-point values is comparable under equality. For example, the equality 1.0 = 1.0 returns true, placing both representations in the same equivalence class, whereas NaN = NaN returns false, excluding NaNs from any equivalence class.^[21] Equivalence classes within the domain are thus formed by values that compare equal, such as +0 and -0, which are considered identical under IEEE 754 equality despite their differing signs.^[21] This design for handling NaNs was introduced in the original IEEE 754-1985 standard to represent results of undefined or exceptional operations—such as division by zero or square root of a negative number—without causing program termination or requiring explicit error checking in every arithmetic operation.^[21] The standard's rationale emphasized propagating such exceptions through computations while allowing orderly comparisons, thereby supporting robust numerical software in computing systems.^[21]

Applications

In Set Theory and Logic

In set theory, partial equivalence relations (PERs) provide a framework for modeling extensional quotients in ill-founded sets and hypersets, particularly under Aczel's anti-foundation axiom (AFA), which posits that every set graph admits a unique decoration.^[22] This axiom, introduced in 1988, allows the construction of non-well-founded sets by equating structures via bisimulation, where a PER captures the largest such equivalence relation on transition systems or set graphs, enabling the representation of infinite descending membership chains without violating other ZF axioms.^[23] In logic, PERs serve as models for partial inductive definitions and feature prominently in realizability semantics, originating from Kreisel's work in the 1950s and developed through his modified realizability interpretations in the 1960s and 1970s.^[24] These semantics interpret intuitionistic logic and type theory by associating proofs with realizers in a partial computable functional, where a PER on the set of natural numbers or terms defines equivalence classes of realizers that validate the same propositions, accommodating partiality in non-constructive proofs.^[25] For instance, in ZF set theory without the axiom of foundation, PERs define equivalence up to bisimulation for infinite structures, such as hypersets representing cyclic or infinitely branching graphs, by quotienting the universe under the largest bisimulation relation, which aligns set membership with structural isomorphism. PERs also connect to Scott's domain theory, where they classify continuous functions between domains by modeling the logical relations that preserve approximations in cpos (complete partial orders), facilitating the semantics of recursive and higher-order functions in a denotational framework.^[26] A distinctive aspect of PERs is their allowance for partial membership in equivalence classes, where elements may lack a relation to themselves or others, which is crucial for constructing non-well-founded models that capture self-referential or infinite processes without requiring total reflexivity.^[23]

In Computer Science and Programming

In type theory and proof assistants such as Coq and Agda, partial equivalence relations (PERs) are employed to model setoids, which consist of a carrier type and a PER representing computational equality. This framework enables the construction of quotient types where equality proofs may be partial, accommodating undefined or unprovable equalities without requiring full reflexivity. For instance, setoids allow heterogeneous equality to be handled via coercion mechanisms, facilitating modular reasoning in constructive mathematics.^[27]^[28] PERs play a key role in univalent foundations, as developed by Vladimir Voevodsky in the 2010s, where they support the definition of quotients and higher inductive types in proof assistants. By interpreting types as PERs on terms, this approach aligns intensional type theory with homotopy theory, enabling equivalences between types to be treated computationally. In systems like Coq, PER-based setoids are used for partial proofs in quotient constructions, bridging classical univalence with constructive verification.^[15] In algorithms, union-find data structures often model partitions via PERs, supporting partial unions that leave undefined elements isolated. For example, in proof-producing union-find implementations, the structure maintains a partial equivalence where elements not yet unioned remain unrelated, ensuring transitivity and symmetry only on the defined domain. This partiality aids in verifying amortized complexity and correctness in concurrent or incremental settings.^[29] In programming, PERs handle partial data for approximate or error-tolerant equality comparisons, such as in fuzzy matching algorithms where incomplete inputs yield undefined relations. The equality operator on IEEE 754 floating-point types exemplifies a PER, as NaN values are not reflexive (NaN ≠ NaN), allowing symmetric and transitive comparisons while excluding invalid cases. Similarly, in databases, NULL values in relational joins invoke three-valued logic, where equality with NULL is undefined, modeling a partial relation that avoids false equivalences in queries.^[30]^[31]^[32] Computing the transitive closure to extend a symmetric relation into a PER can be achieved using Warshall's algorithm adapted for partial domains, running in O(n³) time on n elements by iteratively propagating relations through intermediate vertices while respecting undefined pairs. This method ensures the resulting PER is minimal and efficient for dense representations in software implementations.^[33]

References

[1]
partial equivalence relation in nLab
Mar 26, 2025 · A partial equivalence relation (sometimes abbreviated PER) is a binary relation satisfying the symmetry and transitivity conditions of an equivalence relation.
[2]
[PDF] Proof-Relevant Partial Equivalence Relations - Sam Speight
Jun 18, 2024 · A partial equivalence relation (PER) is an homogeneous binary relation that is symmetric and transitive. PERs are important in semantics of type ...
[3]
The pro-PER meaning of "proper" - Lysxia's blog
Apr 7, 2022 · In a partial equivalence relation, some elements are not related to any element, not even themselves. Formally, we simply drop the reflexivity ...<|control11|><|separator|>
[4]
Nuprl Basics - Types: Ontic, Semantic, and Intensional
The general semantic form we adopt for types is to associate with each type expression a so-called partial equivalence relation, i.e. a symmetric transitive ...
[5]
[PDF] A Type Theory with Partial Equivalence Relations as Types - l'IRIF
Allen gave a semantics of CTT where a type is a Partial Equivalence Relation (PER) on closed terms [1], which is connected to Russell's original definition of a ...
[6]
Categories of partial equivalence relations as localizations
If ρ ∈ A ( A × A ) satisfies (sym) and (trans), we call it a partial equivalence relation. If ...
[7]
[PDF] The Algebra of Partial Equivalence Relations - Radboud Repository
Keywords: PROP, distributive law, string diagram, partial equivalence relation, Frobenius algebra ... Definition 5.2 The PROP PFr is defined as PMn + PMnop ...
[8]
Partial equivalence relation - Wikipedia - Index of /
Jul 15, 2018 · Every partial equivalence relation is a difunctional relation, but the converse does not hold. ... f\approx f means that f induces a well-defined ...
[9]
[PDF] Constructing Variants of the Category of Partial Equivalence Relations
Oct 28, 2014 · Much of the application of this category is in providing semantics for programming languages, especially for polymorphism. [1], where there is ...
[10]
partial equivalence relation in nLab
### Formal Definition of Partial Equivalence Relation
[11]
https://doi.org/10.1016/j.entcs.2016.09.046
[12]
[PDF] Deciding 𝛽𝜂-Equivalence for Product and Function Types
A symmetric and transitive binary relation is called a partial equivalence relation (per). Note that a per is an equivalence relation on its domain, for if ...
[13]
[PDF] On being the “same” or “different”: Introduction to Apartness
Aug 7, 2014 · A partial equivalence relation (PER) is any binary relation, E, with the following properties. In fact, there is some redundancy in this ...
[14]
[PDF] Categories of partial equivalence relations as localizations - arXiv
Apr 19, 2022 · Notation and Terminology 3.2 (a) If ρ ∈ A(A × A) satisfies (sym) and (trans), we call it a partial equivalence relation. If f : A → B ...
[15]
[PDF] Quotient Types in Type Theory
In this case if we simply define a quotient by replacing the underlying partial equivalence relation with a new one R, undefined ele- ments in the base ...
[16]
[1111.1390] On extension of partial orders to total preorders ... - arXiv
Nov 6, 2011 · For a partial order \preceq on a set X and an equivalency relation S defined on the same set X we derive a necessary and sufficient condition ...
[17]
The classification of preordered spaces in terms of monotones
Aug 25, 2022 · Notice, a preorder \preceq is a partial order on the quotient set X/\mathord {\sim } = \{[x]|x\in X\}, consisting of all equivalence classes ...
[18]
https://doi.org/10.1016/j.jlamp.2015.10.006
[19]
[PDF] Slightly Infinite Sets - mimuw
Nov 30, 2018 · Define the kernel of f to be the partial equivalence relation on An which identifies two tuples if they are both in the domain of f and have ...<|control11|><|separator|>
[20]
Kernels, in a nutshell - ScienceDirect.com
... as an equivalence relation on the source of a partial function: Definition 5. The kernel ker f ⊆ A × A of a partial function f : A B is the set of pairs.
[21]
[PDF] An Enactivist-Inspired Mathematical Model of Cognition - arXiv
Jun 10, 2022 · An equivalence relation E is a refinement of equivalence relation E , if. E ⊆ E , also denoted E ≤r E. A labeling function h is a ...
[22]
Mappings and equivalence
Not all equivalence relations in a group correspond to homomorphisms. ... respect to a homomorphism. Homomorphic images of ... coset cosets. There is still another ...
[23]
[PDF] NON-WELL-FOUNDED SETS - Les-Mathematiques.net
Of course we must relinquish the foundation axiom, but it will turn out that we need drop none of the other axioms of set theory. 1.3 Example: Consider the apg.
[24]
Non-wellfounded Set Theory - Stanford Encyclopedia of Philosophy
Apr 16, 2008 · Non-wellfounded set refers to sets which contain themselves as members, and more generally which are part of an infinite sequence of sets.
[25]
[PDF] Computational interpretation of proofs: An introduction to realizability
Apr 9, 2014 · 3 Kreisel's modified realizability. 4 Negative translations from LK ... Definition of the realizability relation n A n = Gödel code of a ...<|separator|>
[26]
[PDF] Notes on realizability | Andrej Bauer
Feb 21, 2025 · 3 Realizability categories. 50. 6: A partial equivalence relation is a transitive symmetric relation. Because every 𝑥 is realized by ...
[27]
[PDF] Equilogical Spaces - Mathematics and Computation
Mar 2, 2001 · x ≈D y =⇒ f(x) ≈E g(y) . We say that a partial equivalence relation ≈D on a domain D is dense when its domain dom(≈D) = ...
[28]
[PDF] Setoids in type theory
A partial setoid consists of a type T (the carrier), a binary relation R on T (the book equality) and a proof that R is a partial equivalence relation over T.
[29]
[PDF] A Type Theory with Partial Equivalence Relations as ... - Vincent Rahli
... Partial Equivalence Relation (PER) on closed terms [1], which is connected to Russell's original definition of a type as “the range of significance of a ...
[30]
[PDF] Verifying the Correctness and Amortized Complexity of a Union-Find ...
... partial equivalence relation E in- stead of a domain D and a total function R. Indeed, every function except find can be given a useful specification in ...
[31]
Understanding Partial Equivalence in Rust's Floating-Point Types
Sep 30, 2024 · PartialEq: Allows for partial comparison where equivalence might not always hold. This trait is used by types like f32 and f64, where ...
[32]
Exclude some types (eg floating point types) from Smithy's sets #1072
Feb 1, 2022 · The EQ relation included in the IEEE standard is explicitly noted as a partial equivalence relation. It is not reflexive as there does not exist ...
[33]
[PDF] Database Relations with Null Values - UCLA Computer Science
Null values in database relations, represented by “-”, denote that no information exists on that attribute, acting as a place holder for nonexistent or unknown ...
[34]
Computing the closure of a relation: Floyd-Warshall Algorithm
Initial relation: · Find all transitivity relation that uses a node b as intermediary: We look for: Every possible combination (x ⇒ b) (b ⇒ z) · Repeat: for node ...