Fragments of ML decidable by nested data class memory automata

DOI10.1007/978-3-662-46678-0_16MaRDI QIDQ2949443zbMATH OpenOpenAlexFDO

Authors

Publication date 1 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1501.04511

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55)

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.

Recommendations

• A fragment of ML decidable by visibly pushdown automata
• ML and extended branching VASS
• Functions with local state: regularity and undecidability
• Algorithmic games for full ground references
• Algorithmic games for full ground references

Cited in

(9)

• Algorithmic games for full ground references
• Leafy automata for higher-order concurrency
• Block structure vs scope extrusion: between innocence and omniscience
• ML and extended branching VASS
• A fragment of ML decidable by visibly pushdown automata
• Algorithmic games for full ground references
• Functions with local state: regularity and undecidability
• Saturating automata for game semantics
• Contextual equivalence for state and control via nested data

This page was built for publication: Fragments of ML decidable by nested data class memory automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2949443)