|
|||
|
IMADA - Department of Mathematics and Computer Science |
|
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 |