Narrowing is a generalization of term rewriting that allows free variables in terms (as in logic programming) and replaces pattern matching by unification in order to (non-deterministically) reduce these terms. Narrowing was originally introduced as a mechanism for solving equational unification problems and then generalized to solve the more general problem of symbolic reachability. The narrowing mechanism has a number of important applications including automated proofs of termination, execution of functional-logic programming languages, partial evaluation, verification of cryptographic protocols, symbolic model checking, and equational unification.
A search command based on narrowing and a narrowing-based unification command for symbols with associativity, commutativity, and identity have been included in Full Maude. Details on their features and syntax, as well as several examples, are available in the Maude Manual.
Maude-NPA is an analysis tool for cryptographic protocols that takes into account many of the algebraic properties of cryptosystems that are not included in other tools. These include cancellation of encryption and decryption, Abelian groups (including exclusive-or), and exponentiation. Maude-NPA uses an approach similar to the original NRL Protocol Analyzer; it is based on unification, and performs backwards search from a final state to determine whether or not it is reachable. Unlike the original NPA, it has a theoretical basis in rewriting logic and narrowing, and offers support for a wider basis of equational theories that includes associative-commutative (AC) theories.
We have developed other tools and experiments associated to the Maude-NPA tool that we store locally at our site.
An Incremental Curry Interpreter with polymorphic types and monadic declarative I/OHere you can find an example Curry program which simulates the ecological behavior of the Segura river's basin. A description of this application (in spanish) can be found here.
A prototype system for the analysis and elimination of redundant arguments in functions.
An abstract diagnosis based debugger for functional programs.
A ``natural rewriting and narrowing'' prototype interpreter which improves (weakly) outermost-needed rewriting and (weakly) outermost-needed narrowing for non-inductively sequential CSs.