# Defining Functions on Equivalence Classes

arXiv: https://arxiv.org/abs/1907.07591 · HTML: https://mlsanity.com/paper/1907.07591/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jul 2019.

## Built on by (most cited first, 1 of 1)

- [SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification](https://mlsanity.com/paper/2609.00728/) (2026)

## Abstract (arXiv)

A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are equivalence classes: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.