Терм

Терм (Term) - правильно построенная формула над некоторым алфавитом [math]\displaystyle{ \Sigma }[/math], образованным из множества символов переменных [math]\displaystyle{ V }[/math] и символов [math]\displaystyle{ r }[/math]-арных функций [math]\displaystyle{ \Sigma_r }[/math], где [math]\displaystyle{ r\geq 0 }[/math] - арность функций (количество ее "аргументов").

Если терм [math]\displaystyle{ t }[/math] имеет вид

[math]\displaystyle{ f(t_1, t_2, \ldots, t_r), }[/math]

где [math]\displaystyle{ f \in \Sigma_r }[/math], [math]\displaystyle{ r\gt 0 }[/math], то [math]\displaystyle{ f }[/math] называется внешним (корневым) символом терма [math]\displaystyle{ t }[/math], а термы [math]\displaystyle{ t_1 }[/math], [math]\displaystyle{ t_2 }[/math], [math]\displaystyle{ \ldots }[/math], [math]\displaystyle{ t_r }[/math] и их подтермы - подтермами терма [math]\displaystyle{ t }[/math]. Терм [math]\displaystyle{ t }[/math] - замкнутый, если в нем нет переменных, и линейный, если он не содержит двух вхождений одной и той же переменной.

Терм [math]\displaystyle{ t }[/math] называется редуцируемым (относительно некоторой системы переписывания термов [math]\displaystyle{ R }[/math]), если существует такой терм [math]\displaystyle{ s }[/math], отличный от [math]\displaystyle{ t }[/math], что [math]\displaystyle{ t \longrightarrow_R s }[/math], и нередуцируемым (или тупиковым) в противном случае. Термы [math]\displaystyle{ t }[/math] и [math]\displaystyle{ s }[/math] эквивалентны, если [math]\displaystyle{ t \longrightarrow_R s }[/math] или [math]\displaystyle{ s \longrightarrow_R t }[/math].

Если [math]\displaystyle{ t \longrightarrow_R s }[/math] и [math]\displaystyle{ s }[/math] нередуцируемый, то [math]\displaystyle{ s }[/math] называется нормальной формой терма [math]\displaystyle{ t }[/math]. Термы конвергентны, если их нормальные формы совпадают.

В качестве графововых представлений терма используются дерево выражения и дэг выражения.

Литература

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