При абстрактной перезаписи [ 1] объект находится в нормальной форме , если он не может быть переписан дальше, т. е. неприводим. В зависимости от системы перезаписи объект может быть переписан в несколько нормальных форм или вообще ни в какую. Многие свойства систем перезаписи относятся к нормальным формам.
Формально говоря, если ( A ,→) — абстрактная система перезаписи , x ∈ A находится в нормальной форме , если не существует y ∈ A , такого что x → y , т . е. x — неприводимый терм.
Объект a является слабо нормализующим , если существует хотя бы одна конкретная последовательность перезаписей, начинающаяся с a , которая в конечном итоге приводит к нормальной форме. Система перезаписи обладает свойством слабой нормализации или является (слабо) нормализующей (WN), если каждый объект слабо нормализуется. Объект а строго нормализуется , если каждая последовательность перезаписей, начинающаяся с а, в конце концов заканчивается нормальной формой. Абстрактная система перезаписи является строго нормализующей , завершающей , нетеровской или обладает свойством (сильной) нормализации .(SN), если каждый из его объектов сильно нормализующий. [2]
Система перезаписи обладает свойством нормальной формы (NF), если для всех объектов a и нормальных форм b до b можно добраться из a с помощью серии перезаписей и обратных перезаписей, только если a сводится к b . Система перезаписи обладает уникальным свойством нормальной формы (UN), если для всех нормальных форм a , b ∈ S , a может быть достигнута из b с помощью серии перезаписей и обратных перезаписей, только если a равно b . Система перезаписи имеетуникальное свойство нормальной формы по отношению к редукции (UN → ), если для каждого терма, сводящегося к нормальным формам a и b , a равно b . [3]
Слияние (сокращенно CR) подразумевает, что NF подразумевает, что UN подразумевает UN → . [3] Обратные импликации, как правило, не выполняются. {a→b,a→c,c→c,d→c,d→e} является UN → , но не UN, поскольку b=e и b,e являются нормальными формами. {a→b,a→c,b→b} — это UN, но не NF, поскольку b=c, c — нормальная форма и b не сводится к c. {a→b,a→c,b→b,c→c} является NF, так как нет нормальных форм, но не CR, поскольку a сводится к b и c, а b,c не имеют общего редукции.
Например, используя термин система перезаписи с одним правилом g ( x , y ) → x , термин g ( g (4,2), g (3,1)) можно переписать следующим образом, применяя правило к самое внешнее вхождение [примечание 1 ] g :