计算即重写 · 逻辑计算的本质 · 符号计算的艺术

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

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

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

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

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

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）：

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

符号计算里，处处都是 TRS：

求导：上面那五条规则。
化简： $x+x\to 2x$ 、 $\sin^2+\cos^2\to 1$ …… 一批化简规则反复应用。
积分、解方程、三角变换：各有各的规则库。

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

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

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

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

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

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

图表加载中…

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

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

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

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

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

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 推理，会明白它们是同一种火焰的不同形状。

小结与下一站

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

看清了内核，接下来我们把它用起来，进入符号计算的硬核腹地——代数引擎。第一块砖是贯穿一切的主力——多项式。👉 多项式：符号计算的主力。

参考文献

[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》—— 以项重写为核心的语言设计。

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