Variant Narrowing and Extreme Termination
Santiago Escobar, José Meseguer, Ralf Sasse · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2009
Abstract. For narrowing with a set of rules ∆ 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 = ∅, 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, ∆, B–pattern narrowing with history, and ∆, B–pattern narrowing with history and folding, such that given a set ∆ of confluent, terminating, and coherent rules modulo B: (i) ∆, B–pattern narrowing with history (and folding) are strictly more restrictive than basic narrowing; (ii) ∆, 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) ∆, B–pattern narrowing with history and folding terminates on all terms iff ∆ ∪ B has the finite variant property; and (iv) ∆, B–pattern narrowing with history and folding yields a complete and minimal ∆ ∪ B-unification algorithm, which is finitary when ∆ ∪ B has the finite variant property. 1