Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909519767928832 |
|---|---|
| author | Caires-Santos, Ali K. Fernández, Maribel Nantes-Sobrinho, Daniele |
| author_facet | Caires-Santos, Ali K. Fernández, Maribel Nantes-Sobrinho, Daniele |
| contents | Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and $α$-renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in $α$-equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the $π$-calculus. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_19287 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version) Caires-Santos, Ali K. Fernández, Maribel Nantes-Sobrinho, Daniele Logic in Computer Science Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and $α$-renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in $α$-equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the $π$-calculus. |
| title | Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2502.19287 |