Quartz 4

GMA25

12 min read

By Prof. Dan Ghica, Koko Muroya, Todd Waugh Ambridge 2024-10-03 Research gate Arxiv

A Robust Graph-Based Approach to Observational Equivalence

Abstract

We propose a new step-wise approach to proving observational equivalence, and in particular reasoning about fragility of observational equivalence. Our approach is based on what we call local reasoning. The local reasoning exploits the graphical concept of neighbourhood, and it extracts a new, formal, concept of robustness as a key sufficient condition of observational equivalence. Moreover, our proof methodology is capable of proving a generalised notion of Observational equivalence. The generalised notion can be quantified over syntactically restricted contexts instead of all contexts, and also quantitatively constrained in terms of the number of reduction steps. The operational machinery we use is given by a hypergraph-rewriting abstract machine inspired by Girard’s Geometry of Interaction. The behaviour of language features, including function abstraction and application, is provided by hypergraph-rewriting rules. We demonstrate our proof methodology using the call-by-value lambda-calculus equipped with (higherorder) state.

Contributions

Develop step-wise method for proving observational equivalence

Motivation

Develop method for reasoning about Fragility of observational equivalence

Challenges

Desiderata

  • general semantical framework with which one can directly analyse fragility, or robustness, of observational equivalence.

New approach

Focused hypernet rewriting

Step-wise and local reasoning centered around robustness. Main contribution is to show how the Graphical concept of neighborhood can be exploited to reason about Observational equivalence.

The focus is a directed edge that ‘passes’ around the hypernet.

Main difference to present state of the art

This uses of hypernets instead of terms

This makes renaming of variables irrelevant.

This uses of the focus instead of evaluation contexts

In conventional reduction semantics, redexes are identified using evaluation contexts. Whenever the focus triggers an update of a Hypernet, its position in the hypernet coincides with where the hole is in an evaluation context.

A new step-wise approach.

This work takes a new Coinductive, Step-wise, approach to proving observational equivalence. We introduce a novel variant of the weak simulation dubbed counting simulation. We demonstrate that, to prove observational equivalence, it suffices to construct a counting simulation that is closed under contexts by definition. This approach is opposite to the known coinductive approach which uses Applicative bisimimilarity; one first constructs an applicative bisimulation and then proves that it is a congruence, typically using Howe’s method How96

Local reasoning

Focussed hypernet rewriting facilitates what we call local reasoning. Our key observation is that, to obtain the counting simulation that is closed under contexts by definition, it suffices to simply trace sub-graphs and analyse their interaction with the focus. The interaction can namely be analysed by inspecting updates that happen around the focus and how these updates can interfere with the sub-graphs of interest. The reasoning principal here is the Graphical concept of neighborhood, or graph locality. The local reasoning is a graph counterpart of analysing interaction between (sub-)terms and contexts using the conventional reduction semantics. In fact, it is not just a counterpart but an enhancement in two directions. Firstly, sub-graphs are more expressive than sub- terms; sub-graphs can represent parts of a program that are not necessarily well-formed. Secondly, the focus can indicate which part of a context is relevant in the interaction between the context and a term, which is not easy to make explicit in the conventional semantics that uses evaluation contexts.

Robustness

Reasoning extracts a formal concept of robustness.

Definitions

Hypernet

Focus

Step-wise

Coinductive

Semantical framework

Applicative bisimimilarity

Applicative bisimulation

Weak simulation

AKA ‘Counting simulation’

Subgraph tracing

Updates

Robustness

Robustness is identified as the key sufficient condition that ensures two sub-graphs that we wish to equate interact with updates of a hypernet, which is triggered by the focus, in the same way; for example, if one sub-graph is duplicated (or discarded), the other is also duplicated (or discarded)

  • Is this related to graph identification (whether an object is a single node in one place or multiple places)?

Introduction

Topics

References: (old)

References

ABM14

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, September 1-3 2014, Gothenburg, Sweden, pages 363–376, 2014.

Abr90

Samson Abramsky. The lazy lambda-calculus, page 65–117. Addison Wesley, 1990.

Abr97

Samson Abramsky. Game semantics for programming languages. In 22nd International Symposium on Mathematical Foundations of Computer Science, MFCS 1997, August 25-29 1997, Bratislava, Slovakia, pages 3–4, 1997.

ADV20

Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The machinery of interaction. In PPDP 2020, pages 4:1–4:15. ACM, 2020.

ADV21

Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The (in)efficiency of interaction. Proc. ACM Program. Lang., 5(POPL):1–33, 2021.

AG09

Beniamino Accattoli and Stefano Guerrini. Jumping boxes. In CSL 2009, volume 5771 of Lect. Notes Comp. Sci., pages 55–70. Springer, 2009.

AGSZ21

Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi. Functorial string diagrams for reverse-mode automatic differentiation. CoRR, abs/2107.13433, 2021.

AGSZ22

Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi. Rewriting for monoidal closed categories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs, pages 29:1–29:20. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik, 2022.

AJM00

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409–470, 2000.

BGK+22a

Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: rewriting with frobenius structure. J. ACM, 69(2):14:1–14:58, 2022.

BGK+22b

Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory II: rewriting with symmetric monoidal structure. Math. Struct. Comput. Sci., 32(4):511–541, 2022.

BGK+22c

Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory III: confluence with and without frobenius. Math. Struct. Comput. Sci., 32(7):829–869, 2022. ###:BPPR17 Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Inf., 54(2):127–190, 2017.

DGL17

Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. Effectful applicative bisimilarity: Monads, relators, and howe’s method. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017. [DHP02] Frank Drewes, Berthold Hoffmann, and Detlef Plump. Hierarchical graph transformation. J. Comput. Syst. Sci., 64(2):249–283, 2002.

DMMZ12

Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. On inter-deriving small-step and big-step semantics: A case study for storeless call-by-need evaluation. Theor. Comput. Sci., 435:21–42, 2012.

DNB12

Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program., 22(4-5):477–528, 2012.

DNRB10

Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. A relational modal logic for higher-order stateful adts. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, pages 185–198, New York, NY, USA, 2010. ACM.

DR96

Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal lambda-machines. Elect. Notes in Theor. Comp. Sci., 3:40–60, 1996.

DTY17

Ugo Dal Lago, Ryo Tanaka, and Akira Yoshimizu. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12, 2017.

Ghi23

Dan R. Ghica. The far side of the cube. In Alessandra Palmigiano and Mehrnoosh Sadrzadeh, editors, Samson Abramsky on Logic and Structure in Computer Science and Beyond, pages 219–250. Springer Verlag, 2023.

Gir87

Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1–102, 1987.

Gir89

Jean-Yves Girard. Geometry of Interaction I: interpretation of system F. In Logic Colloquium 1988, volume 127 of Studies in Logic & Found. Math., pages 221–260. Elsevier, 1989.

GT12

Dan R. Ghica and Nikos Tzevelekos. A system-level game semantics. Electr. Notes Theor. Comput. Sci., 286:191–211, 2012.

Gur18

Yuri Gurevich. Evolving algebras 1993: Lipari guide. arXiv preprint arXiv:1808.06255, 2018.

GZ23

Dan Ghica and Fabio Zanasi. String diagrams for λ-calculi and functional computation. arXiv preprint arXiv:2305.18945, 2023.52 D. R. GHICA, K. MUROYA, AND T. WAUGH AMBRIDGE [HMH14] Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. Memoryful geometry of interaction: from coalgebraic components to algebraic effects. In Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, July 14-18 2014, Vienna, Austria, pages 52:1–52:10, 2014.

HO00

J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285–408, 2000.

How96

Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Inf. Comput., 124(2):103–112, 1996.

JR05

Alan Jeffrey and Julian Rathke. Java jr: Fully abstract trace semantics for a core java language. In 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, April 4-8 2005, Edinburgh, UK, pages 423–438, 2005.

KLS11

Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. From applicative to environmental bisimulation. In Michael W. Mislove and Jo¨el Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 of Electronic Notes in Theoretical Computer Science, pages 215–235. Elsevier, 2011.

Laf90

Yves Lafont. Interaction nets. In 17th Annual ACM Symposium on Principles of Programming Languages, POPL 1990, January 1990, San Francisco, California, USA, pages 95–108, 1990.

Laf95

Yves Lafont. From proof nets to interaction nets, page 225–248. London Mathematical Society Lecture Note Series. Cambridge University Press, 1995.

Mac95

Ian Mackie. The Geometry of Interaction machine. In POPL 1995, pages 198–208. ACM, 1995.

Mac98

Ian Mackie. Linear logic With boxes. In 13th IEEE Symposium on Logic in Computer Science, June 21-24 1998, Indianapolis, IN, USA, pages 309–320, 1998.

MCG18

Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica. The geometry of computation-graph abstraction. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12 2018, pages 749–758, 2018.

Mel06

Paul-Andr´e Melli`es. Functorial boxes in string diagrams. In 20th International Workshop on Computer Science Logic, CSL 2006, 15th Annual Conference of the EACSL, September 25-29 2006, Szeged, Hungary, pages 1–30, 2006.

MG17

Koko Muroya and Dan R. Ghica. The dynamic geometry of interaction machine: A call-by-need graph rewriter. In 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24 2017, Stockholm, Sweden, pages 32:1–32:15, 2017.

MH24

Koko Muroya and Makoto Hamana. Term evaluation systems with refinements: First-order, second-order, and contextual improvement. In Jeremy Gibbons and Dale Miller, editors, Functional and Logic Programming - 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024, Proceedings, volume 14659 of Lecture Notes in Computer Science, pages 31–61. Springer, 2024.

MHH16

Koko Muroya, Naohiko Hoshino, and Ichiro Hasuo. Memoryful geometry of interaction II: re- cursion and adequacy. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22 2016, pages 748–760, 2016.

Mil01

Robin Milner. Bigraphical reactive systems. In International Conference on Concurrency Theory, pages 16–35. Springer, 2001.

MJ69

James Hiram Morris Jr. Lambda-calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, 1969.

MS11

Rasmus Ejlers Møgelberg and Sam Staton. Linearly-used state in models of call-by-value. In 4th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2011, August 30 - September 2 2011, Winchester, UK, pages 298–313, 2011.

MSU24

Koko Muroya, Takahiro Sanada, and Natsuki Urabe. Preorder-constrained simulations for program refinement with effects. In CMCS 2024, 2024. To appear.

Mur20

Koko Muroya. Hypernet Semantics of Programming Languages. PhD thesis, University of Birmingham, 2020.

OP99

Peter W O’Hearn and David J Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.

OT97

Peter O’Hearn and Robert Tennent, editors. Algol-like languages. Progress in theoretical computer science. Birkhauser, 1997.

Pav13

Dusko Pavlovic. Monoidal computer I: Basic computability by string diagrams. Information and Computation, 226:94–116, 2013.

Pit00

Andrew M. Pitts. Operational semantics and program equivalence. In Gilles Barthe, Peter Dybjer, Lu´ıs Pinto, and Jo˜ao Saraiva, editors, Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, volume 2395 of Lecture Notes in Computer Science, pages 378–412. Springer, 2000.

PP08

Gordon D. Plotkin and John Power. Tensors of comodels and models for operational semantics. Electr. Notes Theor. Comput. Sci., 218:295–311, 2008.

Pre15

Matija Pretnar. An introduction to algebraic effects and handlers. invited tutorial paper. Elect. Notes in Theor. Comp. Sci., 319:19–35, 2015.

Rey02

John C Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 55–74. IEEE, 2002.

Roz97

Grzegorz Rozenberg, editor. Handbook of graph grammars and computing by graph transformations, volume 1: foundations. World Scientific, 1997.

San95

David Sands. Total correctness by local improvement in program transformation. In Ron K. Cytron and Peter Lee, editors, Conference Record of POPL’95: 22nd ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 221–232. ACM Press, 1995.

Sin05

Fran¸cois-R´egis Sinot. Call-by-name and call-by-value as token-passing interaction nets. In 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005, April 21-23 2005, Nara, Japan, pages 386–400, 2005.

Sin06

Fran¸cois-R´egis Sinot. Call-by-need in token-passing nets. Mathematical Structures in Computer Science, 16(4):639–666, 2006.

SKS07

Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higherorder languages. In LICS 2007, pages 293–302. IEEE Computer Society, 2007.

Sta85

Richard Statman. Logical relations and the typed lambda-calculus. Information and Control, 65(2/3):85–97, 1985.

SV18

Alex Simpson and Niels F. W. Voorneveld. Behavioural equivalence via modalities for algebraic effects. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 300–326. Springer, 2018.

Wad98

Philip Wadler. The marriage of effects and monads. In ACM SIGPLAN Notices, volume 34:1, pages 63–74. ACM, 1998.

PDF:

Graph View

Backlinks