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