(Logo)   IMADA
University of Southern Denmark IMADA - Department of Mathematics and Computer Science


Termination of Narrowing using Dependency Pairs

Josť Iborra
Department of Information Systems and Computation
Universidad Politecnica de Valencia, Spain

Thursday, 26 February, 2009 at 14:15
Auditorium U44


In this work, we extend the dependency pair approach for automated proofs of termination in order to automate the termination proofs of narrowing. Narrowing is a generalization of term rewriting that allows free variables in terms (as in logic programming) and replaces pattern matching by syntactic unification. Narrowing has a number of important applications including execution of functional-logic programming languages, verification of cryptographic protocols, and equational unification. Termination of narrowing is, therefore, of great interest to these applications. Our extension of the dependency pair approach generalizes the standard notion of dependency pairs by taking specifically into account the dependencies between the left-hand side of a rewrite rule and its own argument subterms. We demonstrate that the new narrowing dependency pairs exactly capture the narrowing termination behavior and provide an effective termination criterion which we prove to be sound and complete. Finally, we discuss how our method can be automated and report on a prototype implementation of a termination tool that implements our approach.

Host: Peter Schneider-Kamp

SDU HOME | IMADA HOME | Previous Page
Daniel Merkle