Критическая пара: различия между версиями

Перейти к навигации Перейти к поиску
нет описания правки
Нет описания правки
Нет описания правки
 
Строка 1: Строка 1:
'''Критическая пара''' (''[[Critical pair]]'') - играет ключевую роль при анализе локальной конфлюэнтности ''[[система переписывания термов|системы переписывания термов]]''.
'''Критическая пара''' (''[[Critical pair]]'') играет ключевую роль при анализе локальной конфлюэнтности ''[[система переписывания термов|системы переписывания термов]]''.


Пусть <math>s_1\rightarrow t_1</math> и <math>s_2\rightarrow t_2</math> --- два [[правило переписывания|правила переписывания]] из некоторой системы переписывания термов <math>R</math>, не содержащих общих переменных. Пусть <math>u_1</math> --- отличный от переменной [[подтерм]] [[терм|терма]] <math>s_1</math>, который [[унифицируемый терм|унифицируем]] с <math>s_2</math>. Тогда пара термов <math>\sigma(s'_1)</math> и <math>\sigma(t_1)</math>, где <math>s'_1</math> --- терм, получаемый из <math>s_1</math>
Пусть <math>s_1\rightarrow t_1</math> и <math>s_2\rightarrow t_2</math> два [[правило переписывания|правила переписывания]] из некоторой системы переписывания термов <math>\,R</math>, не содержащих общих переменных. Пусть <math>\,u_1</math> отличный от переменной [[подтерм]] [[терм|терма]] <math>\,s_1</math>, который [[унифицируемый терм|унифицируем]] с <math>\,s_2</math>. Тогда пара термов <math>\,\sigma(s'_1)</math> и <math>\,\sigma(t_1)</math>, где <math>\,s'_1</math> терм, получаемый из <math>\,s_1</math>
заменой <math>u_1</math> на <math>t_2</math>, а <math>\sigma</math> --- ''[[наибольший общий унификатор]]'' <math>u_1</math> и <math>s_2</math>, называется ''критической парой'', получаемой в результате совмещения правил <math>s_2\rightarrow t_2</math>
заменой <math>\,u_1</math> на <math>\,t_2</math>, а <math>\,\sigma</math> ''[[наибольший общий унификатор]]'' <math>\,u_1</math> и <math>\,s_2</math>, называется ''критической парой'', получаемой в результате совмещения правил <math>\,s_2\rightarrow t_2</math>
и <math>s_1\rightarrow t_1</math>.
и <math>\,s_1\rightarrow t_1</math>.


Справедлива теорема Кнута---Бендикса---Уэ (D.Knuth, P.Bendix, G.Huet) о том, что ''<math>R</math> локально-конфлюэнтна тогда и только тогда, когда для каждой ее критической пары <math>t_1</math> и <math>t_2</math> существует терм <math>t</math>, в который они оба [[редуцируюмый терм|редуцируются]] с помощью <math>R</math>''.
Справедлива теорема Кнута—Бендикса—Уэ (D.Knuth, P.Bendix, G.Huet) о том, что ''<math>\,R</math> локально-конфлюэнтна тогда и только тогда, когда для каждой ее критической пары <math>\,t_1</math> и <math>\,t_2</math> существует терм <math>\,t</math>, в который они оба [[редуцируемый терм|редуцируются]] с помощью <math>\,R</math>''.
==Литература==
==Литература==
[Евстигнеев-Касьянов/94]
* Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.

Навигация