1
$\begingroup$

An optional exercise from Programming Language Foundations asks

Can you think of a relation on commands that is an equivalence but not a congruence?

An equivalence here refers to an ordinary equivalence relation. A congruence refers to an equivalence relation where the equivalence of two subprograms implies the equivalence of the larger programs in which they are embedded, e.g., if $a_1$ and $a_1'$ are equivalent expressions, then so are $(x ::= a_1)$ and $(x ::= a_1')$.

I am unable to think of an example, although I would think one exists. The context of this exercise has to do with an imperative programming language, but an example in another context is welcomed as well.

Any ideas?

$\endgroup$
1
$\begingroup$

Let $x,y$ be two fixed distinct variable names.

Call $P$ and $Q$ equivalent iff $Q$ is obtained from $P$ by optionally swapping the variable names $x$ and $y$. That is, either $Q=P$ or $Q=P\{x/y,y/x\}$ where the latter uses simultaneous substitution.

It is an equivalence. Reflexivity follows by construction. For symmetry, $P\equiv Q$ swaps if $Q\equiv P$ swaps. For transitivity, we consider the four cases: in the swap-swap case we get the same program back.

It is not a congruence since

$$ x:=x+1 \equiv y:=y+1 \quad \mbox{ but }\quad (x:=0;x:=x+1) \not\equiv (x:=0;y:=y+1) $$


Less formally, you can build many examples as follows. Take $f : \mathbb N \to \mathbb N$ to be a function which does NOT in general satisfy

$$ f(n)=f(m) \implies f(n+1)=f(m+1) $$

Say, $f$ is a hash function.

Then, we can say $P\equiv Q$ whenever $f(\# vars(P))=f(\# vars(Q))$, where $\#vars$ counts the number of variables.

This is an equivalence (trivially), but not a congruence since if we add another fresh variable to both $P,Q$ we increment their variable count by one, but $f$ does not preserve that value in general.

$\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.