Критическая пара

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