Ali K. Caires-Santos ; Maribel Fernández ; Daniele Nantes-Sobrinho - Strong Nominal Semantics for Fixed-Point Constraints

entics:14777 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14777
Strong Nominal Semantics for Fixed-Point ConstraintsArticle

Authors: Ali K. Caires-Santos ; Maribel Fernández ; Daniele Nantes-Sobrinho

    Nominal algebra includes $\alpha$-equality and freshness constraints on nominal terms endowed with a nominal set semantics that facilitates reasoning about languages with binders. Nominal unification is decidable and unitary, however, its extension with equational axioms such as Commutativity (which has a finitary first-order unification type) is no longer finitary unless permutation fixed-point constraints are used. In this paper, we extend the notion of nominal algebra by introducing fixed-point constraints and provide a sound semantics using strong nominal sets. We show, by providing a counter-example, that the class of nominal sets is not a sound denotation for this extended nominal algebra. To recover soundness we propose two different formulations of nominal algebra, one obtained by restricting to a class of fixed-point contexts that are in direct correspondence with freshness contexts and another obtained by using a different set of derivation rules.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 18, 2024
    Submitted on: November 15, 2024
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 31 times.
    This article's PDF has been downloaded 8 times.