Clément Aubert ; Jean Krivine - Reversible computations are computations

entics:16677 - Electronic Notes in Theoretical Informatics and Computer Science, December 20, 2025, Volume 5 - Proceedings of MFPS XLI - https://doi.org/10.46298/entics.16677
Reversible computations are computationsArticle

Authors: Clément Aubert ; Jean Krivine

    Causality serves as an abstract notion of time for concurrent systems. A computation is causal, or simply valid, if each observation of a computation event is preceded by the observation of its causes. The present work establishes that this simple requirement is equally relevant when the occurrence of an event is invertible. We propose a conservative extension of causal models for concurrency that accommodates reversible computations. We first model reversible computations using a symmetric residuation operation in the general model of configuration structures. We show that stable configuration structures, which correspond to prime algebraic domains, remain stable under the action of this residuation. We then derive a semantics of reversible computations for prime event structures, which is shown to coincide with a switch operation that dualizes conflict and causality.


    Volume: Volume 5 - Proceedings of MFPS XLI
    Published on: December 20, 2025
    Accepted on: October 15, 2025
    Submitted on: April 3, 2025
    Keywords: Logic in Computer Science, Logic, 68Q85, 03B70, 68N19, F.1.1; F.1.2; F.3.2