4625
правок
Система переписывания термов: различия между версиями
Перейти к навигации
Перейти к поиску
Система переписывания термов (посмотреть исходный код)
Версия от 18:41, 1 февраля 2010
, 1 февраля 2010нет описания правки
Glk (обсуждение | вклад) (Создана новая страница размером '''Система переписывания термов''' (''Term-rewriting system'') - конечное множество прави...) |
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> называется ''нетеровой'' (или ''конечно завершаемой''), если не существует бесконечной цепочки | ||
| Строка 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> | ||