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