An approach to deciding the observational equivalence of Algol-like languages

We prove that the observational equivalence of third-order finitary (i.e. recursion-free) Idealized Algol (IA) is decidable using Game Semantics. By modelling the state explicitly in our games, we show that the denotation of a term M of this fragment of IA is a compactly innocent strategy-with-state, i.e. the strategy is generated by a finite view function f_M. Given any such f_M, we construct a real-time deterministic pushdown automaton (DPDA) that recognizes the complete plays of the knowing-strategy denotation of M. Since such plays characterize observational equivalence, and there is an algorithm for deciding whether any two DPDAs recognize the same language, we obtain a procedure for deciding the observational equivalence of third-order finitary IA. Restricted to second-order terms, the DPDA representation cuts down to a deterministic finite automaton; thus our approach gives a new proof of Ghica and McCusker’s regular-expression characterization for this fragment. Our algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of IA and other cognate programming languages. Another result concerns second-order IA with full recursion: we show that observational equivalence for this fragment is undecidable.