Congruence relation

A congruence relation on a language is an equivalence relation that is compatible with the term constructors of that language.

Consider the untyped lambda-calculus:

$e ::= x \mid \lambda x.\, e \mid e_1\ e_2$

A congruence relation $\texttt{}e_1 = e_2$ must be closed under the equivalence rules,

${\; \over e = e} \mbox{refl} \qquad { e_1 = e_2 \over e_2 = e_1 } \mbox{symm} \qquad { e_1 = e_2 \qquad e_2 = e_3 \over e_1 = e_3 } \mbox{trans},$

and the compatibility rules,

${\; \over x = x} \qquad { e_1 = e_2 \over \lambda x.\, e_1 = \lambda x.\, e_2 } \qquad { e_1 = e_1' \qquad e_2 = e_2' \over e_1\ e_2 = e_1'\ e_2' }.$