Введение

Выражение, которое не может быть переписано дальше В абстрактном переписывании объект находится в нормальной форме, если его нельзя переписать дальше, т.е. он не редуцируется. В зависимости от системы перезаписи объект может перезаписываться в несколько нормальных форм или вообще не переписываться. Многие свойства систем переписывания относятся к нормальным формам.

Определения

Формально говоря, если (A,→) является абстрактной системой переписывания, x∈A находится в нормальной форме, если не существует y∈A, так что x→y, т. е. x является необратимым термином. Объект a слабо нормализуется, если существует по крайней мере одна конкретная последовательность переписей, начинающаяся с a, которая в конечном итоге дает нормальную форму. Система переписывания имеет свойство слабой нормализации или (слабо) нормализуется (WN), если каждый объект слабо нормализуется. Объект a сильно нормализуется, если каждая последовательность переписей, начинающаяся с a, в конечном итоге заканчивается нормальной формой. Абстрактная система переписывания является сильно нормализующей, терминационной, ноэтерианской или имеет свойство (сильной) нормализации (SN), если каждый из ее объектов сильно нормализует. Система переписывания имеет свойство нормальной формы (NF), если для всех объектов a и нормальных форм b, b можно достичь из a серией переписей и обратных переписей только если a сводится к b. Система переписывания имеет уникальное свойство нормальной формы (UN), если для всех нормальных форм a, b ∈ S, a может быть достигнуто от b серией переписей и обратных переписей только если a равен b. Система переписывания имеет уникальное свойство нормальной формы относительно уменьшения (UN→), если для каждого термина, уменьшающегося до нормальных форм a и b, a равен b.

Результаты

В этом разделе представлены некоторые известные результаты. Во-первых, SN подразумевает WN. Конфлюенс (сокращенно CR) подразумевает NF подразумевает UN подразумевает UN→.