Abstract
Quantitative equational reasoning provides a framework that extends equality to an abstract notion of proximity by endowing equations with an element of a quantale. In this paper, we discuss the unification problem for a special class of shallow subterm-collapse-free quantitative equational theories. We outline rule-based algorithms for solving such equational unification problems over generic as well as idempotent Lawvereian quantales and study their properties.
You have full access to this open access chapter, Download conference paper PDF
Keywords
1 Introduction
Extending the equality predicate to a notion that expresses similarity or proximity is a task that has been addressed in various ways. While fuzzy reasoning [8, 23] approaches this endeavor by equipping equations with real numbers between 0 and 1 to express the degree to which they hold true, quantitative algebraic reasoning [4, 17] follows a more proximity-oriented approach, attempting to establish a notion of distance between two terms.
Recently, Gavazzo and Di Florio [12] introduced a framework of metric and quantitative equational reasoning that generalizes these approaches (with a slight modification). It is based on the idea of modeling abstract quantities in quantales [22], following Lawvere’s fundamental work [16]. In this framework, equations between terms are endowed with an element of a Lawvereian quantale that expresses, in one sense or another, the degree to which they hold true. The exact meaning of this degree depends on the choice of the quantale; for instance, it could correspond to the distance of two terms in a metric space, or to the probability that the terms are equal. This approach is quite general and includes various known quantitative theories as special cases.
In recent years, quantitative and approximate techniques have become increasingly popular due to various applications. In these applications, e.g., in those related to reasoning about probabilistic computations [5], reasoning about privacy and security of systems [1, 21], reasoning about resource consumption during computation [7], approximate program transformations [13], etc. equalities are replaced with their quantitative approximations to model distances between programs, processes, or systems, resulting in metric-based approximate relations. Various techniques have been used to model such metric reasoning principles, among them quantitative equational logic, discussed in [3, 4, 17, 18].
In this paper, we address one of the central problems in equational reasoning: unification (or solving equations). We approach this problem in the framework as described in [12], studying a generalization of classical unification to solving equations in a quantitative equational theory in Lawvereian quantales.
The theories we consider in this paper are induced by shallow subterm-collapse-free equations of a special form, between terms whose arguments are the same sequence of variables, e.g. \(f(x_1,\ldots ,x_n)\) and \(g(x_1,\ldots ,x_n)\). This is a natural first step toward investigating quantitative equational unification since such quantitative equations generalize the principle of “extending proximity between function symbols to proximity between terms” of unification in the fuzzy quantale to unification in an arbitrary Lawvereian quantale. Despite their simple form, such theories still pose several challenges (originating from, e.g., tensor-based transitivity or extending proximity between arguments to whole terms), which affect the notions of completeness and minimality of unifier sets. We redefine these notions and show that unification (modulo the abovementioned theories) in arbitrary Lawvereian quantale is finitary, while for idempotent Lawvereian quantales, it becomes unitary. We develop the corresponding unification algorithms and study their properties. Due to space limitations, we refer to the more detailed technical report [10] for some of the proofs.
2 Preliminaries
We start by introducing the basic notions and fixing the terminology. Quantales. For the notions in this part, we follow [11, 12].
Definition 1
(Quantale). A (unital) quantale \(\mathbb {\varOmega }= (\varOmega , \precsim , \otimes , \kappa )\) consists of a monoid \((\varOmega , k, \otimes )\) and a complete lattice \((\varOmega , \precsim )\) (with join \(\vee \) and meet \(\wedge \)) satisfying the following distributivity laws: \(\delta \otimes \left( \bigvee _{i\in I} \varepsilon _i \right) = \bigvee _{i\in I} (\delta \otimes \varepsilon _i)\) and \(\left( \bigvee _{i\in I} \varepsilon _i \right) \otimes \delta = \bigvee _{i\in I} (\varepsilon _i \otimes \delta )\).
The element \(\kappa \) is called the unit of the quantale, and \(\otimes \) is called its tensor (or multiplication). Besides \(\kappa \), we use Greek letters \(\varepsilon , \delta , \eta , \zeta , \iota \), and \(\omega \) to denote elements of \(\varOmega \). The top and bottom elements of a quantale are denoted by \(\top \) and \(\bot \), respectively. Quantales in which the unit \(\kappa \) coincides with \(\top \) are called integral quantales. A quantale is commutative if its underlying monoid is. It is non-trivial if \(\kappa \ne \bot \). It is cointegral if \(\varepsilon \otimes \delta = \bot \) implies either \(\varepsilon = \bot \) or \(\delta = \bot \).
We assume our quantales are commutative, integral, cointegral, and nontrivial. Such quantales are called Lawvereian. (Note that the fuzzy quantale \(\mathbb {I}\) is Lawvereian for the Gödel and product T-norms, but not for the Łukasiewicz T-norm.)
Tensors in quantales always have left and right adjoints. For commutative quantales, these adjoints are the same, defined as \(\varepsilon \multimap \delta {:}{=}\bigvee \{\eta \mid \varepsilon \otimes \eta \precsim \delta \}.\)
An element \(\iota \in \varOmega \) is an idempotent element (or simply an idempotent) of a quantale \(\mathbb {\varOmega }\) if it satisfies \(\iota \otimes \iota =\iota \). A quantale is called idempotent if every element is idempotent. Among the quantales in Table 1, the idempotent ones are \(\mathbb {2}\), \(\mathbb {L}^{\max }\), and \(\mathbb {I}\) for the minimum (Gödel) T-norm.
In any Lawvereian quantale, (i) \(\otimes \) is monotonous: \(\alpha \precsim \beta \Rightarrow \alpha \otimes \gamma \precsim \beta \otimes \gamma \) (using distributivity: \((\alpha \otimes \gamma )\vee (\beta \otimes \gamma )=(\alpha \vee \beta )\otimes \gamma = \beta \otimes \gamma \)); (ii) \(\alpha \otimes \beta \precsim \alpha \wedge \beta \) (using monotonicity and integrality: \(\alpha \otimes \beta \precsim \alpha \otimes \top =\alpha \)).
Given a quantale \(\mathbb {\varOmega }\) and \(\varepsilon ,\delta \in \varOmega \), the way-below relation \(\ll \) is defined as \(\delta \ll \varepsilon \) iff for every \(\varPsi \subseteq \varOmega \), if \(\varepsilon \precsim \bigvee \varPsi \) then there exists a finite subset \(\varPsi _0 \subseteq \varPsi \) such that \(\delta \! \precsim \! \bigvee \varPsi _0\). A quantale \(\mathbb {\varOmega }\) is called continuous if \(\varepsilon = \bigvee _{\delta \ll \varepsilon } \delta \) for all \(\varepsilon \in \varOmega \).
Definition 2
(\(\mathbb {\varOmega }\)-relations, \(\mathbb {\varOmega }\)-ternary relations). An \(\mathbb {\varOmega }\)-relation R between sets A and B is a function \(R:A\times B \rightarrow \varOmega \). For any set A, the identity \(\mathbb {\varOmega }\)-relation \(\varDelta _A:A\times A \rightarrow \varOmega \) maps the diagonal elements (a, a) to \(\kappa \), and all other elements to \(\bot \). The composition \((R;S):A\times C \rightarrow \varOmega \) of two \(\mathbb {\varOmega }\)-relations \(R:A\times B\rightarrow \varOmega \) and \(S:B\times C\rightarrow \varOmega \) is defined as \((R;S)(a,c){:}{=}\bigvee _{b\in B} \big ( R(a,b)\otimes S(b,c)\big )\).
An \(\mathbb {\varOmega }\)-ternary relation over \(A\times B\) is a ternary relation \(R\subseteq A\times \varOmega \times B\) such that \(R(a,\varepsilon ,b)\) implies \(R(a,\delta ,b)\) for any \(\delta \precsim \varepsilon \).
Any \(\mathbb {\varOmega }\)-ternary relation R induces an \(\mathbb {\varOmega }\)-relation \(R^\bullet (a,b){:}{=}\bigvee _{R(a,\varepsilon , b)} \varepsilon \), and any \(\mathbb {\varOmega }\)-relation R induces an \(\mathbb {\varOmega }\)-ternary relation \(R^\circ (a,\varepsilon , b) :\Longleftrightarrow \varepsilon \precsim R(a,b)\). Moreover, we have \(R^{\bullet \circ } = R^{\circ \bullet }=R\), and we can freely switch between \(\mathbb {\varOmega }\)-ternary relations and \(\mathbb {\varOmega }\)-relations.
The complete lattice structure of \(\mathbb {\varOmega }\) lifts to \(\mathbb {\varOmega }\)-relations pointwise, and we can say that an \(\mathbb {\varOmega }\)-relation R on \(A\times A\) is reflexive if \(\varDelta _A \precsim R\); transitive if \((R;R)\precsim R\); symmetric if \(R^{-} \precsim R\) (where \(R^{-}\) is defined as \(R^{-}(b,a){:}{=}R(a,b)\)). Thus, we get the notions of a preorder (i.e., reflexive and transitive) and equivalence (i.e., reflexive, transitive, and symmetric) \(\mathbb {\varOmega }\)-relation.
Terms and Substitutions. We assume that the reader is familiar with the standard notions of unification theory, see, e.g., [2]. A signature \(\mathcal {F}\) is a set of function symbols, each equipped with a fixed nonnegative arity. The set of terms over a signature \(\mathcal {F}\) and a set of variables \(\mathcal {V}\) is denoted by \(T(\mathcal {F},\mathcal {V})\). Given a term \(t\in T(\mathcal {F},\mathcal {V})\), we denote by \(\mathcal {V}(t)\) the set of variables appearing in t. A term is ground if it contains no variables. The notion of a position in a term is defined in the standard way.
The set of leaves of a term is defined as \(\ell (e){:}{=}\{e\}\), if e is a constant symbol or a variable, and \(\ell (f(t_1,\dots ,t_n)){:}{=}\bigcup _{i=1}^n \ell (t_i)\). (The leaves of a term t correspond to the leaves of the tree representing t.) If s is a subterm of t, then the depth of s in t as the minimal length of a position at which s occurs in t.
A substitution is a map \(\sigma :\mathcal {V}\rightarrow T(\mathcal {F},\mathcal {V})\) which maps all but finitely many variables to themselves. Greek letters \(\sigma ,\varphi ,\vartheta ,\tau \) are used for them, while \( Id \) denotes the identity substitution. The set of substitutions is denoted by \( Sub \). We use the set notation for substitutions, writing \(\sigma \) explicitly as a finite set \(\{x\mapsto \sigma (x) \mid x\ne \sigma (x)\} \). The domain of \(\sigma \) is defined as \( dom (\sigma ){:}{=}\{x \mid x\ne \sigma (x)\}\). A substitution \(\sigma \) extends naturally to an endomorphism on \(T(\mathcal {F},\mathcal {V})\). The image of a term t under this endomorphism is denoted \(t\sigma \).
3 Quantitative Equational Theories
We now fix a signature \(\mathcal {F}\), a set of variables \(\mathcal {V}\), and a Lawvereian quantale \(\mathbb {\varOmega }\).
Let \(\approx _E\) be an \(\mathbb {\varOmega }\)-ternary relation, assumed to be induced from a given set E of triples \((t,\varepsilon ,s)\), which we write as \(\varepsilon \Vdash t\approx _E s\) (called \(\mathbb {\varOmega }\)-equalities). A quantitative equational theory (or \(\mathbb {\varOmega }\)-equational theory) \(=_E\) is an \(\mathbb {\varOmega }\)-ternary relation generated from \(\approx _E\) by the rules in Fig. 1. We call E a presentation of \(=_E\). Informally, we read \(\varepsilon \Vdash t =_E s\) as “t and s are at most \(\varepsilon \)-apart modulo E” or “t and s are equal modulo E with degree \(\varepsilon \)”.
Observe that the \(\mathbb {\varOmega }\)-relation \(=^\bullet _E\) induced from \(=_E\) (i.e., \(t =^\bullet _E s {:}{=}\bigvee _{\varepsilon \Vdash t =_E s} \varepsilon \)) is a reflexive, symmetric, transitive quantitative relation that contains \(\approx ^\bullet _E\) and where function symbols and substitutions behave in a non-expansive way:
We will often slightly abuse terminology by calling both \(=^\bullet _E\) and a presentation E a quantitative equational theory.
The rules in Fig. 1 were introduced in [11] with the aim of generalizing previous approaches to quantitative reasoning [4, 17]. This generalization is achieved up to a slight modification of the (NExp) rule, whose analogue in [17] would feature the join of \(\varepsilon _1,\dots ,\varepsilon _n\) rather than their tensor product.Footnote 1
It should further be remarked that the (Join) rule also applies to an empty hypothesis, whence \(\bot \Vdash t=_E s\) holds for any t and s. The infinitary (Arch) rule is needed to guarantee the semantic completeness of the deduction system in [17], but has no effect on \(=_E\) whenever the presentation E is finite, whence it can be safely ignored in that case.
Analogous to classical equational theories, an \(\mathbb {\varOmega }\)-equation \(\varepsilon \Vdash t=s\), where s is a proper subterm of t, is called a subterm-collapse equation. A quantitative equational theory E is said to be simple (or subterm-collapse-free) if whenever \(\varepsilon \Vdash t=_E s\) with \(\varepsilon \ne \bot \) holds, the equation \(\varepsilon \Vdash t= s\) is not subterm-collapsing. An equation \(\varepsilon \Vdash t=s\) is called shallow [6] if the depth of each variable occurrence in t or in s is at most 1. An equational theory is called shallow if each equation in its presentation is shallow.
Definition 3
Let E be an \(\mathbb {\varOmega }\)-equational theory and \(\mathcal {X}\) be a set of variables. A ternary relation \(\lessapprox _{E,\mathcal {X}}\subseteq Sub \times \varOmega \times Sub \) is defined as
\(\lessapprox _{E,\mathcal {X}}(\sigma ,\varepsilon , \vartheta )\) iff there exists a \(\varphi \) such that \(\varepsilon \Vdash x\sigma \varphi =_E x\vartheta \) for all \(x \in \mathcal {X}\).
In this case, we say that the substitution \(\sigma \) is more general than \(\vartheta \) modulo E on \(\mathcal {X}\) up to \(\varepsilon \). We shortly write \(\sigma \lessapprox _{E,\mathcal {X},\varepsilon } \vartheta \) and call \(\vartheta \) an \((E,\mathcal {X},\varepsilon )\)-instance of \(\sigma \) (or an \((E,\mathcal {X})\)-instance with degree \(\varepsilon \)).
It is not hard to see that \(\lessapprox _{E,\mathcal {X}}\) is an \(\mathbb {\varOmega }\)-ternary relation over \( Sub \times Sub \). To show this, we need to prove that \(\sigma \lessapprox _{E,\mathcal {X},\varepsilon } \vartheta \) implies \(\sigma \lessapprox _{E,\mathcal {X},\delta } \vartheta \) for any \(\delta \precsim \varepsilon \), which follows from the definition of \(=_E\).
Lemma 1
If \(\sigma \lessapprox _{E,\mathcal {X},\varepsilon } \vartheta \) and \(\vartheta \lessapprox _{E,\mathcal {Y},\delta } \psi \), then \(\sigma \lessapprox _{E,\mathcal {X}\cap \mathcal {Y},\varepsilon \otimes \delta } \psi \).
Proof
By definition of \(\lessapprox _{E,\mathcal {X}}\) and \(\lessapprox _{E,\mathcal {Y}}\), we have \(\varepsilon \Vdash x\sigma \varphi _1 =_E x\vartheta \) for all \(x \in \mathcal {X}\), and \(\delta \Vdash y\vartheta \varphi _2 =_E y\psi \) for all \(y \in \mathcal {Y}\). From these equalities, for all \(z \in \mathcal {X}\cap \mathcal {Y}\) by the Subst rule we get \(\varepsilon \Vdash z\sigma \varphi _1\varphi _2 =_E z\vartheta \varphi _2\) and \(\delta \Vdash z\vartheta \varphi _2 =_E z\psi \). Therefore, by \(\otimes \)-transitivity (the Trans rule) we obtain \(\varepsilon \otimes \delta \Vdash z\sigma \varphi _1\varphi _2 =_E z\psi \) for all \(z \in \mathcal {X}\cap \mathcal {Y}\), which, by definition of \(\lessapprox _{E,\mathcal {X}\cap \mathcal {Y}}\), gives \(\sigma \lessapprox _{E,\mathcal {X}\cap \mathcal {Y},\varepsilon \otimes \delta } \psi \). \(\square \)
Corollary 1
If \(\sigma \lessapprox _{E,\mathcal {X},\varepsilon } \vartheta \) and \(\vartheta \lessapprox _{E,\mathcal {X},\delta } \psi \), then \(\sigma \lessapprox _{E,\mathcal {X},\varepsilon \otimes \delta } \psi \).
Theorem 1
Given a set of \(\mathbb {\varOmega }\)-equalities E and a set of variables \(\mathcal {X}\), the \(\mathbb {\varOmega }\)-relation \(\lessapprox _{E,\mathcal {X}}^\bullet \) induced by \(\lessapprox _{E,\mathcal {X}}\) is a preorder on \( Sub \).
Proof
We should show that \(\lessapprox _{E,\mathcal {X}}^\bullet \) is reflexive and transitive.
-
Reflexivity: We need to show \(\kappa \precsim \sigma \lessapprox _{E,\mathcal {X}}^\bullet \sigma \) for all \(\sigma \), which follows directly from the definitions of \(\lessapprox _{E,\mathcal {X}}\) and \(=_E\).
-
Transitivity: We should prove \( \big ( \sigma \lessapprox _{E,\mathcal {X}}^\bullet \vartheta \otimes \vartheta \lessapprox _{E,\mathcal {X}}^\bullet \psi \big ) \precsim \big ( \sigma \lessapprox _{E,\mathcal {X}}^\bullet \psi \big )\) for all \(\sigma ,\vartheta \), and \(\psi \). This statement can be inferred from Corollary 1. \(\square \)
The equivalence relation on substitutions induced by \(\lessapprox _{E,\mathcal {X}}\) is denoted by \(\cong _{E,\mathcal {X}}\). It is an \(\mathbb {\varOmega }\)-ternary relation. We write \(\sigma \cong _{E,\mathcal {X},\varepsilon } \vartheta \) if \(\varepsilon \precsim (\sigma \cong ^\bullet _{E,\mathcal {X}} \vartheta )\).
Example 1
Let \(\mathbb {\varOmega }\) be the Lawvere quantale \(\mathbb {L}=([0,\infty ],\geqslant ,+,0)\) and consider \(E=\{1\Vdash a\approx b, 1\Vdash b \approx c\}\), \(\varepsilon =2\) and \(\mathcal {X}=\{x\}\). Let \(\sigma =\{x \mapsto a\}\), \(\vartheta =\{x \mapsto b\}\), and \(\varphi =\{x \mapsto c\}\). Then we have:
-
\(\sigma \lessapprox _{E,\mathcal {X},\varepsilon } \vartheta \), because \( x\sigma Id = a\), \(x\vartheta =b\), and \(1\Vdash a=_E b \);
-
\(\vartheta \lessapprox _{E,\mathcal {X},\varepsilon } \varphi \), because \( x\vartheta Id = b\), \(x\varphi =c\), and \(1\Vdash b=_E c\);
-
\( \varphi \lessapprox _{E,\mathcal {X},\varepsilon } \sigma \), because \( x\varphi Id = c\), \(x\sigma =a\), and \(2 \Vdash c=_E a\).
Hence, \(\sigma \cong _{E,\mathcal {X},\varepsilon } \vartheta \), \(\vartheta \cong _{E,\mathcal {X},\varepsilon } \varphi \), and \(\sigma \cong _{E,\mathcal {X},\varepsilon } \varphi \). \(\blacksquare \)
Theorem 2
Given E, \(\mathcal {X}\), t, and s such that \(\mathcal {V}(t)\cup \mathcal {V}(s)\subseteq \mathcal {X}\), let R denote \(=^\bullet _E\) and S denote \(\lessapprox ^\bullet _{E,\mathcal {X}}\). Assume \(\sigma \) and \(\vartheta \) are substitutions such that \(R(t\sigma ,s\sigma )=\varepsilon \) and \(S(\sigma ,\vartheta )=\delta \). Then \(\varepsilon \otimes \otimes _{i=1}^{n+m}\delta \precsim R(t\vartheta ,s\vartheta ) \), where n and m are the number of occurrences of variables from \(\mathcal {X}\) in t and s, respectively.
Proof
From \(S(\sigma ,\vartheta )=\delta \) we know that there exists \(\varphi \) such that \(\delta \precsim R(x\sigma \varphi ,x\vartheta )\) holds for all \(x\in \mathcal {X}\). From this, by structural induction over terms, we can prove \(\otimes _{i=1}^n \delta \precsim R(t\sigma \varphi ,t\vartheta )\) and \(\otimes _{i=1}^m \delta \precsim R(s\sigma \varphi ,s\vartheta )\). From \(R(t\sigma ,s\sigma )=\varepsilon \) we get \(\varepsilon \precsim R(t\sigma \varphi ,s\sigma \varphi )\). Applying transitivity twice we get \(\varepsilon \otimes \otimes _{i=1}^{n+m}\delta \precsim R(t\vartheta ,s\vartheta )\). \(\square \)
Example 2
In the Boolean quantale \(\mathbb {2}\), this theorem implies the well-known fact that if \(\sigma \) is a unifier of t and s and \(\vartheta \) is an instance of \(\sigma \), then \(\vartheta \) is also a unifier of t and s. (In that case, \(\varepsilon =\delta =1\).)
Consider the fuzzy quantale \(\mathbb {I}\) with the minimum T-norm, \(E=\{0.5 \Vdash a \approx b, 0.7 \Vdash b \approx c\}\), \(t=f(x,x,y)\), \(s=f(y,b,c)\), \(\mathcal {X}=\{x,y\}\), \(\sigma =\{x\mapsto b, y\mapsto b \}\), and \(\vartheta =\{x\mapsto a, y\mapsto c\}\). Then \(0.5\Vdash a =_E c\) and
Now consider the Lawvere quantale \(\mathbb {L}\) with \(E=\{1 \Vdash a \approx b, 1 \Vdash b \approx c, 1 \Vdash c \approx d, 1 \Vdash f(x) \approx g(x)\}\), \(t=x\), \(s=f(y)\), \(\mathcal {X}=\{x,y\}\), \(\sigma =\{x\mapsto g(y)\}\), and \(\vartheta =\{x\mapsto g(a), y\mapsto d\}\). Besides, \({\precsim } ={\geqslant }\) and we have
Theorem 2 implies that if \(\delta \) is an idempotent element of the quantale and it can be absorbed by \(\varepsilon \) (i.e., \(\varepsilon \otimes \delta = \varepsilon \)), then \(\varepsilon \Vdash t\vartheta =_E s\vartheta \). Obviously, this will be fulfilled if \(\delta =\kappa \). In idempotent quantales, it will also hold when \(\varepsilon \precsim \delta \). For idempotent elements, a stronger version of transitivity holds. Namely, if \(\iota \) is an idempotent element of a quantale, then we have for all \(E,t,s,r,\mathcal {X},\sigma ,\vartheta ,\varphi \):
-
\(\iota \Vdash t =_E s\) and \(\iota \Vdash s =_E r\) imply \(\iota \Vdash t =_E r\),
-
\(\sigma \lessapprox _{E,\mathcal {X},\iota } \vartheta \) and \(\vartheta \lessapprox _{E,\mathcal {X},\iota } \varphi \) imply \(\sigma \lessapprox _{E,\mathcal {X},\iota } \varphi \).
4 Quantitative Equational Unification
Definition 4
(Quantitative equational unification). A quantitative equational unification problem is formulated as follows:
We call this problem \((E,\varepsilon )\)-unification problem over \(\mathbb {\varOmega }\). The quantale name is usually skipped when it does not cause confusion. For unification problems, we use the notation \(\varepsilon \Vdash t=^?_E s\), called a unification equation, where the question mark indicates that the equation is supposed to be solved. For simplicity, we write the problem as \(t=^?_{E,\varepsilon } s\), and further skip E if it is clear from the context.
The substitution \(\sigma \), if it exists, is called an \((E,\varepsilon )\)-unifier of t and s (alternatively, a unifier or a solution of \(t=^?_{E,\varepsilon } s\)) over \(\mathbb {\varOmega }\). In such a case we say that the given unification problem is solvable, or that the terms t and s are \((E,\varepsilon )\)-unifiable over \(\mathbb {\varOmega }\). The set of all unifiers of \(t=^?_{E,\varepsilon } s\) is denoted by \(\mathfrak {U}_{E,\varepsilon }(t,s)\).
For a given presentation E, a function symbol from \(\mathcal {F}\) is called free if it does not appear in E. If \(\mathcal {F}\) contains a free m-ary function symbol for some \(m>1\), the unification problem formulated above is equivalent to a problem of finding a solution of a system of unification equations (instead of a single equation) formulated as a constrained problem:
In such a case we can write the unification problem as a pair of a set of unification equations and a \(\precsim \)-constraint: \(\{ t_1 =^?_{E,{\boldsymbol{\upalpha }}_1} s_1, \ldots , t_n =^?_{E,{\boldsymbol{\upalpha }}_n} s_n\}; \varepsilon \precsim {\boldsymbol{\upalpha }}_1 \otimes \cdots \otimes {\boldsymbol{\upalpha }}_n\), where \({\boldsymbol{\upalpha }}_i\) are new metavariables whose values are also to be found alongside with variables that appear in the given t’s and s’s. This problem can be transformed to a single-equation problem. For instance, the constrained problem \(\{ t_1 =^?_{E,{\boldsymbol{\upalpha }}_1} s_1,\, t_2 =^?_{E,{\boldsymbol{\upalpha }}_2} s_2,\, t_3 =^?_{E,{\boldsymbol{\upalpha }}_3} s_3\};\varepsilon \precsim {\boldsymbol{\upalpha }}_1\otimes {\boldsymbol{\upalpha }}_2\otimes {\boldsymbol{\upalpha }}_3\) can be transformed to \(f(f(t_1,t_2),t_3)=_{E,\varepsilon }^? f(f(s_1,s_2),s_3)\), where f is a free binary function symbol. The two problems are equivalent in the sense that they have exactly the same set of \((E,\varepsilon )\)-unifiers.If the arity of f is bigger than the number of equations, the missing arguments will be filled in by fresh variables. For instance, for a quaternary f, the problem above can be encoded as \(f(t_1,t_2,t_3,x)=_{E,\varepsilon }^? f(s_1,s_2,s_3,x)\), where x is fresh.
In classical unification, an important property of the instantiation relation is that any substitution that is less general than a given unifier of two terms will still be a unifier. In the quantitative case, we should take into account the approximation, which complicates things. First, we have the following fact as a consequence of Theorem 2:
Fact 1
If \(\sigma \) is an \((E,\varepsilon )\)-unifier of t and s and \(\sigma \lessapprox _{E,\mathcal {V}(t,s),\delta }\! \vartheta \) for some \(\delta \), then \(\vartheta \) is an \((E,\varepsilon \otimes \delta ^k)\)-unifier of t and s, where k is the total number of occurrences of variables in t and s.
Some results become simpler for idempotent elements:
Lemma 2
Let \(\iota \) be an idempotent element of \(\mathbb {\varOmega }\), and \(\sigma \) and \(\vartheta \) be substitutions.
-
(i)
If \(\iota \Vdash y\sigma =_E y\vartheta \) holds for every \(y\in \mathcal {Y}\subseteq \mathcal {V}\), then \(\iota \Vdash r\sigma =_E r\vartheta \) holds for every term \(r\in T(\mathcal {F},\mathcal {Y})\).
-
(ii)
Suppose that \(\varepsilon \in \varOmega \) satisfies \(\varepsilon \otimes \iota =\varepsilon \). If \(\sigma \lessapprox _{E,\mathcal {V}(t,s),\iota } \vartheta \) and \(\sigma \) is an \((E,\varepsilon )\)-unifier of the terms t and s, then so is \(\vartheta \).
Proof
Part (i) is proved by structural induction, using idempotence. For (ii), as \(\sigma \lessapprox _{E,\mathcal {V}(t,s),\iota } \vartheta \), there exists a substitution \(\varphi \) such that \(\iota \Vdash x \sigma \varphi =_E x\vartheta \) holds for every variable \(x\in \mathcal {V}(t,s)\). Thus, \(\iota \Vdash r \sigma \varphi =_E r\vartheta \) holds for any term \(r\in T(\mathcal {F},\mathcal {V}(t,s))\) by (i). Hence, we have \(\iota \Vdash s\vartheta =_E s\sigma \varphi \), \(\varepsilon \Vdash s\sigma \varphi =_E t\sigma \varphi \), and \(\iota \Vdash t\sigma \varphi =_E t\vartheta \). From these equalities, using \(\varepsilon \otimes \iota =\varepsilon \), we get \(\varepsilon \Vdash s\vartheta =_E t\vartheta \). \(\square \)
This lemma implies that \((E,\mathcal {V}(t,s),\kappa )\)-instances of \((E,\varepsilon )\)-unifiers of t and s are still their \((E,\varepsilon )\)-unifiers. Besides, it has the following corollary:
Corollary 2
Let \(\mathbb {\varOmega }\) be an idempotent quantale, in which \(\sigma \) is an \((E,\varepsilon )\)-unifier of t and s, \(\sigma \lessapprox _{E,\mathcal {V}(t,s),\delta }\! \vartheta \), and \(\varepsilon \precsim \delta \). Then \(\vartheta \) is an \((E,\varepsilon )\)-unifier of t and s in \(\mathbb {\varOmega }\).
These results motivate a specialized version of the notion of a minimal complete set of unifiers that we use in this paper:
Definition 5
(Minimal \(\iota \)-complete set of unifiers). Let P be an \((E,\varepsilon )\)-unification problem over a quantale \(\mathbb {\varOmega }\) and signature \(\mathcal {F}\). Let \(\mathcal {X}= \mathcal {V}(P)\) be the set of all variables of P, and let \(\iota \) be an idempotent element of \(\mathbb {\varOmega }\) such that \(\varepsilon \otimes \iota =\varepsilon \). An \(\iota \)-complete set of \((E,\varepsilon )\)-unifiers of P is a set \(\mathcal {C}\) of substitutions such that
-
(1)
\(\mathcal {C}\subseteq \mathfrak {U}_{E,\varepsilon } (P) \), i.e., each element of \(\mathcal {C}\) is an \((E,\varepsilon )\)-unifier of P,
-
(2)
for each \(\vartheta \in \mathfrak {U}_{E,\varepsilon } (P)\) there exists \(\sigma \in \mathcal {C}\) such that \(\sigma \lessapprox _{E,\mathcal {X},\iota } \vartheta \).
The set \(\mathcal {C}\) is a minimal \(\iota \)-complete set of \((E,\varepsilon )\)-unifiers of P iff it is an \(\iota \)-complete set that satisfies the following minimality property:
-
(3)
for all \(\sigma , \sigma '\in \mathcal {C}\), if \(\sigma \lessapprox _{E,\mathcal {X},\iota } \sigma '\), then \(\sigma =\sigma '\).
We denote a minimal \(\iota \)-complete set of \((E,\varepsilon )\)-unifiers of P by \( mcsu _{E,\varepsilon ,\iota }(P)\).
Given a unification problem with threshold \(\varepsilon \), in order to make use of this definition, one first needs to find an idempotent element \(\iota \) such that \(\varepsilon \otimes \iota =\varepsilon \). In an arbitrary quantale, we can always take \(\iota =\kappa \). If \(\varepsilon \) is idempotent itself, then we can also choose \(\iota =\varepsilon \).Footnote 2
Let P be an \((E,\varepsilon )\)-unification problem. If it is unsolvable, then for any idempotent \(\iota \) with \(\varepsilon \otimes \iota =\varepsilon \) we have \( mcsu _{E,\varepsilon ,\iota }(t,s)=\emptyset \). Depending on E, \(\varepsilon \), and \(\iota \), minimal \(\iota \)-complete sets of \((E,\varepsilon )\)-unifiers may not always exist. Even if they do, they may be infinite. When they exist, they are unique modulo the instantiation equivalence relation \(\cong _{E,\mathcal {X},\iota }\).Footnote 3
Example 3
Let \(\mathbb {\varOmega }\) be the Lawvere quantale \(\mathbb {L}\), E be the set of equations \(E=\{1\Vdash a\approx b, 1\Vdash b\approx c, 1\Vdash c\approx d\}\), \(\varepsilon = 1\), \(t=f(x,b)\), and \(s=f(c,x)\).
The substitutions \(\sigma =\{x\mapsto b\}\), \(\vartheta =\{x\mapsto c\}\) are \((E,\varepsilon )\)-unifiers of t and s:
-
\(t\sigma = f(b,b)\), \(s\sigma = f(c,b)\) and \(1 \Vdash f(b,b) =_E f(c,b)\),
-
\(t\vartheta = f(c,b)\), \(s\vartheta = f(c,c)\) and \(1 \Vdash f(c,b) =_E f(c,c)\).
In fact, \(\{\sigma , \vartheta \}= mcsu _{E,\varepsilon ,0}(t,s)\). Note that we have \(\sigma \cong _{E,\mathcal {X},1}\vartheta \), but also \(\sigma \cong _{E,\mathcal {X},1}\{x\mapsto a\}\) and \(\vartheta \cong _{E,\mathcal {X},1}\{x\mapsto d\}\). However, neither \(\{x\mapsto a\}\) nor \(\{x\mapsto d\}\) is an \((E,\varepsilon )\)-unifier of t and s (but they are (E, 3)-unifiers of t and s). \(\blacksquare \)
The notion of an occurrence cycle will be needed later on.
Definition 6
(Occurrence cycle). A set of unification equations \(\{x_1\approx ^?_{\varepsilon _1} t_1,\dots ,x_n\approx ^?_{\varepsilon _n} t_n\}\) constitutes an occurrence cycle if \(t_i\) is a non-variable term for at least one i, \(x_i\in \mathcal {V}(t_{i-1})\) for \(1< i\leqslant n\) and \(x_1\in \mathcal {V}(t_n)\).
4.1 Unification: Simple Shallow Theories (Special Form)
In this section, we will consider \(\mathbb {\varOmega }\)-equational theories that admit a presentation consisting of a finite number of equations of the form \(\gamma \! \Vdash \! f(x_1,\ldots ,x_n) \approx g(x_1,\ldots ,x_n)\), where \(n\geqslant 0\), \(f\ne g\), and all x’s are pairwise distinct. Also, the \(\gamma \)’s in different equations can be different. This is the very basic form of quantitative axioms. The quantale \(\mathbb {\varOmega }\), as said above, is an arbitrary Lawvereian quantale. In the next subsection we consider the special case of idempotent Lawvereian quantales.
The presentation is shallow. One can easily show that the theory generated from such a presentation is simple. Hence, we consider simple shallow quantitative equational theories (of a special form). We will refer to such theories by \(E_\textsf{ssh}\). In them, it makes sense to speak about the approximation degree of two function symbols, which is defined as \(\mathfrak {d}_{E_\textsf{ssh}}(f,g){:}{=}\big (f(x_1,\dots ,x_n)=^\bullet _{E_\textsf{ssh}} g(x_1,\dots ,x_m) \big )\) for an n-ary f and m-ary g. (Obviously, \(\mathfrak {d}_{E_\textsf{ssh}}(f,g)=\bot \) if \(n\ne m\).) We say that f and g are \((E_\textsf{ssh},\varepsilon )\)-proximal, if \(\varepsilon \precsim \mathfrak {d}_{E_\textsf{ssh}}(f,g)\).
Remark 1
Since the equational theories we consider here are finitely presented, the degree of two function symbols of the same arity can be effectively computed as \(\mathfrak {d}_{E_\textsf{ssh}}(f,g)=\bigvee \{\gamma \mid \gamma \Vdash f(x_1,\dots ,x_n)= g(x_1,\dots ,x_n)\in C\},\) where C is the closure of the presentation of \(E_\textsf{ssh}\) under the (Trans) and (Sym) rules.
Theorem 3
\(E_\textsf{ssh}\)-unification is finitary in a Lawvereian quantale \(\mathbb {\varOmega }\) in the sense that for any \(\varepsilon \in \varOmega \), every \((E_\textsf{ssh},\varepsilon )\)-unification problem \(t=^?_{E_\textsf{ssh},\varepsilon } s\) has a finite minimal \(\kappa \)-complete set of unifiers.
Proof (Sketch)
[Sketch] Let \(N_{E_\textsf{ssh},\varepsilon }(r)\) denote an \(\varepsilon \)-neighborhood of a term r with respect to \(E_\textsf{ssh}\), defined as the set of all terms obtained from r by replacing some function symbols by their \((E_\textsf{ssh},\varepsilon )\)-proximal ones. Then \( mcsu _{E_\textsf{ssh},\varepsilon ,\kappa }(t,s)\subseteq \cup _{t'\in T,s'\in S} \{ mgu (t'=^?s')\}\), where \(T= N_{E_\textsf{ssh},\varepsilon }(t)\), \(S=N_{E_\textsf{ssh},\varepsilon }(s)\), and \( mgu (t'=^?s')\) is a most general unifier of the syntactic unification problem \(t'=^? s'\). Since the presentation of theories of the form \(E_\textsf{ssh}\) is finite, the set \(N_{E_\textsf{ssh},\varepsilon }(r)\) is finite for \(\varepsilon \ne \bot \) for any r. Hence, the set \(\cup _{t'\in T,s'\in S} \{ mgu (t'=^?s')\}\) is finite, which implies that \( mcsu _{E_\textsf{ssh},\varepsilon ,\kappa }(t,s)\) is finite as well. \(\square \)
Remark 2
In principle, the above proof already outlines an \(E_\textsf{ssh}\)-unification algorithm. However, there are several reasons for not using it: first, it would be a brute-force approach blindly replacing symbols with all their proximal ones in all possible ways. Second, it would not be sound because non-unifier answers would be returned and we would have to clean the computed set afterwards. Third, we want to keep our approach flexible, leaving equations between variables as a part of the output instead of forcing them to have only a syntactic solution.
In the following, we use bold-face upright Greek letters \({\boldsymbol{\upalpha }}, {\boldsymbol{\upbeta }}, {\boldsymbol{\upgamma }}\) for metavariables that range over the domain of the quantale. The rules constituting our unification method operate on configurations whose form is stated below.
Definition 7
(Configuration). A configuration is either a special symbol F or a quadruple \(P;C;\delta ;\sigma \), where
-
P is a set of unification equations of the form \(t=^?_{{\boldsymbol{\upalpha }}} s\), where \({\boldsymbol{\upalpha }}\) is a metavariable (intuitively, P is the remaining problem to be solved),
-
C is a constraint of the form \(\varepsilon \precsim {\boldsymbol{\upalpha }}_1\otimes \dots \otimes {\boldsymbol{\upalpha }}_n\), where \({\boldsymbol{\upalpha }}_1,\dots ,{\boldsymbol{\upalpha }}_n\) are metavariables and \(\varepsilon \in \varOmega \),
-
\(\delta \) is an element of the quantale domain (the current approximation degree),
-
\(\sigma \) is a substitution (part of the unifier computed so far).
In C, we also allow for the case where \(n=0\), in which the empty product on the right-hand side is \(\kappa \) by convention.
The solving rules for a theory \(E_\textsf{ssh}\) are given below. They operate on configurations and are formulated modulo associativity and commutativity of \(\otimes \). We use f and g to denote (not necessarily distinct) n-ary function symbols, t, \(t_i\) and \(s_i\) for terms and x to denote a variable symbol. The symbol \(\varDelta \) denotes the tensor product of finitely many metavariables.
To solve an \((E_\textsf{ssh},\varepsilon )\)-unification problem between terms t and s, we create the initial configuration \(\{t =^?_{{\boldsymbol{\upalpha }}} s\}; \varepsilon \precsim {\boldsymbol{\upalpha }}; \kappa ; Id \) and start applying the rules as long as possible. The equation to be transformed is chosen arbitrarily (“don’t care nondeterminism”). We call the obtained algorithm QUnif.
Note that a configuration \(P;C;\sigma \) obtained from an \((E_\textsf{ssh},\varepsilon )\)-unification problem satisfies the following properties:
-
Any metavariable occurring in P also occurs in C and vice versa.
-
No metavariable appears more than once in P or C.
-
The domain of \(\sigma \) is disjoint from the set of variables occurring in P.
We will refer to such configurations as admissible.
To prove termination of QUnif, we introduce some terminology.
Definition 8
Let P be a set of quantitative equations and let \(P_\textsf{st}\) be the set of standard equations obtained from P by ignoring the indices: \(P_\textsf{st}{:}{=}\{t = s \mid \varepsilon \Vdash t=s \in P\}\). Then \(\textsf{DecNF}_{E_\textsf{ssh}}(P)\) denotes the decomposition normal form of P with respect to \(E_\textsf{ssh}\), which is the set of standard equations obtained from \(P_\textsf{st}\) by applying the following version of the decomposition rule as long as possible:
where \(\mathfrak {d}_{E_\textsf{ssh}}(f,g)\ne \bot \).
It is easy to see that every equation in \(\textsf{DecNF}_{E_\textsf{ssh}}(P)\) is of the form \(x=s\) where s is an arbitrary term, or \(t=x\) where t is not a variable.
For a set of (quantitative) equations P, the variable dependency graph \(\Gamma (P)\) is constructed as follows:
-
For each variable x appearing in P, add a node with label x to \(\Gamma (P)\).
-
Add a node with label G (the “ground node”).
-
For every equation \(x= y\in \textsf{DecNF}(P)\) between variables x and y, merge the nodes corresponding to x and y.
-
In order to construct the set of edges of \(\Gamma (P)\), we consider all equations of the form \(x= t\) (or \(t= x\)) in \(\textsf{DecNF}(P)\), where t is a non-variable term. For such an equation, we consider the set of leaves of t. For each element \(l\in \ell (t)\), if d is the depth in which l appears in t, we add an weighted edge to \(\Gamma (P)\):
-
If l is a constant, then we add an edge \(x\rightarrow _{d+1} G\) (with weight \(d+1\)).
-
If l is a variable y, then we add an edge \(x\rightarrow _{d} y\) (with weight d).
-
In this way, we obtain a directed, weighted graph \(\Gamma (P)\), which is acyclic (hence, a dag) if and only if P does not contain any occurrence cycles.
For any variable x occurring in P, we define now the level \( lev _P(x)\) of x with respect to P as the maximal weight of a walk in \(\Gamma (P)\) starting in x. Here, the weight of a walk is defined as the sum of the weights of its edges. Note that \( lev _P\) may take the value \(\infty \) if P contains occurrence cycles.
We now consider the multiset \(\lambda (P){:}{=}\{ lev _P(x)\mid x\in \mathcal {V}(P)\}\). (It will be used as a component of a termination measure below.) We compare such multisets via the multiset extension \(>_ m \) of the standard order on \(\mathbb {N}\cup \{\infty \}\), which is well-founded. The following lemma is the main ingredient for the termination proof. Its proof can be found in [10].
Lemma 3
Let \(\mathfrak {C}=P;C;\delta ;\sigma \) be a configuration.
-
(i)
If \(P';C';\delta ';\sigma '\) is obtained from \(\mathfrak {C}\) by L-Sub, then \(\lambda ({P})>_{ m }\lambda ({P'}). \)
-
(ii)
If \(P';C';\delta ';\sigma '\) is obtained from \(\mathfrak {C}\) by Tri, Dec, or Ori, then \(\lambda ({P})\!\geqslant _{ m }\!\lambda ({P'}).\)
Theorem 4
(Termination of QUnif). For a given \((E_\textsf{ssh},\varepsilon )\)-unification problem, the algorithm QUnif terminates either with the configuration F (indicating failure) or with a configuration of the form \(V; C; \delta ; \sigma \) (indicating success), where V is a set of unification equations between variables.
Proof
A simple analysis of the rules of QUnif shows that all terminal configurations are of the form described above. In order to prove that the algorithm terminates, first note that the Cla and CCh rules terminate the derivation immediately, so it suffices to show that the remaining rules cannot yield an infinite derivation. For this purpose, we consider the measures \(\lambda , n_2\) and \(n_3\), where \(n_2\) is the size of P and \(n_3\) is the number of equations of the form \(t=^?_{\boldsymbol{\upalpha }}x\) in P such that t is a non-variable term. By Lemma 3, L-Sub decreases \(\lambda \) while all other rules do not increase it; Dec and Tri decrease \(n_2\), and Ori decreases \(n_3\) while leaving \(n_2\) invariant. Hence, the lexicographical combination of \(\lambda \) with \(n_2\) and \(n_3\) yields a measure that strictly decreases upon each of the aforementioned rules with respect to a well-founded order, thus proving termination. \(\square \)
Proceeding now to the soundness and completeness proofs for QUnif, we fix a notion of solution of a configuration.
Definition 9
(Solution of a configuration). A substitution \(\tau \) is a solution of the configuration \(P;\zeta \precsim {\boldsymbol{\upalpha }}_1\otimes {\boldsymbol{\upalpha }}_2\otimes \dots \otimes {\boldsymbol{\upalpha }}_n; \delta ; \sigma \) if there exists a function \(\mu \) mapping metavariables to elements of \(\varOmega \) such that
-
(S1)
\(\zeta \precsim \mu ({\boldsymbol{\upalpha }}_1)\otimes \mu ({\boldsymbol{\upalpha }}_2)\otimes \dots \otimes \mu ({\boldsymbol{\upalpha }}_n)\) is valid,
-
(S2)
\(\mu ({\boldsymbol{\upbeta }})\Vdash s\tau =_{E} t\tau \) holds for every equation \(s=^?_{\boldsymbol{\upbeta }}t\) in P.
-
(S3)
\(x\tau =x\sigma \tau \) (syntactic equality) holds for every variable \(x\in dom (\sigma )\).
The configuration F has no solutions.
This definition is compatible with Definition 4 in the following sense:
Lemma 4
Let \(\varepsilon \in \varOmega \). A substitution \(\tau \) is an \((E,\varepsilon )\)-unifier of t and s if and only if \(\tau \) is a solution for the corresponding initial configuration \(\{t=^?_{\boldsymbol{\upalpha }}s\};\varepsilon \precsim {\boldsymbol{\upalpha }};\kappa ; Id \).
Proof
By definition, \(\tau \) solves \(\{t=^?_{\boldsymbol{\upalpha }}s\};\varepsilon \precsim {\boldsymbol{\upalpha }};\kappa ; Id \) iff there exists \(\mu \) such that \(\varepsilon \precsim \mu ({\boldsymbol{\upalpha }}) \) and \(\mu ({\boldsymbol{\upalpha }})\Vdash t\tau =_E s\tau \), which is equivalent to \(\varepsilon \Vdash t\tau =_E s\tau \). \(\square \)
The lemma below is needed to show soundness and completeness of \({{\textsc {QUnif}}}\). Its proof can be found in [10].
Lemma 5
Let \(\mathfrak {C}\) be an admissible configuration.
-
(i)
If \(\mathfrak {C}\Longrightarrow \mathfrak {C}'\) and \(\tau \) solves \(\mathfrak {C}'\), then \(\tau \) solves \(\mathfrak {C}\).
-
(ii)
If \(\tau \) solves \(\mathfrak {C}\), then either \(\mathfrak {C}\) is terminal, or there exist a configuration \(\mathfrak {C}'\) and a substitution \(\tau '\) such that \(\mathfrak {C}\Longrightarrow \mathfrak {C}'\), \(\tau '\vert _{ dom (\tau )}=\tau \) and \(\tau '\) solves \(\mathfrak {C}'\).
Theorem 5
(Soundness and completeness of QUnif). Consider an \((E_\textsf{ssh},\varepsilon )\)-unification problem between terms t and s.
-
Soundness: If QUnif terminates in a configuration \(V;C;\delta ;\sigma \) starting from the initial configuration \(\{t =^?_{\boldsymbol{\upalpha }}s\}; \varepsilon \precsim {\boldsymbol{\upalpha }};\kappa ; Id \), then any solution of \(V;C;\delta ;\sigma \) is an \((E_\textsf{ssh},\varepsilon )\)-unifier of t and s.
-
Completeness: If \(\tau \) is an \((E,\varepsilon )\)-unifier of t and s, then there is a run of QUnif starting from the initial configuration \(\{t =^?_{\boldsymbol{\upalpha }}s\}; \varepsilon \precsim {\boldsymbol{\upalpha }}; \kappa ; Id \) that terminates in a configuration \(\{x_1=_{{\boldsymbol{\upalpha }}_1} y_1,\dots ,x_n=_{{\boldsymbol{\upalpha }}_n} y_n\};\zeta \precsim {\boldsymbol{\upalpha }}_1\otimes \dots \otimes {\boldsymbol{\upalpha }}_n;\delta ;\sigma \) such that there exist a substitution \(\varphi \) and a map \(\mu \) satisfying the following conditions:
-
(i)
\(\zeta \precsim \mu ({\boldsymbol{\upalpha }}_1)\otimes \dots \otimes \mu ({\boldsymbol{\upalpha }}_n)\);
-
(ii)
\(\mu ({\boldsymbol{\upalpha }}_i)\Vdash x_i \varphi =_{E_\textsf{ssh}} y_i\varphi \) for all \(1\leqslant i \leqslant n\);
-
(iii)
\(x\sigma \varphi = x\tau \) for all \(x\in \mathcal {V}(s,t)\).
-
(i)
Proof
For soundness, suppose that QUnif produces a derivation \(\mathfrak {C}_0\Longrightarrow \dots \Longrightarrow \mathfrak {C}_m\), where \(\mathfrak {C}_0\) is the initial configuration \(\{t =^?_{\boldsymbol{\upalpha }}s\}; \varepsilon \precsim {\boldsymbol{\upalpha }}; \kappa ; Id \) and \(\mathfrak {C}_m\) is a terminal configuration given by \(V;S;\delta ;\sigma \). If \(\tau \) is a solution of \(\mathfrak {C}_m\) then \(\tau \) is also a solution of \(\mathfrak {C}_0\) (by Lemma 5(i)), and therefore, \(\tau \) is an \((E_\textsf{ssh},\varepsilon )\)-unifier of t and s (by Lemma 4).
For completeness, suppose that \(\tau \) is an \((E,\varepsilon )\)-unifier of t and s. Then \(\tau \) solves the corresponding initial configuration \(\mathfrak {C}_0\) (by Lemma 4). If \(\mathfrak {C}_0\) is not terminal, then there exists a rule application \(\mathfrak {C}_0\Longrightarrow \mathfrak {C}_1\) and a substitution \(\tau _1\) such that \(\tau _1\vert _{ dom (\tau )}=\tau \) and \(\tau _1\) solves \(\mathfrak {C}_1\) (by Lemma 5(ii)). Iterating this argument, we obtain a derivation \(\mathfrak {C}_0\Longrightarrow \mathfrak {C}_1\Longrightarrow \dots \) and a sequence of substitutions \(\tau ,\tau _1,\dots \). After a finite number of steps, this derivation reaches a terminal configuration \(\mathfrak {C}_m\) by Theorem 4, and with it, we obtain a solution \(\tau _m\) such that \(\tau _m\vert _{\mathcal {V}(s,t)}=\tau \). Since \(\tau _m\) solves \(\mathfrak {C}_m\), there exist \(\varphi \) and \(\mu \) satisfying (i) and (ii), as well as \(x\sigma \varphi = x\tau _m\) for all \(x\in \mathcal {V}(\mathfrak {C}_m)\), yielding (iii). \(\square \)
Remark 3
In particular, a \(\kappa \)-complete set of solutions for the problem \(t\!=^?_\varepsilon \! s\) can be obtained by determining for every terminal configuration obtained via QUnif the set of substitutions that meet conditions (i)–(iii) above. If one is just interested in finding some solution, it suffices to compute a terminal configuration \(V; \zeta \precsim \varDelta ; \delta ; \sigma \) and compose \(\sigma \) with a substitution that maps all variables in V to a fresh variable. The value of \(\delta \) corresponds to the “degree” to which such a solution \(\tau \) solves the unification problem, i.e. \(\delta =(t\tau =^\bullet _{E_\textsf{ssh}} s\tau \)).
Example 4
Consider the unification problem \(f(y,g(x,x))=^?_{E,\varepsilon } g(f(c,a),y)\), where \(\mathbb {\varOmega }=\mathbb {L}\), \(E=\{1\Vdash a\approx b, 1\Vdash b\approx c, 1\Vdash f(x_1,x_2)\approx g(x_1,x_2)\}\) and \(\varepsilon = 5\). The following derivation can be obtained by QUnif:
This leads to the solution \(\{y\mapsto f(b,a), x\mapsto a \}\) (with degree 4). Further solutions can be obtained via different choices in the Subst steps. \(\blacksquare \)
Example 5
Consider \(\mathbb {\varOmega }=\mathbb {L}\), \(E=\{1\Vdash f(x,y)\approx g(x,y)\}\), and the E-unification problem \(g(a,x)=^?_3 f(y,g(b,z))\). A derivation of QUnif is given below.
The computed terminal configuration still contains equations between variables. For any \(\psi \) such that \(1\Vdash x_2\psi =_E z\psi \), the substitution \(\{y\mapsto a, x\mapsto f(b,x_2)\}\psi \) is an \((E,\varepsilon )\)-unifier of the given terms. In particular, unifiers that can be obtained from this configuration include, e.g., \(\{y\mapsto a, x\mapsto f(b,u), z\mapsto u\}\), where u is a fresh variable (with degree 2), and also \(\{y\mapsto a, x\mapsto f(b,f(a,a)), z\mapsto g(a,a)\}\) (with degree 3). \(\blacksquare \)
4.2 Idempotent Quantales
Now we consider the case where \(\mathbb {\varOmega }\) is idempotent. Under this hypothesis, we can strengthen our results and show that – with the right definitions – the unification problem is unitary, and that a simplified version of QUnif computes a most general unifier of two given terms. For the fuzzy quantale \(\mathbb {\varOmega }=\mathbb {I}_{\min } =([0, 1],{\leqslant ,} \min )\), our algorithm coincides with Sessa’s weak unification algorithm [23].
Note that in any integral idempotent quantale, meet and tensor coincide. As a consequence, in an idempotent quantale, \(\alpha \precsim \beta \) implies \(\beta \multimap \alpha = \alpha \).
Definition 10
(Weak mgu). A substitution \(\sigma \) is a weak most general \((E,\varepsilon )\)-unifier of t and s, denoted \( wmgu _{E,\varepsilon }(t,s)\), if \(\mathfrak {U}_{E,\varepsilon }(t,s) = \{\tau \,\mid \,\sigma \lessapprox _{E,\mathcal {V}(t,s),\varepsilon } \tau \}\).
By Lemma 2 (ii), \(\sigma = wmgu _{E,\varepsilon }(t,s)\) iff \(\sigma \in \mathfrak {U}_{E,\varepsilon }(t,s)\) and \(\sigma \lessapprox _{E,\mathcal {V}(t,s),\varepsilon }\tau \) holds for every \(\tau \in \mathfrak {U}_{E,\varepsilon }(t,s)\); that is, iff \(\{\sigma \} = mcsu _{E,\varepsilon ,\varepsilon } (t,s)\).
In the idempotent setting, the rules L-Sub and CCh from QUnif can be replaced by simpler versions:
Note that both of these rules constitute steps that could also be achieved by the rules from QUnif: E-Sub can be viewed as a composition of L-Sub and Dec steps, and OCh is just a restricted version of CCh. As before, we use these rules to transform the initial configuration corresponding to a given \((E_\textsf{ssh},\iota )\)-unification problem. As an output, we return Failure if F has been obtained, or \(\sigma \) if a terminal configuration \(P;C;\delta ;\sigma \) has been reached. We denote the resulting algorithm by QUnif-id.
In order to obtain a stronger completeness theorem than in the general case, we refine the notion of a solution of a configuration.
Definition 11
(\(\iota \)-solution of a configuration). Let \(\iota \in \varOmega \) be idempotent. A substitution \(\tau \) is an \(\iota \)-solution of the configuration \(P;\zeta \precsim {\boldsymbol{\upalpha }}_1\otimes {\boldsymbol{\upalpha }}_2\otimes \dots \otimes {\boldsymbol{\upalpha }}_n;\delta ;\sigma \) if there exists a function \(\mu \) mapping metavariables to elements of \(\varOmega \) such that
-
(\(\iota \)1) \(\zeta \precsim \mu ({\boldsymbol{\upalpha }}_1)\otimes \mu ({\boldsymbol{\upalpha }}_2)\otimes \dots \otimes \mu ({\boldsymbol{\upalpha }}_n)\) is valid,
-
(\(\iota \)2) \(\mu ({\boldsymbol{\upbeta }})\Vdash t\tau =_{E} s\tau \) holds for every equation \(t=^?_{\boldsymbol{\upbeta }}s\) in P.
-
(\(\iota \)3) \(\iota \Vdash x\tau =_{E} x\sigma \tau \) holds for every variable \(x\in dom (\sigma )\).
The configuration F has no solutions.
Note that the only difference in comparison with Definition 9 is that (\(\iota \)3) features a quantitative equality over \(E_\textsf{ssh}\), whereas in (S3) we have a syntactic equality.
The lemmas below are needed in the proof of soundness and completeness of QUnif-id (see [10] for their proofs).
Lemma 6
Let \(\mathbb {\varOmega }\) be a (not necessarily idempotent) quantale, \(\iota \in \varOmega \) be an idempotent element of \(\mathbb {\varOmega }\), \(\tau \) be a substitution, and t and s be terms.
-
(i)
\(\tau \) is an \((E,\iota )\)-unifier of t and s iff \(\tau \) is an \(\iota \)-solution for the corresponding initial configuration \(\{t=^?_{\boldsymbol{\upalpha }}s\};\iota \precsim {\boldsymbol{\upalpha }};\kappa ; Id \).
-
(ii)
\(\tau \) is an \(\iota \)-solution for an admissible configuration of the form \(\emptyset ; C;\delta ; \sigma \) iff \(\sigma \lessapprox _{E, dom (\sigma ),\iota }\tau \).
Lemma 7
Let \(\mathbb {\varOmega }\) be an idempotent quantale, \(\iota \in \varOmega \), and \(\mathfrak {C}\) be a configuration obtained from an \((E_\textsf{ssh},\iota )\)-unification problem in \(\mathbb {\varOmega }\) by applying rules from QUnif-id. If \(\mathfrak {C}'\) is obtained from \(\mathfrak {C}\) by a rule from QUnif-id, then a substitution \(\tau \) is an \(\iota \)-solution of \(\mathfrak {C}\) iff it is an \(\iota \)-solution of \(\mathfrak {C}'\).
Theorem 6
(Soundness and completeness of \({{{\textsc {QUnif-id}}}}\)). Consider an \((E_\textsf{ssh},\iota )\)-unification problem between terms t and s in an idempotent quantale \(\mathbb {\varOmega }\), where \(\iota \in \varOmega \). Any run of QUnif-id starting from \( \{t=^?_{{\boldsymbol{\upalpha }}} s\}; {\boldsymbol{\upalpha }}\precsim \iota ;\kappa ; Id \) terminates and returns \( wmgu _{E_\textsf{ssh},\iota }(t,s)\) if it exists, or fails otherwise.
Proof
Termination follows from termination of QUnif (Theorem 4). For soundness and completeness, by Lemma 6(i), a substitution \(\tau \) is an \((E_\textsf{ssh},\iota )\)-unifier of t and s iff it is an \(\iota \)-solution of the initial configuration \(\mathfrak {C}_0\). By Lemma 7, the latter holds iff \(\tau \) is an \(\iota \)-solution for any terminal configuration \(\emptyset ;C;\delta ;\sigma \), or equivalently, iff \(\sigma \lessapprox _{E_\textsf{ssh},\mathcal {V}(t,s),\iota }\tau \) (by Lemma 6(ii)), concluding the proof. \(\square \)
Example 6
We demonstrate algorithm QUnif-id for the problem \(f(x,c)\! =^?_{\mathbb {I},0.4,E} h(a,x)\) in the (idempotent) fuzzy quantale \(\mathbb {I}\) with the \(\min \) T-norm modulo \(E=\{0.5\Vdash a\approx b, \, 0.5\Vdash b \approx c,\, 0.6 \Vdash f(x_1,x_2) \approx g(x_1,x_2), \,0.7 \Vdash g(x_1,x_2) \approx h(x_1,x_2)\}\).
A derivation of QUnif-id is shown below:
Choosing the other equation in the L-Sub step would lead to a different unifier \(\{x\mapsto c\}\) with the same degree 0.5. The solution \(\{x\mapsto b\}\) (with degree 0.5) is not computed. All three solutions are 0.5-equivalent. \(\blacksquare \)
5 Conclusion
In the quantitative setting, equality is replaced by its quantitative counterpart modeling the abstract notion of proximity between terms. A quantitative unification problem asks for finding a substitution that brings the given terms close to each other within a predefined range (with respect to this abstract proximity). However, unlike the standard unification, here it is not guaranteed that an instance of a unifier is still a unifier. The reason is that the instantiation is also quantitative, and it might move the more specific substitution “too far away” from a unifier of the given problem.
In studying quantitative unification, one has to address such and related challenges. We investigated the quantitative equational unification problem in Lawvereian quantales modulo theories presented by axioms of the form \(\gamma \Vdash f(x_1,\ldots ,x_n) \approx g(x_1,\ldots ,x_n)\). Our notion of a minimal complete set of unifiers takes into account two (abstract) distances: between terms to be unified and between substitutions via instantiation. We showed that our unification problems in arbitrary Lawvereian quantales are finitary, while for idempotent Lawvereian quantales, they are unitary. The corresponding algorithms were developed and their properties were studied.
The equational theories that we considered here are a special case of simple shallow theories. An interesting future work would be to extend this work to a larger class of shallow theories (which have some desirable properties in the standard case [6]). Further, the related problem of disunification in Lawvereian quantales is worth investigating.
Notes
- 1.
The reason for this modification in [11] is that (NExp) should be compatible with (Trans), which is based on the tensor rather than the join. Without it, one would obtain a system where performing various transformation steps one after the other would lead to a different distance than performing the same steps in parallel.
- 2.
- 3.
\(\cong _{E,\mathcal {X},\iota }\) is a standard binary relation on \( Sub \) induced by the \(\mathbb {\varOmega }\)-ternary relation \(\cong _{E,\mathcal {X}}\) for a fixed \(\iota \).
References
de Amorim, A.A., Gaboardi, M., Hsu, J., Katsumata, S., Cherigui, I.: A semantic account of metric preservation. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017, pp. 545–556. ACM (2017). https://doi.org/10.1145/3009837.3009890
Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–533. North-Holland, Amsterdam (2001). https://doi.org/10.1016/B978-044450813-3/50010-2
Bacci, G., Mardare, R., Panangaden, P., Plotkin, G.D.: An algebraic theory of Markov processes. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09–12 July 2018, pp. 679–688. ACM (2018). https://doi.org/10.1145/3209108.3209177
Bacci, G., Mardare, R., Panangaden, P., Plotkin, G.D.: Quantitative equational reasoning. In: Barthe, G., Katoen, J.P., Silva, A. (eds.) Foundations of Probabilistic Programming, pp. 333–360. Cambridge University Press, Cambridge (2020). https://doi.org/10.1017/9781108770750.011
Barthe, G., Katoen, J.P., Silva, A. (eds.): Foundations of Probabilistic Programming. Cambridge University Press, Cambridge (2020). https://doi.org/10.1017/9781108770750
Comon, H., Haberstrau, M., Jouannaud, J.P.: Syntacticness, cycle-syntacticness, and shallow theories. Inf. Comput. 111(1), 154–191 (1994). https://doi.org/10.1006/INCO.1994.1043
Dal Lago, U., Gavazzo, F.: A relational theory of effects and coeffects. Proc. ACM Program. Lang. 6(POPL), 1–28 (2022). https://doi.org/10.1145/3498692
Dubois, D., Prade, H.: Fuzzy Sets and Systems: Theory and Applications. Mathematics in Science and Engineering, vol. 144. Academic Press (1980). https://www.worldcat.org/oclc/05726778
Dundua, B., Kutsia, T., Marin, M., Pau, I.: Constraint solving over multiple similarity relations. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, 29 June–6 July 2020, Paris, France (Virtual Conference). LIPIcs, vol. 167, pp. 30:1–30:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPICS.FSCD.2020.30
Ehling, G., Kutsia, T.: Solving quantitative equations. Technical report, RISC, JKU Linz (2024). https://doi.org/10.35011/risc.24-03
Gavazzo, F., Di Florio, C.: Quantitative and metric rewriting: abstract, non-expansive, and graded systems. CoRR abs/2206.13610 (2022). https://doi.org/10.48550/ARXIV.2206.13610
Gavazzo, F., Di Florio, C.: Elements of quantitative rewriting. Proc. ACM Program. Lang. 7(POPL), 1832–1863 (2023). https://doi.org/10.1145/3571256
Geoffroy, G., Pistone, P.: A partial metric semantics of higher-order types and approximate program transformations. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, 25–28 January 2021, Ljubljana, Slovenia (Virtual Conference). LIPIcs, vol. 183, pp. 23:1–23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPICS.CSL.2021.23
Julián-Iranzo, P., Rubio-Manzano, C.: Proximity-based unification theory. Fuzzy Sets Syst. 262, 21–43 (2015). https://doi.org/10.1016/j.fss.2014.07.006
Kutsia, T., Pau, C.: A framework for approximate generalization in quantitative theories. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 578–596. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-10769-6_34
Lawvere, F.W.: Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano 43, 135–166 (1973)
Mardare, R., Panangaden, P., Plotkin, G.D.: Quantitative algebraic reasoning. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 700–709. Association for Computing Machinery, New York (2016). https://doi.org/10.1145/2933575.2934518
Mardare, R., Panangaden, P., Plotkin, G.D.: On the axiomatizability of quantitative algebras. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, 20–23 June 2017, pp. 1–12. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005102
Pau, C.: Symbolic techniques for approximate reasoning. Ph.D. thesis, RISC, Johannes Kepler University Linz (2022)
Pau, C., Kutsia, T.: Proximity-based unification and matching for fully fuzzy signatures. In: 30th IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2021, Luxembourg, 11–14 July 2021, pp. 1–6. IEEE (2021). https://doi.org/10.1109/FUZZ45933.2021.9494438
Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, 27–29 September 2010, pp. 157–168. ACM (2010). https://doi.org/10.1145/1863543.1863568
Rosenthal, K.I.: Quantales and Their Applications. Pitman Research Notes in Mathematics, Longman Scientific & Technical (1990)
Sessa, M.I.: Approximate reasoning by similarity-based SLD resolution. Theor. Comput. Sci. 275(1–2), 389–426 (2002). https://doi.org/10.1016/S0304-3975(01)00188-8
Acknowledgments
Supported by the Austrian Science Fund (FWF) under project P 35530 (SQUEE).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Ethics declarations
Disclosure of Interests
The authors have no competing interests to declare that are relevant to the content of this article.
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2024 The Author(s)
About this paper
Cite this paper
Ehling, G., Kutsia, T. (2024). Solving Quantitative Equations. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science(), vol 14740. Springer, Cham. https://doi.org/10.1007/978-3-031-63501-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-031-63501-4_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-63500-7
Online ISBN: 978-3-031-63501-4
eBook Packages: Computer ScienceComputer Science (R0)