Lambda Calculus in Rewriting systems

How to do or implement Lambda Calculus in a Rewriting systems?

Rewriting systems are Turing complete.

But I can't figure out how to do lambda calculus or functions with them.

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, []) &\rightarrow& [] \\
map(f, cons(x, l)) &\rightarrow& 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.

StackExchange Computer Science Q#74237, answer score: 9