Using Class Memory Automata in Algorithmic Game Semantics

Automata over infinite alphabets are a powerful extension of traditional automata theory, which have begun to be used in solving problems in verification and databases. The infinite nature of the alphabet allows the automata to model potentially unbounded processes or structures at a higher level of precision than finite alphabet automata. Game semantics provides a powerful framework for ascribing fully abstract semantics to higher-order programs, by modelling programs as strategies for interaction between the program and the environment. Questions about properties of programs can then be reduced to checking properties of these strategies. This thesis aims to continue the classification of the fragments of the higher-order call-by-value language RML for which observational equivalence is decidable. To do so, we will develop new variants of class memory automata that allow us to express and compare languages representing game semantic strategies. We begin our contributions by looking at class memory automata, a natural form of automata over infinite alphabets. We identify a natural restriction – which we call weakness – that leads to better algorithmic and complexity properties. We then admit a tree-structure to the infi- nite alphabets being used, and present a decidable form of class memory automata over these structured inputs. We also introduce and study a form of automaton combining the class memory operation over infinite alphabets with a visibly pushdown stack. Next, we use these form of class memory automata in deciding observational equivalence of RML programs. RML can be viewed as the restricton of Standard ML to ground-type references, with a “bad variable” construct. Using the game semantics of RML, we reduce observational equivalence to equivalence of these variants of class memory automata. These methods provide new results on which fragments of RML have decidable observational equivalence. We also present several new undecidability and results, showing fragments of RML to have an undecidable observational equivalence problem.