Система переписывания термов

Материал из WikiGrapp
Перейти к:навигация, поиск

Система переписывания термов (Term-rewriting system) — конечное множество правил переписывания \,R, определяющее на множестве термов бинарное отношение \longrightarrow_R, называемое отношением редукции. Сокращенное название - СПТ.

R называется нетеровой (или конечно завершаемой), если не существует бесконечной цепочки редукций

t_1 \longrightarrow_R t_2 \longrightarrow_R t_3 \longrightarrow_R \ldots .

\,R порождает на множестве термов отношение эквивалентности \,=_R, являющееся транзитивно-рефлексивно-симметричным замыканием отношения редукции.

Следующие два свойства \,R являются эквивалентными:

\,R обладает свойством Черча-Россера, если для любых термов \,t_1 и \,t_2 выполняется t_1 =_R^* t_2 тогда и только тогда, когда существует такой терм \,t_3, что t_1 \longrightarrow_R^* t_3 и t_2 \longrightarrow_R^* t_3;

\,R называется конфлюэнтной, если для любых термов \,t_1, \,t_2 и \,t_3 таких, что t_1 \longrightarrow_R^* t_2 и t_1 \longrightarrow_R^* t_3, найдется терм \,t_4, для которого t_2 \longrightarrow_R^* t_4 и t_3 \longrightarrow_R^* t_4.

Нетеровая и конфлюэнтная СПТ называется полной (конвергентной, канонической).

В случае полной СПТ нормальная форма любого терма всегда существует и единственна. Отношение =_R^* в этом случае разрешимо: для эквивалентности двух термов необходимо совпадение их нормальных форм.

R называется локально-конфлюэнтной, если для любых термов \,t_1, \,t_2 и \,t_3 таких, что t_1 \longrightarrow_R t_2 и t_1 \longrightarrow_R t_3, найдется терм t_4, для которого t_2 \longrightarrow_R^* t_4 и t_3 \longrightarrow_R^* t_4.

Справедлива теорема Ньюмена (M.H.Newman): для нетеровой СПТ свойства конфлюэнтности и локальной конфлюэнтности эквивалентны.

Литература

  • Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.