在一個系統中，根據有限的重寫規則，形式語言的詞語（表示式）可以被轉換，這樣的系統被稱為歸約系統。雖然歸約系統也稱為字串重寫系統或項重寫系統，但術語“歸約系統”更通用。
Lambda 演算是一個歸約系統的例子，其中lambda 轉換規則構成了其重寫規則。
如果歸約系統的任何重寫規則都不適用於表示式 
，則稱 
對於該歸約系統處於正規化。
如果表示式對 
中的 
和 
都可以透過零個或多個歸約步驟（即，重寫規則的應用）歸約到相同的表示式，則稱該表示式對是可連線的。
如果 
在一步中歸約到 
，則表示為 
。如果 
在零個或多個步驟中歸約到 
，則表示為 
。如果存在一個序列 
使得 
，
，並且對於每一對 
，要麼 
要麼 
，則使用符號 
。
