Критическая пара: различия между версиями
KEV (обсуждение | вклад) Нет описания правки |
KEV (обсуждение | вклад) Нет описания правки |
||
| Строка 1: | Строка 1: | ||
'''Критическая пара''' (''[[Critical pair]]'') | '''Критическая пара''' (''[[Critical pair]]'') — играет ключевую роль при анализе локальной конфлюэнтности ''[[система переписывания термов|системы переписывания термов]]''. | ||
Пусть <math>s_1\rightarrow t_1</math> и <math>s_2\rightarrow t_2</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>\,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>''. | ||
==Литература== | ==Литература== | ||
* Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994. | |||
Текущая версия от 12:18, 15 апреля 2011
Критическая пара (Critical pair) — играет ключевую роль при анализе локальной конфлюэнтности системы переписывания термов.
Пусть [math]\displaystyle{ s_1\rightarrow t_1 }[/math] и [math]\displaystyle{ s_2\rightarrow t_2 }[/math] — два правила переписывания из некоторой системы переписывания термов [math]\displaystyle{ \,R }[/math], не содержащих общих переменных. Пусть [math]\displaystyle{ \,u_1 }[/math] — отличный от переменной подтерм терма [math]\displaystyle{ \,s_1 }[/math], который унифицируем с [math]\displaystyle{ \,s_2 }[/math]. Тогда пара термов [math]\displaystyle{ \,\sigma(s'_1) }[/math] и [math]\displaystyle{ \,\sigma(t_1) }[/math], где [math]\displaystyle{ \,s'_1 }[/math] — терм, получаемый из [math]\displaystyle{ \,s_1 }[/math] заменой [math]\displaystyle{ \,u_1 }[/math] на [math]\displaystyle{ \,t_2 }[/math], а [math]\displaystyle{ \,\sigma }[/math] — наибольший общий унификатор [math]\displaystyle{ \,u_1 }[/math] и [math]\displaystyle{ \,s_2 }[/math], называется критической парой, получаемой в результате совмещения правил [math]\displaystyle{ \,s_2\rightarrow t_2 }[/math] и [math]\displaystyle{ \,s_1\rightarrow t_1 }[/math].
Справедлива теорема Кнута—Бендикса—Уэ (D.Knuth, P.Bendix, G.Huet) о том, что [math]\displaystyle{ \,R }[/math] локально-конфлюэнтна тогда и только тогда, когда для каждой ее критической пары [math]\displaystyle{ \,t_1 }[/math] и [math]\displaystyle{ \,t_2 }[/math] существует терм [math]\displaystyle{ \,t }[/math], в который они оба редуцируются с помощью [math]\displaystyle{ \,R }[/math].
Литература
- Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.