重写系统 1. 基本概念 重写系统（Rewriting System）是研究如何通过规则替换来简化或转换表达式的形式系统。其核心思想是：给定一组规则（如 \( a \rightarrow b \)），将复杂结构中的 \( a \) 替换为 \( b \)，重复此过程直到无法继续。例如，算术中的“\( 3+2 \rightarrow 5 \)”即是一条重写规则。 2. 形式化定义 项（Term） ：由函数符号（如 \( f \)）和变量（如 \( x \)）构成的表达式（如 \( f(x, g(y)) \)）。 规则（Rule） ：形如 \( l \rightarrow r \) 的有序对，其中 \( l, r \) 为项，且 \( l \) 不是单一变量（避免无限循环）。 重写步骤 ：若存在规则 \( l \rightarrow r \) 和替换 \( \sigma \)（将变量映射为项），使得表达式 \( C \) 的子项匹配 \( \sigma(l) \)，则将其替换为 \( \sigma(r) \)，记为 \( C \rightarrow C' \)。 3. 关键性质 终止性（Termination） ：不存在无限重写序列（如 \( a \rightarrow b \rightarrow c \rightarrow \cdots \)）。例如，规则集 \( \{ x \rightarrow f(x) \} \) 不终止。 合流性（Confluence） ：若项 \( t \) 可重写为 \( u \) 和 \( v \)，则存在 \( w \) 使得 \( u \) 和 \( v \) 均可重写为 \( w \)（即结果唯一）。 收敛性（Convergence） ：同时满足终止性与合流性时，每个项有唯一不可约形式（规范形）。 4. 应用场景 λ演算 ：β-归约（\( (\lambda x.t) u \rightarrow t[ u/x ] \)）是重写规则，用于研究程序语义。 代数化简 ：如多项式化简（\( x+0 \rightarrow x \)）基于重写规则。 程序分析 ：编译器优化中的表达式简化（如常量传播）可建模为重写过程。 5. 高级扩展 条件重写系统 ：规则附带条件（如 \( l \rightarrow r \ \text{if} \ P \)），仅当条件 \( P \) 满足时应用规则。 图重写 ：将项推广为图结构，用于模型并行计算或化学反应网络。 高阶重写 ：允许规则中的变量匹配函数（如 \( F(x) \rightarrow g(x) \)），需谨慎处理变量捕获问题。 通过逐步理解上述层次，可掌握重写系统如何为计算逻辑提供统一的化简框架。