Operational and Semantic Equivalence Between Recursive Programs
Jean-Claude Raoult, Jean E. Vuillemin · Journal of the ACM · 1980
It IS shown that two widely different notions of program equivalence coincide for the language of recurslve definitions with simplification rules The first is the now classical equivalence for fixed-point semantics.The other is purely operational in nature and is much closer to a programmer's intuition of program equivalence KEY WORDS AND PHgASES semantics of programming languages, algebraic semantics, subtree replacement systems CR CATEGORIES: 4 2, 5 2, 5 24