Abstract
Let G be a directed graph such that for each vertex v in G, the successors of v are ordered Let C be any equivalence relation on the vertices of G. The congruence closure C* of C is the finest equivalence relation containing C and such that any two vertices having corresponding successors equivalent under C* are themselves equivalent under C* Efficient algorithms are described for computing congruence closures in the general case and in the following two special cases. 0) G under C* is acyclic, and (it) G is acychc and C identifies a single pair of vertices. The use of these algorithms to test expression eqmvalence (a problem central to program verification) and to test losslessness of joins in relational databases is described.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 758-771 |
| Number of pages | 14 |
| Journal | Journal of the ACM (JACM) |
| Volume | 27 |
| Issue number | 4 |
| DOIs | |
| State | Published - Oct 1 1980 |
Keywords
- common subexpresslon
- congruence closure
- decision procedure
- expression equivalence
- graph algorithm
- lossless join
- relational database
- theory of equality
- unification
- uniform word problem
ASJC Scopus subject areas
- Software
- Control and Systems Engineering
- Information Systems
- Hardware and Architecture
- Artificial Intelligence