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:

A congruence relation must be closed under the equivalence rules,

and the compatibility rules,