Narrowing is a generalisation of term rewriting, in which pattern-matching rewrite rules is replaced by unification. That is: instead of simply rewriting, we may also instantiate some variables with terms.
Narrowing is one of the main techniques for implementing functional logic programming languages.
The following description of narrowing is given by [Giovannetti et al. 1991]:
Narrowing a functional expression is applying to it the minimum substitution such that the resulting expression is reducible and then reduce it. The substitution is found by unifying the expression with the left-hand sides of equations. In general there will be several narrowings for an expression, one for each equation whose left-hand side is unifiable with the expression. An expression (or an equation) containing existentially quantified variables (logical variables) can be narrowed, possibly yielding a set of narrowing substitutions (answers). This is essentially the same situation of query evaluation in relational logic programs. Narrowing can be implemented as a proper extension of reduction, and is (the base for) a complete goal-solving algorithm for canonical, i.e., confluent and terminating, equational theories.
Narrowing is attributed to [Slagle 1974] and [Lankford 1975], where it is presented as an optimization of the general paramodulation rule in cases where a canonical TRS is available.
The first description of narrowing as a general E-unification procedure appears to be due to [Fay 1990].
A very short textbook presentation of narrowing appears as the very last section of the textbook
Baader, Franz, and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139172752. [pdf]
@book{baader_1998,
title = {Term Rewriting and All That},
publisher = {Cambridge University Press},
author = {Baader, Franz and Nipkow, Tobias},
date = {1998},
doi = {10.1017/CBO9781139172752},
}
James R. Slagle. 1974. Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity. J. ACM 21, 4 (Oct. 1974), 622–642. https://doi.org/10.1145/321850.321859
@article{10.1145/321850.321859,
author = {Slagle, James R.},
title = {Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity},
year = {1974},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {21},
number = {4},
url = {https://doi.org/10.1145/321850.321859},
doi = {10.1145/321850.321859},
journal = {Journal of the ACM},
pages = {622–642},
}
Giovannetti, Elio, Giorgio Levi, Corrado Moiso, and Catuscia Palamidessi. 1991. ‘Kernel-LEAF: A Logic plus Functional Language’. Journal of Computer and System Sciences 42 (2): 139–85. https://doi.org/10.1016/0022-0000(91)90009-T.
@article{giovannetti_1991,
title = {Kernel-{LEAF}: {A} logic plus functional language},
volume = {42},
doi = {10.1016/0022-0000(91)90009-T},
number = {2},
journal = {Journal of Computer and System Sciences},
author = {Giovannetti, Elio and Levi, Giorgio and Moiso, Corrado and Palamidessi, Catuscia},
year = {1991},
pages = {139--185}
}