4625
правок
Система переписывания термов: различия между версиями
Перейти к навигации
Перейти к поиску
Система переписывания термов (посмотреть исходный код)
Версия от 11:54, 8 сентября 2011
, 8 сентября 2011нет описания правки
KEV (обсуждение | вклад) Нет описания правки |
KEV (обсуждение | вклад) Нет описания правки |
||
| Строка 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> | :::<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</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: | ||
''для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.'' | ''для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.'' | ||
==Литература== | ==Литература== | ||
* Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994. | |||