Система переписывания термов: различия между версиями

Материал из WEGA
Перейти к навигации Перейти к поиску
(Создана новая страница размером '''Система переписывания термов''' (''Term-rewriting system'') - конечное множество прави...)
 
Нет описания правки
Строка 1: Строка 1:
'''Система переписывания термов''' (''Term-rewriting system'') -  
'''Система переписывания термов''' (''[[Term-rewriting system]]'') -  
конечное множество правил переписывания <math>R</math>, определяющее
конечное множество правил переписывания <math>R</math>, определяющее
на множестве термов бинарное отношение <math>\longrightarrow_R</math>,
на множестве [[терм|термов]] бинарное отношение <math>\longrightarrow_R</math>,
называемое ''отношением редукции''. Сокращенное название
называемое ''отношением редукции''. Сокращенное название - ''СПТ''.
--- ''СПТ''.


<math>R</math> называется ''нетеровой'' (или ''конечно завершаемой''), если не существует бесконечной цепочки
<math>R</math> называется ''нетеровой'' (или ''конечно завершаемой''), если не существует бесконечной цепочки
Строка 16: Строка 15:
Следующие два свойства <math>R</math> являются эквивалентными:
Следующие два свойства <math>R</math> являются эквивалентными:


<math>R</math> обладает ''свойством Черча---Россера'', если
<math>R</math> обладает ''[[свойство Черча-Россера|свойством Черча-Россера]]'', если
для любых термов <math>t_1</math> и <math>t_2</math> выполняется
для любых термов <math>t_1</math> и <math>t_2</math> выполняется
<math>t_1 =_R^* t_2</math>
<math>t_1 =_R^* t_2</math>

Версия от 18:41, 1 февраля 2010

Система переписывания термов (Term-rewriting system) - конечное множество правил переписывания [math]\displaystyle{ R }[/math], определяющее на множестве термов бинарное отношение [math]\displaystyle{ \longrightarrow_R }[/math], называемое отношением редукции. Сокращенное название - СПТ.

[math]\displaystyle{ R }[/math] называется нетеровой (или конечно завершаемой), если не существует бесконечной цепочки редукций [math]\displaystyle{ t_1 \longrightarrow_R t_2 \longrightarrow_R t_3 \longrightarrow_R \ldots . }[/math]

[math]\displaystyle{ R }[/math] порождает на множестве термов отношение эквивалентности [math]\displaystyle{ =_R }[/math], являющееся транзитивно-рефлексивно-симметричным замыканием отношения редукции.

Следующие два свойства [math]\displaystyle{ R }[/math] являются эквивалентными:

[math]\displaystyle{ R }[/math] обладает свойством Черча-Россера, если для любых термов [math]\displaystyle{ t_1 }[/math] и [math]\displaystyle{ t_2 }[/math] выполняется [math]\displaystyle{ t_1 =_R^* t_2 }[/math] тогда и только тогда, когда существует такой терм [math]\displaystyle{ t_3 }[/math], что [math]\displaystyle{ t_1 \longrightarrow_R^* t_3 }[/math] и [math]\displaystyle{ t_2 \longrightarrow_R^* t_3 }[/math];

[math]\displaystyle{ R }[/math] называется конфлюэнтной, если для любых термов [math]\displaystyle{ t_1 }[/math], [math]\displaystyle{ t_2 }[/math] и [math]\displaystyle{ t_3 }[/math] таких, что [math]\displaystyle{ t_1 \longrightarrow_R^* t_2 }[/math] и [math]\displaystyle{ t_1 \longrightarrow_R^* t_3 }[/math], найдется терм [math]\displaystyle{ t_4 }[/math], для которого [math]\displaystyle{ t_2 \longrightarrow_R^* t_4 }[/math] и [math]\displaystyle{ t_3 \longrightarrow_R^* t_4 }[/math].

Нетеровая и конфлюэнтная СПТ называется полной (конвергентной, канонической).

В случае полной СПТ нормальная форма любого терма всегда существует и единственна. Отношение [math]\displaystyle{ =_R^* }[/math] в этом случае разрешимо: для эквивалентности двух термов необходимо совпадение их нормальных форм.

[math]\displaystyle{ R }[/math] называется локально-конфлюэнтной, если для любых термов [math]\displaystyle{ t_1 }[/math], [math]\displaystyle{ t_2 }[/math] и [math]\displaystyle{ t_3 }[/math] таких, что [math]\displaystyle{ t_1 \longrightarrow_R t_2 }[/math] и [math]\displaystyle{ t_1 \longrightarrow_R t_3 }[/math], найдется терм [math]\displaystyle{ t_4 }[/math], для которого [math]\displaystyle{ t_2 \longrightarrow_R^* t_4 }[/math] и [math]\displaystyle{ t_3 \longrightarrow_R^* t_4 }[/math].

Справедлива теорема Ньюмена (M.H.Newman): для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.

Литература

[Евстигнеев-Касьянов/94]