Lambda Calculus in Rewriting systems
See also this question: "How is Lambda Calculus a specific type of Term Writing system?".

Term rewriting, as introduced in (1), and described in e.g. (2), is a first-order system that cannot handle binding. Consider the $map$ function.

$$
  \begin{array}{lcl}
  map(f, []) &amp;\rightarrow&amp; [] \\
  map(f, cons(x, l)) &amp;\rightarrow&amp; cons( f\ x, map\ f\ l) 
  \end{array}
  $$

The problem is that $f$ is used both as a variable and a function
  symbol, which is not permitted by first-order term-rewriting system.

This lead to higher-order rewriting, see e.g (3) for an overview. Another approach to unification of term-rewriting with the $\lambda$-calculus is
the rewriting calculus (4). Yet another approach  towards rewriting with binders -- arguably the most modern -- is nominal rewriting (5).





D. E. Knuth, P. Bendix, Simple Word Problems in Universal Algebras.
F. Baader, T. Nipkow, Term Rewriting and All That.
T. Nipkow, C. Prehofer, Higher-Order Rewriting and Equational Reasoning.
H. Cirstea, C. Kirchner, Introduction to the rewriting calculus.
M. Fernandez, M. J. Gabbay, Nominal Rewriting.