Congruence Closure

This is a summary of how to compute congruence closure. I implemented the algorithm to compute congruence closure and thought I’d never forget it. But my memory starts to get blurry just after two days. So I figured I’d put things down so I don’t have to watch the entire lecture again the next time I need it.

Equivalence Relation

Equivalence relation has three properties: reflexive, symmetric, and transitive. (E.g. \(\geq\) is not an equivalence relation because it break the symmetric property. \(4 \geq 6\) does not imply that \(6 \geq 4\). For example, a binary relation $R$ over a set $S$ meeting these three properties can be expressed as:

• Reflexive: $\forall s \in S.\ sRs$
• Symmetric : $\forall s_1, s_2 \in S.\ s_1 R s_2 \rightarrow s_2 R s_1$
• Transitive: $\forall s_1, s_2, s_3 \in S.\ s_1 R s_2 \land s_2 R s_3 \rightarrow s_1 Rs_3$

Congruence Relation

Given a set $S$ equipped with functions $F = {f_1, …, f_n}$, a relation $R$ over $S$ is a congruence relation if $R$ is an equivalence relation and for every $n$‘ary function $f \in F$ we have:

\[\forall \overset{\rightarrow}{s}, \overset{\rightarrow}{t}.\ \bigwedge\limits_{i=1}^{n}s_i R t_i \rightarrow f(\overset{\rightarrow}{s}) R f(\overset{\rightarrow}{t})\]

A counter example would...