При абстрактной перезаписи объект находится в нормальной форме, если он не может быть переписан дальше. В зависимости от системы перезаписи и объекта может существовать несколько нормальных форм или вообще не существовать.
Определение
Формально говоря, если ( A , →) - абстрактная система перезаписи , то некоторый x ∈ A находится в нормальной форме, если не существует y ∈ A такого, что x → y .
Например, используя систему переписывания терминов с одним правилом g ( x , y ) → x , член g ( g (4,2), g (3,1)) можно переписать следующим образом, применяя правило к наружное возникновение [примечание 1] из г :
- g ( g (4,2), g (3,1)) → g (4,2) → 4.
Поскольку к последнему члену 4 не применяется какое-либо правило, его нельзя переписать дальше, и, следовательно, он является нормальной формой члена g ( g (4,2), g (3,1)) по отношению к этой системе переписывания терминов. .
Свойства нормализации
Связанные понятия относятся к возможности переписать элемент в нормальную форму. Объект абстрактной системы перезаписи называется слабо нормализующим, если его можно каким-либо образом переписать в нормальную форму, то есть если некоторая последовательность перезаписи, начинающаяся с него, не может быть расширена дальше. Говорят, что объект строго нормализующий, если его можно каким-либо образом переписать в нормальную форму, то есть если каждая последовательность перезаписи, начинающаяся с него, в конечном итоге не может быть расширена дальше. Абстрактная система перезаписи называется слабо и сильно нормализующей или обладающей свойством слабой и сильной нормализации , если каждый из ее объектов является соответственно слабой и сильной нормализацией.
Например, вышеупомянутая система с одним правилом является строго нормализующей, поскольку каждое приложение правила должным образом уменьшает размер термина и, следовательно, не может быть бесконечной последовательности перезаписи, начинающейся с любого члена. Напротив, система двух правил { g ( x , y ) → x , g ( x , x ) → g (3, x )} является слабой, [примечание 2], но не сильно [примечание 3] нормализующей, хотя каждая член, не содержащий g (3,3), сильно нормализует. [примечание 4] Член g (4,4) имеет две нормальные формы в этой системе, а именно. g (4,4) → 4 и g (4,4) → g (3,4) → 3, следовательно, система не является конфлюэнтной .
Другой пример: система с одним правилом { r ( x , y ) → r ( y , x )} не имеет нормализующих свойств (не слабых или сильных), поскольку из любого члена, например, r (4,2), одна последовательность перезаписи начинается, а именно. r (4,2) → r (2,4) → r (4,2) → r (2,4) → ..., что бесконечно долго.
Нормализация и конфлюентность
Лемма Ньюман утверждает , что если абстрактная система переписывания сильно нормализующие и слабо вырожденный , то является вырожденным .
Результат позволяет еще больше обобщить лемму о критической паре . [ требуется разъяснение ]
Смотрите также
Заметки
- ^ Каждое вхождение g, где применяется правило, выделено жирным шрифтом .
- ^ Поскольку каждый член, содержащий g, может быть переписан конечным числом применений первого правила к члену без g , который находится в нормальной форме.
- ^ Поскольку к члену g (3,3), второе правило можно применять снова и снова, не достигая какой-либо нормальной формы.
- ^ Для данного члена пусть m и n обозначают общее количество g и g, примененных к идентичным аргументам, соответственно. Правильное применение любого правила уменьшает значение m + n , что возможно только конечное число раз.
Рекомендации
- Баадер, Франц ; Нипков, Тобиас (1998). Перезапись терминов и все такое . Издательство Кембриджского университета. ISBN 9780521779203. CS1 maint: обескураженный параметр ( ссылка )