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

Перейти к навигации Перейти к поиску
нет описания правки
(Создана новая страница размером '''Система переписывания термов''' (''Term-rewriting system'') - конечное множество прави...)
 
Нет описания правки
Строка 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>

Навигация