2 added 574 characters in body
source | link

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
source | link

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) $$