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

Материал из WEGA
Перейти к навигации Перейти к поиску
(Создана новая страница размером '''Критическая пара''' (''Critical pair'') - играет ключевую роль при анализе локально...)
 
Нет описания правки
Строка 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>s_2</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>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]
[Евстигнеев-Касьянов/94]

Версия от 12:28, 16 ноября 2009

Критическая пара (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].

Литература

[Евстигнеев-Касьянов/94]