Search code examples
coq

Equivalence but not congruence

All

I'm working on sf/plf chapter Equiv. There is an exercise

We've shown that the [cequiv] relation is both an equivalence and a congruence on commands. Can you think of a relation on commands that is an equivalence but not a congruence?

I do not quite understand the difference between equivalence and congruence. It seems both behavioral equivalence of a program. Can any one explain more about this?

Thanks

Solution

  • There are other equivalences than "behavioral equivalence". An equivalence is any relation which is reflexive, symmetric and transitive. A congruence is a structure-preserving equivalence.

    A common example for an equivalence which is a congruence is arithmetic modulo n. Equality say modulo 10 is an equivalence relation which preserves addition and multiplication, so it is a congruence for the integer ring arithmetic. But it is not a congruence e.g. for "round to 0 integer division". E.g. 23/11=2 but 3/1=3, that is 23 mod 10 = 3 mod 10 and 11 mod 10 = 1 mod 10, but 23/11 mod 10 <> 3/1 mod 10.