HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

What is congruence in lambda-calculus

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
lambdacongruencewhatcalculus

Problem

I see a lot of lecture notes where they use the term "congruence" (ex: congruence relation) or deriving usages such as "the expression e is alpha-congruent to e2".

Could someone please explain what congurence means exactly in this context and give some examples to a noob without much knowledge about math/lambda-calculus.

Thanks in advance

Solution

Generally speaking, in algebra, a congruence relation is an equivalence relation such that operations on equivalent objects yield equivalent objects. In the lambda calculus, a congruence is an equivalence relation such that constructing terms from equivalent terms yields equivalent terms: if $M \equiv M'$ and $N \equiv N'$ then $M\,N \equiv M\,N'$, and if $M \equiv M'$ then $\lambda x.M \equiv \lambda x.M'$.

“Alpha congruence” is another name for alpha equivalence, which is the relation such that two terms are alpha-equivalent if they are, intuitively speaking, the same except for renaming internal variables. Since this is not only an equivalence but even a congruence, it's called both “alpha equivalence” and “alpha congruence”.

Context

StackExchange Computer Science Q#134577, answer score: 6

Revisions (0)

No revisions yet.