<p>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: <a href="https://channel9.msdn.com/Series/Beckman-Meijer-Overdrive/Beckman-Meijer-Overdrive-The-Lambda-Calculus-and-Food-Nutrition" rel="noreferrer">https://channel9.msdn.com/Series/Beckman-Meijer-Overdrive/Beckman-Meijer-Overdrive-The-Lambda-Calculus-and-Food-Nutrition</a> </p>

CC BY-SA 3.0
2018-04-29T02:59:07.777Z
2018-04-29T02:59:07.777Z
ajw
<p>The answer is <strong>it depends what you mean by Term Rewrite System</strong>.</p>

<p>When it was introduced, the concept of <a href="https://en.wikipedia.org/wiki/Rewriting#Term_rewriting_systems" rel="noreferrer">Term Rewrite Systems</a>, or TRSes, described what is now called <em>first order TRSes</em>, which is simply a set of computation rules of the form</p>

<p>$$ l\rightarrow r $$</p>

<p>where $l$ and $r$ are <em>first order terms</em> of the form</p>

<p>$$ t :=\ x\ \mid\ f(t_1,\ldots,t_n) $$</p>

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

<p>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.</p>

<p>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$" <em>binds</em> 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.</p>

<p>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)) $$</p>

<p>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.</p>

<hr>

<p>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 <strong>Higher Order Rewrite Systems</strong>. Terms are now taken of the form</p>

<p>$$ 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) $$</p>

<p>Where again $f\in\Sigma$, but now each $x^i_j$ is <em>bound</em> 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.</p>

<p>Here there is less consensus about what constitutes a <strong>rewrite rule</strong>. 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!).</p>

<p>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.</p>

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

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

<p>$$\mathrm{app}(\mathrm{abs}(x.y(x)),z)\rightarrow y(z) $$</p>

<p>A pretty decent overview of the definitions and basic results is given by Nipkow and Prehofer <a href="https://www21.in.tum.de/~nipkow/pubs/ded-book.ps.gz" rel="noreferrer">here</a>.</p>

CC BY-SA 3.0
2016-07-01T20:39:09.183Z
2016-07-01T20:39:09.183Z
cody
<p><a href="https://en.wikipedia.org/wiki/Alonzo_Church" rel="nofollow noreferrer">Church</a> <a href="https://en.wikipedia.org/wiki/Lambda_calculus#Typed_lambda_calculi" rel="nofollow noreferrer">was associated with</a> the <a href="https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus" rel="nofollow noreferrer">Simply</a> Typed <a href="https://en.wikipedia.org/wiki/Typed_lambda_calculus" rel="nofollow noreferrer">Lambda Calculus</a>. Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda Calculus.</p>
<p>When John McCarthy created Lisp - he <a href="https://en.wikipedia.org/wiki/John_McCarthy_(computer_scientist)#Career_in_computer_science" rel="nofollow noreferrer">based it on the Lambda Calculus</a>. This is by his own admission when he published <a href="https://dl.acm.org/doi/10.1145/367177.367199" rel="nofollow noreferrer">&quot;Recursive functions of symbolic expressions and their computation by machine, Part I&quot;</a>. You can <a href="https://dspace.mit.edu/bitstream/handle/1721.1/6096/AIM-008.pdf?sequence=2" rel="nofollow noreferrer">read it here</a>.</p>
<p>At the core of <a href="https://www.wolfram.com/mathematica/" rel="nofollow noreferrer">Mathematica</a> is a <a href="https://www.wolfram.com/language/faq/" rel="nofollow noreferrer">Lisp-like system</a>, but instead of being based purely on the Lambda Calculus, it is <a href="https://web.archive.org/web/20160707125523/http://mathforum.org/kb/message.jspa?messageID=8083007" rel="nofollow noreferrer">based on a term-rewriting system</a>.</p>
<p><a href="https://web.archive.org/web/20160707125523/http://mathforum.org/kb/message.jspa?messageID=8083007" rel="nofollow noreferrer">Here</a> the author states state:</p>
<blockquote>
<p>Mathematica is fundamentally a term rewriting system... a more general concept than the Lambda Calculus behind Lisp.</p>
</blockquote>
<p>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.</p>
<p>My question is: <strong>How is Lambda Calculus a specific type of Term Writing system?</strong></p>

<lambda-calculus><term-rewriting-systems><lisp>
How is Lambda Calculus a specific type of Term Writing system?
hawkeye
# How is Lambda Calculus a specific type of Term Writing system?

(Asked by: username_0 on 2016-07-01)

[Church](https://en.wikipedia.org/wiki/Alonzo_Church) [was associated with](https://en.wikipedia.org/wiki/Lambda_calculus#Typed_lambda_calculi) the [Simply](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus) Typed [Lambda Calculus](https://en.wikipedia.org/wiki/Typed_lambda_calculus). Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda Calculus.

When John McCarthy created Lisp - he [based it on the Lambda Calculus](https://en.wikipedia.org/wiki/John_McCarthy_(computer_scientist)#Career_in_computer_science). This is by his own admission when he published ["Recursive functions of symbolic expressions and their computation by machine, Part I"](https://dl.acm.org/doi/10.1145/367177.367199). You can [read it here](https://dspace.mit.edu/bitstream/handle/1721.1/6096/AIM-008.pdf?sequence=2).

At the core of [Mathematica](https://www.wolfram.com/mathematica/) is a [Lisp-like system](https://www.wolfram.com/language/faq/), but instead of being based purely on the Lambda Calculus, it is [based on a term-rewriting system](https://web.archive.org/web/20160707125523/http://mathforum.org/kb/message.jspa?messageID=8083007).

[Here](https://web.archive.org/web/20160707125523/http://mathforum.org/kb/message.jspa?messageID=8083007) 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?**

**Tags:** lambda-calculus, term-rewriting-systems, lisp


---

## 2 answers

### Answer by username_2 on 2016-07-01. Score: 22 | Accepted answer

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

When it was introduced, the concept of [Term Rewrite Systems](https://en.wikipedia.org/wiki/Rewriting#Term_rewriting_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](https://www21.in.tum.de/~nipkow/pubs/ded-book.ps.gz).


---

### Answer by username_1 on 2018-04-29. Score: 5

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>


---

