Modular termination of basic narrowing and equational unification (Q2889572)

This paper consists of two parts. The first, larger part addresses the problem of modularity of termination of basic narrowing. In the second part, the problem of modular combination of equational unification algorithms (using basic narrowing) is discussed.NEWLINENEWLINENarrowing is a mechanism that generalizes rewriting, replacing matching by unification. Basic narrowing is a restriction of narrowing, where the narrowing steps are permitted only in certain positions (basic positions). Essentially, the terms forbidden for narrowing are those introduced by instantiation. The problem of modularity of basic narrowing computations aims at finding conditions on term rewriting systems (TRSs), which guarantee that if basic narrowing terminates for TRSs \(\mathcal R_1\) and \(\mathcal R_2\), then it also terminates for the TRS obtained by their combination \({\mathcal R}_1 \cup {\mathcal R}_2\).NEWLINENEWLINEIn the first part, from the beginning, the standard classes of modular combinations of TRSs are considered: Disjoint (\texttt{Disj}), constructor sharing (\texttt{CSh}), and composable (\texttt{Comp}) unions, hierarchical combination (\texttt{HC}) and generalized hierarchical combination (\texttt{GHC}). They are related to each other in the following way: (a) \texttt{CSh} generalizes the \texttt{Disj} class, (b) Both \texttt{HC} and \texttt{Comp} generalize \texttt{CSh}, but in such a way that they (i.e., \texttt{HC} and \texttt{Comp}) are not comparable to each other, and (c) \texttt{GHC} generalizes both \texttt{HC} and \texttt{Comp} classes. The authors demonstrate that termination of basic narrowing is a modular property of disjoint, constructor sharing, and composable unions. For the class of (generalized) hierarchical combinations, termination of basic narrowing is not modular in general. The main result of this part of the paper is the discovery of a new class of hierarchical combinations, called generalized relaxed proper extensions, for which basic termination is modular. The second part of the paper addresses the problem of combination of equational unification algorithms. Modular combination of equational theories for unification aims at finding conditions which make sure that decidability of unification in the ingredient theories implies decidability of unification in the combined theory. The authors are interested in modularity of unification in hierarchical combinations of theories. There is a well-known relationship between \(E\)-unification and basic narrowing: If the equational theory \(E\) can be represented by a canonical set of rewrite rules, then basic narrowing is a complete equational unification procedure. (There are other, more general results, relaxing the requirement on TRSs to be canonical.) The technique used in the paper to find sufficient conditions for modularity of \(E\)-unification in hierarchical combinations relies on the preservation of the effectiveness of basic narrowing as an E-unification algorithm in modular combinations. The simplest such condition is established for modular unification in composable unions: Decidability of \(E\)-unification via basic narrowing is a modular property for the union of composable confluent systems for which basic narrowing is terminating. The other classes of hierarchical combinations do not enjoy this property of modularity of unification, in general. The results of this part of the paper identify (a) additional sufficient conditions for modularity of \(E\)-unification via basic narrowing in the case of combination when one ingredient system is a generalized relaxed proper extension of the other, and (b) restrictions of generalized (relaxed) proper extensions, for which \(E\)-unification via basic narrowing is modular without additional conditions.