Dan R. Ghica ; Koko Muroya ; Todd Waugh Ambridge - A robust graph-based approach to observational equivalence

lmcs:8524 - Logical Methods in Computer Science, April 24, 2025, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:8)2025
A robust graph-based approach to observational equivalenceArticle

Authors: Dan R. Ghica ; Koko Muroya ; Todd Waugh Ambridge

    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 (higher-order) state.


    Volume: Volume 21, Issue 2
    Published on: April 24, 2025
    Accepted on: February 18, 2025
    Submitted on: September 27, 2021
    Keywords: Computer Science - Programming Languages,F.3.2

    Consultation statistics

    This page has been seen 333 times.
    This article's PDF has been downloaded 137 times.