Как Лямбда-исчисление является специфическим типом системы письменности?

Теперь мы видим , что церковь была связана с в Просто типизированных лямбда - исчислению . Действительно, кажется, что он объяснил Лямбда-исчисление Простого Типа, чтобы уменьшить недопонимание о Лямбда-исчислении.

Теперь, когда Джон Маккарти создал Лисп - он основал его на лямбда-исчислении . По его собственному признанию, он опубликовал «Рекурсивные функции символьных выражений и их вычисление на машине, часть I» . Вы можете прочитать это здесь .

Теперь мы знаем, что в основе Mathematica лежит Lisp-подобная система , но вместо того, чтобы основываться исключительно на лямбда-исчислении, она основана на системе переписывания терминов .

Здесь автор заявляет:

Mathematica - это система переписывания терминов, более общая концепция, чем лямбда-исчисление, стоящее за Лиспом.

Похоже, что лямбда-исчисление является небольшой частью гораздо более общей категории. (Довольно откровенно, как мысль, это было больше основополагающей концепции). Я пытаюсь прочитать больше об этом, чтобы получить некоторое представление об этом.

Мой вопрос: как Lambda Calculus является специфическим типом системы письменности?

Ответ зависит от того, что вы подразумеваете под термином переписать систему .

Когда это было введено, концепция Term Rewrite Systems , или TRSes, описывала то, что сейчас называется TRSes первого порядка , что является просто набором правил вычисления вида

$$l\rightarrow r$$

$l$$r$

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

$x$$f$$\Sigma$$f\in\Sigma$

$\mathrm{Var}(r)\subseteq\mathrm{Var}(l)$

$\beta$

$$(\lambda x. t)\ u \rightarrow t[u/x]$$ $\lambda$$x$$t$$\lambda$

$SK$$\Sigma=\{S,\ K, \mathrm{app}\}$

$$\mathrm{app}(\mathrm{app}(K,x),y)\rightarrow x$$ $$\mathrm{app}(\mathrm{app}(\mathrm{app}(S, x), y), z)\rightarrow \mathrm{app}(\mathrm{app}(x, z),\mathrm{app}(y, z))$$

Есть еще одно, более интуитивное кодирование, которое включает лямбда-термины с индексами де Брюина и явными подстановками, но я не буду здесь вдаваться в подробности.

---

$\lambda$

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

$f\in\Sigma$$x^i_j$$t_i$$\mathrm{abs}(x.t)$$\lambda x.t$

$\beta\eta$$\beta$

Поэтому левые стороны ограничены некоторым хорошим подмножеством, часто «паттернами Миллера». Обобщается ряд результатов для случая первого порядка, хотя есть несколько неприятных сюрпризов.

$\lambda$ $\beta$$\eta$

$\lambda$$\beta$

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

Довольно приличный обзор определений и основных результатов дан Nipkow и Prehofer здесь .

В этой презентации Бекмана и Мейера рассматриваются лямбда-исчисление, переписывание терминов и упоминается Mathematica. Я думаю, что он отвечает на вопрос в интуитивно понятном виде: https://channel9.msdn.com/Series/Beckman-Meijer-Overdrive/Beckman-Meijer-Overdrive-The-Lambda-Calculus-and-Food-Nutrition