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

Перейти к навигации Перейти к поиску
нет описания правки
Нет описания правки
Нет описания правки
 
Строка 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.

Навигация