结构化表达式与规则
项重写系统（term rewriting system，TRS）由一组有方向的规则构成。项由变量、常量和函数符号按结构组合，例如f(x,g(a))。规则l→r表示：找到某个子项符合左侧模式时，用相同变量替换所得到的右侧实例取代它。它操作的是表达式结构，不是编辑器中任意字符的查找替换。
应用规则需要匹配和替换。对于x＋0→x，子项b＋0可用替换x↦b匹配，结果为b；同一次规则应用中，同一变量的各处必须使用一致替换。整个表达式中未被选中的部分构成上下文，保持不变。多个位置或规则可能同时适用，因此重写关系通常允许不同选择。
两条化简路径
考虑只有x＋0→x和0＋x→x的系统，对项(0＋a)＋0，可以先处理外层，得到0＋a，再得到a；也可以先处理内层，得到a＋0，再得到a。两条路径虽有不同中间项，却能汇合。这个小例子说明为什么讨论重写时不能只展示某一次执行。
当一个项已没有适用规则时，它是该系统的正常形。正常形是相对于规则集合而言的，并不意味着人眼看来最短或数学上所有化简都已完成。若系统没有有关乘法的规则，a乘1可能已经是正常形，即使在所解释的代数中它等于a。
参考：[1]
终止与合流各管一件事
终止性指不存在无限重写序列，可通过找到每步严格下降的良基度量来证明。上面的两条加零规则每步都减少符号数量，因此不会无限进行。合流性则要求：从同一项经过若干步到达的任意两个项，都还能各自继续归约到共同后继。它不承诺归约一定结束。
如果系统终止且合流，每个项就有唯一正常形。两种条件不能互相替代：a→b、a→c且b、c不能再变换，是终止但不合流的简单例子；a→b、b→a则可能无限循环，虽然分叉结果仍可互达。指定一种优先策略只能固定执行方式，不等于证明整个规则系统合流。
参考：[2]
规则重叠与规范化
关键对用于分析规则左侧在非变量位置重叠时产生的局部分叉。对终止系统，若这些潜在冲突都可汇合，就能借助关键对分析和纽曼引理建立合流性。没有终止条件时，局部合流不能直接替代全局合流，必须使用额外判据。
把语义等式改写成箭头时，方向尤其重要。无条件使用x＋y→y＋x会在交换后再次匹配，造成来回变换；等式本身成立并不能挽救这种循环。补全过程尝试用合适次序定向等式并消解关键对，但可能失败或不终止。编译器优化、符号计算和等式证明使用重写技术时，都需要分别论证语义保持、终止与结果一致性。