Contextual Equivalence for State and Control via Nested Data
Article No.: 19, Pages 1 - 14
Abstract
We consider contextual equivalence in an ML-like language, where contexts have access to both general references and continuations. We show that in a finitary setting, i.e. when the base types are finite and there is no recursion, the problem is decidable for all programs with first-order references and continuations, assuming they have continuation- and reference-free interfaces. This is the best one can hope for in this case, because the addition of references to functions, to continuations or to references makes the problem undecidable.
The result is notable since, unlike earlier work in the area, we need not impose any restrictions on type-theoretic order or the use of first-order references inside terms. In particular, the programs concerned can generate unbounded heaps.
Our decidability argument relies on recasting the corresponding fully abstract trace semantics of terms as instances of automata with a decidable equivalence problem. The automata used for this purpose belong to the family of automata over infinite alphabets (aka data automata), where the infinite alphabet (dataset) has the shape of a forest.
References
[1]
Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent representation independence. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 340--353.
[2]
Henrik Björklund and Mikołaj Bojańczyk. 2007. Shuffle Expressions and Words with Nested Data. In Proceedings of MFCS (Lecture Notes in Computer Science, Vol. 4708). Springer, 750--761.
[3]
Henrik Björklund and Thomas Schwentick. 2010. On notions of regularity for data languages. Theor. Comput. Sci. 411, 4-5 (2010), 702--715.
[4]
Benedict Bunting and Andrzej S. Murawski. 2023. Operational Algorithmic Game Semantics. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1--13.
[5]
Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, and C.-H. Luke Ong. 2015. Fragments of ML Decidable by Nested Data Class Memory Automata. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science, Vol. 9034), Andrew M. Pitts (Ed.). Springer, 249--263.
[6]
Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong. 2015. Weak and Nested Class Memory Automata. In Language and Automata Theory and Applications. Springer International Publishing, 188--199.
[7]
Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong. 2019. ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States. ACM Trans. Program. Lang. Syst. 41, 2 (2019), 11:1--11:38.
[8]
Normann Decker, Peter Habermehl, Martin Leucker, and Daniel Thoma. 2014. Ordered Navigation on Multi-attributed Data Words. In Proceedings of CONCUR (Lecture Notes in Computer Science, Vol. 8704), Paolo Baldan and Daniele Gorla (Eds.). Springer, 497--511.
[9]
Derek Dreyer, Georg Neis, and Lars Birkedal. 2012. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22, 4-5 (2012), 477--528.
[10]
Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 1-2 (2001), 63--92.
[11]
Daniel Hirschkoff, GuilhemJaber, and Enguerrand Prebet. 2023. Deciding Contextual Equivalence of v-Calculus with Effectful Contexts. In Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 13992), Orna Kupferman and Paweł Sobociński (Eds.). Springer, 24--45.
[12]
Martin Hyland and C.-H. Luke Ong. 2000. On Full Abstraction for PCF: I, II, and III. Inf. Comput. 163, 2 (2000), 285--408.
[13]
Guilhem Jaber. 2019. SyTeCi: automating contextual equivalence for higher-order programs with references. Proceedings of the ACM on Programming Languages 4, POPL (dec 2019), 1--28.
[14]
Guilhem Jaber and Andrzej S. Murawski. 2021. Complete trace models of state and control. In Proceedings of ESOP. Springer International Publishing, 348--374.
[15]
Guilhem Jaber and Andrzej S. Murawski. 2021. Complete trace models of state and control (full version). (Jan. 2021). https://hal.science/hal-03116698 Preprint.
[16]
Guilhem Jaber and Andrzej S. Murawski. 2021. Compositional relational reasoning via operational game semantics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 1--13.
[17]
Neil D. Jones and Steven S. Muchnick. 1978. The Complexity of Finite Memory Programs with Recursion. J. ACM 25, 2 (1978), 312--321.
[18]
Ralph Loader. 1995. Normalisation by Calculation. (1995). https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.8157 Unpublished.
[19]
Ralph Loader. 1998. Notes on simply typed lambda calculus. Technical Report ECS-LFCS-98-381. Laboratory for Foundations of Computer Science, University of Edinburgh. https://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/
[20]
Andrzej S. Murawski. 2003. On Program Equivalence in Languages with Ground-Type References. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings. IEEE Computer Society, 108.
[21]
Andrzej S. Murawski. 2005. Functions with local state: Regularity and undecidability. Theor. Comput. Sci. 338, 1-3 (2005), 315--349.
[22]
Andrzej S. Murawski and Nikos Tzevelekos. 2017. Algorithmic games for full ground references. Formal Methods in System Design 52, 3 (aug 2017), 277--314.
[23]
Andrew M. Pitts and Ian Stark. 1999. Operational Reasoning for Functions with Local State. Cambridge University Press, USA, 227--274.
[24]
Philippe Schnoebelen. 2002. Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83, 5 (2002), 251--261.
[25]
Kristian Støvring and Søren B. Lassen. 2007. A complete, co-inductive syntactic theory of sequential control and state. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, Martin Hofmann and Matthias Felleisen (Eds.). ACM, 161--172.
Recommendations
Two-Way Finite State Transducers with Nested Pebbles
MFCS '02: Proceedings of the 27th International Symposium on Mathematical Foundations of Computer ScienceTwo-way finite state transducers are considered with a fixed number of pebbles, of which the life times are nested. In the deterministic case, the transductions computed by such pebble transducers are closed under composition, and they can be realized ...
Nondeterministic state complexity of nested word automata
We study the nondeterministic state complexity of Boolean operations on regular languages of nested words. For union and intersection we obtain matching upper and lower bounds. For complementation of a nondeterministic nested word automaton with n ...
Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
AbstractFinite transducers, two-tape automata, and biautomata are related computational models descended from the concept of finite-state automaton. In these models an automaton controls two heads that read or write symbols on the tapes in the one-way ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2024
988 pages
ISBN:9798400706608
DOI:10.1145/3661814
- Conference Chair:
- Pawel Sobocinski,
- Program Chairs:
- Ugo Dal Lago,
- Javier Esparza
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
- SIGLOG: ACM Special Interest Group on Logic and Computation
- IEEE Computer Society
In-Cooperation
- EACSL
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 July 2024
Check for updates
Qualifiers
- Research-article
Funding Sources
Conference
LICS '24
Sponsor:
LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science
July 8 - 11, 2024
Tallinn, Estonia
Acceptance Rates
LICS '24 Paper Acceptance Rate 72 of 236 submissions, 31%;
Overall Acceptance Rate 215 of 622 submissions, 35%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 80Total Downloads
- Downloads (Last 12 months)80
- Downloads (Last 6 weeks)30
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in