Variant Narrowing and Extreme Termination

Escobar, Santiago; Meseguer, José; Sasse, Ralf

Permalink

https://hdl.handle.net/2142/11535 Copy

Description

Title

Variant Narrowing and Extreme Termination

Author(s)

• Escobar, Santiago
• Meseguer, José
• Sasse, Ralf

Issue Date

2009-03

Keyword(s)

computer science

Abstract

For narrowing with a set of rules \Delta modulo a set of axioms B almost nothing is known about terminating narrowing strategies, and basic narrowing is known to be incomplete for B=AC. In this work we ask and answer the question: Is there such a thing as an extremely terminating narrowing strategy modulo B? where we call a narrowing strategy S enjoying appropriate completeness properties extremely terminating iff whenever any other narrowing strategy S' enjoying the same completeness properties terminates on a term t, then S is guaranteed to terminate on t as well. We show that basic narrowing is not extremely terminating already for B=\emptyset, and provide a positive answer to the above question by means of a sequence of increasingly more restrictive variant narrowing strategies, called variant narrowing, variant narrowing with history, \Delta,B--pattern narrowing with history, and \Delta,B--pattern narrowing with history and folding, such that given a set \Delta of confluent, terminating, and coherent rules modulo B: (i) \Delta,B--pattern narrowing with history (and folding) are strictly more restrictive than basic narrowing; (ii) \Delta,B--pattern narrowing with history and folding is an extremely terminating strategy modulo B, which terminates on a term t iff t has a finite, complete set of minimal variants; (iii) \Delta,B--pattern narrowing with history and folding terminates on all terms iff \Delta \cup B has the finite variant property; and (iv) \Delta,B--pattern narrowing with history and folding yields a complete and minimal \Delta \cup B-unification algorithm, which is finitary when \Delta \cup B has the finite variant property.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11535

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections