Система переписывания термов: различия между версиями
Glk (обсуждение | вклад) (Создана новая страница размером '''Система переписывания термов''' (''Term-rewriting system'') - конечное множество прави...) |
KEV (обсуждение | вклад) Нет описания правки |
||
| (не показана 1 промежуточная версия этого же участника) | |||
| Строка 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>. | ||
| Строка 36: | Строка 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>, для которого | ||
| Строка 45: | Строка 39: | ||
''для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.'' | ''для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.'' | ||
==Литература== | ==Литература== | ||
* Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 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.