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 |
Externally published | Yes |
All Science Journal Classification (ASJC) codes
- Software
- Artificial Intelligence
- Information Systems
- Control and Systems Engineering
- Hardware and Architecture
Keywords
- common subexpresslon
- congruence closure
- decision procedure
- expression equivalence
- graph algorithm
- lossless join
- relational database
- theory of equality
- unification
- uniform word problem