On program equivalence in Idealized Algol

Andrzej Murawski

Game semantics has recently been used to relate second- and third-order fragments of Idealized Algol (IA) with respectively regular and deterministic context-free languages, leading to procedures for verifying program equivalences at these orders.

In this talk we employ strategies induced by IA terms to represent various language classes. It turns out that any recursively enumerable language can be represented at fourth order, which implies that program equivalence at that order is not decidable.