Graded Quantitative Narrowing

TL;DR

This paper introduces quantitative narrowing within the framework of graded quantitative rewriting, enabling the solving of unification problems in quantitative equational theories with metric considerations.

Contribution

It extends traditional narrowing to a quantitative setting, allowing for unification in richer theories using Lawverean quantales, with established soundness and conditions for completeness.

Findings

Quantitative narrowing generalizes traditional narrowing with unification.

It enables solving equations in richer quantitative theories.

Soundness is established, with discussion on completeness conditions.

Abstract

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.