# How is Lambda Calculus a specific type of Term Writing system?

Now we can see that Church was associated with the Simply Typed Lambda Calculus. Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda Calculus.

Now when John McCarthy created Lisp - he based it on the Lambda Calculus. This is by his own admission when he published "Recursive functions of symbolic expressions and their computation by machine, Part I". You can read it here.

Now we know that at the core of Mathematica is a Lisp-like system, but instead of being based purely on the Lambda Calculus, it is based on a term-rewriting system.

Here the author states state:

Mathematica is fundamentally a term rewriting system... a more general concept than the Lambda Calculus behind Lisp.

It seems that the Lambda Calculus is a small part of a much more general category. (Quite eye-opening as a thought this was more of a foundational concept). I'm trying to read more about this to get some perspective on it.

My question is: How is Lambda Calculus a specific type of Term Writing system?

The answer is it depends what you mean by Term Rewrite System.

When it was introduced, the concept of Term Rewrite Systems, or TRSes, described what is now called first order TRSes, which is simply a set of computation rules of the form

$$l\rightarrow r$$

where $l$ and $r$ are first order terms of the form

$$t :=\ x\ \mid\ f(t_1,\ldots,t_n)$$

where $x$ is a variable and $f$ is a function symbol taken from some arbitrary, but fixed set $\Sigma$, called the signature, which also fixes a number of arguments for each $f\in\Sigma$.

There are a couple of common restrictions imposed on rules, e.g. $\mathrm{Var}(r)\subseteq\mathrm{Var}(l)$ but we don't need to go into them here.

With this definition, the usual lambda calculus, with the $\beta$ rule: $$(\lambda x. t)\ u \rightarrow t[u/x]$$ cannot be expressed, as the constructor "$\lambda$" binds the occurrence of $x$ in $t$ (application is fine though). One possible solution, and one which is older than the theory of rewriting systems itself, is to turn each $\lambda$ term into another kind of term, which does not involve binding.

One way is the famous $SK$ combinator calculus, which is a rewrite rule with the signature $\Sigma=\{S,\ K, \mathrm{app}\}$ and the rules $$\mathrm{app}(\mathrm{app}(K,x),y)\rightarrow x$$ and $$\mathrm{app}(\mathrm{app}(\mathrm{app}(S, x), y), z)\rightarrow \mathrm{app}(\mathrm{app}(x, z),\mathrm{app}(y, z))$$

There is another, more intuitive encoding which involves lambda terms with de Bruijn indices and explicit substitutions, but I won't go into it here.

Despite the first order encodings, it became clear that the technical issues with the reduction behavior of the $\lambda$ calculus were better addressed by extending the notion of TRS to include constructors with binders. This is often referred to by the term Higher Order Rewrite Systems. Terms are now taken of the form

$$t\ :=\ x(t_1,\ldots, t_n)\ \mid\ f(x^1_1\ldots x^1_{i_1}.t_1,\ldots,x^n_1\ldots x^n_{i_n}.t_n)$$

Where again $f\in\Sigma$, but now each $x^i_j$ is bound in $t_i$. Signatures need to specify how many variables are bound by each argument. Now we can write $\mathrm{abs}(x.t)$ for the term representing $\lambda x.t$. With a little work, you can define appropriate notions of substitution.

Here there is less consensus about what constitutes a rewrite rule. One issue is that we want rewriting to be decidable, and so it needs to be decidable whether a left hand side matches a term. But this is usually taken to be modulo $\beta\eta$ which is believed to be decidable, but with only extremely complex and slow algorithms (and just $\beta$ is undecidable!).

Therefore left-hand sides are restricted to be in some nice subset, often the "Miller patterns". A number of results for the first-order case generalize, though there are a few nasty surprises.

It's also common to just take first order systems, and simply add $\lambda$ and application to the term structure, along with ad hoc $\beta$ and $\eta$ reductions. This yields rather reasonable systems, at the cost of (some) generality.

Of course the usual $\lambda$ calculus can be directly written in these systems. For example the $\beta$ rule:

$$\mathrm{app}(\mathrm{abs}(x.y(x)),z)\rightarrow y(z)$$

A pretty decent overview of the definitions and basic results is given by Nipkow and Prehofer here.

This presentation by Beckman and Meijer goes over lambda calculus, term rewriting, and mentions Mathematica. I think it answers the question in an intuitive way: https://channel9.msdn.com/Series/Beckman-Meijer-Overdrive/Beckman-Meijer-Overdrive-The-Lambda-Calculus-and-Food-Nutrition