Fragments of ML Decidable by Nested Data Class Memory Automata

TL;DR

This paper identifies specific fragments of the RML language where observational equivalence is decidable, using automata over data words with tree-structured data values, and proves undecidability results for higher-order types.

Contribution

It introduces automata-based techniques to decide observational equivalence for certain RML fragments and delineates the boundaries of decidability in higher-order types.

Findings

Decidability of observational equivalence for certain RML fragments.

Automata over data words with tree-structured data values are used for analysis.

Undecidability results for higher-order types beyond certain levels.

Abstract

The call-by-value language RML may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct in the sense of Reynolds. We consider the fragment of (finitary) RML terms of order at most 1 with free variables of order at most 2, and identify two subfragments of this for which we show observational equivalence to be decidable. The first subfragment consists of those terms in which the P-pointers in the game semantic representation are determined by the underlying sequence of moves. The second subfragment consists of terms in which the O-pointers of moves corresponding to free variables in the game semantic representation are determined by the underlying moves. These results are shown using a reduction to a form of automata over data words in which the data values have a tree-structure, reflecting the tree-structure of the threads in the game semantic plays. In addition we show that observational equivalence is undecidable at every third- or higher-order type, every second-order type which takes at least two first-order arguments, and every second-order type (of arity greater than one) that has a first-order argument which is not the final argument.