有窮終止

如果不存在無限的重寫序列，則稱歸約系統為有窮終止的（或諾特式的）。此屬性保證任何重寫演算法都將在任何輸入上終止。

排序表示式可能有助於找出歸約系統是否是有窮終止的。用於此目的的順序基於表示式複雜性的某種度量。與項重寫系統規則相容的歸約序的存在保證了該系統是有窮終止的。

確定給定歸約系統是否是有窮終止的問題是遞迴不可判定的。