What is congruence in lambda-calculus

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.

• Have you checked Wikipedia? How about the lecture notes? They should define all terms used. Jan 19 '21 at 20:30

"Congruence" in the context of lambda calculus is usually "alpha-congruence". "alpha-congruent" means "differring only if at all in the names of bound variables".

For instance, $$\lambda x. x \equiv_\alpha \lambda y.y$$ and $$\lambda xy.x(xy) \equiv_\alpha \lambda yx.y(yx)$$ (bound variables $$x$$ and $$y$$ were swapped), but $$\lambda x.x \not \equiv_\alpha \lambda x.xy$$ (different term structure).

Formally,

$$P[\lambda x.M] \equiv_{1\alpha} P[\lambda y.M[y/x]]$$

where $$P[\lambda x.M]$$ means that $$\lambda x.M$$ is a subterm in $$P$$, $$y$$ is a new variable that does not occur free in $$M$$, and $$M[y/x]$$ is the result of substituting every occurrence of $$x$$ with $$y$$ in $$M$$;

$$P \equiv_\alpha Q \text{ iff } P = P_1 \equiv_{1\alpha} \ldots \equiv_{1\alpha} P_n = Q$$

i.e. $$P$$ is alpha-congruent to $$Q$$ if there is a chain of bound variable renamings from $$P$$ to $$Q$$.

The idea is that alpha-congruent terms "mean" the same, because the choice of names for bound variables does not affect a term's behavior in abstraction and application.

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”.