About the undecidability of program equivalence in finitary languages with state
Andrzej S. Murawski · ACM Transactions on Computational Logic · 2005
We show how game semantics can be employed to prove that program equivalence in finitary Idealized Algol with active expressions is undecidable. We also investigate a notion of representability of languages by terms and show that finitary Idealized Algol terms of respectively second, third and higher orders define exactly regular, context-free and recursively enumerable languages.