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

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

[math]\displaystyle{ R }[/math] называется нетеровой (или конечно завершаемой), если не существует бесконечной цепочки редукций [math]\displaystyle{ t_1 \longrightarrow_R t_2 \longrightarrow_R t_3 \longrightarrow_R \ldots . }[/math]

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

Следующие два свойства [math]\displaystyle{ R }[/math] являются эквивалентными:

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

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

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

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

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

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

Литература

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