Strong Nominal Semantics for Fixed-Point Constraints
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929634549956608 |
|---|---|
| author | Caires-Santos, Ali K. Fernández, Maribel Nantes-Sobrinho, Daniele |
| author_facet | Caires-Santos, Ali K. Fernández, Maribel Nantes-Sobrinho, Daniele |
| contents | Nominal algebra includes $α$-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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_14253 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Strong Nominal Semantics for Fixed-Point Constraints Caires-Santos, Ali K. Fernández, Maribel Nantes-Sobrinho, Daniele Logic in Computer Science Nominal algebra includes $α$-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. |
| title | Strong Nominal Semantics for Fixed-Point Constraints |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.14253 |