Showing that an equivalence relation on programs need not be a congruence

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?

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.

StackExchange Computer Science Q#98866, answer score: 2