# 计算即重写 · 逻辑计算的本质

> 这是全专栏最深的一章。求导只是 5 条规则的递归应用；把这个想法推到极致，你会发现符号计算的全部，乃至「计算」本身，都是同一件事——按规则把符号一步步重写。这条线索把 CAS、λ 演算、Lisp 和数理逻辑连成了一体。

- 作者：David（道雾轩）
- 专栏：符号计算的艺术（https://daiw.org/manual/symbolic-computing.md）
- 最后更新：2026-10-01
- 原文：https://daiw.org/manual/symbolic-computing/term-rewriting
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

# 计算即重写 · 逻辑计算的本质

这是本专栏思想上的最高峰。前面我们看到，符号操作的内核是[「模式 + 替换」](https://daiw.org/manual/symbolic-computing/substitution-matching)。现在把这个想法**推到极致**，你会触到一个朴素又惊人的事实：**符号计算的全部，乃至「计算」这个概念本身，都是同一件事——按规则重写符号。**

## 先看一个真相：求导就是 5 条规则

微分听起来是门「学问」，但在计算机里，它平淡得令人失望——**只是几条重写规则，递归地作用在树上**。不信，我们**从零手写**一个微分器，只用五条规则：

```python
from sympy import *
x = symbols('x')

def D(e):
    if e == x:            return Integer(1)                    # 规则①  dx/dx = 1
    if e.is_number:       return Integer(0)                    # 规则②  d(常数) = 0
    if e.func == Add:     return Add(*[D(t) for t in e.args])  # 规则③  和的导数 = 导数的和
    if e.func == Mul:                                          # 规则④  乘积法则
        f, g = e.args[0], Mul(*e.args[1:])
        return D(f)*g + f*D(g)
    if e.func == Pow and e.args[1].is_number:                 # 规则⑤  幂法则 d(uⁿ)=n·uⁿ⁻¹·u'
        u, n = e.args
        return n * u**(n-1) * D(u)
    raise NotImplementedError(e)

expr = x**3 + 2*x**2 + 5*x + 7
print(expand(D(expr)))          # 3*x**2 + 4*x + 5
print(expand(diff(expr, x)))    # 3*x**2 + 4*x + 5   —— 和 SymPy 一模一样
```

**二十行、五条规则，复刻了 SymPy 的求导。** 每条规则都是「**看到这个模式的树 → 换成那个模式的树**」：看到和，就拆成导数的和；看到乘积，就套乘积法则；看到幂，就套幂法则。函数**递归**地钻进树的每个角落，把每处都按规则改写。**这就是符号微分的全部真相——没有魔法，只有重写。**

## 推广：项重写系统

把这个模式抽象出来，就是计算机科学里一个基础概念——**项重写系统（Term Rewriting System， TRS）**：

<Callout type="info">
  **一个项重写系统 = 一堆「模式 → 替换」的规则 + 一个动作「反复应用这些规则，直到没有规则能再用为止」。** 最后那个「谁也改不动了」的状态，叫**范式（normal form）**，就是计算的结果。

  符号计算里，处处都是 TRS：
  - **求导**：上面那五条规则。
  - **化简**：$x+x\to 2x$、$\sin^2+\cos^2\to 1$…… 一批[化简规则](https://daiw.org/manual/symbolic-computing/auto-simplification)反复应用。
  - **积分、解方程、三角变换**：各有各的规则库。

  「算一个东西」在符号计算里，就是「**拿规则不停地重写这棵树，直到它稳定下来**」。
</Callout>

关于 TRS 有两个经典问题，值得一提：

- **停机性（termination）**：规则会不会永远改下去、停不下来？（比如规则 $a\to b$ 和 $b\to a$ 就会死循环。）一个可用的规则系统必须**保证终止**。
- **合流性（confluence，又称 Church-Rosser 性质）**：如果一棵树有好几处能改，**先改哪个、后改哪个，会不会影响最终结果？** 若不影响、殊途同归，就叫**合流**——这保证了「范式唯一」，即结果**良定义**。合流 + 终止，是一个重写系统「靠谱」的黄金标准。

这两个词你不必深究，但记住：**符号计算的严谨性，建立在「重写会停、且结果唯一」之上。**

## 惊人的统一：这就是「计算」本身

到这里，真正的震撼才开始。**「按规则重写符号」不只是符号计算的内核——它是「计算」这个概念最古老、最本质的一副面孔。** 二十世纪那几个奠定计算理论的伟大思想，说的其实是**同一件事**：

```mermaid
flowchart TD
    R["计算 = 按规则重写符号"]
    R --> L["λ 演算 (Church, 1936)<br/>计算 = β-归约这一条重写规则"]
    R --> P["Lisp (McCarthy, 1958)<br/>求值 = 重写 S-表达式(树)"]
    R --> M["Mathematica<br/>整门语言就是项重写"]
    R --> T["数理逻辑 / 定理证明<br/>推理规则 = 重写规则,证明 = 重写序列"]
    R --> C["符号计算 (CAS)<br/>求导/化简/积分 = 应用规则库"]
```

**λ 演算**（Alonzo Church，1936）：整个计算模型只有**一条**重写规则——**β-归约**，即「把函数应用到参数上」：

```text
(λx. x·x) 3   →   3·3   →   9
```

就靠这一条重写规则反复施加，λ 演算和图灵机**等价**，能表达一切可计算的东西。**计算，被归结为一种符号重写。**

**Lisp**（John McCarthy，1958）：程序求值 `eval` 的过程，就是**重写 S-表达式**——而 S-表达式正是[我们说的树](https://daiw.org/manual/symbolic-computing/expression-tree)！在 Lisp 里**代码和数据是同一种树**，程序运行就是把这棵树按规则改写。史上第一批计算机代数系统（如 Macsyma）**正是用 Lisp 写的**——这绝非巧合：符号计算是 Lisp「重写树」思想的天然应用。

**Mathematica / Wolfram 语言**：把这一切做到了极致——**整门语言就是一个项重写系统**。里面一切都是 `头[参数]` 形式的树，`/.` 就是「应用规则」。你在 Mathematica 里写：

```text
x^2 + 1 /. x -> 3      (* 结果 10:把规则 x->3 施加到表达式上 *)
```

这和我们 SymPy 里的 `(x**2 + 1).subs(x, 3)`（结果也是 `10`）**是同一个动作**。Mathematica 的「编程」，本质就是「定义重写规则」。

**数理逻辑与定理证明**：逻辑里的**推理规则**（从 $A$ 和 $A\to B$ 推出 $B$），形式上就是**重写规则**；一个**证明**，就是从公理出发、一步步重写到结论的**重写序列**。自动定理证明器，底层跑的也是重写。

## 揭示的本质

于是我们抵达了这个专栏想让你看见的东西：

> **符号计算不是「模拟数学家推公式」的障眼法。它触到的，是「计算」最本质的样子——按规则把符号一步步变换。** 图灵机、λ 演算、Lisp、Mathematica、逻辑推理，这些看似天各一方的东西，底下是**同一句话**：计算，就是符号的重写。

数值计算把世界近似成浮点数去逼近；而符号计算，连同它背后的 λ 演算与逻辑，揭开的是更古老的一层：**思维中「推导」这个动作，本身就是机械的符号变换。** 这，就是「逻辑计算的本质」。理解了它，你再看 SymPy 求导、Mathematica 化简、Prolog 推理，会明白它们是**同一种火焰**的不同形状。

## 小结与下一站

**符号计算的一切，拆到底都是项重写**：一组「模式 → 替换」规则，反复应用到[树](https://daiw.org/manual/symbolic-computing/expression-tree)上直到**范式**（手写 5 条规则即复刻求导）。靠谱的重写系统要**终止**且**合流**（结果唯一）。更深地，「按规则重写符号」正是**计算本身**的样子——**λ 演算（β-归约）、Lisp（重写 S-表达式）、Mathematica（整门语言即重写）、逻辑证明**说的是同一件事。这就是逻辑计算的本质。

看清了内核，接下来我们把它用起来，进入符号计算的硬核腹地——**代数引擎**。第一块砖是贯穿一切的主力——**多项式**。👉 [多项式：符号计算的主力](https://daiw.org/manual/symbolic-computing/polynomials)。

## 参考文献

- [1] Baader & Nipkow.《Term Rewriting and All That》—— 项重写系统、合流与终止的标准教材。
- [2] Alonzo Church.「An Unsolvable Problem of Elementary Number Theory.」1936. —— λ 演算。
- [3] John McCarthy.「Recursive Functions of Symbolic Expressions.」1960. —— Lisp 与符号表达式的重写。
- [4] Stephen Wolfram.《An Elementary Introduction to the Wolfram Language》—— 以项重写为核心的语言设计。