Folding variant narrowing and optimal variant termination
type: Item
instance of: scholarly article
title: Folding variant narrowing and optimal variant termination
zbMATH Open document ID: 1291.68217
author: Santiago Escobar
author: Ralf Sasse
author: José Meseguer
published in: The Journal of Logic and Algebraic Programming
publication date: 2013-01-16T00:00:00Z
review text: This paper presents a detailed discussion of narrowing strategies modulo axioms. If an equational theory can be represented as a disjoint union \(E\cup Ax\) of a set of equations \(E\) and a set of equational axioms \(Ax\), where \(E\) is confluent, terminating, sort-decreasing, and coherent modulo \(Ax\), then narrowing with \(E\) modulo \(Ax\) provides a complete \((E\cup Ax)\)-unification algorithm. Full narrowing is quite inefficient. Therefore, to reduce the search space, narrowing strategies are employed. It is desirable that a narrowing strategy retains the completeness property of unrestricted narrowing. In particular, for narrowing with \(E\) modulo \(Ax\), one would wish to have an efficient strategy which is complete for computing \(E\cup Ax\) unifiers. Another potential benefit of narrowing strategies is that they may sometimes terminate when the full narrowing generates an infinite search space. The paper studies such strategies for narrowing modulo axioms. Their definition is based on the notion of \textit{variant}, introduced in [\textit{H.~Comon-Lundh} and \textit{S.~Delaune}, Lect. Notes Comput. Sci. 3467, 294--307 (2005; Zbl 1078.68059)]. The notions of variant-complete and optimally variant-terminating strategies are introduced. Variant-complete strategies compute a complete set of variants. Optimally variant-terminating ones terminate iff there is a finite complete set of variants. For narrowing with \(E\) modulo \(Ax\), variant-complete and optimally variant-terminating strategies can be used to construct complete \((E\cup Ax)\)-unification algorithms (if \(E\) is confluent, terminating, sort-decreasing, and coherent modulo \(Ax\)). To characterize concrete instances of variant-complete and optimally variant-terminating strategies, the authors associate to each narrowing strategy its folding version. While the strategy specifies which narrowing steps are allowed from a term, its folding version avoids repeated generation of variants. It is prove…
reviewed by: Temur Kutsia
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 6126076
zbMATH Keywords: narrowing modulo
zbMATH Keywords: terminating narrowing strategy
zbMATH Keywords: variants
zbMATH Keywords: equational unification
describes a project that uses: Maude
MaRDI profile type: Publication
full work available at URL: j.jlap.2012.01.002
OpenAlex ID: W2316113835
DOI: 10.1016/J.JLAP.2012.01.002
description: scientific article; zbMATH DE number 6126076