Graded Quantitative Narrowing
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908468276887552 |
|---|---|
| author | Ayala-Rincón, Mauricio de Lima, Thaynara Arielly Ehling, Georg Kutsia, Temur |
| author_facet | Ayala-Rincón, Mauricio de Lima, Thaynara Arielly Ehling, Georg Kutsia, Temur |
| contents | The recently introduced framework of Graded Quantitative Rewriting is an innovative extension of traditional rewriting systems, in which rules are annotated with degrees drawn from a quantale. This framework provides a robust foundation for equational reasoning that incorporates metric aspects, such as the proximity between terms and the complexity of rewriting-based computations. Quantitative narrowing, introduced in this paper, generalizes quantitative rewriting by replacing matching with unification in reduction steps, enabling the reduction of terms even when they contain variables, through simultaneous instantiation and rewriting. In the standard (non-quantitative) setting, narrowing has been successfully applied in various domains, including functional logic programming, theorem proving, and equational unification. Here, we focus on quantitative narrowing to solve unification problems in quantitative equational theories over Lawverean quantales. We establish its soundness and discuss conditions under which completeness can be ensured. This approach allows us to solve quantitative equations in richer theories than those addressed by previous methods. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_19630 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Graded Quantitative Narrowing Ayala-Rincón, Mauricio de Lima, Thaynara Arielly Ehling, Georg Kutsia, Temur Logic in Computer Science The recently introduced framework of Graded Quantitative Rewriting is an innovative extension of traditional rewriting systems, in which rules are annotated with degrees drawn from a quantale. This framework provides a robust foundation for equational reasoning that incorporates metric aspects, such as the proximity between terms and the complexity of rewriting-based computations. Quantitative narrowing, introduced in this paper, generalizes quantitative rewriting by replacing matching with unification in reduction steps, enabling the reduction of terms even when they contain variables, through simultaneous instantiation and rewriting. In the standard (non-quantitative) setting, narrowing has been successfully applied in various domains, including functional logic programming, theorem proving, and equational unification. Here, we focus on quantitative narrowing to solve unification problems in quantitative equational theories over Lawverean quantales. We establish its soundness and discuss conditions under which completeness can be ensured. This approach allows us to solve quantitative equations in richer theories than those addressed by previous methods. |
| title | Graded Quantitative Narrowing |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.19630 |