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

Материал из WEGA
Перейти к навигации Перейти к поиску
Нет описания правки
Нет описания правки
 
Строка 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> называется ''нетеровой'' (или ''конечно завершаемой''), если не существует бесконечной цепочки редукций  
редукций <math>t_1 \longrightarrow_R t_2 \longrightarrow_R t_3
\longrightarrow_R \ldots . </math>


<math>R</math> порождает на множестве термов
:::<math>t_1 \longrightarrow_R t_2 \longrightarrow_R t_3 \longrightarrow_R \ldots . </math>
отношение эквивалентности <math>=_R</math>, являющееся
транзитивно-рефлексивно-симметричным замыканием отношения
редукции.


Следующие два свойства <math>R</math> являются эквивалентными:
<math>\,R</math> порождает на множестве термов отношение эквивалентности <math>\,=_R</math>, являющееся транзитивно-рефлексивно-симметричным замыканием отношения редукции.


<math>R</math> обладает ''[[свойство Черча-Россера|свойством Черча-Россера]]'', если
Следующие два свойства <math>\,R</math> являются эквивалентными:
для любых термов <math>t_1</math> и <math>t_2</math> выполняется
<math>t_1 =_R^* t_2</math>
тогда и только тогда, когда существует такой терм <math>t_3</math>,
что <math>t_1 \longrightarrow_R^* t_3</math> и <math>t_2 \longrightarrow_R^* t_3</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_3</math> таких, что
тогда и только тогда, когда существует такой терм <math>\,t_3</math>, что <math>t_1 \longrightarrow_R^* t_3</math> и <math>t_2 \longrightarrow_R^* t_3</math>;
 
<math>\,R</math> называется ''конфлюэнтной'', если
для любых термов <math>\,t_1</math>, <math>\,t_2</math>
и <math>\,t_3</math> таких, что
<math>t_1 \longrightarrow_R^* t_2</math> и <math>t_1 \longrightarrow_R^* t_3</math>,
<math>t_1 \longrightarrow_R^* t_2</math> и <math>t_1 \longrightarrow_R^* t_3</math>,
найдется терм <math>t_4</math>, для которого
найдется терм <math>\,t_4</math>, для которого
<math>t_2 \longrightarrow_R^* t_4</math> и <math>t_3 \longrightarrow_R^* t_4</math>.
<math>t_2 \longrightarrow_R^* t_4</math> и <math>t_3 \longrightarrow_R^* t_4</math>.


Строка 35: Строка 30:


<math>R</math> называется ''локально-конфлюэнтной'', если
<math>R</math> называется ''локально-конфлюэнтной'', если
для любых термов <math>t_1</math>, <math>t_2</math>
для любых термов <math>\,t_1</math>, <math>\,t_2</math>
и <math>t_3</math> таких, что
и <math>\,t_3</math> таких, что
<math>t_1 \longrightarrow_R t_2</math> и <math>t_1 \longrightarrow_R t_3</math>,
<math>t_1 \longrightarrow_R t_2</math> и <math>t_1 \longrightarrow_R t_3</math>,
найдется терм <math>t_4</math>, для которого
найдется терм <math>t_4</math>, для которого
Строка 44: Строка 39:
''для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.''
''для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.''
==Литература==
==Литература==
[Евстигнеев-Касьянов/94]
* Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.

Текущая версия от 11:54, 8 сентября 2011

Система переписывания термов (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): для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.

Литература

  • Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.