Congruence relation

From The Twelf Project

Jump to: navigation, search

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' }.

Retrieved from "http://twelf.org/wiki/Congruence_relation"
Personal tools