# 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.

• As an aside to Martin's excellent answer, simulating the $\lambda$-calculus with rewrite systems (which is all that is implied by the statement "Turing complete") is actually quite simple: rewrite systems are essentially like ML or Haskell with only top-level functions and pattern matching (no lambdas or maps). However you would write a $\lambda$-calculus simulator in those languages probably carries over to rewrite systems as well. – cody Apr 23 '17 at 1:41

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).

1. D. E. Knuth, P. Bendix, Simple Word Problems in Universal Algebras.

2. F. Baader, T. Nipkow, Term Rewriting and All That.

3. T. Nipkow, C. Prehofer, Higher-Order Rewriting and Equational Reasoning.

4. H. Cirstea, C. Kirchner, Introduction to the rewriting calculus.

5. M. Fernandez, M. J. Gabbay, Nominal Rewriting.