2 added 574 characters in body edited Oct 21 '18 at 8:23 chi 13.2k2121 silver badges3333 bronze badges 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. 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)$$ 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. 1 answered Oct 21 '18 at 8:13 chi 13.2k2121 silver badges3333 bronze badges 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)$$