6th International School on Rewriting
July 16th - 20th, 2012. Valencia, Spain
NTA: Narrowing Techniques and Applications
Narrowing has received growing attention due to the many important applications, such as the execution of functional-logic programming languages, automated proofs of termination, symbolic reachability analysis, equational unification, equational constraint solving, verification of cryptographic protocols, model checking, program synthesis, declarative debugging, and partial deduction of functional languages, among others.
The narrowing mechanism can be seen as a generalization of term rewriting where unification replaces matching: both the rewrite rule and the term to be rewritten can be instantiated. Under the narrowing mechanism, functional programs behave like logic programs: narrowing solves equations by computing solutions with respect to a given set of rules, and is complete in the sense of functional programming (computation of normal forms) as well as logic programming (computation of answers).
In this course, we consider the class of rule-based languages that combine a rule-based syntax for programs with the goal-solving operational principle of narrowing. This class includes rewriting-based languages equipped with the narrowing mechanism such as Maude, and functional logic languages, which combine the most important features of functional programming (expressivity of functions and types, higher-order functions, nested expressions, efficient reduction strategies, sophisticated abstraction facilities) and logic programming (unification, logical variables, partial data-structures, built-in search).
The course describes the foundations of narrowing, its optimization by means of narrowing strategies, the problem of analyzing narrowing termination, and the above-mentioned narrowing applications.
