One of the fundamental questions in programming languages is the following:
Given two programs, when are they equal/the same/equivalent?
This is a question of great importance, as we often want to know when we can swap one program by another (e.g. an optimized version).
A notion of program equivalence may arise from a semantics of that language, whether that is operational or denotational. However, that need not be the case: a direct definition of an equivalence may be possible.
Depending on the programming paradigm in use, and the particular programming language in question, the notion of program equivalence may differ. However, most program equivalences are expected to be at a minimum equivalence relations.
Additionally, they are sometimes expected to be congruences, or compatible relations. This means that they preserve constructs of the language. For example, in a language of natural numbers and addition, we would expect that if then . In this way we can reason about parts of a program separately, and then integrate them in larger calculations. This may not be the case in highly intensional languages.
Common notions of program equivalence include: