Damien Pous ; Jurriaan Rot - Companions, Causality and Codensity

lmcs:4166 - Logical Methods in Computer Science, August 8, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:14)2019
Companions, Causality and CodensityArticle

Authors: Damien Pous ; Jurriaan Rot

    In the context of abstract coinduction in complete lattices, the notion of compatible function makes it possible to introduce enhancements of the coinduction proof principle. The largest compatible function, called the companion, subsumes most enhancements and has been proved to enjoy many good properties. Here we move to universal coalgebra, where the corresponding notion is that of a final distributive law. We show that when it exists, the final distributive law is a monad, and that it coincides with the codensity monad of the final sequence of the given functor. On sets, we moreover characterise this codensity monad using a new abstract notion of causality. In particular, we recover the fact that on streams, the functions definable by a distributive law or GSOS specification are precisely the causal functions. Going back to enhancements of the coinductive proof principle, we finally obtain that any causal function gives rise to a valid up-to-context technique.


    Volume: Volume 15, Issue 3
    Published on: August 8, 2019
    Accepted on: June 18, 2019
    Submitted on: December 25, 2017
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Coinduction for Verification and Certification; Funder: European Commission; Code: 678157
    • Community of mathematics and fundamental computer science in Lyon; Funder: French National Research Agency (ANR); Code: ANR-10-LABX-0070
    • PROJET AVENIR LYON SAINT-ETIENNE; Funder: French National Research Agency (ANR); Code: ANR-11-IDEX-0007
    • Quantum Computation, Logic, and Security; Funder: European Commission; Code: 320571

    1 Document citing this article

    Consultation statistics

    This page has been seen 1772 times.
    This article's PDF has been downloaded 455 times.