3
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ Have you checked Wikipedia? How about the lecture notes? They should define all terms used. $\endgroup$ – Yuval Filmus Jan 19 at 20:30
2
$\begingroup$

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

$\endgroup$
6
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.