有穷终止

如果不存在无限的重写序列，则称归约系统为有穷终止的（或诺特式的）。此属性保证任何重写算法都将在任何输入上终止。

排序表达式可能有助于找出归约系统是否是有穷终止的。用于此目的的顺序基于表达式复杂性的某种度量。与项重写系统规则兼容的归约序的存在保证了该系统是有穷终止的。

确定给定归约系统是否是有穷终止的问题是递归不可判定的。