Functions with local state: regularity and undecidability

Journal article

We study programs of a finitary ML-like language RML_f with ground-type references. RML_f permits the use of functions with locally declared variables that remain private and persist from one use of the function to the next. Using game semantics we show that this leads to undecidability of program equivalence already at second order. We also examine the extent to which this feature can be captured by regular languages. This gives a decidability result for a second-order fragment RML_f^- of RML_f, which comprises many examples studied in the literature.

Authors: Murawski, A

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Theoretical Computer Science
• Volume: 338
• Issue: 1-3
• Pages: 315–349
• Publication date: 2005-06-01
• Edition: Publisher's version
• DOI: 10.1016/j.tcs.2004.12.036
• ISSN: 0304-3975
• Language: English
• Keywords: game semantics; software verification; automata; model checking
• Subjects: Game semantics; Theory and automated verification