Algorithmic games for full ground references

We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is [Formula: see text] . At the technical level, our result...

Descripción completa

Detalles Bibliográficos
Autores principales: Murawski, Andrzej S., Tzevelekos, Nikos
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Springer US 2017
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6560680/
https://www.ncbi.nlm.nih.gov/pubmed/31258247
http://dx.doi.org/10.1007/s10703-017-0292-9
_version_ 1783425996144246784
author Murawski, Andrzej S.
Tzevelekos, Nikos
author_facet Murawski, Andrzej S.
Tzevelekos, Nikos
author_sort Murawski, Andrzej S.
collection PubMed
description We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is [Formula: see text] . At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation.
format Online
Article
Text
id pubmed-6560680
institution National Center for Biotechnology Information
language English
publishDate 2017
publisher Springer US
record_format MEDLINE/PubMed
spelling pubmed-65606802019-06-26 Algorithmic games for full ground references Murawski, Andrzej S. Tzevelekos, Nikos Form Methods Syst Des Article We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is [Formula: see text] . At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation. Springer US 2017-08-09 2018 /pmc/articles/PMC6560680/ /pubmed/31258247 http://dx.doi.org/10.1007/s10703-017-0292-9 Text en © The Author(s) 2017 Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
spellingShingle Article
Murawski, Andrzej S.
Tzevelekos, Nikos
Algorithmic games for full ground references
title Algorithmic games for full ground references
title_full Algorithmic games for full ground references
title_fullStr Algorithmic games for full ground references
title_full_unstemmed Algorithmic games for full ground references
title_short Algorithmic games for full ground references
title_sort algorithmic games for full ground references
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6560680/
https://www.ncbi.nlm.nih.gov/pubmed/31258247
http://dx.doi.org/10.1007/s10703-017-0292-9
work_keys_str_mv AT murawskiandrzejs algorithmicgamesforfullgroundreferences
AT tzevelekosnikos algorithmicgamesforfullgroundreferences

Ejemplares similares