Терм

Материал из WikiGrapp

Терм (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]. Термы конвергентны, если их нормальные формы совпадают.

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

Литература

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